---

Step * of Lemma lifting-strict-isint

∀[F:Base]. ∀[p,q,r:Top].
  ∀[a,b,c:Top].  (F[if a is an integer then b else c;p;q;r] ~ if a is an integer then F[b;p;q;r] else F[c;p;q;r]) 
  supposing strict4(λx,y,z,w. F[x;y;z;w])
BY
{ SqReasoning }

---

Latex:

---

Latex:
\mforall{}[F:Base].  \mforall{}[p,q,r:Top].
    \mforall{}[a,b,c:Top].
        (F[if  a  is  an  integer  then  b
              else  c;p;q;r]  \msim{}  if  a  is  an  integer  then  F[b;p;q;r]
                                              else  F[c;p;q;r]) 
    supposing  strict4(\mlambda{}x,y,z,w.  F[x;y;z;w])


By

---

Latex:
SqReasoning

---

Home Index