---

Step * of Lemma squash_thru_uequiv_rel

∀[T:Type]. ∀[E:T ⟶ T ⟶ ℙ].  ((↓UniformEquivRel(T;x,y.E[x;y])) ⇒ UniformEquivRel(T;x,y.↓E[x;y]))
BY
{ (RepUnfolds ``uequiv_rel urefl usym utrans`` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[E:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].    ((\mdownarrow{}UniformEquivRel(T;x,y.E[x;y]))  {}\mRightarrow{}  UniformEquivRel(T;x,y.\mdownarrow{}E[x;y]))


By

---

Latex:
(RepUnfolds  ``uequiv\_rel  urefl  usym  utrans``  0  THEN  Auto)

---

Home Index