---

Step * of Lemma bag-subtype-list

∀T:Type. (bag(T) ⊆r (Top List))
BY
{ (Auto THEN D 0 THEN Auto) }

1
.....subterm..... T:t
1:n
1. T : Type
2. x : bag(T)
⊢ x ∈ Top List

---

Latex:

---

Latex:
\mforall{}T:Type.  (bag(T)  \msubseteq{}r  (Top  List))


By

---

Latex:
(Auto  THEN  D  0  THEN  Auto)

---

Home Index