---

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


1. T : Type
2. canonicalizable(T)
3. P : T ⟶ ℙ
4. ∀t:T. ⇃(P t)
⊢ ⇃(∀t:T. (P t))
BY
{ ((InstLemma `all-quotient-dependent` [⌜T⌝;⌜P⌝;⌜so_lambda(t,x,y.True)⌝]⋅ THENA Auto)
   THEN D -1
   THEN Thin (-1)
   THEN (D -1 THENA Auto)) }

1
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))

---

Latex:

---

Latex:

1.  T  :  Type
2.  canonicalizable(T)
3.  P  :  T  {}\mrightarrow{}  \mBbbP{}
4.  \mforall{}t:T.  \00D9(P  t)
\mvdash{}  \00D9(\mforall{}t:T.  (P  t))


By

---

Latex:
((InstLemma  `all-quotient-dependent`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}P\mkleeneclose{};\mkleeneopen{}so\_lambda(t,x,y.True)\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  D  -1
  THEN  Thin  (-1)
  THEN  (D  -1  THENA  Auto))

---

Home Index