---

Step * 1 of Lemma hdf-compose1-transformation0


1. f : Top
2. F : Top
⊢ f o fix((λmk-hdf.(inl (λa.<mk-hdf, F[a]>)))) ~ fix((λmk-hdf.(inl (λa.let v ←─ bag-map(f;F[a])
                                                                       in <mk-hdf, v>))))
BY
{ (SqequalInductionUsing' UnrollLoopsOnce⋅
   THEN Auto
   THEN SqequalNNonCanonicalCD⋅
   THEN Try (Complete (Auto))
   THEN SqequalNCanonicalCD⋅
   THEN Auto
   THEN BackThruSomeHyp⋅
   THEN Auto) }

---

Latex:



1.  f  :  Top
2.  F  :  Top
\mvdash{}  f  o  fix((\mlambda{}mk-hdf.(inl  (\mlambda{}a.<mk-hdf,  F[a]>))))  \msim{}  fix((\mlambda{}mk-hdf.(inl  (\mlambda{}a.let  v  \mleftarrow{}{}  bag-map(f;F[a])
                                                                                                                                              in  <mk-hdf,  v>))))


By

(SqequalInductionUsing'  UnrollLoopsOnce\mcdot{}
  THEN  Auto
  THEN  SqequalNNonCanonicalCD\mcdot{}
  THEN  Try  (Complete  (Auto))
  THEN  SqequalNCanonicalCD\mcdot{}
  THEN  Auto
  THEN  BackThruSomeHyp\mcdot{}
  THEN  Auto)

---

Home Index