all2S - ../examples/peano.mm1

Step	Hyp	Ref	Expression
1		bitr4	(a : l1, b : l2 e. all2 R <-> len (a : l1) = len (b : l2) /\ A. a2 A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) -> (a, b e. R /\ l1, l2 e. all2 R <-> len (a : l1) = len (b : l2) /\ A. a2 A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) -> (a : l1, b : l2 e. all2 R <-> a, b e. R /\ l1, l2 e. all2 R)
2		elall22	a : l1, b : l2 e. all2 R <-> len (a : l1) = len (b : l2) /\ A. a2 A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))
3	1, 2	ax_mp	(a, b e. R /\ l1, l2 e. all2 R <-> len (a : l1) = len (b : l2) /\ A. a2 A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) -> (a : l1, b : l2 e. all2 R <-> a, b e. R /\ l1, l2 e. all2 R)
4		bitr	(a, b e. R /\ l1, l2 e. all2 R <-> a, b e. R /\ (len l1 = len l2 /\ A. a1 A. _2 (nth a1 l1 = suc _2 -> A. _1 (nth a1 l2 = suc _1 -> _2, _1 e. R)))) -> (a, b e. R /\ (len l1 = len l2 /\ A. a1 A. _2 (nth a1 l1 = suc _2 -> A. _1 (nth a1 l2 = suc _1 -> _2, _1 e. R))) <-> len (a : l1) = len (b : l2) /\ A. a2 A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) -> (a, b e. R /\ l1, l2 e. all2 R <-> len (a : l1) = len (b : l2) /\ A. a2 A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)))
5		elall22	l1, l2 e. all2 R <-> len l1 = len l2 /\ A. a1 A. _2 (nth a1 l1 = suc _2 -> A. _1 (nth a1 l2 = suc _1 -> _2, _1 e. R))
6	5	aneq2i	a, b e. R /\ l1, l2 e. all2 R <-> a, b e. R /\ (len l1 = len l2 /\ A. a1 A. _2 (nth a1 l1 = suc _2 -> A. _1 (nth a1 l2 = suc _1 -> _2, _1 e. R)))
7	4, 6	ax_mp	(a, b e. R /\ (len l1 = len l2 /\ A. a1 A. _2 (nth a1 l1 = suc _2 -> A. _1 (nth a1 l2 = suc _1 -> _2, _1 e. R))) <-> len (a : l1) = len (b : l2) /\ A. a2 A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) -> (a, b e. R /\ l1, l2 e. all2 R <-> len (a : l1) = len (b : l2) /\ A. a2 A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)))
8		bitr4	(a, b e. R /\ (len l1 = len l2 /\ A. a1 A. _2 (nth a1 l1 = suc _2 -> A. _1 (nth a1 l2 = suc _1 -> _2, _1 e. R))) <-> len l1 = len l2 /\ (a, b e. R /\ A. a1 A. _2 (nth a1 l1 = suc _2 -> A. _1 (nth a1 l2 = suc _1 -> _2, _1 e. R)))) -> (len (a : l1) = len (b : l2) /\ A. a2 A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)) <-> len l1 = len l2 /\ (a, b e. R /\ A. a1 A. _2 (nth a1 l1 = suc _2 -> A. _1 (nth a1 l2 = suc _1 -> _2, _1 e. R)))) -> (a, b e. R /\ (len l1 = len l2 /\ A. a1 A. _2 (nth a1 l1 = suc _2 -> A. _1 (nth a1 l2 = suc _1 -> _2, _1 e. R))) <-> len (a : l1) = len (b : l2) /\ A. a2 A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)))
9		anlass	a, b e. R /\ (len l1 = len l2 /\ A. a1 A. _2 (nth a1 l1 = suc _2 -> A. _1 (nth a1 l2 = suc _1 -> _2, _1 e. R))) <-> len l1 = len l2 /\ (a, b e. R /\ A. a1 A. _2 (nth a1 l1 = suc _2 -> A. _1 (nth a1 l2 = suc _1 -> _2, _1 e. R)))
10	8, 9	ax_mp	(len (a : l1) = len (b : l2) /\ A. a2 A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)) <-> len l1 = len l2 /\ (a, b e. R /\ A. a1 A. _2 (nth a1 l1 = suc _2 -> A. _1 (nth a1 l2 = suc _1 -> _2, _1 e. R)))) -> (a, b e. R /\ (len l1 = len l2 /\ A. a1 A. _2 (nth a1 l1 = suc _2 -> A. _1 (nth a1 l2 = suc _1 -> _2, _1 e. R))) <-> len (a : l1) = len (b : l2) /\ A. a2 A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)))
11		aneq	(len (a : l1) = len (b : l2) <-> len l1 = len l2) -> (A. a2 A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)) <-> a, b e. R /\ A. a1 A. _2 (nth a1 l1 = suc _2 -> A. _1 (nth a1 l2 = suc _1 -> _2, _1 e. R))) -> (len (a : l1) = len (b : l2) /\ A. a2 A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)) <-> len l1 = len l2 /\ (a, b e. R /\ A. a1 A. _2 (nth a1 l1 = suc _2 -> A. _1 (nth a1 l2 = suc _1 -> _2, _1 e. R))))
12		bitr	(len (a : l1) = len (b : l2) <-> suc (len l1) = suc (len l2)) -> (suc (len l1) = suc (len l2) <-> len l1 = len l2) -> (len (a : l1) = len (b : l2) <-> len l1 = len l2)
13		eqeq	len (a : l1) = suc (len l1) -> len (b : l2) = suc (len l2) -> (len (a : l1) = len (b : l2) <-> suc (len l1) = suc (len l2))
14		lenS	len (a : l1) = suc (len l1)
15	13, 14	ax_mp	len (b : l2) = suc (len l2) -> (len (a : l1) = len (b : l2) <-> suc (len l1) = suc (len l2))
16		lenS	len (b : l2) = suc (len l2)
17	15, 16	ax_mp	len (a : l1) = len (b : l2) <-> suc (len l1) = suc (len l2)
18	12, 17	ax_mp	(suc (len l1) = suc (len l2) <-> len l1 = len l2) -> (len (a : l1) = len (b : l2) <-> len l1 = len l2)
19		peano2	suc (len l1) = suc (len l2) <-> len l1 = len l2
20	18, 19	ax_mp	len (a : l1) = len (b : l2) <-> len l1 = len l2
21	11, 20	ax_mp	(A. a2 A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)) <-> a, b e. R /\ A. a1 A. _2 (nth a1 l1 = suc _2 -> A. _1 (nth a1 l2 = suc _1 -> _2, _1 e. R))) -> (len (a : l1) = len (b : l2) /\ A. a2 A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)) <-> len l1 = len l2 /\ (a, b e. R /\ A. a1 A. _2 (nth a1 l1 = suc _2 -> A. _1 (nth a1 l2 = suc _1 -> _2, _1 e. R))))
22		bitr	(A. a2 A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)) <-> A. a2 ((a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) /\ (~a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))))) -> (A. a2 ((a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) /\ (~a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)))) <-> a, b e. R /\ A. a1 A. _2 (nth a1 l1 = suc _2 -> A. _1 (nth a1 l2 = suc _1 -> _2, _1 e. R))) -> (A. a2 A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)) <-> a, b e. R /\ A. a1 A. _2 (nth a1 l1 = suc _2 -> A. _1 (nth a1 l2 = suc _1 -> _2, _1 e. R)))
23		bitr3	(a2 = 0 \/ ~a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)) <-> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) -> (a2 = 0 \/ ~a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)) <-> (a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) /\ (~a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)))) -> (A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)) <-> (a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) /\ (~a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))))
24		biim1	a2 = 0 \/ ~a2 = 0 -> (a2 = 0 \/ ~a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)) <-> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)))
25		em	a2 = 0 \/ ~a2 = 0
26	24, 25	ax_mp	a2 = 0 \/ ~a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)) <-> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))
27	23, 26	ax_mp	(a2 = 0 \/ ~a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)) <-> (a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) /\ (~a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)))) -> (A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)) <-> (a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) /\ (~a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))))
28		imor	a2 = 0 \/ ~a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)) <-> (a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) /\ (~a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)))
29	27, 28	ax_mp	A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)) <-> (a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) /\ (~a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)))
30	29	aleqi	A. a2 A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)) <-> A. a2 ((a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) /\ (~a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))))
31	22, 30	ax_mp	(A. a2 ((a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) /\ (~a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)))) <-> a, b e. R /\ A. a1 A. _2 (nth a1 l1 = suc _2 -> A. _1 (nth a1 l2 = suc _1 -> _2, _1 e. R))) -> (A. a2 A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)) <-> a, b e. R /\ A. a1 A. _2 (nth a1 l1 = suc _2 -> A. _1 (nth a1 l2 = suc _1 -> _2, _1 e. R)))
32		bitr	(A. a2 ((a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) /\ (~a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)))) <-> A. a2 (a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) /\ A. a2 (~a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)))) -> (A. a2 (a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) /\ A. a2 (~a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) <-> a, b e. R /\ A. a1 A. _2 (nth a1 l1 = suc _2 -> A. _1 (nth a1 l2 = suc _1 -> _2, _1 e. R))) -> (A. a2 ((a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) /\ (~a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)))) <-> a, b e. R /\ A. a1 A. _2 (nth a1 l1 = suc _2 -> A. _1 (nth a1 l2 = suc _1 -> _2, _1 e. R)))
33		alan	A. a2 ((a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) /\ (~a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)))) <-> A. a2 (a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) /\ A. a2 (~a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)))
34	32, 33	ax_mp	(A. a2 (a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) /\ A. a2 (~a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) <-> a, b e. R /\ A. a1 A. _2 (nth a1 l1 = suc _2 -> A. _1 (nth a1 l2 = suc _1 -> _2, _1 e. R))) -> (A. a2 ((a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) /\ (~a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)))) <-> a, b e. R /\ A. a1 A. _2 (nth a1 l1 = suc _2 -> A. _1 (nth a1 l2 = suc _1 -> _2, _1 e. R)))
35		aneq	(A. a2 (a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) <-> a, b e. R) -> (A. a2 (~a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) <-> A. a1 A. _2 (nth a1 l1 = suc _2 -> A. _1 (nth a1 l2 = suc _1 -> _2, _1 e. R))) -> (A. a2 (a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) /\ A. a2 (~a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) <-> a, b e. R /\ A. a1 A. _2 (nth a1 l1 = suc _2 -> A. _1 (nth a1 l2 = suc _1 -> _2, _1 e. R)))
36		id	_2 = a -> _2 = a
37		eqidd	_2 = a -> b = b
38	36, 37	preqd	_2 = a -> _2, b = a, b
39		eqsidd	_2 = a -> R == R
40	38, 39	eleqd	_2 = a -> (_2, b e. R <-> a, b e. R)
41	40	aleqe	A. _2 (_2 = a -> _2, b e. R) <-> a, b e. R
42		eqcomb	a = _2 <-> _2 = a
43		peano2	suc a = suc _2 <-> a = _2
44		nthZ	nth 0 (a : l1) = suc a
45		ntheq1	a2 = 0 -> nth a2 (a : l1) = nth 0 (a : l1)
46	44, 45	syl6eq	a2 = 0 -> nth a2 (a : l1) = suc a
47	46	eqeq1d	a2 = 0 -> (nth a2 (a : l1) = suc _2 <-> suc a = suc _2)
48	43, 47	syl6bb	a2 = 0 -> (nth a2 (a : l1) = suc _2 <-> a = _2)
49	42, 48	syl6bb	a2 = 0 -> (nth a2 (a : l1) = suc _2 <-> _2 = a)
50		eqidd	_1 = b -> _2 = _2
51		id	_1 = b -> _1 = b
52	50, 51	preqd	_1 = b -> _2, _1 = _2, b
53		eqsidd	_1 = b -> R == R
54	52, 53	eleqd	_1 = b -> (_2, _1 e. R <-> _2, b e. R)
55	54	aleqe	A. _1 (_1 = b -> _2, _1 e. R) <-> _2, b e. R
56		eqcomb	b = _1 <-> _1 = b
57		peano2	suc b = suc _1 <-> b = _1
58		nthZ	nth 0 (b : l2) = suc b
59		ntheq1	a2 = 0 -> nth a2 (b : l2) = nth 0 (b : l2)
60	58, 59	syl6eq	a2 = 0 -> nth a2 (b : l2) = suc b
61	60	eqeq1d	a2 = 0 -> (nth a2 (b : l2) = suc _1 <-> suc b = suc _1)
62	57, 61	syl6bb	a2 = 0 -> (nth a2 (b : l2) = suc _1 <-> b = _1)
63	56, 62	syl6bb	a2 = 0 -> (nth a2 (b : l2) = suc _1 <-> _1 = b)
64	63	imeq1d	a2 = 0 -> (nth a2 (b : l2) = suc _1 -> _2, _1 e. R <-> _1 = b -> _2, _1 e. R)
65	64	aleqd	a2 = 0 -> (A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R) <-> A. _1 (_1 = b -> _2, _1 e. R))
66	55, 65	syl6bb	a2 = 0 -> (A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R) <-> _2, b e. R)
67	49, 66	imeqd	a2 = 0 -> (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R) <-> _2 = a -> _2, b e. R)
68	67	aleqd	a2 = 0 -> (A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)) <-> A. _2 (_2 = a -> _2, b e. R))
69	41, 68	syl6bb	a2 = 0 -> (A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)) <-> a, b e. R)
70	69	aleqe	A. a2 (a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) <-> a, b e. R
71	35, 70	ax_mp	(A. a2 (~a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) <-> A. a1 A. _2 (nth a1 l1 = suc _2 -> A. _1 (nth a1 l2 = suc _1 -> _2, _1 e. R))) -> (A. a2 (a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) /\ A. a2 (~a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) <-> a, b e. R /\ A. a1 A. _2 (nth a1 l1 = suc _2 -> A. _1 (nth a1 l2 = suc _1 -> _2, _1 e. R)))
72		bitr	(A. a2 (~a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) <-> A. a2 A. a1 (a2 = suc a1 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)))) -> (A. a2 A. a1 (a2 = suc a1 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) <-> A. a1 A. _2 (nth a1 l1 = suc _2 -> A. _1 (nth a1 l2 = suc _1 -> _2, _1 e. R))) -> (A. a2 (~a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) <-> A. a1 A. _2 (nth a1 l1 = suc _2 -> A. _1 (nth a1 l2 = suc _1 -> _2, _1 e. R)))
73		bitr	(~a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)) <-> E. a1 a2 = suc a1 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) -> (E. a1 a2 = suc a1 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)) <-> A. a1 (a2 = suc a1 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)))) -> (~a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)) <-> A. a1 (a2 = suc a1 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))))
74		exsuc	a2 != 0 <-> E. a1 a2 = suc a1
75	74	conv ne	~a2 = 0 <-> E. a1 a2 = suc a1
76	75	imeq1i	~a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)) <-> E. a1 a2 = suc a1 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))
77	73, 76	ax_mp	(E. a1 a2 = suc a1 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)) <-> A. a1 (a2 = suc a1 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)))) -> (~a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)) <-> A. a1 (a2 = suc a1 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))))
78		eexb	E. a1 a2 = suc a1 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)) <-> A. a1 (a2 = suc a1 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)))
79	77, 78	ax_mp	~a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)) <-> A. a1 (a2 = suc a1 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)))
80	79	aleqi	A. a2 (~a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) <-> A. a2 A. a1 (a2 = suc a1 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)))
81	72, 80	ax_mp	(A. a2 A. a1 (a2 = suc a1 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) <-> A. a1 A. _2 (nth a1 l1 = suc _2 -> A. _1 (nth a1 l2 = suc _1 -> _2, _1 e. R))) -> (A. a2 (~a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) <-> A. a1 A. _2 (nth a1 l1 = suc _2 -> A. _1 (nth a1 l2 = suc _1 -> _2, _1 e. R)))
82		bitr	(A. a2 A. a1 (a2 = suc a1 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) <-> A. a1 A. a2 (a2 = suc a1 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)))) -> (A. a1 A. a2 (a2 = suc a1 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) <-> A. a1 A. _2 (nth a1 l1 = suc _2 -> A. _1 (nth a1 l2 = suc _1 -> _2, _1 e. R))) -> (A. a2 A. a1 (a2 = suc a1 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) <-> A. a1 A. _2 (nth a1 l1 = suc _2 -> A. _1 (nth a1 l2 = suc _1 -> _2, _1 e. R)))
83		alcomb	A. a2 A. a1 (a2 = suc a1 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) <-> A. a1 A. a2 (a2 = suc a1 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)))
84	82, 83	ax_mp	(A. a1 A. a2 (a2 = suc a1 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) <-> A. a1 A. _2 (nth a1 l1 = suc _2 -> A. _1 (nth a1 l2 = suc _1 -> _2, _1 e. R))) -> (A. a2 A. a1 (a2 = suc a1 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) <-> A. a1 A. _2 (nth a1 l1 = suc _2 -> A. _1 (nth a1 l2 = suc _1 -> _2, _1 e. R)))
85		nthS	nth (suc a1) (a : l1) = nth a1 l1
86		ntheq1	a2 = suc a1 -> nth a2 (a : l1) = nth (suc a1) (a : l1)
87	85, 86	syl6eq	a2 = suc a1 -> nth a2 (a : l1) = nth a1 l1
88	87	eqeq1d	a2 = suc a1 -> (nth a2 (a : l1) = suc _2 <-> nth a1 l1 = suc _2)
89		nthS	nth (suc a1) (b : l2) = nth a1 l2
90		ntheq1	a2 = suc a1 -> nth a2 (b : l2) = nth (suc a1) (b : l2)
91	89, 90	syl6eq	a2 = suc a1 -> nth a2 (b : l2) = nth a1 l2
92	91	eqeq1d	a2 = suc a1 -> (nth a2 (b : l2) = suc _1 <-> nth a1 l2 = suc _1)
93	92	imeq1d	a2 = suc a1 -> (nth a2 (b : l2) = suc _1 -> _2, _1 e. R <-> nth a1 l2 = suc _1 -> _2, _1 e. R)
94	93	aleqd	a2 = suc a1 -> (A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R) <-> A. _1 (nth a1 l2 = suc _1 -> _2, _1 e. R))
95	88, 94	imeqd	a2 = suc a1 -> (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R) <-> nth a1 l1 = suc _2 -> A. _1 (nth a1 l2 = suc _1 -> _2, _1 e. R))
96	95	aleqd	a2 = suc a1 -> (A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)) <-> A. _2 (nth a1 l1 = suc _2 -> A. _1 (nth a1 l2 = suc _1 -> _2, _1 e. R)))
97	96	aleqe	A. a2 (a2 = suc a1 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) <-> A. _2 (nth a1 l1 = suc _2 -> A. _1 (nth a1 l2 = suc _1 -> _2, _1 e. R))
98	97	aleqi	A. a1 A. a2 (a2 = suc a1 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) <-> A. a1 A. _2 (nth a1 l1 = suc _2 -> A. _1 (nth a1 l2 = suc _1 -> _2, _1 e. R))
99	84, 98	ax_mp	A. a2 A. a1 (a2 = suc a1 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) <-> A. a1 A. _2 (nth a1 l1 = suc _2 -> A. _1 (nth a1 l2 = suc _1 -> _2, _1 e. R))
100	81, 99	ax_mp	A. a2 (~a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) <-> A. a1 A. _2 (nth a1 l1 = suc _2 -> A. _1 (nth a1 l2 = suc _1 -> _2, _1 e. R))
101	71, 100	ax_mp	A. a2 (a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) /\ A. a2 (~a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) <-> a, b e. R /\ A. a1 A. _2 (nth a1 l1 = suc _2 -> A. _1 (nth a1 l2 = suc _1 -> _2, _1 e. R))
102	34, 101	ax_mp	A. a2 ((a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) /\ (~a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)))) <-> a, b e. R /\ A. a1 A. _2 (nth a1 l1 = suc _2 -> A. _1 (nth a1 l2 = suc _1 -> _2, _1 e. R))
103	31, 102	ax_mp	A. a2 A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)) <-> a, b e. R /\ A. a1 A. _2 (nth a1 l1 = suc _2 -> A. _1 (nth a1 l2 = suc _1 -> _2, _1 e. R))
104	21, 103	ax_mp	len (a : l1) = len (b : l2) /\ A. a2 A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)) <-> len l1 = len l2 /\ (a, b e. R /\ A. a1 A. _2 (nth a1 l1 = suc _2 -> A. _1 (nth a1 l2 = suc _1 -> _2, _1 e. R)))
105	10, 104	ax_mp	a, b e. R /\ (len l1 = len l2 /\ A. a1 A. _2 (nth a1 l1 = suc _2 -> A. _1 (nth a1 l2 = suc _1 -> _2, _1 e. R))) <-> len (a : l1) = len (b : l2) /\ A. a2 A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))
106	7, 105	ax_mp	a, b e. R /\ l1, l2 e. all2 R <-> len (a : l1) = len (b : l2) /\ A. a2 A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))
107	3, 106	ax_mp	a : l1, b : l2 e. all2 R <-> a, b e. R /\ l1, l2 e. all2 R

