Theorem revrev ≪ | index | src | ≫ 

theorem revrev (l: nat): $ rev (rev l) = l $;
StepHypRefExpression
1 id 
_1 = l -> _1 = l
2 1 reveqd 
_1 = l -> rev _1 = rev l
3 2 reveqd 
_1 = l -> rev (rev _1) = rev (rev l)
4 3, 1 eqeqd 
_1 = l -> (rev (rev _1) = _1 <-> rev (rev l) = l)
5 id 
_1 = 0 -> _1 = 0
6 5 reveqd 
_1 = 0 -> rev _1 = rev 0
7 6 reveqd 
_1 = 0 -> rev (rev _1) = rev (rev 0)
8 7, 5 eqeqd 
_1 = 0 -> (rev (rev _1) = _1 <-> rev (rev 0) = 0)
9 id 
_1 = a2 -> _1 = a2
10 9 reveqd 
_1 = a2 -> rev _1 = rev a2
11 10 reveqd 
_1 = a2 -> rev (rev _1) = rev (rev a2)
12 11, 9 eqeqd 
_1 = a2 -> (rev (rev _1) = _1 <-> rev (rev a2) = a2)
13 id 
_1 = a1 : a2 -> _1 = a1 : a2
14 13 reveqd 
_1 = a1 : a2 -> rev _1 = rev (a1 : a2)
15 14 reveqd 
_1 = a1 : a2 -> rev (rev _1) = rev (rev (a1 : a2))
16 15, 13 eqeqd 
_1 = a1 : a2 -> (rev (rev _1) = _1 <-> rev (rev (a1 : a2)) = a1 : a2)
17 eqtr 
rev (rev 0) = rev 0 -> rev 0 = 0 -> rev (rev 0) = 0
18 reveq 
rev 0 = 0 -> rev (rev 0) = rev 0
19 rev0 
rev 0 = 0
20 18, 19 ax_mp 
rev (rev 0) = rev 0
21 17, 20 ax_mp 
rev 0 = 0 -> rev (rev 0) = 0
22 21, 19 ax_mp 
rev (rev 0) = 0
23 reveq 
rev (a1 : a2) = rev a2 |> a1 -> rev (rev (a1 : a2)) = rev (rev a2 |> a1)
24 revS 
rev (a1 : a2) = rev a2 |> a1
25 23, 24 ax_mp 
rev (rev (a1 : a2)) = rev (rev a2 |> a1)
26 revsnoc 
rev (rev a2 |> a1) = a1 : rev (rev a2)
27 conseq2 
rev (rev a2) = a2 -> a1 : rev (rev a2) = a1 : a2
28 26, 27 syl5eq 
rev (rev a2) = a2 -> rev (rev a2 |> a1) = a1 : a2
29 25, 28 syl5eq 
rev (rev a2) = a2 -> rev (rev (a1 : a2)) = a1 : a2
30 4, 8, 12, 16, 22, 29 listind 
rev (rev l) = l

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp, itru), axs_pred_calc (ax_gen, ax_4, ax_5, ax_6, ax_7, ax_10, ax_11, ax_12), axs_set (elab, ax_8), axs_the (theid, the0), axs_peano (peano1, peano2, peano5, addeq, muleq, add0, addS, mul0, mulS)