---

Step * of Lemma es-interface-or-right-property

∀[Info,A:Type]. ∀[X:EClass(Top)]. ∀[Y:EClass(A)].
  es-interface-or-right((X | Y)) = Y ∈ EClass(A) supposing Singlevalued(Y)
BY
{ (Auto
   THEN Unfold `eclass` 0
   THEN Ext
   THEN Auto
   THEN RenameVar `es' (-1)
   THEN (Try ((Fold `eclass` 0 THEN Auto))
         THEN Ext
         THEN Auto
         THEN RenameVar `e' (-1)
         THEN (Try ((Fold `eclass` 0 THEN Auto))
               THEN (RepUR ``es-interface-or-right es-interface-or eclass-compose2 `` 0
                     THEN RepUR ``oob-apply es-filter-image eclass-compose1`` 0
                     THEN RepeatFor 2 (AutoSplit)
                     THEN (ElimBagSizeOne'
                           THEN RepUR ``oob-getright? oob-hasright oob-getright`` 0
                           THEN Auto
                           THEN RWO "bag-size-zero" 0
                           THEN Auto
                           THEN Try ((Fold `empty-bag` 0⋅ THEN Auto))
                           THEN ((With ⌜es⌝ (D 5)⋅ THENA Auto) THEN InstHyp [⌜e⌝] (-1)⋅ THEN Auto')⋅)⋅)⋅
               )⋅)⋅) }

---

Latex:

---

Latex:
\mforall{}[Info,A:Type].  \mforall{}[X:EClass(Top)].  \mforall{}[Y:EClass(A)].
    es-interface-or-right((X  |  Y))  =  Y  supposing  Singlevalued(Y)


By

---

Latex:
(Auto
  THEN  Unfold  `eclass`  0
  THEN  Ext
  THEN  Auto
  THEN  RenameVar  `es'  (-1)
  THEN  (Try  ((Fold  `eclass`  0  THEN  Auto))
              THEN  Ext
              THEN  Auto
              THEN  RenameVar  `e'  (-1)
              THEN  (Try  ((Fold  `eclass`  0  THEN  Auto))
                          THEN  (RepUR  ``es-interface-or-right  es-interface-or  eclass-compose2  ``  0
                                      THEN  RepUR  ``oob-apply  es-filter-image  eclass-compose1``  0
                                      THEN  RepeatFor  2  (AutoSplit)
                                      THEN  (ElimBagSizeOne'
                                                  THEN  RepUR  ``oob-getright?  oob-hasright  oob-getright``  0
                                                  THEN  Auto
                                                  THEN  RWO  "bag-size-zero"  0
                                                  THEN  Auto
                                                  THEN  Try  ((Fold  `empty-bag`  0\mcdot{}  THEN  Auto))
                                                  THEN  ((With  \mkleeneopen{}es\mkleeneclose{}  (D  5)\mcdot{}  THENA  Auto)  THEN  InstHyp  [\mkleeneopen{}e\mkleeneclose{}]  (-1)\mcdot{}  THEN  Auto')\mcdot{})
                                      \mcdot{})\mcdot{}
                          )\mcdot{})\mcdot{})

---

Home Index