---

Step * of Lemma hdf-out-run

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

---

Latex:


\mforall{}[P,x:Top].    (hdf-out(hdf-run(P);x)  \msim{}  snd((P  x)))


By

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

---

Home Index