---

Step * of Lemma strictness-callbyvalue

∀[F:Top]. (eval x = ⊥ in F[x] ~ ⊥)
BY
{ (SqReasoning THEN BotDiv) }

---

Latex:

---

Latex:
\mforall{}[F:Top].  (eval  x  =  \mbot{}  in  F[x]  \msim{}  \mbot{})


By

---

Latex:
(SqReasoning  THEN  BotDiv)

---

Home Index