---

Step * of Lemma comp-op-to-comp-fun-univ-comp

No Annotations
∀[G:j⊢]. (cop-to-cfun(univ-comp{i:l}()) ∈ composition-structure{[i' | j]:l, i':l}(G; c𝕌))
BY
{ (Intro
   THEN (InstLemma `comp-op-to-comp-fun_wf2` [⌜parm{[i' | j]}⌝;⌜parm{i'}⌝;⌜G⌝;⌜c𝕌⌝;⌜univ-comp{i:l}()⌝]⋅ THENA Auto)
   THEN (Assert univ-comp{i:l}() ∈ () ⊢ CompOp(c𝕌) BY
               ((InstLemma  `univ-comp-sq` [⌜()⌝]⋅ THENA Auto) THEN RWO "-1" 0 THEN Auto))
   THEN DoSubsume
   THEN Try (Trivial)) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[G:j\mvdash{}].  (cop-to-cfun(univ-comp\{i:l\}())  \mmember{}  composition-structure\{[i'  |  j]:l,  i':l\}(G;  c\mBbbU{}))


By

---

Latex:
(Intro
  THEN  (InstLemma  `comp-op-to-comp-fun\_wf2`  [\mkleeneopen{}parm\{[i'  |  j]\}\mkleeneclose{};\mkleeneopen{}parm\{i'\}\mkleeneclose{};\mkleeneopen{}G\mkleeneclose{};\mkleeneopen{}c\mBbbU{}\mkleeneclose{};\mkleeneopen{}univ-comp\{i:l\}()\mkleeneclose{}]
              \mcdot{}
              THENA  Auto
              )
  THEN  (Assert  univ-comp\{i:l\}()  \mmember{}  ()  \mvdash{}  CompOp(c\mBbbU{})  BY
                          ((InstLemma    `univ-comp-sq`  [\mkleeneopen{}()\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  RWO  "-1"  0  THEN  Auto))
  THEN  DoSubsume
  THEN  Try  (Trivial))

---

Home Index