---

Step * 1 1 of Lemma not_has-value_decidable_on_base


1. magic : ∀t:Base. ((t)↓ ∨ (¬(t)↓))@i
2. (λx.x)↓
⊢ ¬(case magic ⊥ of inl(a) => ⊥ | inr(b) => λx.x ≤ case magic (λx.x) of inl(a) => ⊥ | inr(b) => λx.x)
BY
{ (InstLemma `bottom_diverge` [] THEN InstLemma `not-id-sqle-bottom` []) }

1
1. magic : ∀t:Base. ((t)↓ ∨ (¬(t)↓))@i
2. (λx.x)↓
3. ¬(⊥)↓
4. ¬(λx.x ≤ ⊥)
⊢ ¬(case magic ⊥ of inl(a) => ⊥ | inr(b) => λx.x ≤ case magic (λx.x) of inl(a) => ⊥ | inr(b) => λx.x)

---

Latex:

---

Latex:

1.  magic  :  \mforall{}t:Base.  ((t)\mdownarrow{}  \mvee{}  (\mneg{}(t)\mdownarrow{}))@i
2.  (\mlambda{}x.x)\mdownarrow{}
\mvdash{}  \mneg{}(case  magic  \mbot{}  of  inl(a)  =>  \mbot{}  |  inr(b)  =>  \mlambda{}x.x  \mleq{}  case  magic  (\mlambda{}x.x)
          of  inl(a)  =>
          \mbot{}
          |  inr(b)  =>
          \mlambda{}x.x)


By

---

Latex:
(InstLemma  `bottom\_diverge`  []  THEN  InstLemma  `not-id-sqle-bottom`  [])

---

Home Index