---

Step * 1 1 of Lemma bag-size-bag-member


1. T : Type
2. bs : T List
3. b : T
4. L : T List
5. L = bs ∈ bag(T)
6. (b ∈ L)
⊢ 0 < #(bs)
BY
{ ((EqTypeD (-2) THEN Auto)
   THEN (FLemma `member-permutation` [-2] THEN Auto)
   THEN (Assert (b ∈ bs) BY
               Auto)
   THEN Unfold `bag-size` 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  bs  :  T  List
3.  b  :  T
4.  L  :  T  List
5.  L  =  bs
6.  (b  \mmember{}  L)
\mvdash{}  0  <  \#(bs)


By

---

Latex:
((EqTypeD  (-2)  THEN  Auto)
  THEN  (FLemma  `member-permutation`  [-2]  THEN  Auto)
  THEN  (Assert  (b  \mmember{}  bs)  BY
                          Auto)
  THEN  Unfold  `bag-size`  0
  THEN  Auto)

---

Home Index