---

Step * 1 of Lemma respects-equality-list-type


1. [A] : Type
2. [B] : Type
3. [%] : respects-equality(A;B)
⊢ ∀L:A List. ((∀i:ℕ||L||. (L[i] ∈ B)) ⇒ (L ∈ B List))
BY
{ InductionOnList }

1
1. A : Type
2. B : Type
3. respects-equality(A;B)
⊢ (∀i:ℕ||[]||. ([][i] ∈ B)) ⇒ ([] ∈ B List)

2
1. A : Type
2. B : Type
3. respects-equality(A;B)
4. u : A
5. v : A List
6. (∀i:ℕ||v||. (v[i] ∈ B)) ⇒ (v ∈ B List)
⊢ (∀i:ℕ||[u / v]||. ([u / v][i] ∈ B)) ⇒ ([u / v] ∈ B List)

---

Latex:

---

Latex:

1.  [A]  :  Type
2.  [B]  :  Type
3.  [\%]  :  respects-equality(A;B)
\mvdash{}  \mforall{}L:A  List.  ((\mforall{}i:\mBbbN{}||L||.  (L[i]  \mmember{}  B))  {}\mRightarrow{}  (L  \mmember{}  B  List))


By

---

Latex:
InductionOnList

---

Home Index