---

Step * of Lemma fun_thru_ite

∀[S,T:Type]. ∀[f:S ⟶ T]. ∀[b:𝔹]. ∀[p,q:S].  ((f if b then p else q fi ) = if b then f p else f q fi  ∈ T)
BY
{ Auto }

---

Latex:

---

Latex:
\mforall{}[S,T:Type].  \mforall{}[f:S  {}\mrightarrow{}  T].  \mforall{}[b:\mBbbB{}].  \mforall{}[p,q:S].
    ((f  if  b  then  p  else  q  fi  )  =  if  b  then  f  p  else  f  q  fi  )


By

---

Latex:
Auto

---

Home Index