---

Step * 1 1 of Lemma single-eclass-val


1. T : Type
2. A : es:EO+(T) ─→ E ─→ Type
3. X : es:EO+(T) ─→ e:E ─→ bag(A[es;e])
4. eo : EO+(T)
5. e : E
6. v : bag(A[eo;e])@i
7. (X eo e) = v ∈ bag(A[eo;e])@i
⊢ (↑(#(v) =z 1)) ⇒ (v = {only(v)} ∈ bag(A[eo;e]))
BY
{ ((Auto THEN RWO "bag-size-one<" 0⋅) THEN Auto) }

---

Latex:



1.  T  :  Type
2.  A  :  es:EO+(T)  {}\mrightarrow{}  E  {}\mrightarrow{}  Type
3.  X  :  es:EO+(T)  {}\mrightarrow{}  e:E  {}\mrightarrow{}  bag(A[es;e])
4.  eo  :  EO+(T)
5.  e  :  E
6.  v  :  bag(A[eo;e])@i
7.  (X  eo  e)  =  v@i
\mvdash{}  (\muparrow{}(\#(v)  =\msubz{}  1))  {}\mRightarrow{}  (v  =  \{only(v)\})


By

((Auto  THEN  RWO  "bag-size-one<"  0\mcdot{})  THEN  Auto)

---

Home Index