bs ; a.as' [a / (as' @ bs)] (recursive)
T:Type, as,bs:T List. (as @ bs) 
T List
b == if b True else False fib:
. b PropT:Type, P:(T
), T':Type, f:({x:T| P(x) }T'), L:T List. mapfilter(f;P;L) T' List| Some definitions of interest. | |
| 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 | |
| assert | Def b == if b True else False fi |
| Thm* b:. b Prop | |
| mapfilter | Def mapfilter(f;P;L) == map(f;filter(P;L)) |
| Thm* T:Type, P:(T), T':Type, f:({x:T| P(x) }T'), L:T List. mapfilter(f;P;L) T' List |
About:
 |  |  |  |
 |  |  |  |  |
 |  |  |  |  |  |  |
 |