1

(a : l1, b : l2 e. all2 R <-> len (a : l1) = len (b : l2) /\ A. a2 A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) ->
  (a, b e. R /\ l1, l2 e. all2 R <-> len (a : l1) = len (b : l2) /\ A. a2 A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)))
  ->
  (a : l1, b : l2 e. all2 R <-> a, b e. R /\ l1, l2 e. all2 R)

2

elall22

a : l1, b : l2 e. all2 R <-> len (a : l1) = len (b : l2) /\ A. a2 A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))

3

1, 2

ax_mp

(a, b e. R /\ l1, l2 e. all2 R <-> len (a : l1) = len (b : l2) /\ A. a2 A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) ->
  (a : l1, b : l2 e. all2 R <-> a, b e. R /\ l1, l2 e. all2 R)

4

bitr

(a, b e. R /\ l1, l2 e. all2 R <-> a, b e. R /\ (len l1 = len l2 /\ A. a1 A. _2 (nth a1 l1 = suc _2 -> A. _1 (nth a1 l2 = suc _1 -> _2, _1 e. R)))) ->
  (a, b e. R /\ (len l1 = len l2 /\ A. a1 A. _2 (nth a1 l1 = suc _2 -> A. _1 (nth a1 l2 = suc _1 -> _2, _1 e. R))) <->
    len (a : l1) = len (b : l2) /\ A. a2 A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) ->
  (a, b e. R /\ l1, l2 e. all2 R <-> len (a : l1) = len (b : l2) /\ A. a2 A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)))

