---

Step * 1 of Lemma free-from-atom-outr


1. A : Type
2. x : A
3. a : Atom1
4. a#inr x :Top + A
5. ¬False
⊢ a#x:A
BY
{ ((Subst' x ~ (λx.case x of inl(a) => 0 | inr(a) => a) (inr x ) 0 THEN Try ((Reduce 0 THEN Complete (Auto))))⋅
   THEN ((Assert inr x  ∈ Top + A BY
                Auto)
         THEN Subst' A ~ case inr x  of inl(a) => ℤ | inr(a) => A 0
         THEN Try ((Reduce 0 THEN Complete (Auto))))
   THEN (FreeFromAtomApElim ⌜inr x ⌝⋅ THEN FreeFromAtomTriviality THEN Auto)
   THEN D -1
   THEN Reduce 0
   THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  A  :  Type
2.  x  :  A
3.  a  :  Atom1
4.  a\#inr  x  :Top  +  A
5.  \mneg{}False
\mvdash{}  a\#x:A


By

---

Latex:
((Subst'  x  \msim{}  (\mlambda{}x.case  x  of  inl(a)  =>  0  |  inr(a)  =>  a)  (inr  x  )  0
    THEN  Try  ((Reduce  0  THEN  Complete  (Auto)))
    )\mcdot{}
  THEN  ((Assert  inr  x    \mmember{}  Top  +  A  BY
                            Auto)
              THEN  Subst'  A  \msim{}  case  inr  x    of  inl(a)  =>  \mBbbZ{}  |  inr(a)  =>  A  0
              THEN  Try  ((Reduce  0  THEN  Complete  (Auto))))
  THEN  (FreeFromAtomApElim  \mkleeneopen{}inr  x  \mkleeneclose{}\mcdot{}  THEN  FreeFromAtomTriviality  THEN  Auto)
  THEN  D  -1
  THEN  Reduce  0
  THEN  Auto)\mcdot{}

---

Home Index