---

Step * 1 1 of Lemma axiom-choice-C0

.....rewrite subgoal..... 
1. P : n:ℕ ⟶ (ℕn ⟶ 𝔹) ⟶ ℙ@i'
2. ∀f:ℕ ⟶ 𝔹. ⇃(∃m:ℕ. (P m f))@i
⊢ ⇃(canonicalizable(ℕ ⟶ 𝔹))
BY
{ ((BLemma `implies-prop-truncation`⋅ THENA Auto) THEN BLemma `canonicalizable-function` THEN Auto) }

---

Latex:

---

Latex:
.....rewrite  subgoal..... 
1.  P  :  n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  \mBbbB{})  {}\mrightarrow{}  \mBbbP{}@i'
2.  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}.  \00D9(\mexists{}m:\mBbbN{}.  (P  m  f))@i
\mvdash{}  \00D9(canonicalizable(\mBbbN{}  {}\mrightarrow{}  \mBbbB{}))


By

---

Latex:
((BLemma  `implies-prop-truncation`\mcdot{}  THENA  Auto)  THEN  BLemma  `canonicalizable-function`  THEN  Auto)

---

Home Index