---

Step * of Lemma not-assert-isname

∀[L:Cname List]. ∀[z:extd-nameset(L)].  uiff(¬↑isname(z);z ∈ ℕ2)
BY
{ (TACTIC:Intros THEN (RepeatFor 2 (D 0) THENW ((Assert z ∈ Base BY Auto) THEN Auto))) }

1
1. L : Cname List
2. z : extd-nameset(L)
3. ¬↑isname(z)
⊢ z ∈ ℕ2

2
1. L : Cname List
2. z : extd-nameset(L)
3. z ∈ ℕ2
⊢ ¬↑isname(z)

---

Latex:

---

Latex:
\mforall{}[L:Cname  List].  \mforall{}[z:extd-nameset(L)].    uiff(\mneg{}\muparrow{}isname(z);z  \mmember{}  \mBbbN{}2)


By

---

Latex:
(TACTIC:Intros  THEN  (RepeatFor  2  (D  0)  THENW  ((Assert  z  \mmember{}  Base  BY  Auto)  THEN  Auto)))

---

Home Index