Who Cites append?
append	Def as @ bs == Case of as; nil bs ; a.as' a.(as' @ bs) (recursive)
	Thm* T:Type, as,bs:T List. (as @ bs) T List
discrete_equality	Def {T=} == {eq:(TT)| x,y:T. (eq(x,y)) x = y }
	Thm* T:Type. {T=} Type
assert	Def b == if b True else False fi
	Thm* b:. b Prop
iff	Def P Q == (P Q) & (P Q)
	Thm* A,B:Prop. (A B) Prop
is_member	Def x(eq) L == (letrec is_member x eq L = (Case of L; nil false ; h.t if eq(x,h) true else is_member(x,eq,t) fi) ) (x,eq,L)
	Thm* T:Type, eq:(TT), u:T. u(eq) nil
	Thm* T:Type, eq:(TT), x:T, L:T List. x(eq) L
remove	Def remove(eq;x;L) == (letrec remove eq x L = (Case of L; nil nil ; h.t if eq(x,h) t else h.remove(eq,x,t) fi) ) (eq,x,L)
	Thm* T:Type, eq:(TT), x:T, L:T List. remove(eq;x;L) T List
rev_implies	Def P Q == Q P
	Thm* A,B:Prop. (A B) Prop
letrec_body	Def = b == b
letrec_arg	Def x b(x) (x) == b(x)
letrec	Def (letrec f b(f)) == b((letrec f b(f)) ) (recursive)

About: