---

Step * of Lemma free-from-atom-subtype

∀[A,B:Type].  ∀[x:A]. ∀[a:Atom1].  a#x:B supposing a#x:A supposing A ⊆r B
BY
{ (Repeat (D 0 THENA Complete Auto)
   THEN At ⌜Type⌝ Auto⋅
   THEN FreeFromAtomApElim x⋅
   THEN FreeFromAtomTriviality
   THEN Auto
   THEN DoSubsume
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A,B:Type].    \mforall{}[x:A].  \mforall{}[a:Atom1].    a\#x:B  supposing  a\#x:A  supposing  A  \msubseteq{}r  B


By

---

Latex:
(Repeat  (D  0  THENA  Complete  Auto)
  THEN  At  \mkleeneopen{}Type\mkleeneclose{}  Auto\mcdot{}
  THEN  FreeFromAtomApElim  x\mcdot{}
  THEN  FreeFromAtomTriviality
  THEN  Auto
  THEN  DoSubsume
  THEN  Auto)

---

Home Index