---

Step * 1 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
{ (GenUnivCD THENA Auto) }

1
1. [T] : Type
2. [E] : T ⟶ T ⟶ ℙ
3. EquivRel(T;x,y.E x y)
4. [F] : (x,y:T//(E x y)) ⟶ ℙ
5. ∀w:x,y:T//(E x y). SqStable(F w)
6. ∀z:x,y:T//(E x y). (F z)
7. z : T
⊢ F z

2
1. [T] : Type
2. [E] : T ⟶ T ⟶ ℙ
3. EquivRel(T;x,y.E x y)
4. [F] : (x,y:T//(E x y)) ⟶ ℙ
5. ∀w:x,y:T//(E x y). SqStable(F w)
6. ∀z:T. (F z)
7. z : x,y:T//(E x y)
⊢ 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:
(GenUnivCD  THENA  Auto)

---

Home Index