---

Step * of Lemma sv-bag-is-bag-rep-lousy-proof

∀[A:Type]. ∀[as:bag(A)].  ∀a:A. (a ↓∈ as ⇒ (as = bag-rep(#(as);a) ∈ bag(A))) supposing single-valued-bag(as;A)
BY
{ Auto }

1
1. A : Type
2. as : bag(A)
3. single-valued-bag(as;A)
4. a : A@i
5. a ↓∈ as@i
⊢ as = bag-rep(#(as);a) ∈ bag(A)

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[as:bag(A)].
    \mforall{}a:A.  (a  \mdownarrow{}\mmember{}  as  {}\mRightarrow{}  (as  =  bag-rep(\#(as);a)))  supposing  single-valued-bag(as;A)


By

---

Latex:
Auto

---

Home Index