A,B:Type, s:(A+B) List, x:A. (x 
mapoutl(s)) 
(
y:A+B. (y s) & isl(y) & x = outl(y))
P:(T
), T':Type, f:({x:T| P(x) }T'), L:T List, x:T'. (x mapfilter(f;P;L)) (y:T. (y L) & P(y) & x = f(y))
0))
THENA
(Auto THEN (All Reduce) THEN (Try ((Analyze -1) THEN Unhide)))
None
About:
| | | | | | |
 |  |  |  |  |