| | Who Cites discrete equality? |
|
| discrete_equality | Def {T= } == {eq:(T  T )|  x,y:T.  (eq(x,y))   x = y } |
| | | Thm* T:Type. {T=}  Type |
|
| iff | Def P Q == (P  Q) & (P Q) |
| | | Thm* A,B:Prop. (A B) Prop |
|
| list_all | Def xL.P(x) == (letrec list_all L = (Case of L; nil  True ; h.t P(h) & list_all(t)) ) (L) |
| | | Thm* T:Type, P:(TProp), L:T List. xL.P(x) Type |
| | | Thm* T:Type, P:(TType). xnil.P(x) Type |
|
| assert | Def b == if b True else False fi |
| | | Thm* b:. b 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) |
