---

Step * of Lemma ite_rw_false

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

---

Latex:

---

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


By

---

Latex:
Auto

---

Home Index