---

Step * of Lemma glued-Q-R-glued

∀[Info:Type]
  ∀es:EO+(Info)
    ∀[A,B:Type].
      ∀Ia:EClass(A). ∀Ib:EClass(B). ∀f:E(Ia) ─→ B.  (glued(es;B;f;Ia;Ib) ⇐⇒ Ia:λe,e'. e ≤loc e'  →─f─→  Ib:λe,e'. e ≤lo\000Cc e' )
BY
{ (Auto THEN (All (Unfolds ``glued Q-R-glued``) THEN ParallelLast THEN All (Unfold `glues`) THEN Trivial)⋅) }

---

Latex:

---

Latex:
\mforall{}[Info:Type]
    \mforall{}es:EO+(Info)
        \mforall{}[A,B:Type].
            \mforall{}Ia:EClass(A).  \mforall{}Ib:EClass(B).  \mforall{}f:E(Ia)  {}\mrightarrow{}  B.
                (glued(es;B;f;Ia;Ib)  \mLeftarrow{}{}\mRightarrow{}  Ia:\mlambda{}e,e'.  e  \mleq{}loc  e'    \mrightarrow{}{}f{}\mrightarrow{}    Ib:\mlambda{}e,e'.  e  \mleq{}loc  e'  )


By

---

Latex:
(Auto
  THEN  (All  (Unfolds  ``glued  Q-R-glued``)  THEN  ParallelLast  THEN  All  (Unfold  `glues`)  THEN  Trivial)\mcdot{}
  )

---

Home Index