symbol const Set : TYPE // type of set codes
symbol injective S : Set ⇒ TYPE // interpretation of set codes in TYPE
symbol const list : Set ⇒ Set
definition L a ≔ S (list a)
symbol const nil {a} : L a
symbol const cons {a} : S a ⇒ L a ⇒ L a
symbol const nat : Set // set code of natural numbers
definition N ≔ S nat
symbol const zero : N
symbol const succ : N ⇒ N
symbol length {a} : L a ⇒ N // length of a list
rule length nil → zero
//and length (cons _ &l) → succ (length &l) // not accepted FIXME
and length (@cons &a _ &l) → succ (@length &a &l)
