---

Step * of Lemma hdf-sqequal1

∀[F:Top]. (hdf-base(m.F[m]) ~ fix((λmk-hdf.(inl (λm.<mk-hdf, F[m]>)))))
BY
{ (Auto THEN RepUR ``hdf-base mk-hdf`` 0 THEN (SqequalInductionUsing' UnrollLoopsOnce⋅ THEN Auto)) }

---

Latex:


\mforall{}[F:Top].  (hdf-base(m.F[m])  \msim{}  fix((\mlambda{}mk-hdf.(inl  (\mlambda{}m.<mk-hdf,  F[m]>)))))


By

(Auto  THEN  RepUR  ``hdf-base  mk-hdf``  0  THEN  (SqequalInductionUsing'  UnrollLoopsOnce\mcdot{}  THEN  Auto))

---

Home Index