---

Step * of Lemma band_bnot

∀[a:Top]. (a ∧b (¬ba) ~ a ∧b ff)
BY
{ (RepUR ``band bnot ifthenelse`` 0 THEN SqReasoning) }

---

Latex:

---

Latex:
\mforall{}[a:Top].  (a  \mwedge{}\msubb{}  (\mneg{}\msubb{}a)  \msim{}  a  \mwedge{}\msubb{}  ff)


By

---

Latex:
(RepUR  ``band  bnot  ifthenelse``  0  THEN  SqReasoning)

---

Home Index