---

Step * of Lemma new-name_wf

∀[I:fset(ℕ)]. (new-name(I) ∈ {i:ℕ| ¬i ∈ I} )
BY
{ (Auto THEN (Assert new-name(I) ∈ ℕ BY ProveWfLemma) THEN MemTypeCD THEN Auto) }

1
.....set predicate..... 
1. I : fset(ℕ)
2. new-name(I) ∈ ℕ
⊢ ¬new-name(I) ∈ I

---

Latex:

---

Latex:
\mforall{}[I:fset(\mBbbN{})].  (new-name(I)  \mmember{}  \{i:\mBbbN{}|  \mneg{}i  \mmember{}  I\}  )


By

---

Latex:
(Auto  THEN  (Assert  new-name(I)  \mmember{}  \mBbbN{}  BY  ProveWfLemma)  THEN  MemTypeCD  THEN  Auto)

---

Home Index