---

Step * of Lemma not-canonicalizable-implies-subtype-base

¬(∀[T:Type]. (canonicalizable(T) ⇒ (T ⊆r Base)))
BY
{ (D 0 THENA Auto) }

1
1. ∀[T:Type]. (canonicalizable(T) ⇒ (T ⊆r Base))
⊢ False

---

Latex:

---

Latex:
\mneg{}(\mforall{}[T:Type].  (canonicalizable(T)  {}\mRightarrow{}  (T  \msubseteq{}r  Base)))


By

---

Latex:
(D  0  THENA  Auto)

---

Home Index