---

Step * of Lemma csm-contr-center

∀[c,s:Top].  ((contr-center(c))s ~ contr-center((c)s))
BY
{ ((Intros THEN RepUR ``contr-center csm-ap-term cubical-fst`` 0) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[c,s:Top].    ((contr-center(c))s  \msim{}  contr-center((c)s))


By

---

Latex:
((Intros  THEN  RepUR  ``contr-center  csm-ap-term  cubical-fst``  0)  THEN  Auto)

---

Home Index