---

Step * of Lemma Sierpinski-unequal

¬(⊥ = ⊤ ∈ Sierpinski)
BY
{ TACTIC:(InstLemma `Sierpinski-unequal-1` [] THEN Auto THEN (D 0 THENA Auto) THEN EqTypeHD (-1) THEN Auto) }

---

Latex:

---

Latex:
\mneg{}(\mbot{}  =  \mtop{})


By

---

Latex:
TACTIC:(InstLemma  `Sierpinski-unequal-1`  []
                THEN  Auto
                THEN  (D  0  THENA  Auto)
                THEN  EqTypeHD  (-1)
                THEN  Auto)

---

Home Index