---

Step * of Lemma list-subtype-bag

∀[A,B:Type].  (A List) ⊆r bag(B) supposing A ⊆r B
BY
{ (((Auto THEN D 0) THENM MemTypeCD) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A,B:Type].    (A  List)  \msubseteq{}r  bag(B)  supposing  A  \msubseteq{}r  B


By

---

Latex:
(((Auto  THEN  D  0)  THENM  MemTypeCD)  THEN  Auto)

---

Home Index