---

Step * 1 of Lemma respects-equality-list

.....assertion..... 
1. A : Type
2. B : Type
3. respects-equality(A;B)
⊢ ∀n:ℕ. respects-equality({as:A List| ||as|| = n ∈ ℤ} ;{bs:B List| ||bs|| = n ∈ ℤ} )
BY
{ InductionOnNat }

1
.....basecase..... 
1. A : Type
2. B : Type
3. respects-equality(A;B)
4. n : ℤ
⊢ respects-equality({as:A List| ||as|| = 0 ∈ ℤ} ;{bs:B List| ||bs|| = 0 ∈ ℤ} )

2
.....upcase..... 
1. A : Type
2. B : Type
3. respects-equality(A;B)
4. n : ℤ
5. 0 < n
6. respects-equality({as:A List| ||as|| = (n - 1) ∈ ℤ} ;{bs:B List| ||bs|| = (n - 1) ∈ ℤ} )
⊢ respects-equality({as:A List| ||as|| = n ∈ ℤ} ;{bs:B List| ||bs|| = n ∈ ℤ} )

---

Latex:

---

Latex:
.....assertion..... 
1.  A  :  Type
2.  B  :  Type
3.  respects-equality(A;B)
\mvdash{}  \mforall{}n:\mBbbN{}.  respects-equality(\{as:A  List|  ||as||  =  n\}  ;\{bs:B  List|  ||bs||  =  n\}  )


By

---

Latex:
InductionOnNat

---

Home Index