---

Step * 1 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 ~ {only(b)}
6. x : A@i
7. #({x}) ≤ 1@i
8. True
9. single-valued-bag({x};A)
⊢ 0 < #({x})
BY
{ (RW (SubC (TagC (mk_tag_term 30))) 0 THEN Auto) }

---

Latex:

---

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.  True
9.  single-valued-bag(\{x\};A)
\mvdash{}  0  <  \#(\{x\})


By

---

Latex:
(RW  (SubC  (TagC  (mk\_tag\_term  30)))  0  THEN  Auto)

---

Home Index