---

Step * of Lemma test-bnot-nbot

∀[p:Top]. (¬b¬bp ~ p ∧b tt)
BY
{ ((UnivCD THENA Auto) THEN SymbComp 0 THEN Auto)⋅ }

---

Latex:

---

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


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  SymbComp  0  THEN  Auto)\mcdot{}

---

Home Index