---

Step * of Lemma csm-path_comp

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

---

Latex:

---

Latex:
\mforall{}[G,H,A,a,b,cA,tau:Top].    ((path\_comp(G;A;a;b;cA))tau  \msim{}  path\_comp(H;(A)tau;(a)tau;(b)tau;(cA)tau))


By

---

Latex:
(Intros  THEN  RepUR  ``path\_comp  csm-comp-structure``  0  THEN  CsmUnfolding  THEN  EqCD)

---

Home Index