Who Cites equivalence?
equivalence	Def {T} == {f:(TT)| (x:T. (f(x,x))) & (x,y:T. (f(x,y)) (f(y,x))) & (x,y,z:T. (f(x,y)) (f(y,z)) (f(x,z))) }
	Thm* T:Type{i}. {T} Type{i'}
assert	Def b == if b True else False fi
	Thm* b:. b Prop
ge	Def ij == ji
	Thm* i,j:. (ij) Prop
hd	Def hd(l) == Case of l; nil "?" ; h.t h
	Thm* A:Type, l:A List. ||l||1 hd(l) A
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
length	Def ||as|| == Case of as; nil 0 ; a.as' ||as'||+1 (recursive)
	Thm* A:Type, l:A List. ||l||
	Thm* ||nil||
	Thm* T:Type, L:T List. ||L||
iff	Def P Q == (P Q) & (P Q)
	Thm* A,B:Prop. (A B) Prop
le	Def AB == B < A
	Thm* i,j:. (ij) 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)
rev_implies	Def P Q == Q P
	Thm* A,B:Prop. (A B) Prop
not	Def A == A False
	Thm* A:Prop. (A) Prop

About: