---

Step * of Lemma return-class-val

∀[Info:Type]. ∀[x:Top]. ∀[es:EO+(Info)]. ∀[e:E].  return-class(x)(e) ~ x supposing ↑e ∈b return-class(x)
BY
{ (Auto THEN RepUR ``return-class eclass-val`` 0 THEN OldAutoSplit) }

1
1. Info : Type
2. x : Top
3. es : EO+(Info)
4. e : E
5. ↑e ∈b return-class(x)
6. ¬↑first(e)
⊢ only({}) ~ x

---

Latex:


\mforall{}[Info:Type].  \mforall{}[x:Top].  \mforall{}[es:EO+(Info)].  \mforall{}[e:E].
    return-class(x)(e)  \msim{}  x  supposing  \muparrow{}e  \mmember{}\msubb{}  return-class(x)


By

(Auto  THEN  RepUR  ``return-class  eclass-val``  0  THEN  OldAutoSplit)

---

Home Index