---

Step * of Lemma single-eclass-val

∀[T:Type]. ∀[A:es:EO+(T) ─→ E ─→ Type]. ∀[X:EClass(A[es;e])]. ∀[eo:EO+(T)]. ∀[e:E].
  (X eo e) = {X(e)} ∈ bag(A[eo;e]) supposing ↑e ∈b X
BY
{ Auto }

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

---

Latex:


\mforall{}[T:Type].  \mforall{}[A:es:EO+(T)  {}\mrightarrow{}  E  {}\mrightarrow{}  Type].  \mforall{}[X:EClass(A[es;e])].  \mforall{}[eo:EO+(T)].  \mforall{}[e:E].
    (X  eo  e)  =  \{X(e)\}  supposing  \muparrow{}e  \mmember{}\msubb{}  X


By

Auto

---

Home Index