---

Step * of Lemma free-from-atom-bool

∀[a:Atom1]. ∀[n:𝔹].  a#n:𝔹
BY
{ (Auto THEN AutoBoolCase ⌜n⌝⋅) }

---

Latex:

---

Latex:
\mforall{}[a:Atom1].  \mforall{}[n:\mBbbB{}].    a\#n:\mBbbB{}


By

---

Latex:
(Auto  THEN  AutoBoolCase  \mkleeneopen{}n\mkleeneclose{}\mcdot{})

---

Home Index