---

Step * of Lemma smallbag-subtype-list

∀T:Type. ({b:bag(T)| #(b) < 2}  ⊆r {b:T List| ||b|| < 2} )
BY
{ (Auto THEN D 0 THEN Auto THEN D -1 THEN Unfold `bag-size` -1 THEN MemTypeCD THEN Auto) }

1
1. T : Type
2. x : bag(T)
3. ||x|| < 2
⊢ x ∈ T List

---

Latex:

---

Latex:
\mforall{}T:Type.  (\{b:bag(T)|  \#(b)  <  2\}    \msubseteq{}r  \{b:T  List|  ||b||  <  2\}  )


By

---

Latex:
(Auto  THEN  D  0  THEN  Auto  THEN  D  -1  THEN  Unfold  `bag-size`  -1  THEN  MemTypeCD  THEN  Auto)

---

Home Index