---

Step * of Lemma null-ite

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

---

Latex:

---

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


By

---

Latex:
xxx((UnivCD  THENA  Auto)  THEN  SplitOnConclITE  THEN  Auto)xxx

---

Home Index