---

Step * of Lemma exception-not-value

∀[t:Base]. is-exception(t) ⇒ False supposing (t)↓
BY
{ (Auto THEN Unfold `is-exception` -1 THEN FLemma `exception-not-value_1` [-1] THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[t:Base].  is-exception(t)  {}\mRightarrow{}  False  supposing  (t)\mdownarrow{}


By

---

Latex:
(Auto  THEN  Unfold  `is-exception`  -1  THEN  FLemma  `exception-not-value\_1`  [-1]  THEN  Auto)

---

Home Index