---

Step * of Lemma pscm-adjoin-comp

∀[Gamma,Delta,X,A,sigma,u,g:Top].  ((sigma;u) o g ~ (sigma o g;(u)g))
BY
{ (Auto THEN RepUR ``pscm-adjoin pscm-comp compose pscm-ap pscm-ap-term`` 0 THEN EqCD) }

---

Latex:

---

Latex:
\mforall{}[Gamma,Delta,X,A,sigma,u,g:Top].    ((sigma;u)  o  g  \msim{}  (sigma  o  g;(u)g))


By

---

Latex:
(Auto  THEN  RepUR  ``pscm-adjoin  pscm-comp  compose  pscm-ap  pscm-ap-term``  0  THEN  EqCD)

---

Home Index