---

Step * 1 of Lemma single-eclass-val


1. T : Type
2. A : es:EO+(T) ─→ E ─→ Type
3. X : EClass(A[es;e])
4. eo : EO+(T)
5. e : E
6. ↑e ∈b X
⊢ (X eo e) = {X(e)} ∈ bag(A[eo;e])
BY
{ (MoveToConcl (-1) THEN RepUR ``in-eclass eclass-val`` 0 THEN Unfold `eclass` 3 THEN GenConclAtAddr [1;1;1;1]) }

1
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]))

---

Latex:



1.  T  :  Type
2.  A  :  es:EO+(T)  {}\mrightarrow{}  E  {}\mrightarrow{}  Type
3.  X  :  EClass(A[es;e])
4.  eo  :  EO+(T)
5.  e  :  E
6.  \muparrow{}e  \mmember{}\msubb{}  X
\mvdash{}  (X  eo  e)  =  \{X(e)\}


By

(MoveToConcl  (-1)
  THEN  RepUR  ``in-eclass  eclass-val``  0
  THEN  Unfold  `eclass`  3
  THEN  GenConclAtAddr  [1;1;1;1])

---

Home Index