---

Step * 1 of Lemma csm-universe-comp-fun


1. s : Top
2. A : Top
3. G : Top
4. H : Top
5. X : Top
6. compOp(A) = X ∈ Top
⊢ (cop-to-cfun(X))s ~ cop-to-cfun((X)s)
BY
{ (RepUR ``comp-op-to-comp-fun composition-term csm-composition`` 0 THEN CsmUnfoldingComp THEN Auto) }

---

Latex:

---

Latex:

1.  s  :  Top
2.  A  :  Top
3.  G  :  Top
4.  H  :  Top
5.  X  :  Top
6.  compOp(A)  =  X
\mvdash{}  (cop-to-cfun(X))s  \msim{}  cop-to-cfun((X)s)


By

---

Latex:
(RepUR  ``comp-op-to-comp-fun  composition-term  csm-composition``  0  THEN  CsmUnfoldingComp  THEN  Auto)

---

Home Index