---

Step * of Lemma pscm-id-comp-sq

∀[A,B,C,D,x,y,X,Y,Z:Top].  (1(D) o x o y ~ x o y)
BY
{ xxx(Intros THEN RepUR ``pscm-comp compose pscm-id`` 0 THEN Auto)xxx }

---

Latex:

---

Latex:
\mforall{}[A,B,C,D,x,y,X,Y,Z:Top].    (1(D)  o  x  o  y  \msim{}  x  o  y)


By

---

Latex:
xxx(Intros  THEN  RepUR  ``pscm-comp  compose  pscm-id``  0  THEN  Auto)xxx

---

Home Index