---

Step * of Lemma primed-class-prior-val

∀[Info,T:Type]. ∀[X:EClass(T)].  Prior(X) = (X)' ∈ EClass(T) supposing Singlevalued(X)
BY
{ (Auto
   THEN Unfold `eclass` 0
   THEN RepeatFor 2 ((Ext THEN Auto THEN Try ((Fold `eclass` 0 THEN Auto))))
   THEN RenameVar `es' (-2)
   THEN RenameVar `e' (-1)) }

1
1. Info : Type
2. T : Type
3. X : EClass(T)
4. Singlevalued(X)
5. es : EO+(Info)
6. e : E
⊢ (Prior(X) es e) = ((X)' es e) ∈ bag(T)

---

Latex:

---

Latex:
\mforall{}[Info,T:Type].  \mforall{}[X:EClass(T)].    Prior(X)  =  (X)'  supposing  Singlevalued(X)


By

---

Latex:
(Auto
  THEN  Unfold  `eclass`  0
  THEN  RepeatFor  2  ((Ext  THEN  Auto  THEN  Try  ((Fold  `eclass`  0  THEN  Auto))))
  THEN  RenameVar  `es'  (-2)
  THEN  RenameVar  `e'  (-1))

---

Home Index