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))| Rank | Theorem | Name |
| 3 | Thm* s:(A+B) List, x:A. (x mapoutl(s)) (y:A+B. (y s) & isl(y) & x = outl(y)) | [member_mapoutl] |
| cites | ||
| 2 | Thm* 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)) | [member_map_filter] |