---

Step * of Lemma csm+-comp-csm+

No Annotations
∀[H,K,X:j⊢]. ∀[A:{H ⊢ _}]. ∀[tau:K j⟶ H]. ∀[s:X j⟶ K].  (tau+ o s+ = tau o s+ ∈ X.((A)tau)s ij⟶ H.A)
BY
{ (Intros THEN RWO  "csm+-comp-csm+-sq" 0 THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[H,K,X:j\mvdash{}].  \mforall{}[A:\{H  \mvdash{}  \_\}].  \mforall{}[tau:K  j{}\mrightarrow{}  H].  \mforall{}[s:X  j{}\mrightarrow{}  K].    (tau+  o  s+  =  tau  o  s+)


By

---

Latex:
(Intros  THEN  RWO    "csm+-comp-csm+-sq"  0  THEN  Auto)

---

Home Index