---

Step * of Lemma cubical-pi-comp-structure

No Annotations
∀X:j⊢. ∀A:{X ⊢ _}. ∀B:{X.A ⊢ _}.  (X ⊢ Compositon(A) ⇒ X.A +⊢ Compositon(B) ⇒ X ⊢ Compositon(ΠA B))
BY
{ (Intros
   THEN ((FLemma `composition-structure-implies-composition-op` [4] THENA Auto) THEN RenameVar `cA' (-1))
   THEN (FLemma `composition-structure-implies-composition-op` [5] THENA Auto)
   THEN RenameVar `cB' (-1)
   THEN InstLemma `composition-op-implies-composition-structure` [⌜X⌝;⌜ΠA B⌝;⌜pi-comp(X;A;B;cA;cB)⌝]⋅
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}X:j\mvdash{}.  \mforall{}A:\{X  \mvdash{}  \_\}.  \mforall{}B:\{X.A  \mvdash{}  \_\}.
    (X  \mvdash{}  Compositon(A)  {}\mRightarrow{}  X.A  +\mvdash{}  Compositon(B)  {}\mRightarrow{}  X  \mvdash{}  Compositon(\mPi{}A  B))


By

---

Latex:
(Intros
  THEN  ((FLemma  `composition-structure-implies-composition-op`  [4]  THENA  Auto)
              THEN  RenameVar  `cA'  (-1)
              )
  THEN  (FLemma  `composition-structure-implies-composition-op`  [5]  THENA  Auto)
  THEN  RenameVar  `cB'  (-1)
  THEN  InstLemma  `composition-op-implies-composition-structure`  [\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}\mPi{}A  B\mkleeneclose{};\mkleeneopen{}pi-comp(X;A;B;cA;cB)\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index