---

Step * 1 of Lemma class-pred-cases

.....assertion..... 
∀[T:Type]. ∀[b:bag(T)].  (↓∃x:T. x ↓∈ b ⇐⇒ 0 < #(b))
BY
{ (InstLemma `bag-member-iff-size` [] THEN RepeatFor 2 (ParallelLast) THEN Auto) }

---

Latex:

---

Latex:
.....assertion..... 
\mforall{}[T:Type].  \mforall{}[b:bag(T)].    (\mdownarrow{}\mexists{}x:T.  x  \mdownarrow{}\mmember{}  b  \mLeftarrow{}{}\mRightarrow{}  0  <  \#(b))


By

---

Latex:
(InstLemma  `bag-member-iff-size`  []  THEN  RepeatFor  2  (ParallelLast)  THEN  Auto)

---

Home Index