---

Step * of Lemma respects-equality-sets

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

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  RepeatFor  4  (ParallelLast)  THEN  EqTypeHD    (-1)  THEN  Auto)

---

Home Index