Def (rec) LShort(l) == Case of l : null nil ; h.l' h.(LShort(l') \ h)

Thm* l:St*, eq:(StSt). LShort(l) St*

Def (rec) l \ a == Case of l : null nil ; h.l' if eq(a,h) l' \ a else h.(l' \ a) fi

Thm* l:St*, s:St, eq:(StSt). (l \ s) St*

Def (rec) mem_f(T;a;bs) == Case of bs : null False ; b.bs' b = a T mem_f(T;a;bs')

Thm* a:T, bs:T*. mem_f(T;a;bs) Prop

Def b == if b True else False fi

Thm* b:. b Prop