---

Step * of Lemma lifting-strict-isaxiom

∀[F:Base]. ∀[p,q,r:Top].
  ∀[a,b,c:Top].  (F[if a = Ax then b otherwise c;p;q;r] ~ if a = Ax then F[b;p;q;r] otherwise 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  =  Ax  then  b  otherwise  c;p;q;r]  \msim{}  if  a  =  Ax  then  F[b;p;q;r]  otherwise  F[c;p;q;r]) 
    supposing  strict4(\mlambda{}x,y,z,w.  F[x;y;z;w])


By

---

Latex:
SqReasoning

---

Home Index