---

Step * 1 1 1 1 of Lemma all-quotient-true


1. T : Type
2. canonicalizable(T)
3. P : T ⟶ ℙ
4. ∀t:T. ⇃(P t)
5. f,g:∀t:T. P[t]//dep-fun-equiv(T;t,x,y.↓True;f;g)
⊢ ⇃(∀t:T. (P t))
BY
{ (RenameVar `f' (-1) THEN UseWitness ⌜f⌝⋅ THEN (D -1 THENA EAuto 2) THEN EqTypeCD THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  canonicalizable(T)
3.  P  :  T  {}\mrightarrow{}  \mBbbP{}
4.  \mforall{}t:T.  \00D9(P  t)
5.  f,g:\mforall{}t:T.  P[t]//dep-fun-equiv(T;t,x,y.\mdownarrow{}True;f;g)
\mvdash{}  \00D9(\mforall{}t:T.  (P  t))


By

---

Latex:
(RenameVar  `f'  (-1)  THEN  UseWitness  \mkleeneopen{}f\mkleeneclose{}\mcdot{}  THEN  (D  -1  THENA  EAuto  2)  THEN  EqTypeCD  THEN  Auto)

---

Home Index