Step * of Lemma ite_rw_false

[T:Type]. ∀[b:𝔹]. ∀[x,y:T].  if then else fi  y ∈ 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