---

Step * of Lemma Q-R-glued-empty

∀[Info:Type]. ∀es:EO+(Info). ∀[Q,R:E ⟶ E ⟶ ℙ]. ∀[B:Type].  ∀f:Top. Empty:Q →─f⟶  Empty:R
BY
{ (Auto
   THEN RepUR ``Q-R-glued Q-R-glues Q-R-pre-preserving
                es-interface-predicate in-eclass
                weak-antecedent-surjection weak-antecedent-function
                  inject es-E-interface`` 0⋅
   THEN (InstConcl [⌜λe.⋅⌝])⋅
   THEN Auto
   THEN ∀h:hyp. (DSetType Auto h THEN Complete (Auto)) ) }

---

Latex:

---

Latex:
\mforall{}[Info:Type].  \mforall{}es:EO+(Info).  \mforall{}[Q,R:E  {}\mrightarrow{}  E  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[B:Type].    \mforall{}f:Top.  Empty:Q  \mrightarrow{}{}f{}\mrightarrow{}    Empty:R


By

---

Latex:
(Auto
  THEN  RepUR  ``Q-R-glued  Q-R-glues  Q-R-pre-preserving
                            es-interface-predicate  in-eclass
                            weak-antecedent-surjection  weak-antecedent-function
                                inject  es-E-interface``  0\mcdot{}
  THEN  (InstConcl  [\mkleeneopen{}\mlambda{}e.\mcdot{}\mkleeneclose{}])\mcdot{}
  THEN  Auto
  THEN  \mforall{}h:hyp.  (DSetType  Auto  h  THEN  Complete  (Auto))  )

---

Home Index