---

Step * of Lemma Q-R-glues-conditional2

∀[Info:Type]
  ∀es:EO+(Info)
    ∀[Q1,Q2,R:E ─→ E ─→ ℙ]. ∀[A,B:Type].
      ∀Ia1,Ia2:EClass(A). ∀Ib1,Ib2:EClass(B). ∀f:E([Ia1?Ia2]) ─→ B. ∀g1:E(Ib1) ─→ E. ∀g2:E(Ib2) ─→ E.
        (g1 glues Ia1:Q1 ──f─→ Ib1:R
           ⇒ g2 glues Ia2:Q2 ──f─→ Ib2:R
           ⇒ [{Ib1}? g1 : g2] glues [Ia1?Ia2]:Q1|{Ia1} ∨ Q2|{Ia2} ──f─→ [Ib1?Ib2]:R) supposing 
           (Ib1 ∩ Ib2 = 0 and 
           Ia1 ∩ Ia2 = 0)
BY
{ ((UnivCD THENA Auto)
   THEN (BLemma `Q-R-glues-conditional`
         THEN Try (CompleteAuto)
         THEN OnMaybeHyp 17 (\h. ((FLemma `Q-R-glues-property` [h]) THEN CompleteAuto)))⋅
   ) }

---

Latex:

---

Latex:
\mforall{}[Info:Type]
    \mforall{}es:EO+(Info)
        \mforall{}[Q1,Q2,R:E  {}\mrightarrow{}  E  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[A,B:Type].
            \mforall{}Ia1,Ia2:EClass(A).  \mforall{}Ib1,Ib2:EClass(B).  \mforall{}f:E([Ia1?Ia2])  {}\mrightarrow{}  B.  \mforall{}g1:E(Ib1)  {}\mrightarrow{}  E.
            \mforall{}g2:E(Ib2)  {}\mrightarrow{}  E.
                (g1  glues  Ia1:Q1  {}{}f{}\mrightarrow{}  Ib1:R
                      {}\mRightarrow{}  g2  glues  Ia2:Q2  {}{}f{}\mrightarrow{}  Ib2:R
                      {}\mRightarrow{}  [\{Ib1\}?  g1  :  g2]  glues  [Ia1?Ia2]:Q1|\{Ia1\}  \mvee{}  Q2|\{Ia2\}  {}{}f{}\mrightarrow{}  [Ib1?Ib2]:R)  supposing 
                      (Ib1  \mcap{}  Ib2  =  0  and 
                      Ia1  \mcap{}  Ia2  =  0)


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (BLemma  `Q-R-glues-conditional`
              THEN  Try  (CompleteAuto)
              THEN  OnMaybeHyp  17  (\mbackslash{}h.  ((FLemma  `Q-R-glues-property`  [h])  THEN  CompleteAuto)))\mcdot{}
  )

---

Home Index