---

Step * of Lemma glued-composes-simple

∀[Info:Type]
  ∀es:EO+(Info)
    ∀[A,B:Type].
      ∀Ia:EClass(A). ∀Ib,Ic:EClass(B). ∀f1:E(Ia) ⟶ B.
        ((glued(es;B;f1;Ia;Ib) ∧ glued(es;B;λe.Ib(e);Ib;Ic)) ⇒ glued(es;B;f1;Ia;Ic))
BY
{ (InstLemma `glued-composes` []⋅
   THEN RepeatFor 4 ((ParallelLast THEN Thin (-3)))
   THEN (InstHyp [⌜B⌝] (-1)⋅ THENA Auto)
   THEN Thin (-2)
   THEN RepeatFor 3 ((ParallelLast THEN Thin (-3)))) }

1
1. [Info] : Type
2. es : EO+(Info)@i'
3. [A] : Type
4. [B] : Type
5. Ia : EClass(A)@i'
6. Ib : EClass(B)@i'
7. Ic : EClass(B)@i'
8. ∀f1:E(Ia) ⟶ B. ∀f2:B ⟶ B.  ((glued(es;B;f1;Ia;Ib) ∧ glued(es;B;λe.(f2 Ib(e));Ib;Ic)) ⇒ glued(es;B;f2 o f1;Ia;Ic))
⊢ ∀f1:E(Ia) ⟶ B. ((glued(es;B;f1;Ia;Ib) ∧ glued(es;B;λe.Ib(e);Ib;Ic)) ⇒ glued(es;B;f1;Ia;Ic))

---

Latex:

---

Latex:
\mforall{}[Info:Type]
    \mforall{}es:EO+(Info)
        \mforall{}[A,B:Type].
            \mforall{}Ia:EClass(A).  \mforall{}Ib,Ic:EClass(B).  \mforall{}f1:E(Ia)  {}\mrightarrow{}  B.
                ((glued(es;B;f1;Ia;Ib)  \mwedge{}  glued(es;B;\mlambda{}e.Ib(e);Ib;Ic))  {}\mRightarrow{}  glued(es;B;f1;Ia;Ic))


By

---

Latex:
(InstLemma  `glued-composes`  []\mcdot{}
  THEN  RepeatFor  4  ((ParallelLast  THEN  Thin  (-3)))
  THEN  (InstHyp  [\mkleeneopen{}B\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)
  THEN  Thin  (-2)
  THEN  RepeatFor  3  ((ParallelLast  THEN  Thin  (-3))))

---

Home Index