---

Step * 1 of Lemma sp-join-top


1. x : Sierpinski
2. ⊤ = ⊥ ∈ Sierpinski
⊢ x = ⊥ ∈ Sierpinski
BY
{ TACTIC:(InstLemma `Sierpinski-unequal` [] THEN Auto) }

---

Latex:

---

Latex:

1.  x  :  Sierpinski
2.  \mtop{}  =  \mbot{}
\mvdash{}  x  =  \mbot{}


By

---

Latex:
TACTIC:(InstLemma  `Sierpinski-unequal`  []  THEN  Auto)

---

Home Index