---

Step * of Lemma no-value-bottom-base

∀[x:Base]. x ~ ⊥ supposing (¬(x)↓) ∧ (¬is-exception(x))
BY
{ (SqReasoning THEN Try ((InstLemma `is-exception_wf` [⌜x⌝]⋅ THEN Auto))) }

---

Latex:

---

Latex:
\mforall{}[x:Base].  x  \msim{}  \mbot{}  supposing  (\mneg{}(x)\mdownarrow{})  \mwedge{}  (\mneg{}is-exception(x))


By

---

Latex:
(SqReasoning  THEN  Try  ((InstLemma  `is-exception\_wf`  [\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THEN  Auto)))

---

Home Index