---

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


1. T : Type
2. bs : bag(T)
3. ∃x:T. x ↓∈ bs
⊢ 0 < #(bs)
BY
{ ((RepeatFor 4 (D -1) THEN RevHypSubst (-2) 0 THEN Auto) THEN ThinVar `bs' THEN Unfold `bag-size` 0 THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  bs  :  bag(T)
3.  \mexists{}x:T.  x  \mdownarrow{}\mmember{}  bs
\mvdash{}  0  <  \#(bs)


By

---

Latex:
((RepeatFor  4  (D  -1)  THEN  RevHypSubst  (-2)  0  THEN  Auto)
  THEN  ThinVar  `bs'
  THEN  Unfold  `bag-size`  0
  THEN  Auto)

---

Home Index