---

Step * of Lemma eclass-ext

∀[T:Type]. ∀[A:es:EO+(T) ─→ E ─→ Type]. ∀[X,Y:EClass(A[es;e])].
  X = Y ∈ EClass(A[es;e]) supposing ∀es:EO+(T). ∀e:E.  ((X es e) = (Y es e) ∈ bag(A[es;e]))
BY
{ (Unfold `eclass` 0 THEN Auto) }

---

Latex:


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


By

(Unfold  `eclass`  0  THEN  Auto)

---

Home Index