---

Step * of Lemma sv-bag-only_wf

∀[T:Type]. ∀[b:bag(T)].  (sv-bag-only(b) ∈ T) supposing (0 < #(b) and single-valued-bag(b;T))
BY
{ ((UnivCD THENA Auto) THEN Unfold `sv-bag-only` 0 THEN BLemma `single-valued-bag-hd` THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[b:bag(T)].    (sv-bag-only(b)  \mmember{}  T)  supposing  (0  <  \#(b)  and  single-valued-bag(b;T))


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  Unfold  `sv-bag-only`  0  THEN  BLemma  `single-valued-bag-hd`  THEN  Auto)

---

Home Index