---

Step * of Lemma interface-part-val

∀[Info,T:Type]. ∀[X:EClass(T)]. ∀[g:∩es:EO+(Info). (E(X) ─→ Id)]. ∀[i:Id]. ∀[es:EO+(Info)]. ∀[e:E].
  (X|g=i)(e) ~ X(e) supposing ↑e ∈b (X|g=i)
BY
{ (Repeat ((D 0 THENA Complete (Auto)))
   THEN (RWO "is-interface-part" (-1) THENA (Auto THEN With ⌈es⌉ (DVar `g')⋅ THEN Auto))
   THEN D -1
   THEN RepUR ``eclass-val es-interface-part let`` 0
   THEN Fold `in-eclass` 0
   THEN RepeatFor 2 (AutoSplit)) }

---

Latex:

---

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


By

---

Latex:
(Repeat  ((D  0  THENA  Complete  (Auto)))
  THEN  (RWO  "is-interface-part"  (-1)  THENA  (Auto  THEN  With  \mkleeneopen{}es\mkleeneclose{}  (DVar  `g')\mcdot{}  THEN  Auto))
  THEN  D  -1
  THEN  RepUR  ``eclass-val  es-interface-part  let``  0
  THEN  Fold  `in-eclass`  0
  THEN  RepeatFor  2  (AutoSplit))

---

Home Index