is mentioned by

Thm* L:(A+B) List, a:A. mapoutl(L) = [a] (L1,L2:(A+B) List. L = (L1 @ [inl(a)] @ L2) & mapoutl(L1) = nil & mapoutl(L2) = nil)	[mapoutl_is_singleton]
Thm* L:(A+B) List, l1,l2:A List. mapoutl(L) = (l1 @ l2) (L1,L2:(A+B) List. L = (L1 @ L2) & mapoutl(L1) = l1 & mapoutl(L2) = l2)	[mapoutl_is_append]
Thm* L1,L2:(A+B) List. mapoutl(L1 @ L2) ~ (mapoutl(L1) @ mapoutl(L2))	[mapoutl_append]
Thm* s:(A+B) List. no_repeats(A+B;s) no_repeats(A;mapoutl(s))	[no_repeats_mapoutl]
Thm* s:(A+B) List, x:A. (x mapoutl(s)) (inl(x) s)	[mapoutl_member]
Thm* s:(A+B) List, x:A. (x mapoutl(s)) (y:A+B. (y s) & isl(y) & x = outl(y))	[member_mapoutl]

Try larger context: Graphs