---

Step * of Lemma csm-composition-exists

No Annotations
∀[Gamma,Delta:j⊢]. ∀[A:{Gamma ⊢ _}].  ∀s:Delta j⟶ Gamma. (Gamma ⊢ CompOp(A) ⇒ Delta ⊢ CompOp((A)s))
BY
{ (Auto THEN RenameVar `cA' (-1) THEN UseWitness ⌜(cA)s⌝⋅ THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[Gamma,Delta:j\mvdash{}].  \mforall{}[A:\{Gamma  \mvdash{}  \_\}].
    \mforall{}s:Delta  j{}\mrightarrow{}  Gamma.  (Gamma  \mvdash{}  CompOp(A)  {}\mRightarrow{}  Delta  \mvdash{}  CompOp((A)s))


By

---

Latex:
(Auto  THEN  RenameVar  `cA'  (-1)  THEN  UseWitness  \mkleeneopen{}(cA)s\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index