---

Step * of Lemma isname-name

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

---

Latex:

---

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


By

---

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

---

Home Index