---

Step * of Lemma hdf-compose1-transformation0-2

∀[f,F:Top].
  (f o fix((λmk-hdf.(inl (λa.<mk-hdf, F[a]>)))) ~ fix((λmk-hdf.(inl (λa.cbva_seq(λn.bag-map(f;F[a]); λg.<mk-hdf
                                                                                                        , g (λx.x)
                                                                                                        >; 1))))))
BY
{ (Auto
   THEN RepUR ``cbva_seq`` 0
   THEN RepeatFor 2 ((RecUnfold `callbyvalueall_seq` 0⋅ THEN Reduce 0))
   THEN SqequalInductionUsing' UnrollLoopsOnce⋅
   THEN Auto
   THEN SqequalNNonCanonicalCD⋅
   THEN Try (Complete (Auto))
   THEN SqequalNCanonicalCD⋅
   THEN Auto
   THEN BackThruSomeHyp⋅
   THEN Auto) }

---

Latex:


\mforall{}[f,F:Top].
    (f  o  fix((\mlambda{}mk-hdf.(inl  (\mlambda{}a.<mk-hdf,  F[a]>))))  \msim{}  fix((\mlambda{}mk-hdf.(inl  (\mlambda{}a.cbva\_seq(\mlambda{}n.bag-map(f;F[a]);
                                                                                                                                                                  \mlambda{}g.<mk-hdf
                                                                                                                                                                        ,  g  (\mlambda{}x.x)
                                                                                                                                                                        >  1))))))


By

(Auto
  THEN  RepUR  ``cbva\_seq``  0
  THEN  RepeatFor  2  ((RecUnfold  `callbyvalueall\_seq`  0\mcdot{}  THEN  Reduce  0))
  THEN  SqequalInductionUsing'  UnrollLoopsOnce\mcdot{}
  THEN  Auto
  THEN  SqequalNNonCanonicalCD\mcdot{}
  THEN  Try  (Complete  (Auto))
  THEN  SqequalNCanonicalCD\mcdot{}
  THEN  Auto
  THEN  BackThruSomeHyp\mcdot{}
  THEN  Auto)

---

Home Index