---

Step * of Lemma free-from-atom-outl

∀[A:Type]. ∀[x:A + Top]. ∀[a:Atom1].  (a#outl(x):A) supposing ((↑isl(x)) and a#x:A + Top)
BY
{ (Repeat ((D 0 THENA Complete (Auto)))⋅
   THEN At ⌜𝕌'⌝ Auto⋅
   THEN (DVar `x' THEN All Reduce)
   THEN Auto
   THEN RenameTo `x' `x1'⋅) }

1
1. A : Type
2. x : A
3. a : Atom1
4. a#inl x:A + Top
5. True
⊢ a#x:A

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[x:A  +  Top].  \mforall{}[a:Atom1].    (a\#outl(x):A)  supposing  ((\muparrow{}isl(x))  and  a\#x:A  +  Top)


By

---

Latex:
(Repeat  ((D  0  THENA  Complete  (Auto)))\mcdot{}
  THEN  At  \mkleeneopen{}\mBbbU{}'\mkleeneclose{}  Auto\mcdot{}
  THEN  (DVar  `x'  THEN  All  Reduce)
  THEN  Auto
  THEN  RenameTo  `x'  `x1'\mcdot{})

---

Home Index