---

Step * of Lemma change-equality-type

∀[A,B:Type].  (respects-equality(A;B) ⇒ (∀x,y:A.  ((x = y ∈ A) ⇒ (x ∈ B) ⇒ (x = y ∈ B))))
BY
{ Intros }

1
1. A : Type
2. B : Type
3. respects-equality(A;B)
4. x : A
5. y : A
6. x = y ∈ A
7. x ∈ B
⊢ x = y ∈ B

---

Latex:

---

Latex:
\mforall{}[A,B:Type].    (respects-equality(A;B)  {}\mRightarrow{}  (\mforall{}x,y:A.    ((x  =  y)  {}\mRightarrow{}  (x  \mmember{}  B)  {}\mRightarrow{}  (x  =  y))))


By

---

Latex:
Intros

---

Home Index