b == if b
True else False fi
b:
. b 
Prop
a,v. if P(a) [a / v] else v fi;nil;l)T:Type, P:(T
), l:T List. filter(P;l) T ListxL.P(x)) == x:T. (x L) 
P(x)T:Type, L:T List, P:(TProp). (xL.P(x)) Prop| Some definitions of interest. | |
| assert | b == if b True else False fi |
| b:. b Prop | |
| filter | a,v. if P(a) [a / v] else v fi;nil;l) |
| T:Type, P:(T), l:T List. filter(P;l) T List | |
| l_all | xL.P(x)) == x:T. (x L) P(x) |
| T:Type, L:T List, P:(TProp). (xL.P(x)) Prop |
About:
 |  |  |  |  |  |  |  |
 |  |  |  |  |  |  |  |
 |