---

Step * of Lemma lifting-strict-ifthenelse

∀[F:Base]. ∀[p,q,r:Top].
  ∀[a,A,B:Top].  (F[if a then A else B fi ;p;q;r] ~ if a then F[A;p;q;r] else F[B;p;q;r] fi ) 
  supposing strict4(λx,y,z,w. F[x;y;z;w])
BY
{ Auto }

1
1. F : Base
2. p : Top
3. q : Top
4. r : Top
5. strict4(λx,y,z,w. F[x;y;z;w])
6. a : Top
7. A : Top
8. B : Top
⊢ F[if a then A else B fi ;p;q;r] ~ if a then F[A;p;q;r] else F[B;p;q;r] fi 

---

Latex:

---

Latex:
\mforall{}[F:Base].  \mforall{}[p,q,r:Top].
    \mforall{}[a,A,B:Top].    (F[if  a  then  A  else  B  fi  ;p;q;r]  \msim{}  if  a  then  F[A;p;q;r]  else  F[B;p;q;r]  fi  ) 
    supposing  strict4(\mlambda{}x,y,z,w.  F[x;y;z;w])


By

---

Latex:
Auto

---

Home Index