---

Step * of Lemma equiv-on-quotient

∀T:Type. ∀R:T ⟶ T ⟶ ℙ.
  (EquivRel(T;x,y.x R y)
  ⇒ (∀Q:(x,y:T//(x R y)) ⟶ (x,y:T//(x R y)) ⟶ ℙ. (EquivRel(x,y:T//(x R y);u,v.u Q v) ⇒ EquivRel(T;x,y.x Q y))))
BY
{ (Auto THEN RepeatFor 7 (ParallelLast)) }

---

Latex:

---

Latex:
\mforall{}T:Type.  \mforall{}R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}.
    (EquivRel(T;x,y.x  R  y)
    {}\mRightarrow{}  (\mforall{}Q:(x,y:T//(x  R  y))  {}\mrightarrow{}  (x,y:T//(x  R  y))  {}\mrightarrow{}  \mBbbP{}
                (EquivRel(x,y:T//(x  R  y);u,v.u  Q  v)  {}\mRightarrow{}  EquivRel(T;x,y.x  Q  y))))


By

---

Latex:
(Auto  THEN  RepeatFor  7  (ParallelLast))

---

Home Index