---

Step * of Lemma strictness-callbyvalueall

∀[F:Top]. (let x ⟵ ⊥ in F[x] ~ ⊥)
BY
{ ((UnivCD THENA Auto)
   THEN Unfold `callbyvalueall` 0
   THEN (Subst' evalall(⊥) ~ ⊥ 0 THENA (RecUnfold `evalall` 0 THEN SqReasoning))
   THEN SqReasoning) }

---

Latex:

---

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


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  Unfold  `callbyvalueall`  0
  THEN  (Subst'  evalall(\mbot{})  \msim{}  \mbot{}  0  THENA  (RecUnfold  `evalall`  0  THEN  SqReasoning))
  THEN  SqReasoning)

---

Home Index