---

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


1. A : Type
2. x : A
3. a : Atom1
4. a#inl x:A + Top
5. True
⊢ a#x:A
BY
{ ((Subst' x ~ (λx.case x of inl(a) => a | inr(a) => 0) (inl x) 0 THEN Try ((Reduce 0 THEN Complete (Auto))))⋅
   THEN ((Assert inl x ∈ A + Top BY
                Auto)
         THEN Subst' A ~ case inl x of inl(a) => A | inr(a) => ℤ 0
         THEN Try ((Reduce 0 THEN Complete (Auto))))
   THEN (FreeFromAtomApElim ⌜inl 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\#inl  x:A  +  Top
5.  True
\mvdash{}  a\#x:A


By

---

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

---

Home Index