---

Step * of Lemma assert-face-name-eq

∀[I:Cname List]. ∀[a,b:nameset(I) × ℕ2].  uiff(↑face-name-eq(a;b);a = b ∈ (nameset(I) × ℕ2))
BY
{ (RepUR ``nameset face-name-eq coordinate_name`` 0
   THEN (UnivCD THENA Auto)
   THEN (RWO "assert-product-deq" 0 THEN Auto)
   THEN HypSubst' (-1) 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[I:Cname  List].  \mforall{}[a,b:nameset(I)  \mtimes{}  \mBbbN{}2].    uiff(\muparrow{}face-name-eq(a;b);a  =  b)


By

---

Latex:
(RepUR  ``nameset  face-name-eq  coordinate\_name``  0
  THEN  (UnivCD  THENA  Auto)
  THEN  (RWO  "assert-product-deq"  0  THEN  Auto)
  THEN  HypSubst'  (-1)  0
  THEN  Auto)

---

Home Index