---

Step * 1 1 1 of Lemma trivial-mFOL-rename


1. x : ℤ
2. y : ℤ
3. name : Atom
4. vars : ℤ List
5. ¬(y ∈ remove-repeats(IntDeq;vars))
6. x1 : ℤ
7. (x1 ∈ vars)
8. x1 = y ∈ ℤ
⊢ x = x1 ∈ ℤ
BY
{ (D -4 THEN EAuto 1) }

---

Latex:

---

Latex:

1.  x  :  \mBbbZ{}
2.  y  :  \mBbbZ{}
3.  name  :  Atom
4.  vars  :  \mBbbZ{}  List
5.  \mneg{}(y  \mmember{}  remove-repeats(IntDeq;vars))
6.  x1  :  \mBbbZ{}
7.  (x1  \mmember{}  vars)
8.  x1  =  y
\mvdash{}  x  =  x1


By

---

Latex:
(D  -4  THEN  EAuto  1)

---

Home Index