---

Step * of Lemma assert-eq-cname

∀[x,y:Cname].  uiff(↑eq-cname(x;y);x = y ∈ Cname)
BY
{ ((UnivCD THENA Auto) THEN Unfold `eq-cname` 0 THEN RWO "assert-deq" 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[x,y:Cname].    uiff(\muparrow{}eq-cname(x;y);x  =  y)


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  Unfold  `eq-cname`  0  THEN  RWO  "assert-deq"  0  THEN  Auto)

---

Home Index