---

Step * of Lemma exception-not-bottom_1

∀[nm,val:Base].  ((exception(nm; val) ≤ ⊥) ⇒ False)
BY
{ (Auto THEN Refine_exceptionNotBottom ⌜nm⌝ ⌜val⌝⋅ THEN Hypothesis) }

---

Latex:

---

Latex:
\mforall{}[nm,val:Base].    ((exception(nm;  val)  \mleq{}  \mbot{})  {}\mRightarrow{}  False)


By

---

Latex:
(Auto  THEN  Refine\_exceptionNotBottom  \mkleeneopen{}nm\mkleeneclose{}  \mkleeneopen{}val\mkleeneclose{}\mcdot{}  THEN  Hypothesis)

---

Home Index