---

Step * of Lemma comp-op-to-comp-fun_wf2

No Annotations
∀[Gamma:j⊢]. ∀[A:{Gamma ⊢ _}]. ∀[cA:Gamma ⊢ CompOp(A)].  (cop-to-cfun(cA) ∈ Gamma ⊢ Compositon(A))
BY
{ (InstLemma `uniform-comp-function_wf` []
   THEN RepeatFor 2 (ParallelLast')
   THEN Intro
   THEN (MemTypeCD THENW (D 3 With ⌜comp⌝  THEN Auto))
   THEN Try ((MemCD THEN Auto))
   THEN RepeatFor 7 ((D 0 THENA Auto))
   THEN BLemma `csm-comp-op-to-comp-fun`
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[Gamma:j\mvdash{}].  \mforall{}[A:\{Gamma  \mvdash{}  \_\}].  \mforall{}[cA:Gamma  \mvdash{}  CompOp(A)].    (cop-to-cfun(cA)  \mmember{}  Gamma  \mvdash{}  Compositon(A))


By

---

Latex:
(InstLemma  `uniform-comp-function\_wf`  []
  THEN  RepeatFor  2  (ParallelLast')
  THEN  Intro
  THEN  (MemTypeCD  THENW  (D  3  With  \mkleeneopen{}comp\mkleeneclose{}    THEN  Auto))
  THEN  Try  ((MemCD  THEN  Auto))
  THEN  RepeatFor  7  ((D  0  THENA  Auto))
  THEN  BLemma  `csm-comp-op-to-comp-fun`
  THEN  Auto)

---

Home Index