---

Step * 1 of Lemma subtype-bag-only


1. T : Type
2. v : T
⊢ {v} ∈ bag({x:T| x = v ∈ T} )
BY
{ (Unfold `single-bag` 0 THEN SubsumeC ⌜{x:T| x = v ∈ T}  List⌝⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  v  :  T
\mvdash{}  \{v\}  \mmember{}  bag(\{x:T|  x  =  v\}  )


By

---

Latex:
(Unfold  `single-bag`  0  THEN  SubsumeC  \mkleeneopen{}\{x:T|  x  =  v\}    List\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index