5

elall22

l1, l2 e. all2 R <-> len l1 = len l2 /\ A. a1 A. _2 (nth a1 l1 = suc _2 -> A. _1 (nth a1 l2 = suc _1 -> _2, _1 e. R))

6

5

aneq2i

a, b e. R /\ l1, l2 e. all2 R <-> a, b e. R /\ (len l1 = len l2 /\ A. a1 A. _2 (nth a1 l1 = suc _2 -> A. _1 (nth a1 l2 = suc _1 -> _2, _1 e. R)))

7

4, 6

ax_mp

(a, b e. R /\ (len l1 = len l2 /\ A. a1 A. _2 (nth a1 l1 = suc _2 -> A. _1 (nth a1 l2 = suc _1 -> _2, _1 e. R))) <->
    len (a : l1) = len (b : l2) /\ A. a2 A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) ->
  (a, b e. R /\ l1, l2 e. all2 R <-> len (a : l1) = len (b : l2) /\ A. a2 A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)))

8

bitr4

(a, b e. R /\ (len l1 = len l2 /\ A. a1 A. _2 (nth a1 l1 = suc _2 -> A. _1 (nth a1 l2 = suc _1 -> _2, _1 e. R))) <->
    len l1 = len l2 /\ (a, b e. R /\ A. a1 A. _2 (nth a1 l1 = suc _2 -> A. _1 (nth a1 l2 = suc _1 -> _2, _1 e. R)))) ->
  (len (a : l1) = len (b : l2) /\ A. a2 A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)) <->
    len l1 = len l2 /\ (a, b e. R /\ A. a1 A. _2 (nth a1 l1 = suc _2 -> A. _1 (nth a1 l2 = suc _1 -> _2, _1 e. R)))) ->
  (a, b e. R /\ (len l1 = len l2 /\ A. a1 A. _2 (nth a1 l1 = suc _2 -> A. _1 (nth a1 l2 = suc _1 -> _2, _1 e. R))) <->
    len (a : l1) = len (b : l2) /\ A. a2 A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)))

