---

Step * of Lemma ite_rw_true

∀[T:Type]. ∀[b:𝔹]. ∀[x,y:T].  if b then x else y fi  = x ∈ T supposing ↑b
BY
{ Auto }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[b:\mBbbB{}].  \mforall{}[x,y:T].    if  b  then  x  else  y  fi    =  x  supposing  \muparrow{}b


By

---

Latex:
Auto

---

Home Index