---

Step * of Lemma Q-R-glues-trivial-restrict

∀[Info:Type]. ∀[P:es:EO+(Info) ─→ E ─→ ℙ].
  ∀p:∀es:EO+(Info). ∀e:E.  Dec(P[es;e])
    ∀[A,B:Type].
      ∀Ia:EClass(A). ∀Ib:EClass(B).
        ((∀es:EO+(Info). ∀e:E.  (Ib es e) = {} ∈ bag(B) supposing ¬P[es;e])
        ⇒ (∀es:EO+(Info)
              ∀[Q,R:E ─→ E ─→ ℙ].
                ∀f:E(Ia) ─→ B. ∀g:E(Ib) ─→ E.  (g glues Ia:Q ──f─→ (Ib|p):R ⇒ g glues Ia:Q ──f─→ Ib:R)))
BY
{ ((Auto THEN Try ((BLemma `es-E-interface-restrict` THEN Auto)))
   THEN (Assert (Ib|p) = Ib ∈ EClass(B) BY
               (BLemma `es-interface-restrict-trivial` THEN Auto))
   ) }

---

Latex:

---

Latex:
\mforall{}[Info:Type].  \mforall{}[P:es:EO+(Info)  {}\mrightarrow{}  E  {}\mrightarrow{}  \mBbbP{}].
    \mforall{}p:\mforall{}es:EO+(Info).  \mforall{}e:E.    Dec(P[es;e])
        \mforall{}[A,B:Type].
            \mforall{}Ia:EClass(A).  \mforall{}Ib:EClass(B).
                ((\mforall{}es:EO+(Info).  \mforall{}e:E.    (Ib  es  e)  =  \{\}  supposing  \mneg{}P[es;e])
                {}\mRightarrow{}  (\mforall{}es:EO+(Info)
                            \mforall{}[Q,R:E  {}\mrightarrow{}  E  {}\mrightarrow{}  \mBbbP{}].
                                \mforall{}f:E(Ia)  {}\mrightarrow{}  B.  \mforall{}g:E(Ib)  {}\mrightarrow{}  E.
                                    (g  glues  Ia:Q  {}{}f{}\mrightarrow{}  (Ib|p):R  {}\mRightarrow{}  g  glues  Ia:Q  {}{}f{}\mrightarrow{}  Ib:R)))


By

---

Latex:
((Auto  THEN  Try  ((BLemma  `es-E-interface-restrict`  THEN  Auto)))
  THEN  (Assert  (Ib|p)  =  Ib  BY
                          (BLemma  `es-interface-restrict-trivial`  THEN  Auto))
  )

---

Home Index