---

Step * of Lemma strictness-decide

∀[F,G:Top].  (case ⊥ of inl(x) => F[x] | inr(x) => G[x] ~ ⊥)
BY
{ (SqReasoning THEN Assert ⌜(⊥)↓⌝⋅ THEN BotDiv THEN ProveHasValue) }

---

Latex:

---

Latex:
\mforall{}[F,G:Top].    (case  \mbot{}  of  inl(x)  =>  F[x]  |  inr(x)  =>  G[x]  \msim{}  \mbot{})


By

---

Latex:
(SqReasoning  THEN  Assert  \mkleeneopen{}(\mbot{})\mdownarrow{}\mkleeneclose{}\mcdot{}  THEN  BotDiv  THEN  ProveHasValue)

---

Home Index