Step * of Lemma trivial_ite_2

[b:𝔹]. ∀[a:Top].  (if then else fi  a)
BY
Auto }


Latex:


Latex:
\mforall{}[b:\mBbbB{}].  \mforall{}[a:Top].    (if  b  then  a  else  a  fi    \msim{}  a)


By


Latex:
Auto




Home Index