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	36	preq1d	_2 = a -> _2, b = a, b
38	37	eleq1d	_2 = a -> (_2, b e. R <-> a, b e. R)
39	38	aleqe	A. _2 (_2 = a -> _2, b e. R) <-> a, b e. R
40		eqcomb	a = _2 <-> _2 = a
41		peano2	suc a = suc _2 <-> a = _2
42		nthZ	nth 0 (a : l1) = suc a
43		ntheq1	a2 = 0 -> nth a2 (a : l1) = nth 0 (a : l1)
44	42, 43	syl6eq	a2 = 0 -> nth a2 (a : l1) = suc a
45	44	eqeq1d	a2 = 0 -> (nth a2 (a : l1) = suc _2 <-> suc a = suc _2)
46	41, 45	syl6bb	a2 = 0 -> (nth a2 (a : l1) = suc _2 <-> a = _2)
47	40, 46	syl6bb	a2 = 0 -> (nth a2 (a : l1) = suc _2 <-> _2 = a)
48		id	_1 = b -> _1 = b
49	48	preq2d	_1 = b -> _2, _1 = _2, b
50	49	eleq1d	_1 = b -> (_2, _1 e. R <-> _2, b e. R)
51	50	aleqe	A. _1 (_1 = b -> _2, _1 e. R) <-> _2, b e. R
52		eqcomb	b = _1 <-> _1 = b
53		peano2	suc b = suc _1 <-> b = _1
54		nthZ	nth 0 (b : l2) = suc b
55		ntheq1	a2 = 0 -> nth a2 (b : l2) = nth 0 (b : l2)
56	54, 55	syl6eq	a2 = 0 -> nth a2 (b : l2) = suc b
57	56	eqeq1d	a2 = 0 -> (nth a2 (b : l2) = suc _1 <-> suc b = suc _1)
58	53, 57	syl6bb	a2 = 0 -> (nth a2 (b : l2) = suc _1 <-> b = _1)
59	52, 58	syl6bb	a2 = 0 -> (nth a2 (b : l2) = suc _1 <-> _1 = b)
60	59	imeq1d	a2 = 0 -> (nth a2 (b : l2) = suc _1 -> _2, _1 e. R <-> _1 = b -> _2, _1 e. R)
61	60	aleqd	a2 = 0 -> (A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R) <-> A. _1 (_1 = b -> _2, _1 e. R))
62	51, 61	syl6bb	a2 = 0 -> (A. _1 (nth a2 (b : l2) = suc _1 -> _2, _1 e. R) <-> _2, b e. R)
63	47, 62	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)
64	63	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))
65	39, 64	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)
66	65	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
67	35, 66	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)))
68		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)))
69		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))))
70		exsuc	a2 != 0 <-> E. a1 a2 = suc a1
71	70	conv ne	~a2 = 0 <-> E. a1 a2 = suc a1
72	71	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))
73	69, 72	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))))
74		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)))
75	73, 74	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)))
76	75	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)))
77	68, 76	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)))
78		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)))
79		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)))
80	78, 79	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)))
81		nthS	nth (suc a1) (a : l1) = nth a1 l1
82		ntheq1	a2 = suc a1 -> nth a2 (a : l1) = nth (suc a1) (a : l1)
83	81, 82	syl6eq	a2 = suc a1 -> nth a2 (a : l1) = nth a1 l1
84	83	eqeq1d	a2 = suc a1 -> (nth a2 (a : l1) = suc _2 <-> nth a1 l1 = suc _2)
85		nthS	nth (suc a1) (b : l2) = nth a1 l2
86		ntheq1	a2 = suc a1 -> nth a2 (b : l2) = nth (suc a1) (b : l2)
87	85, 86	syl6eq	a2 = suc a1 -> nth a2 (b : l2) = nth a1 l2
88	87	eqeq1d	a2 = suc a1 -> (nth a2 (b : l2) = suc _1 <-> nth a1 l2 = suc _1)
89	88	imeq1d	a2 = suc a1 -> (nth a2 (b : l2) = suc _1 -> _2, _1 e. R <-> nth a1 l2 = suc _1 -> _2, _1 e. R)
90	89	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))
91	84, 90	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))
92	91	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)))
93	92	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))
94	93	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))
95	80, 94	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))
96	77, 95	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))
97	67, 96	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))
98	34, 97	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))
99	31, 98	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))
100	21, 99	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)))
101	10, 100	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))
102	7, 101	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))
103	3, 102	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

36

preq1d

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

38

37

eleq1d

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

39

38

aleqe

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

40

eqcomb

a = _2 <-> _2 = a

41

peano2

suc a = suc _2 <-> a = _2

42

nthZ

nth 0 (a : l1) = suc a

43

ntheq1

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

44

42, 43

syl6eq

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

45

44

eqeq1d

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

46

41, 45

syl6bb

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

47

40, 46

syl6bb

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

48

id

_1 = b -> _1 = b

49

48

preq2d

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

50

49

eleq1d

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

51

50

aleqe

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

52

eqcomb

b = _1 <-> _1 = b

53

peano2

suc b = suc _1 <-> b = _1

54

nthZ

nth 0 (b : l2) = suc b

55

ntheq1

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

56

54, 55

syl6eq

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

57

56

eqeq1d

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

58

53, 57

syl6bb

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

59

52, 58

syl6bb

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

60

59

imeq1d

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

61

60

aleqd

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

62

51, 61

syl6bb

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

63

47, 62

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)

64

63

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))

65

39, 64

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)

66

65

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

67

35, 66

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)))

68

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)))

69

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))))

70

exsuc

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

72

71

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))

73

69, 72

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))))

74

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)))

75

73, 74

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)))

76

75

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)))

77

68, 76

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)))

78

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)))

79

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)))

80

78, 79

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)))

81

nthS

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

82

ntheq1

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

83

81, 82

syl6eq

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

84

83

eqeq1d

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

85

nthS

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

86

ntheq1

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

87

85, 86

syl6eq

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

88

87

eqeq1d

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

89

88

imeq1d

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

90

89

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))

91

84, 90

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))

92

91

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)))

93

92

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))

94

93

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))

95

80, 94

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))

96

77, 95

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))

97

67, 96

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))

98

34, 97

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))

99

31, 98

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))

100

21, 99

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)))

101

10, 100

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))

102

7, 101

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))

103

3, 102

ax_mp

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

Theorem all2S ≪ | index | src | ≫

Axiom use