---

Step * of Lemma bor_bnot

∀[a:Top]. (a ∨b(¬ba) ~ a ∨btt)
BY
{ (RepUR ``bor bnot ifthenelse`` 0 THEN SqReasoning) }

---

Latex:

---

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


By

---

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

---

Home Index