---

Step * of Lemma free-from-atom2-int

∀[a:Atom2]. ∀[n:ℤ].  a#n:ℤ
BY
{ (Auto THEN (Decide n < 0 THENA Auto)) }

1
1. a : Atom2
2. n : ℤ
3. n < 0
⊢ a#n:ℤ

2
1. a : Atom2
2. n : ℤ
3. ¬n < 0
⊢ a#n:ℤ

---

Latex:

---

Latex:
\mforall{}[a:Atom2].  \mforall{}[n:\mBbbZ{}].    a\#n:\mBbbZ{}


By

---

Latex:
(Auto  THEN  (Decide  n  <  0  THENA  Auto))

---

Home Index