---

Step * of Lemma choice-iff-canonicalizable

∀T:Type. (ChoicePrinciple(T) ⇐⇒ ⇃(canonicalizable(T)))
BY
{ Auto }

1
1. T : Type
2. ChoicePrinciple(T)
⊢ ⇃(canonicalizable(T))

2
1. T : Type
2. ⇃(canonicalizable(T))
⊢ ChoicePrinciple(T)

---

Latex:

---

Latex:
\mforall{}T:Type.  (ChoicePrinciple(T)  \mLeftarrow{}{}\mRightarrow{}  \00D9(canonicalizable(T)))


By

---

Latex:
Auto

---

Home Index