---

Step * of Lemma path_term-1

∀[H,A,psi,r,a,b,w:Top].
  ((path_term(psi; w; a; b; r))[1(𝕀)] ~ path-term((psi)1(H.A);(w)[1(𝕀)];(a)[1(𝕀)];(b)[1(𝕀)];(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))[1(\mBbbI{})] 
    \msim{}  path-term((psi)1(H.A);(w)[1(\mBbbI{})];(a)[1(\mBbbI{})];(b)[1(\mBbbI{})];(r)1(H.A)))


By

---

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

---

Home Index