---

Step * of Lemma single-valued-bag-hd

∀[T:Type]. ∀[b:bag(T)].  (hd(b) ∈ T) supposing (0 < #(b) and single-valued-bag(b;T))
BY
{ ((UnivCD THENA Auto) THEN newQuotD 2 THEN RepUR ``bag-size`` (-1)) }

1
1. T : Type
2. T List ∈ Type
3. ∀as,bs:T List.  (permutation(T;as;bs) ∈ Type)
4. ∀as:T List. permutation(T;as;as)
5. a : Base
6. b1 : Base
7. c : a = b1 ∈ pertype(λas,bs. ((as ∈ T List) ∧ (bs ∈ T List) ∧ permutation(T;as;bs)))
8. a ∈ T List
9. b1 ∈ T List
10. permutation(T;a;b1)
11. single-valued-bag(a;T)
12. 0 < ||a||
⊢ hd(a) = hd(b1) ∈ T

---

Latex:

---

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


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  newQuotD  2  THEN  RepUR  ``bag-size``  (-1))

---

Home Index