x
L.P(x)) == reduce(
x,b. P(x) 
b;false;L)
T:Type, L:T List, P:(T
). (xL.P(x)) q == if p
true else q fip,q:. (p q) k ; a.as' f(a,reduce(f;k;as')) (recursive)A,B:Type, f:(ABB), k:B, as:A List. reduce(f;k;as) B| Who Cites l bexists? | |
| 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: | (xL.P(x)) | has structure: | l_bexists(L; x.P(x)) |
About:
 |  |  |
 |  |  |  |  |
 |  |  |  |  |
 |