---

Step * of Lemma callbyvalueall-ifthenelse

∀[C:Base]. ∀[a,A,B:Top].
  (let x ⟵ if a then A else B fi 
   in C[x] ~ if a then let x ⟵ A in C[x] else let x ⟵ B in C[x] fi )
BY
{ (Auto
   THEN InstLemma `lifting-strict-ifthenelse` 
   [⌜so_lambda(z,y,u,v.let x ⟵ z in C[x])⌝;⌜⋅⌝;⌜⋅⌝;⌜⋅⌝;⌜a⌝;⌜A⌝;⌜B⌝]⋅
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[C:Base].  \mforall{}[a,A,B:Top].
    (let  x  \mleftarrow{}{}  if  a  then  A  else  B  fi 
      in  C[x]  \msim{}  if  a  then  let  x  \mleftarrow{}{}  A  in  C[x]  else  let  x  \mleftarrow{}{}  B  in  C[x]  fi  )


By

---

Latex:
(Auto
  THEN  InstLemma  `lifting-strict-ifthenelse` 
  [\mkleeneopen{}so\_lambda(z,y,u,v.let  x  \mleftarrow{}{}  z  in  C[x])\mkleeneclose{};\mkleeneopen{}\mcdot{}\mkleeneclose{};\mkleeneopen{}\mcdot{}\mkleeneclose{};\mkleeneopen{}\mcdot{}\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index