---

Step * 1 of Lemma subst-exc-basecase


1. v : Top
2. e : Atom2
⊢ if e=2 e
   then ⊥
   else (exception(e; v)) ~ ⊥
BY
{ AutoSplit }

---

Latex:

---

Latex:

1.  v  :  Top
2.  e  :  Atom2
\mvdash{}  if  e=2  e
      then  \mbot{}
      else  (exception(e;  v))  \msim{}  \mbot{}


By

---

Latex:
AutoSplit

---

Home Index