---

Step * of Lemma hdf-bind-as-gen

∀[X,Y:Top].  (X >>= Y ~ X ({}) >>= Y)
BY
{ (Auto THEN RepUR ``hdf-bind hdf-bind-gen`` 0 THEN Auto) }

---

Latex:


\mforall{}[X,Y:Top].    (X  >>=  Y  \msim{}  X  (\{\})  >>=  Y)


By

(Auto  THEN  RepUR  ``hdf-bind  hdf-bind-gen``  0  THEN  Auto)

---

Home Index