---

Step * of Lemma all_quot_elim

∀[T:Type]. ∀[E:T ⟶ T ⟶ ℙ].
  (EquivRel(T;x,y.E[x;y])
  ⇒ (∀[F:(x,y:T//E[x;y]) ⟶ ℙ]. ((∀w:x,y:T//E[x;y]. SqStable(F w)) ⇒ (∀z:x,y:T//E[x;y]. F[z] ⇐⇒ ∀z:T. F[z]))))
BY
{ Unfolds ``so_apply`` 0 }

1
∀[T:Type]. ∀[E:T ⟶ T ⟶ ℙ].
  (EquivRel(T;x,y.E x y)
  ⇒ (∀[F:(x,y:T//(E x y)) ⟶ ℙ]. ((∀w:x,y:T//(E x y). SqStable(F w)) ⇒ (∀z:x,y:T//(E x y). (F z) ⇐⇒ ∀z:T. (F z)))))

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[E:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].
    (EquivRel(T;x,y.E[x;y])
    {}\mRightarrow{}  (\mforall{}[F:(x,y:T//E[x;y])  {}\mrightarrow{}  \mBbbP{}]
                ((\mforall{}w:x,y:T//E[x;y].  SqStable(F  w))  {}\mRightarrow{}  (\mforall{}z:x,y:T//E[x;y].  F[z]  \mLeftarrow{}{}\mRightarrow{}  \mforall{}z:T.  F[z]))))


By

---

Latex:
Unfolds  ``so\_apply``  0

---

Home Index