---

Step * of Lemma fresh-nat-exists

∀L:ℕ List. ∃n:ℕ. ∀i:ℕ||L||. L[i] < n
BY
{ (Auto THEN D 1 THEN Reduce 0) }

1
∃n:ℕ. ∀i:ℕ0. ⊥ < n

2
1. u : ℕ
2. v : ℕ List
⊢ ∃n:ℕ. ∀i:ℕ||v|| + 1. [u / v][i] < n

---

Latex:

---

Latex:
\mforall{}L:\mBbbN{}  List.  \mexists{}n:\mBbbN{}.  \mforall{}i:\mBbbN{}||L||.  L[i]  <  n


By

---

Latex:
(Auto  THEN  D  1  THEN  Reduce  0)

---

Home Index