---

Step * 1 of Lemma eclass-val_wf


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(e) ∈ A[eo;e]
BY
{ (MoveToConcl (-1) THEN RepUR ``in-eclass eclass-val`` 0 THEN Unfold `eclass` 3 THEN RW assert_pushdownC 0 THEN Auto) }

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. #(X eo e) = 1 ∈ ℤ@i
⊢ single-valued-bag(X eo e;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(e)  \mmember{}  A[eo;e]


By

(MoveToConcl  (-1)
  THEN  RepUR  ``in-eclass  eclass-val``  0
  THEN  Unfold  `eclass`  3
  THEN  RW  assert\_pushdownC  0
  THEN  Auto)

---

Home Index