---

Step * of Lemma equal-wf

∀[X,Y,A:Type].  (respects-equality(Y;A) ⇒ respects-equality(X;A) ⇒ (∀[a:X]. ∀[b:Y].  (a = b ∈ A ∈ ℙ)))
BY
{ (Intros THEN Unfolds ``member prop`` 0) }

1
1. X : Type
2. Y : Type
3. A : Type
4. respects-equality(Y;A)
5. respects-equality(X;A)
6. a : X
7. b : Y
⊢ (a = b ∈ A) = (a = b ∈ A) ∈ Type

---

Latex:

---

Latex:
\mforall{}[X,Y,A:Type].    (respects-equality(Y;A)  {}\mRightarrow{}  respects-equality(X;A)  {}\mRightarrow{}  (\mforall{}[a:X].  \mforall{}[b:Y].    (a  =  b  \mmember{}  \mBbbP{})))


By

---

Latex:
(Intros  THEN  Unfolds  ``member  prop``  0)

---

Home Index