Step
*
of Lemma
trivial_ite_2
∀[b:𝔹]. ∀[a:Top].  (if b then a else a 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