---

Step * of Lemma nameset_subtype

∀[L1,L2:Cname List].  nameset(L1) ⊆r nameset(L2) supposing l_subset(Cname;L1;L2)
BY
{ (Unfold `nameset` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[L1,L2:Cname  List].    nameset(L1)  \msubseteq{}r  nameset(L2)  supposing  l\_subset(Cname;L1;L2)


By

---

Latex:
(Unfold  `nameset`  0  THEN  Auto)

---

Home Index