---

Step * of Lemma mk_lambdas_fun-unroll-ite

∀[F:Top]. ∀[m:ℕ].
  (mk_lambdas_fun(F;m) ~ if (m =z 0) then F (λx.x) else λx.mk_lambdas_fun(λg.(F (λf.(g (f x))));m - 1) fi )
BY
{ (Auto
   THEN AutoSplit
   THEN Try ((BLemma `mk_lambdas_fun-unroll-first` THEN Auto))
   THEN HypSubst' (-1) 0
   THEN RepUR ``mk_lambdas_fun`` 0
   THEN RecUnfold `mk_lambdas-fun` 0
   THEN AutoSplit) }

---

Latex:

---

Latex:
\mforall{}[F:Top].  \mforall{}[m:\mBbbN{}].
    (mk\_lambdas\_fun(F;m)  \msim{}  if  (m  =\msubz{}  0)
    then  F  (\mlambda{}x.x)
    else  \mlambda{}x.mk\_lambdas\_fun(\mlambda{}g.(F  (\mlambda{}f.(g  (f  x))));m  -  1)
    fi  )


By

---

Latex:
(Auto
  THEN  AutoSplit
  THEN  Try  ((BLemma  `mk\_lambdas\_fun-unroll-first`  THEN  Auto))
  THEN  HypSubst'  (-1)  0
  THEN  RepUR  ``mk\_lambdas\_fun``  0
  THEN  RecUnfold  `mk\_lambdas-fun`  0
  THEN  AutoSplit)

---

Home Index