Step * of Lemma lifting-strict-isaxiom

[F:Base]. ∀[p,q,r:Top].
  ∀[a,b,c:Top].  (F[if Ax then otherwise c;p;q;r] if 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