---

Step * of Lemma strictness-spread

∀[F:Top]. (let a,b = ⊥ in F[a;b] ~ ⊥)
BY
{ (SqReasoning THEN Assert ⌜(⊥)↓⌝⋅ THEN BotDiv THEN ProveHasValue) }

---

Latex:

---

Latex:
\mforall{}[F:Top].  (let  a,b  =  \mbot{}  in  F[a;b]  \msim{}  \mbot{})


By

---

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

---

Home Index