---

Step * of Lemma isname-nameset

∀[L:Cname List]. ∀[z:nameset(L)].  (isname(z) ~ tt)
BY
{ (Intros THEN UseWitness ⌜Ax⌝⋅ THEN D -1 THEN D -2 THEN RepUR ``isname`` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[L:Cname  List].  \mforall{}[z:nameset(L)].    (isname(z)  \msim{}  tt)


By

---

Latex:
(Intros  THEN  UseWitness  \mkleeneopen{}Ax\mkleeneclose{}\mcdot{}  THEN  D  -1  THEN  D  -2  THEN  RepUR  ``isname``  0  THEN  Auto)

---

Home Index