---

Step * of Lemma hdf-ap-run

∀[P,a:Top].  (hdf-run(P)(a) ~ P a)
BY
{ (RepUR ``hdf-run hdf-ap`` 0 THEN Auto) }

---

Latex:


\mforall{}[P,a:Top].    (hdf-run(P)(a)  \msim{}  P  a)


By

(RepUR  ``hdf-run  hdf-ap``  0  THEN  Auto)

---

Home Index