---

Step * 1 1 1 1 2 2 of Lemma sv-classrel


1. A : Type
2. v : A@i
3. b : bag(A)@i
4. #(b) ≠ 1
5. #(b) ≤ 1@i
6. v ↓∈ b@i
⊢ v = only(b) ∈ A
BY
{ (FLemma `bag-member-size` [-1] THEN Auto') }

---

Latex:



1.  A  :  Type
2.  v  :  A@i
3.  b  :  bag(A)@i
4.  \#(b)  \mneq{}  1
5.  \#(b)  \mleq{}  1@i
6.  v  \mdownarrow{}\mmember{}  b@i
\mvdash{}  v  =  only(b)


By

(FLemma  `bag-member-size`  [-1]  THEN  Auto')

---

Home Index