---

Step * 1 of Lemma es-sv-class-implies-single-valued-classrel


1. Info : Type
2. T : Type
3. es : EO+(Info)
4. X : EClass(T)
5. ∀e:E. (#(X es e) ≤ 1)
6. e : E@i
7. v1 : T@i
8. v2 : T@i
9. v1 ∈ X(e)@i
10. v2 ∈ X(e)@i
11. #(X es e) ≤ 1
12. #(X es e) = 0 ∈ ℤ
⊢ v1 = v2 ∈ T
BY
{ ((InstLemma `bag-size-zero` [⌈T⌉;⌈X es e⌉]⋅ THENA Auto)
   THEN Unfold `classrel` (-4)
   THEN HypSubst' (-1) (-4)
   THEN BagMemberD (-4)) }

---

Latex:



1.  Info  :  Type
2.  T  :  Type
3.  es  :  EO+(Info)
4.  X  :  EClass(T)
5.  \mforall{}e:E.  (\#(X  es  e)  \mleq{}  1)
6.  e  :  E@i
7.  v1  :  T@i
8.  v2  :  T@i
9.  v1  \mmember{}  X(e)@i
10.  v2  \mmember{}  X(e)@i
11.  \#(X  es  e)  \mleq{}  1
12.  \#(X  es  e)  =  0
\mvdash{}  v1  =  v2


By

((InstLemma  `bag-size-zero`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}X  es  e\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  Unfold  `classrel`  (-4)
  THEN  HypSubst'  (-1)  (-4)
  THEN  BagMemberD  (-4))

---

Home Index