| Who Cites member-right-paren? | |
| member-right-paren | Def member-right-paren(x,y.E(x;y);i;s) == ( x s.InjCase(x; a. false , E(a;i))) |
| l_bexists | Def (xL.P(x)) == reduce( x,b. P(x)  b;false;L) |
Thm*  T:Type, L:T List, P:(T   ). (xL.P(x)) | |
| bor | Def p q == if p true else q fi |
| Thm* p,q:. (p q) | |
| reduce | Def reduce(f;k;as) == Case of as; nil k ; a.as' f(a,reduce(f;k;as')) (recursive) |
| Thm* A,B:Type, f:(ABB), k:B, as:A List. reduce(f;k;as) B |
| Syntax: | member-right-paren(x,y.E(x;y);i;s) | has structure: | member-right-paren(x,y.E(x;y); i; s) |
About:
 |  |  |  |  |
 |  |  |  |
 |  |  |  |  |  |