---

Step * 3 1 1 1 1 1 2 1 of Lemma FOL-bound-rename


1. v : ℤ List
2. ¬(v = [] ∈ (ℤ List))
⊢ ¬(imax-list(v) + 1 ∈ v)
BY
{ (D 0 THEN Auto) }

1
1. v : ℤ List
2. ¬(v = [] ∈ (ℤ List))
3. (imax-list(v) + 1 ∈ v)
⊢ False

---

Latex:

---

Latex:

1.  v  :  \mBbbZ{}  List
2.  \mneg{}(v  =  [])
\mvdash{}  \mneg{}(imax-list(v)  +  1  \mmember{}  v)


By

---

Latex:
(D  0  THEN  Auto)

---

Home Index