---

Step * of Lemma path_term-0

∀[H,A,psi,r,a,b,w:Top].
  ((path_term(psi; w; a; b; r))[0(𝕀)] ~ path-term((psi)1(H.A);(w)[0(𝕀)];(a)[0(𝕀)];(b)[0(𝕀)];(r)1(H.A)))
BY
{ (Intros THEN (RWO "csm-path_term" 0 THENA Auto) THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[H,A,psi,r,a,b,w:Top].
    ((path\_term(psi;  w;  a;  b;  r))[0(\mBbbI{})] 
    \msim{}  path-term((psi)1(H.A);(w)[0(\mBbbI{})];(a)[0(\mBbbI{})];(b)[0(\mBbbI{})];(r)1(H.A)))


By

---

Latex:
(Intros  THEN  (RWO  "csm-path\_term"  0  THENA  Auto)  THEN  Reduce  0  THEN  Auto)

---

Home Index