---

Step * of Lemma csm-path_term

∀[psi,r,s,a,b,w:Top].  ((path_term(psi; w; a; b; r))s ~ path-term(((psi)p)s;(w)s;(a)s;(b)s;((r)p)s))
BY
{ (Intros THEN Unfold `path_term` 0 THEN RWO "csm-path-term" 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[psi,r,s,a,b,w:Top].    ((path\_term(psi;  w;  a;  b;  r))s  \msim{}  path-term(((psi)p)s;(w)s;(a)s;(b)s;((r)p)s))


By

---

Latex:
(Intros  THEN  Unfold  `path\_term`  0  THEN  RWO  "csm-path-term"  0  THEN  Auto)

---

Home Index