---

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


1. A : Type
2. B : Type
3. respects-equality(A;B)
⊢ (∀i:ℕ||[]||. ([][i] ∈ B)) ⇒ ([] ∈ B List)
BY
{ (Reduce 0 THEN Auto) }

---

Latex:

---

Latex:

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


By

---

Latex:
(Reduce  0  THEN  Auto)

---

Home Index