---

Step * 2 of Lemma decidable__exists-single-valued-classrel


1. Info : Type
2. T : Type
3. X : EClass(T)@i'
4. es : EO+(Info)@i'
5. ∀e:E. ∀v1,v2:T.  (v1 ∈ X(e) ⇒ v2 ∈ X(e) ⇒ (v1 = v2 ∈ T))@i
6. e : E@i
7. ∃v:T. v ↓∈ X es e@i
⊢ 0 < #(X es e)
BY
{ ((BLemma `bag-size-bag-member` THENA Auto) THEN D 0 THEN Trivial) }

---

Latex:



1.  Info  :  Type
2.  T  :  Type
3.  X  :  EClass(T)@i'
4.  es  :  EO+(Info)@i'
5.  \mforall{}e:E.  \mforall{}v1,v2:T.    (v1  \mmember{}  X(e)  {}\mRightarrow{}  v2  \mmember{}  X(e)  {}\mRightarrow{}  (v1  =  v2))@i
6.  e  :  E@i
7.  \mexists{}v:T.  v  \mdownarrow{}\mmember{}  X  es  e@i
\mvdash{}  0  <  \#(X  es  e)


By

((BLemma  `bag-size-bag-member`  THENA  Auto)  THEN  D  0  THEN  Trivial)

---

Home Index