---

Step * of Lemma strictness-add-right

∀[a:Top]. (a + ⊥ ~ eval x = a in ⊥)
BY
{ SqReasoning }

---

Latex:

---

Latex:
\mforall{}[a:Top].  (a  +  \mbot{}  \msim{}  eval  x  =  a  in  \mbot{})


By

---

Latex:
SqReasoning

---

Home Index