---

Step * of Lemma lifting-strict-callbyvalue

∀[F:Base]. ∀[p,q,r:Top].  ∀[a,B:Top].  (F[eval x = a in B[x];p;q;r] ~ eval x = a in F[B[x];p;q;r]) supposing strict4(λx,\000Cy,z,w. F[x;y;z;w])
BY
{ SqReasoning }

---

Latex:

---

Latex:
\mforall{}[F:Base].  \mforall{}[p,q,r:Top].
    \mforall{}[a,B:Top].    (F[eval  x  =  a  in  B[x];p;q;r]  \msim{}  eval  x  =  a  in  F[B[x];p;q;r])  supposing  strict4(\mlambda{}x,y,z,\000Cw.  F[x;y;z;w])


By

---

Latex:
SqReasoning

---

Home Index