---

Step * of Lemma csm-sigma_comp3

∀[H,A',X,cA,cB,A,tau:Top].  ((sigma_comp(cA;cB))tau ~ sigma_comp((cA)tau;(cB)tau+))
BY
{ ((Intros THEN RepUR ``sigma_comp let csm-comp-structure`` 0) THEN CsmUnfolding THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[H,A',X,cA,cB,A,tau:Top].    ((sigma\_comp(cA;cB))tau  \msim{}  sigma\_comp((cA)tau;(cB)tau+))


By

---

Latex:
((Intros  THEN  RepUR  ``sigma\_comp  let  csm-comp-structure``  0)  THEN  CsmUnfolding  THEN  Auto)

---

Home Index