---

Step * of Lemma iflift_sq_1

∀[c:𝔹]. ∀[f,x,y:Top].  (f[if c then x else y fi ] ~ if c then f[x] else f[y] fi )
BY
{ Auto }

---

Latex:

---

Latex:
\mforall{}[c:\mBbbB{}].  \mforall{}[f,x,y:Top].    (f[if  c  then  x  else  y  fi  ]  \msim{}  if  c  then  f[x]  else  f[y]  fi  )


By

---

Latex:
Auto

---

Home Index