---

Step * of Lemma CV_property

∀[F,t:Top].  (CV(F) t ~ F t CV(F))
BY
{ ((UnivCD THENA Auto) THEN (RW (AddrC [1] (RecUnfoldC `CV`)) 0) THEN Reduce 0 THEN Trivial) }

---

Latex:

---

Latex:
\mforall{}[F,t:Top].    (CV(F)  t  \msim{}  F  t  CV(F))


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  (RW  (AddrC  [1]  (RecUnfoldC  `CV`))  0)  THEN  Reduce  0  THEN  Trivial)

---

Home Index