9

anlass

a, b e. R /\ (len l1 = len l2 /\ A. a1 A. _2 (nth a1 l1 = suc _2 -> A. _1 (nth a1 l2 = suc _1 -> _2, _1 e. R))) <->
  len l1 = len l2 /\ (a, b e. R /\ A. a1 A. _2 (nth a1 l1 = suc _2 -> A. _1 (nth a1 l2 = suc _1 -> _2, _1 e. R)))

10

8, 9

ax_mp

(len (a : l1) = len (b : l2) /\ A. a2 A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)) <->
    len l1 = len l2 /\ (a, b e. R /\ A. a1 A. _2 (nth a1 l1 = suc _2 -> A. _1 (nth a1 l2 = suc _1 -> _2, _1 e. R)))) ->
  (a, b e. R /\ (len l1 = len l2 /\ A. a1 A. _2 (nth a1 l1 = suc _2 -> A. _1 (nth a1 l2 = suc _1 -> _2, _1 e. R))) <->
    len (a : l1) = len (b : l2) /\ A. a2 A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)))

11

aneq

(len (a : l1) = len (b : l2) <-> len l1 = len l2) ->
  (A. a2 A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)) <->
    a, b e. R /\ A. a1 A. _2 (nth a1 l1 = suc _2 -> A. _1 (nth a1 l2 = suc _1 -> _2, _1 e. R))) ->
  (len (a : l1) = len (b : l2) /\ A. a2 A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)) <->
    len l1 = len l2 /\ (a, b e. R /\ A. a1 A. _2 (nth a1 l1 = suc _2 -> A. _1 (nth a1 l2 = suc _1 -> _2, _1 e. R))))

