---

Step * of Lemma cubical-path-ap-id-adjoin2

∀[pth,x,Z:Top].  (((pth)p @ q)[x] ~ pth @ x)
BY
{ (InstLemma `cubical-path-ap-id-adjoin` [] THEN Trivial) }

---

Latex:

---

Latex:
\mforall{}[pth,x,Z:Top].    (((pth)p  @  q)[x]  \msim{}  pth  @  x)


By

---

Latex:
(InstLemma  `cubical-path-ap-id-adjoin`  []  THEN  Trivial)

---

Home Index