---

Step * of Lemma interface-at-val

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[T:Type]. ∀[X:EClass(T)]. ∀[i:Id]. ∀[e:E].  X@i(e) ~ X(e) supposing ↑e ∈b X@i
BY
{ ((UnivCD THENA Auto)
   THEN (RWO "is-interface-at" (-1) THENA Auto)
   THEN RepUR ``es-interface-at eclass-val do-apply`` 0
   THEN AutoSplit) }

---

Latex:

---

Latex:
\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[T:Type].  \mforall{}[X:EClass(T)].  \mforall{}[i:Id].  \mforall{}[e:E].
    X@i(e)  \msim{}  X(e)  supposing  \muparrow{}e  \mmember{}\msubb{}  X@i


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (RWO  "is-interface-at"  (-1)  THENA  Auto)
  THEN  RepUR  ``es-interface-at  eclass-val  do-apply``  0
  THEN  AutoSplit)

---

Home Index