---

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


1. A : Type
2. v : A@i
3. b : bag(A)@i
4. #(b) = 1 ∈ ℤ
5. b ~ {only(b)}
6. x : A@i
7. #({x}) ≤ 1@i
8. v ↓∈ {x}@i
⊢ v = only({x}) ∈ A
BY
{ (BagMemberD (-1) THEN Reduce 0 THEN Auto) }

---

Latex:



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


By

(BagMemberD  (-1)  THEN  Reduce  0  THEN  Auto)

---

Home Index