---

Step * of Lemma bag-only_wf2

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

1
1. T : Type
2. b : bag(T)
3. single-valued-bag(b;T) ∧ 0 < #(b)
⊢ hd(b) ∈ T

---

Latex:

---

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


By

---

Latex:
(Unfold  `bag-only`  0  THEN  (UnivCD  THENA  Auto))

---

Home Index