---

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


1. ∀[T:Type]. (canonicalizable(T) ⇒ (T ⊆r Base))
⊢ False
BY
{ ((InstHyp [⌜ℕ ⟶ ℕ⌝] (-1)⋅ THEN Try (CpltAuto))
   THEN (Assert ⌜(λx.x) = (λx.(x + 0)) ∈ (ℕ ⟶ ℕ)⌝⋅ THENA Auto)
   THEN (Assert ⌜(λx.x) = (λx.(x + 0)) ∈ Base⌝⋅ THENA Auto)) }

1
1. ∀[T:Type]. (canonicalizable(T) ⇒ (T ⊆r Base))
2. (ℕ ⟶ ℕ) ⊆r Base
3. (λx.x) = (λx.(x + 0)) ∈ (ℕ ⟶ ℕ)
4. (λx.x) = (λx.(x + 0)) ∈ Base
⊢ False

---

Latex:

---

Latex:

1.  \mforall{}[T:Type].  (canonicalizable(T)  {}\mRightarrow{}  (T  \msubseteq{}r  Base))
\mvdash{}  False


By

---

Latex:
((InstHyp  [\mkleeneopen{}\mBbbN{}  {}\mrightarrow{}  \mBbbN{}\mkleeneclose{}]  (-1)\mcdot{}  THEN  Try  (CpltAuto))
  THEN  (Assert  \mkleeneopen{}(\mlambda{}x.x)  =  (\mlambda{}x.(x  +  0))\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (Assert  \mkleeneopen{}(\mlambda{}x.x)  =  (\mlambda{}x.(x  +  0))\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index