---

Step * of Lemma iflift_1

∀[A,B:Type]. ∀[c:𝔹]. ∀[f:A ⟶ B]. ∀[x,y:A].  (f[if c then x else y fi ] = if c then f[x] else f[y] fi  ∈ B)
BY
{ Auto }

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[c:\mBbbB{}].  \mforall{}[f:A  {}\mrightarrow{}  B].  \mforall{}[x,y:A].
    (f[if  c  then  x  else  y  fi  ]  =  if  c  then  f[x]  else  f[y]  fi  )


By

---

Latex:
Auto

---

Home Index