---

Step * of Lemma free-from-atom-outr

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

1
1. A : Type
2. x : A
3. a : Atom1
4. a#inr x :Top + A
5. ¬False
⊢ a#x:A

---

Latex:

---

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


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'  `y'\mcdot{})

---

Home Index