---

Step * of Lemma hdf-base-transformation1-base

∀[F:Base]. (hdf-base(m.F[m]) ~ fix((λmk-hdf.(inl (λa.cbva_seq(λx.⊥; λg.<mk-hdf, F[a]>; 0))))))
BY
{ (Auto
   THEN RepUR ``hdf-base mk-hdf cbva_seq hdf-run`` 0
   THEN RecUnfold `callbyvalueall_seq` 0
   THEN Reduce 0
   THEN SqequalInductionUsing' UnrollLoopsOnce⋅
   THEN Auto) }

---

Latex:


\mforall{}[F:Base].  (hdf-base(m.F[m])  \msim{}  fix((\mlambda{}mk-hdf.(inl  (\mlambda{}a.cbva\_seq(\mlambda{}x.\mbot{};  \mlambda{}g.<mk-hdf,  F[a]>  0))))))


By

(Auto
  THEN  RepUR  ``hdf-base  mk-hdf  cbva\_seq  hdf-run``  0
  THEN  RecUnfold  `callbyvalueall\_seq`  0
  THEN  Reduce  0
  THEN  SqequalInductionUsing'  UnrollLoopsOnce\mcdot{}
  THEN  Auto)

---

Home Index