---

Step * of Lemma csm-pathtype-comp

∀[G,A,cA,H,tau:Top].  ((pathtype-comp(G;A;cA))tau ~ pathtype-comp(H;(A)tau;(cA)tau))
BY
{ ((RepUR ``csm-comp-structure pathtype-comp`` 0 THEN CsmUnfolding) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[G,A,cA,H,tau:Top].    ((pathtype-comp(G;A;cA))tau  \msim{}  pathtype-comp(H;(A)tau;(cA)tau))


By

---

Latex:
((RepUR  ``csm-comp-structure  pathtype-comp``  0  THEN  CsmUnfolding)  THEN  Auto)

---

Home Index