---

Step * of Lemma name-morph-range_wf

∀[I,J:Cname List]. ∀[f:name-morph(I;J)].  (name-morph-range(f;I) ∈ Type)
BY
{ (Auto THEN Unfold `name-morph-range` 0 THEN Auto THEN FLemma `assert-isname` [-1] THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[I,J:Cname  List].  \mforall{}[f:name-morph(I;J)].    (name-morph-range(f;I)  \mmember{}  Type)


By

---

Latex:
(Auto  THEN  Unfold  `name-morph-range`  0  THEN  Auto  THEN  FLemma  `assert-isname`  [-1]  THEN  Auto)

---

Home Index