---

Step * of Lemma subst-exc-basecase

∀[v:Top]. ∀[e:Atom2].  (subst-exc(e;exception(e; v)) ~ ⊥)
BY
{ (Auto THEN (Subst' subst-exc(e;exception(e; v)) ~ if e=2 e then ⊥ else (exception(e; v)) 0 THENA Computation)) }

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

---

Latex:

---

Latex:
\mforall{}[v:Top].  \mforall{}[e:Atom2].    (subst-exc(e;exception(e;  v))  \msim{}  \mbot{})


By

---

Latex:
(Auto
  THEN  (Subst'  subst-exc(e;exception(e;  v))  \msim{}  if  e=2  e
                                                                                            then  \mbot{}
                                                                                            else  (exception(e;  v))  0
              THENA  Computation
              )
  )

---

Home Index