At:
mapoutl is append2
1.
A: Type
2.
B: Type
3.
L: (A+B) List
4.
l1: A List
5.
l2: A List
6.
L1: (A+B) List
7.
L2: (A+B) List
8.
L = (L1 @ L2)
9.
mapoutl(L1) = l1
10.
mapoutl(L2) = l2
mapoutl(L) = (l1 @ l2)
By:
SubstFor L 0
THEN
RWO
Thm*L1,L2:(A+B) List. mapoutl(L1 @ L2) ~ (mapoutl(L1) @ mapoutl(L2))
0
THEN
Analyze
Generated subgoals:
mapoutl(L) = (l1 @ l2)
L1,L2:(A+B) List. mapoutl(L1 @ L2) ~ (mapoutl(L1) @ mapoutl(L2))
0