---

Step * of Lemma free-from-atom2-subtype

∀[A,B:Type].  ∀[x:A]. ∀[a:Atom2].  a#x:B supposing a#x:A supposing A ⊆r B
BY
{ (Intros THEN (Assert a#x:A ∈ Type BY Auto) THEN Auto THEN FreeFromAtomApElim ⌜x⌝⋅) }

---

Latex:

---

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


By

---

Latex:
(Intros  THEN  (Assert  a\#x:A  \mmember{}  Type  BY  Auto)  THEN  Auto  THEN  FreeFromAtomApElim  \mkleeneopen{}x\mkleeneclose{}\mcdot{})

---

Home Index