Step | Hyp | Ref | Expression |
1 |
|
eqtr |
map F (a : l) = (\\ a1, \\ a2, \ a3, F @ a1 : a3) @ (a, l, map F l) ->
(\\ a1, \\ a2, \ a3, F @ a1 : a3) @ (a, l, map F l) = F @ a : map F l ->
map F (a : l) = F @ a : map F l |
2 |
|
lrecS |
lrec 0 (\\ a1, \\ a2, \ a3, F @ a1 : a3) (a : l) = (\\ a1, \\ a2, \ a3, F @ a1 : a3) @ (a, l, lrec 0 (\\ a1, \\ a2, \ a3, F @ a1 : a3) l) |
3 |
2 |
conv map |
map F (a : l) = (\\ a1, \\ a2, \ a3, F @ a1 : a3) @ (a, l, map F l) |
4 |
1, 3 |
ax_mp |
(\\ a1, \\ a2, \ a3, F @ a1 : a3) @ (a, l, map F l) = F @ a : map F l -> map F (a : l) = F @ a : map F l |
5 |
|
anll |
a1 = a /\ a2 = l /\ a3 = map F l -> a1 = a |
6 |
5 |
appeq2d |
a1 = a /\ a2 = l /\ a3 = map F l -> F @ a1 = F @ a |
7 |
|
anr |
a1 = a /\ a2 = l /\ a3 = map F l -> a3 = map F l |
8 |
6, 7 |
conseqd |
a1 = a /\ a2 = l /\ a3 = map F l -> F @ a1 : a3 = F @ a : map F l |
9 |
8 |
applamed |
a1 = a /\ a2 = l -> (\ a3, F @ a1 : a3) @ map F l = F @ a : map F l |
10 |
9 |
appslamed |
a1 = a -> (\\ a2, \ a3, F @ a1 : a3) @ (l, map F l) = F @ a : map F l |
11 |
10 |
appslame |
(\\ a1, \\ a2, \ a3, F @ a1 : a3) @ (a, l, map F l) = F @ a : map F l |
12 |
4, 11 |
ax_mp |
map F (a : l) = F @ a : map F l |