---

Step * 1 of Lemma bag-only_wf2


1. T : Type
2. b : bag(T)
3. single-valued-bag(b;T) ∧ 0 < #(b)
⊢ hd(b) ∈ T
BY
{ (BLemma `single-valued-bag-hd` THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  b  :  bag(T)
3.  single-valued-bag(b;T)  \mwedge{}  0  <  \#(b)
\mvdash{}  hd(b)  \mmember{}  T


By

---

Latex:
(BLemma  `single-valued-bag-hd`  THEN  Auto)

---

Home Index