---

Step * of Lemma respects-equality-list-type

∀[A,B:Type].  ∀L:A List. ((∀i:ℕ||L||. (L[i] ∈ B)) ⇒ (L ∈ B List)) supposing respects-equality(A;B)
BY
{ RepeatFor 3 (Intro) }

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

---

Latex:

---

Latex:
\mforall{}[A,B:Type].    \mforall{}L:A  List.  ((\mforall{}i:\mBbbN{}||L||.  (L[i]  \mmember{}  B))  {}\mRightarrow{}  (L  \mmember{}  B  List))  supposing  respects-equality(A;B)


By

---

Latex:
RepeatFor  3  (Intro)

---

Home Index