s:(A+B) List, x:A. (x 
mapoutl(s)) 
(inl(x) s)s:(A+B) List, x:A. (x mapoutl(s)) (
y:A+B. (y s) & isl(y) & x = outl(y))| Rank | Theorem | Name |
| 4 | Thm* s:(A+B) List, x:A. (x mapoutl(s)) (inl(x) s) | [mapoutl_member] |
| cites | ||
| 3 | Thm* s:(A+B) List, x:A. (x mapoutl(s)) (y:A+B. (y s) & isl(y) & x = outl(y)) | [member_mapoutl] |