---

Step * of Lemma length-copath-tl

∀[p:Top × Top]. (copath-length(copath-tl(p)) ~ copath-length(p) - 1)
BY
{ (Intros THEN (UseWitness ⌜Ax⌝⋅ THEN MemCD) THEN D -1 THEN Computation) }

---

Latex:

---

Latex:
\mforall{}[p:Top  \mtimes{}  Top].  (copath-length(copath-tl(p))  \msim{}  copath-length(p)  -  1)


By

---

Latex:
(Intros  THEN  (UseWitness  \mkleeneopen{}Ax\mkleeneclose{}\mcdot{}  THEN  MemCD)  THEN  D  -1  THEN  Computation)

---

Home Index