---

Step * of Lemma hdf-return-transformation2

∀[x:Top]. (hdf-return(x) ~ inl (λm.<inr Ax , x>))
BY
{ (Auto THEN RepUR ``hdf-return hdf-run hdf-halt it`` 0 THEN Auto) }

---

Latex:


\mforall{}[x:Top].  (hdf-return(x)  \msim{}  inl  (\mlambda{}m.<inr  Ax  ,  x>))


By

(Auto  THEN  RepUR  ``hdf-return  hdf-run  hdf-halt  it``  0  THEN  Auto)

---

Home Index