---

Step * of Lemma strict4-decide

strict4(λx,y,z,w. case x of inl(x) => y[x] | inr(x) => z[x])
BY
{ ProveStrict }

---

Latex:

---

Latex:
strict4(\mlambda{}x,y,z,w.  case  x  of  inl(x)  =>  y[x]  |  inr(x)  =>  z[x])


By

---

Latex:
ProveStrict

---

Home Index