---

Step * of Lemma Q-R-glues-empty

∀[Info:Type]
  ∀es:EO+(Info)
    ∀[Qa,Rb:E ⟶ E ⟶ ℙ]. ∀[A,B:Type].
      ∀Ia:EClass(A). ∀Ib:EClass(B). ∀f,g:Top.
        (g glues Ia:Qa ──f⟶ Ib:Rb) supposing (es-interface-empty(es;Ib) and es-interface-empty(es;Ia))
BY
{ (RepUR
   ``Q-R-glues weak-antecedent-surjection weak-antecedent-function es-interface-predicate`` 0⋅
   THEN RepUR ``es-interface-empty Q-R-pre-preserving inject es-E-interface`` 0
   THEN Repeat ((D 0 THENA Complete (Auto)))
   THEN Try ((Assert ⌜False⌝⋅
              THEN Auto
              THEN DVar `e'
              THEN (OnSomeHyp (\h. ((InstHyp [⌜e⌝] h)⋅ THEN Complete (Auto))))⋅))
   THEN Try ((Assert ⌜False⌝⋅
              THEN Auto
              THEN DVar `a1'
              THEN (OnSomeHyp (\h. ((InstHyp [⌜a1⌝] h)⋅ THEN Complete (Auto))))⋅))) }

---

Latex:

---

Latex:
\mforall{}[Info:Type]
    \mforall{}es:EO+(Info)
        \mforall{}[Qa,Rb:E  {}\mrightarrow{}  E  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[A,B:Type].
            \mforall{}Ia:EClass(A).  \mforall{}Ib:EClass(B).  \mforall{}f,g:Top.
                (g  glues  Ia:Qa  {}{}f{}\mrightarrow{}  Ib:Rb)  supposing 
                      (es-interface-empty(es;Ib)  and 
                      es-interface-empty(es;Ia))


By

---

Latex:
(RepUR
  ``Q-R-glues  weak-antecedent-surjection  weak-antecedent-function  es-interface-predicate``  0\mcdot{}
  THEN  RepUR  ``es-interface-empty  Q-R-pre-preserving  inject  es-E-interface``  0
  THEN  Repeat  ((D  0  THENA  Complete  (Auto)))
  THEN  Try  ((Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}
                        THEN  Auto
                        THEN  DVar  `e'
                        THEN  (OnSomeHyp  (\mbackslash{}h.  ((InstHyp  [\mkleeneopen{}e\mkleeneclose{}]  h)\mcdot{}  THEN  Complete  (Auto))))\mcdot{}))
  THEN  Try  ((Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}
                        THEN  Auto
                        THEN  DVar  `a1'
                        THEN  (OnSomeHyp  (\mbackslash{}h.  ((InstHyp  [\mkleeneopen{}a1\mkleeneclose{}]  h)\mcdot{}  THEN  Complete  (Auto))))\mcdot{})))

---

Home Index