---

Step * 1 1 of Lemma not-btrue-sqeq-bottom


1. tt ~ ⊥@i
2. tt ≤ ⊥
3. ⊥ ≤ tt
⊢ False
BY
{ (InstLemma `not-btrue-sqle-bottom` [] THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  tt  \msim{}  \mbot{}@i
2.  tt  \mleq{}  \mbot{}
3.  \mbot{}  \mleq{}  tt
\mvdash{}  False


By

---

Latex:
(InstLemma  `not-btrue-sqle-bottom`  []  THEN  Auto)\mcdot{}

---

Home Index