12

bitr

(len (a : l1) = len (b : l2) <-> suc (len l1) = suc (len l2)) ->
  (suc (len l1) = suc (len l2) <-> len l1 = len l2) ->
  (len (a : l1) = len (b : l2) <-> len l1 = len l2)

13

eqeq

len (a : l1) = suc (len l1) -> len (b : l2) = suc (len l2) -> (len (a : l1) = len (b : l2) <-> suc (len l1) = suc (len l2))

14

lenS

len (a : l1) = suc (len l1)

15

13, 14

ax_mp

len (b : l2) = suc (len l2) -> (len (a : l1) = len (b : l2) <-> suc (len l1) = suc (len l2))

16

lenS

len (b : l2) = suc (len l2)

17

15, 16

ax_mp

len (a : l1) = len (b : l2) <-> suc (len l1) = suc (len l2)

18

12, 17

ax_mp

(suc (len l1) = suc (len l2) <-> len l1 = len l2) -> (len (a : l1) = len (b : l2) <-> len l1 = len l2)

19

peano2

suc (len l1) = suc (len l2) <-> len l1 = len l2

20

18, 19

ax_mp

len (a : l1) = len (b : l2) <-> len l1 = len l2

21

11, 20

ax_mp

(A. a2 A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)) <->
    a, b e. R /\ A. a1 A. _2 (nth a1 l1 = suc _2 -> A. _1 (nth a1 l2 = suc _1 -> _2, _1 e. R))) ->
  (len (a : l1) = len (b : l2) /\ A. a2 A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)) <->
    len l1 = len l2 /\ (a, b e. R /\ A. a1 A. _2 (nth a1 l1 = suc _2 -> A. _1 (nth a1 l2 = suc _1 -> _2, _1 e. R))))

