| | 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 |
|
| 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:(T  Prop), L:T List. xL.P(x) Type |
| | | Thm* T:Type, P:(TType). xnil.P(x) Type |
|
| 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) |
