---

Step * of Lemma strict4-callbyvalueall

∀[C:Base]. strict4(λx,y,z,w. let x ⟵ x in C[x])
BY
{ (Auto THEN ProveStrict) }

---

Latex:

---

Latex:
\mforall{}[C:Base].  strict4(\mlambda{}x,y,z,w.  let  x  \mleftarrow{}{}  x  in  C[x])


By

---

Latex:
(Auto  THEN  ProveStrict)

---

Home Index