---

Step * 1 of Lemma name-morph_subtype


1. I : Cname List
2. J : Cname List
3. A : Cname List
4. B : Cname List
5. nameset(J) ⊆r nameset(B)
6. nameset(A) ⊆r nameset(I)
⊢ name-morph(I;J) ⊆r name-morph(A;B)
BY
{ (Assert extd-nameset(J) ⊆r extd-nameset(B) BY
         (Unfold `extd-nameset` 0 THEN Auto)) }

1
1. I : Cname List
2. J : Cname List
3. A : Cname List
4. B : Cname List
5. nameset(J) ⊆r nameset(B)
6. nameset(A) ⊆r nameset(I)
7. extd-nameset(J) ⊆r extd-nameset(B)
⊢ name-morph(I;J) ⊆r name-morph(A;B)

---

Latex:

---

Latex:

1.  I  :  Cname  List
2.  J  :  Cname  List
3.  A  :  Cname  List
4.  B  :  Cname  List
5.  nameset(J)  \msubseteq{}r  nameset(B)
6.  nameset(A)  \msubseteq{}r  nameset(I)
\mvdash{}  name-morph(I;J)  \msubseteq{}r  name-morph(A;B)


By

---

Latex:
(Assert  extd-nameset(J)  \msubseteq{}r  extd-nameset(B)  BY
              (Unfold  `extd-nameset`  0  THEN  Auto))

---

Home Index