---

Step * of Lemma respects-equality-set

∀[A,T:Type]. ∀[P:T ⟶ ℙ].  (respects-equality(A;T) ⇒ respects-equality(A;{x:T| P[x]} ))
BY
{ (Auto THEN RepeatFor 5 (ParallelLast) THEN MemTypeHD 9 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A,T:Type].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbP{}].    (respects-equality(A;T)  {}\mRightarrow{}  respects-equality(A;\{x:T|  P[x]\}  ))


By

---

Latex:
(Auto  THEN  RepeatFor  5  (ParallelLast)  THEN  MemTypeHD  9  THEN  Auto)

---

Home Index