---

Step * 2 of Lemma respects-equality-list


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)
BY
{ ((D 0 THENA Auto)
   THEN Intros
   THEN (InstLemma `length_wf_nat` [⌜B⌝;⌜x⌝]⋅ THENA Auto)
   THEN (D 4 With ⌜||x||⌝  THENA Auto)) }

1
1. A : Type
2. B : Type
3. respects-equality(A;B)
4. x : Base
5. y : Base
6. x = y ∈ (A List)
7. x ∈ B List
8. ||x|| ∈ ℕ
9. respects-equality({as:A List| ||as|| = ||x|| ∈ ℤ} ;{bs:B List| ||bs|| = ||x|| ∈ ℤ} )
⊢ x = y ∈ (B List)

---

Latex:

---

Latex:

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


By

---

Latex:
((D  0  THENA  Auto)
  THEN  Intros
  THEN  (InstLemma  `length\_wf\_nat`  [\mkleeneopen{}B\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (D  4  With  \mkleeneopen{}||x||\mkleeneclose{}    THENA  Auto))

---

Home Index