---

Step * of Lemma not_has-value_decidable_on_base

¬(∀t:Base. ((t)↓ ∨ (¬(t)↓)))
BY
{ ((D 0 THENA Auto) THEN RenameVar `magic' (-1)) }

1
1. magic : ∀t:Base. ((t)↓ ∨ (¬(t)↓))@i
⊢ False

---

Latex:

---

Latex:
\mneg{}(\mforall{}t:Base.  ((t)\mdownarrow{}  \mvee{}  (\mneg{}(t)\mdownarrow{})))


By

---

Latex:
((D  0  THENA  Auto)  THEN  RenameVar  `magic'  (-1))

---

Home Index