---

Step * of Lemma name-morphs-equal

∀[I,J:Cname List]. ∀[f:name-morph(I;J)]. ∀[g:nameset(I) ⟶ extd-nameset(J)].
  f = g ∈ name-morph(I;J) supposing f = g ∈ (nameset(I) ⟶ extd-nameset(J))
BY
{ (Auto THEN D 3 THEN EqTypeCD THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[I,J:Cname  List].  \mforall{}[f:name-morph(I;J)].  \mforall{}[g:nameset(I)  {}\mrightarrow{}  extd-nameset(J)].    f  =  g  supposing  f  =  g


By

---

Latex:
(Auto  THEN  D  3  THEN  EqTypeCD  THEN  Auto)

---

Home Index