---

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


1. tt ~ ⊥@i
⊢ False
BY
{ (InstLemma `sqequalIffSqle` [⌜tt⌝;⌜⊥⌝]⋅ THEN Auto)⋅ }

1
1. tt ~ ⊥@i
2. tt ≤ ⊥
3. ⊥ ≤ tt
⊢ False

---

Latex:

---

Latex:

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


By

---

Latex:
(InstLemma  `sqequalIffSqle`  [\mkleeneopen{}tt\mkleeneclose{};\mkleeneopen{}\mbot{}\mkleeneclose{}]\mcdot{}  THEN  Auto)\mcdot{}

---

Home Index