At:
mapoutl is singleton
2
1.
A: Type
2.
B: Type
3.
L: (A+B) List
4.
a: A
5.
L1: (A+B) List
6.
L2: (A+B) List
7.
L = (L1 @ [inl(a)] @ L2)
8.
mapoutl(L1) = nil
9.
mapoutl(L2) = nil
mapoutl(L) = [a]
By:
SubstFor L 0
THEN
RWW
Thm* 
L1,L2:(A+B) List. mapoutl(L1 @ L2) ~ (mapoutl(L1) @ mapoutl(L2))
0
THEN
HypSubst -1 0
THEN
HypSubst -2 0
THEN
Reduce 0
Generated subgoals:
None
About:
