---

Step * of Lemma all-quotient-true3

∀T:Type. (canonicalizable(T) ⇒ (∀P:T ⟶ ℙ. (∀t:T. ⇃(P[t]) ⇐⇒ ⇃(∀t:T. P[t]))))
BY
{ ((UnivCD THENA Auto) THEN D (-2)) }

1
1. T : Type@i'
2. f : T ⟶ Base@i
3. ∀x:T. ((f x) = x ∈ T)@i
4. P : T ⟶ ℙ@i'
⊢ ∀t:T. ⇃(P[t]) ⇐⇒ ⇃(∀t:T. P[t])

---

Latex:

---

Latex:
\mforall{}T:Type.  (canonicalizable(T)  {}\mRightarrow{}  (\mforall{}P:T  {}\mrightarrow{}  \mBbbP{}.  (\mforall{}t:T.  \00D9(P[t])  \mLeftarrow{}{}\mRightarrow{}  \00D9(\mforall{}t:T.  P[t]))))


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  D  (-2))

---

Home Index