22

bitr

(A. a2 A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)) <->
    A. a2 ((a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) /\
      (~a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))))) ->
  (A. a2 ((a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) /\
      (~a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)))) <->
    a, b e. R /\ A. a1 A. _2 (nth a1 l1 = suc _2 -> A. _1 (nth a1 l2 = suc _1 -> _2, _1 e. R))) ->
  (A. a2 A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)) <->
    a, b e. R /\ A. a1 A. _2 (nth a1 l1 = suc _2 -> A. _1 (nth a1 l2 = suc _1 -> _2, _1 e. R)))

23

bitr3

(a2 = 0 \/ ~a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)) <->
    A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) ->
  (a2 = 0 \/ ~a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)) <->
    (a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) /\
      (~a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)))) ->
  (A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)) <->
    (a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) /\
      (~a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))))

24

biim1

a2 = 0 \/ ~a2 = 0 ->
  (a2 = 0 \/ ~a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)) <->
    A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)))

25

em

a2 = 0 \/ ~a2 = 0

26

24, 25

ax_mp

a2 = 0 \/ ~a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)) <->
  A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))

27

23, 26

ax_mp

(a2 = 0 \/ ~a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)) <->
    (a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) /\
      (~a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)))) ->
  (A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)) <->
    (a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) /\
      (~a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))))

28

imor

a2 = 0 \/ ~a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)) <->
  (a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) /\
    (~a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)))

29

27, 28

ax_mp

A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)) <->
  (a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) /\
    (~a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)))

30

29

aleqi

A. a2 A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)) <->
  A. a2 ((a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) /\
    (~a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))))

31

22, 30

ax_mp

(A. a2 ((a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) /\
      (~a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)))) <->
    a, b e. R /\ A. a1 A. _2 (nth a1 l1 = suc _2 -> A. _1 (nth a1 l2 = suc _1 -> _2, _1 e. R))) ->
  (A. a2 A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)) <->
    a, b e. R /\ A. a1 A. _2 (nth a1 l1 = suc _2 -> A. _1 (nth a1 l2 = suc _1 -> _2, _1 e. R)))

32

bitr

(A. a2 ((a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) /\
      (~a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)))) <->
    A. a2 (a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) /\
      A. a2 (~a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)))) ->
  (A. a2 (a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) /\
      A. a2 (~a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) <->
    a, b e. R /\ A. a1 A. _2 (nth a1 l1 = suc _2 -> A. _1 (nth a1 l2 = suc _1 -> _2, _1 e. R))) ->
  (A. a2 ((a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) /\
      (~a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)))) <->
    a, b e. R /\ A. a1 A. _2 (nth a1 l1 = suc _2 -> A. _1 (nth a1 l2 = suc _1 -> _2, _1 e. R)))

33

alan

A. a2 ((a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) /\
    (~a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)))) <->
  A. a2 (a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) /\
    A. a2 (~a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)))

34

32, 33

ax_mp

(A. a2 (a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) /\
      A. a2 (~a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) <->
    a, b e. R /\ A. a1 A. _2 (nth a1 l1 = suc _2 -> A. _1 (nth a1 l2 = suc _1 -> _2, _1 e. R))) ->
  (A. a2 ((a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) /\
      (~a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)))) <->
    a, b e. R /\ A. a1 A. _2 (nth a1 l1 = suc _2 -> A. _1 (nth a1 l2 = suc _1 -> _2, _1 e. R)))

35

aneq

(A. a2 (a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) <-> a, b e. R) ->
  (A. a2 (~a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) <->
    A. a1 A. _2 (nth a1 l1 = suc _2 -> A. _1 (nth a1 l2 = suc _1 -> _2, _1 e. R))) ->
  (A. a2 (a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) /\
      A. a2 (~a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) <->
    a, b e. R /\ A. a1 A. _2 (nth a1 l1 = suc _2 -> A. _1 (nth a1 l2 = suc _1 -> _2, _1 e. R)))

36

id

_2 = a -> _2 = a

37

eqidd

_2 = a -> b = b

38

36, 37

preqd

_2 = a -> _2, b = a, b

39

eqsidd

_2 = a -> R == R

40

38, 39

eleqd

_2 = a -> (_2, b e. R <-> a, b e. R)

