| | Who Cites equivalence? |
|
| equivalence | Def {T  } == {f:(T  T )| ( 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 |
|
| 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 |
|
| nequal | Def a  b T ==  a = b T |
| | | Thm* A:Type, x,y:A. (x y) Prop |
|
| 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) |
|
| not | Def A == A False |
| | | Thm* A:Prop. (A) Prop |
