---

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

∀[pth,x,Z:Top].  (((pth)p @ q)[x] ~ pth @ x)
BY
{ (Intros
   THEN RepUR ``csm-ap-term cubical-path-app cubical-term-at csm-ap csm-id-adjoin cc-fst csm-adjoin csm-id`` 0
   THEN RepUR ``cubicalpath-app cubical-app cc-snd`` 0
   THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(Intros
  THEN  ...
  THEN  RepUR  ``cubicalpath-app  cubical-app  cc-snd``  0
  THEN  Auto)

---

Home Index