---

Step * of Lemma decide-bnot

∀[d,F,G:Top].  (case ¬bd of inl(x) => F | inr(y) => G ~ case d of inl(y) => G | inr(x) => F)
BY
{ ((UnivCD THENA Auto) THEN RepUR ``bnot ifthenelse btrue bfalse`` 0 THEN RW LiftAllC 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[d,F,G:Top].    (case  \mneg{}\msubb{}d  of  inl(x)  =>  F  |  inr(y)  =>  G  \msim{}  case  d  of  inl(y)  =>  G  |  inr(x)  =>  F)


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  RepUR  ``bnot  ifthenelse  btrue  bfalse``  0  THEN  RW  LiftAllC  0  THEN  Auto)

---

Home Index