---

Step * of Lemma glue-comp-agrees2

No Annotations
∀[G:j⊢]. ∀[A:{G ⊢ _}]. ∀[cA:G +⊢ Compositon(A)]. ∀[psi:{G ⊢ _:𝔽}]. ∀[T:{G, psi ⊢ _}]. ∀[cT:G, psi +⊢ Compositon(T)].
∀[f:{G, psi ⊢ _:Equiv(T;A)}].
  comp(Glue [psi ⊢→ (T, f)] A)  = cT ∈ G ⊢ Compositon(T) supposing G ⊢ (1(𝔽) ⇒ psi)
BY
{ (InstLemma `glue-comp-agrees` []
   THEN (RepeatFor 7 (ParallelLast') THEN Intro)
   THEN SubsumeC ⌜G, psi ⊢ Compositon(T)⌝⋅
   THEN Try (Trivial)
   THEN BLemma `composition-structure-subset`
   THEN Auto
   THEN BLemma `face-1-implies-subset`
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[G:j\mvdash{}].  \mforall{}[A:\{G  \mvdash{}  \_\}].  \mforall{}[cA:G  +\mvdash{}  Compositon(A)].  \mforall{}[psi:\{G  \mvdash{}  \_:\mBbbF{}\}].  \mforall{}[T:\{G,  psi  \mvdash{}  \_\}].
\mforall{}[cT:G,  psi  +\mvdash{}  Compositon(T)].  \mforall{}[f:\{G,  psi  \mvdash{}  \_:Equiv(T;A)\}].
    comp(Glue  [psi  \mvdash{}\mrightarrow{}  (T,  f)]  A)    =  cT  supposing  G  \mvdash{}  (1(\mBbbF{})  {}\mRightarrow{}  psi)


By

---

Latex:
(InstLemma  `glue-comp-agrees`  []
  THEN  (RepeatFor  7  (ParallelLast')  THEN  Intro)
  THEN  SubsumeC  \mkleeneopen{}G,  psi  \mvdash{}  Compositon(T)\mkleeneclose{}\mcdot{}
  THEN  Try  (Trivial)
  THEN  BLemma  `composition-structure-subset`
  THEN  Auto
  THEN  BLemma  `face-1-implies-subset`
  THEN  Auto)

---

Home Index