41

40

aleqe

A. _2 (_2 = a -> _2, b e. R) <-> a, b e. R

42

eqcomb

a = _2 <-> _2 = a

43

peano2

suc a = suc _2 <-> a = _2

44

nthZ

nth 0 (a : l1) = suc a

45

ntheq1

a2 = 0 -> nth a2 (a : l1) = nth 0 (a : l1)

46

44, 45

syl6eq

a2 = 0 -> nth a2 (a : l1) = suc a

47

46

eqeq1d

a2 = 0 -> (nth a2 (a : l1) = suc _2 <-> suc a = suc _2)

48

43, 47

syl6bb

a2 = 0 -> (nth a2 (a : l1) = suc _2 <-> a = _2)

49

42, 48

syl6bb

a2 = 0 -> (nth a2 (a : l1) = suc _2 <-> _2 = a)

50

eqidd

_1 = b -> _2 = _2

51

id

_1 = b -> _1 = b

52

50, 51

preqd

_1 = b -> _2, _1 = _2, b

53

eqsidd

_1 = b -> R == R

54

52, 53

eleqd

_1 = b -> (_2, _1 e. R <-> _2, b e. R)

55

54

aleqe

A. _1 (_1 = b -> _2, _1 e. R) <-> _2, b e. R

56

eqcomb

b = _1 <-> _1 = b

57

peano2

suc b = suc _1 <-> b = _1

58

nthZ

nth 0 (b : l2) = suc b

59

ntheq1

a2 = 0 -> nth a2 (b : l2) = nth 0 (b : l2)

60

58, 59

syl6eq

a2 = 0 -> nth a2 (b : l2) = suc b

61

60

eqeq1d

a2 = 0 -> (nth a2 (b : l2) = suc _1 <-> suc b = suc _1)

62

57, 61

syl6bb

a2 = 0 -> (nth a2 (b : l2) = suc _1 <-> b = _1)

63

56, 62

syl6bb

a2 = 0 -> (nth a2 (b : l2) = suc _1 <-> _1 = b)

64

63

imeq1d

a2 = 0 -> (nth a2 (b : l2) = suc _1 -> _2, _1 e. R <-> _1 = b -> _2, _1 e. R)

65

64

aleqd

a2 = 0 -> (A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R) <-> A. _1 (_1 = b -> _2, _1 e. R))

66

55, 65

syl6bb

a2 = 0 -> (A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R) <-> _2, b e. R)

67

49, 66

imeqd

a2 = 0 -> (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R) <-> _2 = a -> _2, b e. R)

68

67

aleqd

a2 = 0 -> (A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)) <-> A. _2 (_2 = a -> _2, b e. R))

69

41, 68

syl6bb

a2 = 0 -> (A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)) <-> a, b e. R)

70

69

aleqe

A. a2 (a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) <-> a, b e. R

71

35, 70

ax_mp

(A. a2 (~a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) <->
    A. a1 A. _2 (nth a1 l1 = suc _2 -> A. _1 (nth a1 l2 = suc _1 -> _2, _1 e. R))) ->
  (A. a2 (a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) /\
      A. a2 (~a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) <->
    a, b e. R /\ A. a1 A. _2 (nth a1 l1 = suc _2 -> A. _1 (nth a1 l2 = suc _1 -> _2, _1 e. R)))

72

bitr

(A. a2 (~a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) <->
    A. a2 A. a1 (a2 = suc a1 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)))) ->
  (A. a2 A. a1 (a2 = suc a1 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) <->
    A. a1 A. _2 (nth a1 l1 = suc _2 -> A. _1 (nth a1 l2 = suc _1 -> _2, _1 e. R))) ->
  (A. a2 (~a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) <->
    A. a1 A. _2 (nth a1 l1 = suc _2 -> A. _1 (nth a1 l2 = suc _1 -> _2, _1 e. R)))

73

bitr

(~a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)) <->
    E. a1 a2 = suc a1 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) ->
  (E. a1 a2 = suc a1 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)) <->
    A. a1 (a2 = suc a1 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)))) ->
  (~a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)) <->
    A. a1 (a2 = suc a1 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))))

74

exsuc

a2 != 0 <-> E. a1 a2 = suc a1

76

75

imeq1i

~a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)) <->
  E. a1 a2 = suc a1 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))

77

73, 76

ax_mp

(E. a1 a2 = suc a1 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)) <->
    A. a1 (a2 = suc a1 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)))) ->
  (~a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)) <->
    A. a1 (a2 = suc a1 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))))

78

eexb

E. a1 a2 = suc a1 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)) <->
  A. a1 (a2 = suc a1 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)))

79

77, 78

ax_mp

~a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)) <->
  A. a1 (a2 = suc a1 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)))

80

79

aleqi

A. a2 (~a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) <->
  A. a2 A. a1 (a2 = suc a1 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)))

81

72, 80

ax_mp

(A. a2 A. a1 (a2 = suc a1 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) <->
    A. a1 A. _2 (nth a1 l1 = suc _2 -> A. _1 (nth a1 l2 = suc _1 -> _2, _1 e. R))) ->
  (A. a2 (~a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) <->
    A. a1 A. _2 (nth a1 l1 = suc _2 -> A. _1 (nth a1 l2 = suc _1 -> _2, _1 e. R)))

82

bitr

