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