---

Step * 1 1 of Lemma sv-class-iff


1. Info : Type
2. A : es:EO+(Info) ─→ E ─→ Type
3. X : EClass(A[es;e])
4. Singlevalued(X)@i'
5. es : EO+(Info)@i'
6. e : E@i
7. (#(X es e) + 1) ≤ 1
⊢ (X es e) = {} ∈ bag(A[es;e])
BY
{ (RWO "bag-size-zero" 0 THEN Auto) }

---

Latex:



1.  Info  :  Type
2.  A  :  es:EO+(Info)  {}\mrightarrow{}  E  {}\mrightarrow{}  Type
3.  X  :  EClass(A[es;e])
4.  Singlevalued(X)@i'
5.  es  :  EO+(Info)@i'
6.  e  :  E@i
7.  (\#(X  es  e)  +  1)  \mleq{}  1
\mvdash{}  (X  es  e)  =  \{\}


By

(RWO  "bag-size-zero"  0  THEN  Auto)

---

Home Index