(A. a2 A. a1 (a2 = suc a1 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) <->
    A. a1 A. a2 (a2 = suc a1 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)))) ->
  (A. a1 A. a2 (a2 = suc a1 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) <->
    A. a1 A. _2 (nth a1 l1 = suc _2 -> A. _1 (nth a1 l2 = suc _1 -> _2, _1 e. R))) ->
  (A. a2 A. a1 (a2 = suc a1 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) <->
    A. a1 A. _2 (nth a1 l1 = suc _2 -> A. _1 (nth a1 l2 = suc _1 -> _2, _1 e. R)))

83

alcomb

A. a2 A. a1 (a2 = suc a1 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) <->
  A. a1 A. a2 (a2 = suc a1 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)))

84

82, 83

ax_mp

(A. a1 A. a2 (a2 = suc a1 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) <->
    A. a1 A. _2 (nth a1 l1 = suc _2 -> A. _1 (nth a1 l2 = suc _1 -> _2, _1 e. R))) ->
  (A. a2 A. a1 (a2 = suc a1 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) <->
    A. a1 A. _2 (nth a1 l1 = suc _2 -> A. _1 (nth a1 l2 = suc _1 -> _2, _1 e. R)))

85

nthS

nth (suc a1) (a : l1) = nth a1 l1

86

ntheq1

a2 = suc a1 -> nth a2 (a : l1) = nth (suc a1) (a : l1)

87

85, 86

syl6eq

a2 = suc a1 -> nth a2 (a : l1) = nth a1 l1

88

87

eqeq1d

a2 = suc a1 -> (nth a2 (a : l1) = suc _2 <-> nth a1 l1 = suc _2)

89

nthS

nth (suc a1) (b : l2) = nth a1 l2

90

ntheq1

a2 = suc a1 -> nth a2 (b : l2) = nth (suc a1) (b : l2)

91

89, 90

syl6eq

a2 = suc a1 -> nth a2 (b : l2) = nth a1 l2

92

91

eqeq1d

a2 = suc a1 -> (nth a2 (b : l2) = suc _1 <-> nth a1 l2 = suc _1)

93

92

imeq1d

a2 = suc a1 -> (nth a2 (b : l2) = suc _1 -> _2, _1 e. R <-> nth a1 l2 = suc _1 -> _2, _1 e. R)

94

93

aleqd

a2 = suc a1 -> (A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R) <-> A. _1 (nth a1 l2 = suc _1 -> _2, _1 e. R))

95

88, 94

imeqd

a2 = suc a1 -> (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R) <-> nth a1 l1 = suc _2 -> A. _1 (nth a1 l2 = suc _1 -> _2, _1 e. R))

96

95

aleqd

a2 = suc a1 ->
  (A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)) <->
    A. _2 (nth a1 l1 = suc _2 -> A. _1 (nth a1 l2 = suc _1 -> _2, _1 e. R)))

97

96

aleqe

A. a2 (a2 = suc a1 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) <->
  A. _2 (nth a1 l1 = suc _2 -> A. _1 (nth a1 l2 = suc _1 -> _2, _1 e. R))

98

97

aleqi

A. a1 A. a2 (a2 = suc a1 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) <->
  A. a1 A. _2 (nth a1 l1 = suc _2 -> A. _1 (nth a1 l2 = suc _1 -> _2, _1 e. R))

99

84, 98

ax_mp

A. a2 A. a1 (a2 = suc a1 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) <->
  A. a1 A. _2 (nth a1 l1 = suc _2 -> A. _1 (nth a1 l2 = suc _1 -> _2, _1 e. R))

100

81, 99

ax_mp

A. a2 (~a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) <->
  A. a1 A. _2 (nth a1 l1 = suc _2 -> A. _1 (nth a1 l2 = suc _1 -> _2, _1 e. R))

101

71, 100

ax_mp

A. a2 (a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) /\
    A. a2 (~a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) <->
  a, b e. R /\ A. a1 A. _2 (nth a1 l1 = suc _2 -> A. _1 (nth a1 l2 = suc _1 -> _2, _1 e. R))

102

34, 101

ax_mp

A. a2 ((a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))) /\
    (~a2 = 0 -> A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)))) <->
  a, b e. R /\ A. a1 A. _2 (nth a1 l1 = suc _2 -> A. _1 (nth a1 l2 = suc _1 -> _2, _1 e. R))

103

31, 102

ax_mp

A. a2 A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)) <->
  a, b e. R /\ A. a1 A. _2 (nth a1 l1 = suc _2 -> A. _1 (nth a1 l2 = suc _1 -> _2, _1 e. R))

104

21, 103

ax_mp

len (a : l1) = len (b : l2) /\ A. a2 A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R)) <->
  len l1 = len l2 /\ (a, b e. R /\ A. a1 A. _2 (nth a1 l1 = suc _2 -> A. _1 (nth a1 l2 = suc _1 -> _2, _1 e. R)))

105

10, 104

ax_mp

a, b e. R /\ (len l1 = len l2 /\ A. a1 A. _2 (nth a1 l1 = suc _2 -> A. _1 (nth a1 l2 = suc _1 -> _2, _1 e. R))) <->
  len (a : l1) = len (b : l2) /\ A. a2 A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))

106

7, 105

ax_mp

a, b e. R /\ l1, l2 e. all2 R <-> len (a : l1) = len (b : l2) /\ A. a2 A. _2 (nth a2 (a : l1) = suc _2 -> A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R))

107

3, 106

ax_mp

a : l1, b : l2 e. all2 R <-> a, b e. R /\ l1, l2 e. all2 R

Theorem all2S ≪ | index | src | ≫

Axiom use