---

Step * of Lemma decide-bottom

∀[x:Top]. (case x of inl(a) => ⊥ | inr(b) => ⊥ ~ eval u = x in ⊥)
BY
{ SqReasoning }

---

Latex:

---

Latex:
\mforall{}[x:Top].  (case  x  of  inl(a)  =>  \mbot{}  |  inr(b)  =>  \mbot{}  \msim{}  eval  u  =  x  in  \mbot{})


By

---

Latex:
SqReasoning

---

Home Index