---

Step * of Lemma ite-same

∀[b:𝔹]. ∀[x:Top].  (if b then x else x fi  ~ x)
BY
{ ((UnivCD THENA Auto) THEN SplitOnConclITE THEN Auto) }

---

Latex:


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


By

((UnivCD  THENA  Auto)  THEN  SplitOnConclITE  THEN  Auto)

---

Home Index