---

Step * of Lemma fresh-nat-exists2

∀L:ℕ List. ∃n:ℕ. (¬(n ∈ L))
BY
{ (InstLemma `fresh-nat-exists` [] THEN RepeatFor 2 (ParallelLast) THEN (D 0 THENA Auto) THEN RepeatFor 2 (D -1)) }

1
1. ∀L:ℕ List. ∃n:ℕ. ∀i:ℕ||L||. L[i] < n
2. L : ℕ List
3. n : ℕ
4. ∀i:ℕ||L||. L[i] < n
5. i : ℕ
6. i < ||L||
7. n = L[i] ∈ ℕ
⊢ False

---

Latex:

---

Latex:
\mforall{}L:\mBbbN{}  List.  \mexists{}n:\mBbbN{}.  (\mneg{}(n  \mmember{}  L))


By

---

Latex:
(InstLemma  `fresh-nat-exists`  []
  THEN  RepeatFor  2  (ParallelLast)
  THEN  (D  0  THENA  Auto)
  THEN  RepeatFor  2  (D  -1))

---

Home Index