---

Step * of Lemma bind-return-right

∀[Info,T:Type]. ∀[X:EClass(T)].  (X >x> return-class(x) = X ∈ EClass(T))
BY
{ (Auto
   THEN RepUR ``eclass`` 0⋅
   THEN Symmetry
   THEN Ext
   THEN Auto
   THEN Try ((Fold `eclass` 0 THEN Auto)⋅)
   THEN RenameVar `es' (-1)⋅
   THEN Ext
   THEN Auto) }

1
1. Info : Type
2. T : Type
3. X : EClass(T)
4. es : EO+(Info)
5. x : E
⊢ (X es x) = (X >x> return-class(x) es x) ∈ bag(T)

---

Latex:


\mforall{}[Info,T:Type].  \mforall{}[X:EClass(T)].    (X  >x>  return-class(x)  =  X)


By

(Auto
  THEN  RepUR  ``eclass``  0\mcdot{}
  THEN  Symmetry
  THEN  Ext
  THEN  Auto
  THEN  Try  ((Fold  `eclass`  0  THEN  Auto)\mcdot{})
  THEN  RenameVar  `es'  (-1)\mcdot{}
  THEN  Ext
  THEN  Auto)

---

Home Index