---

Step * of Lemma strictness-isatom1

∀[a,b:Top].  (isatom1(⊥;a;b) ~ ⊥)
BY
{ (SqReasoning THEN BotDiv) }

---

Latex:

---

Latex:
\mforall{}[a,b:Top].    (isatom1(\mbot{};a;b)  \msim{}  \mbot{})


By

---

Latex:
(SqReasoning  THEN  BotDiv)

---

Home Index