---

Step * of Lemma respects-equality-list

∀[A,B:Type].  respects-equality(A List;B List) supposing respects-equality(A;B)
BY
{ (Intros THEN (Unhide THENA Auto) THEN Assert ⌜∀n:ℕ. respects-equality({as:A List| ||as|| = n ∈ ℤ} ;{bs:B List| ||bs|| \000C= n ∈ ℤ} )⌝⋅) }

1
.....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 ∈ ℤ} )

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

---

Latex:

---

Latex:
\mforall{}[A,B:Type].    respects-equality(A  List;B  List)  supposing  respects-equality(A;B)


By

---

Latex:
(Intros  THEN  (Unhide  THENA  Auto)  THEN  Assert  \mkleeneopen{}\mforall{}n:\mBbbN{}.  respects-equality(\{as:A  List|  ||as||  =  n\}  ;\{bs:B\000C  List|  ||bs||  =  n\}  )\mkleeneclose{}\mcdot{})

---

Home Index