---

Step * of Lemma mk_lambdas_unroll2

∀[F:Top]. ∀[m:ℕ+].  (mk_lambdas(F;m) ~ mk_lambdas(λx.F;m - 1))
BY
{ ((UnivCD THENA Auto)
   THEN SqEqualTopToBase
   THEN MoveToConcl (-1)
   THEN ((NatPlusInd 1 THENM D 0) THENA Auto)
   THEN Try ((RepUR ``mk_lambdas`` 0 THEN Complete (Auto)))
   THEN (RWO "mk_lambdas_unroll" 0 THENA Auto)
   THEN (Subst ⌜(m + 1) - 1 ~ m⌝ 0⋅ THENA Auto)
   THEN MemCD
   THEN BackThruSomeHyp) }

---

Latex:

---

Latex:
\mforall{}[F:Top].  \mforall{}[m:\mBbbN{}\msupplus{}].    (mk\_lambdas(F;m)  \msim{}  mk\_lambdas(\mlambda{}x.F;m  -  1))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  SqEqualTopToBase
  THEN  MoveToConcl  (-1)
  THEN  ((NatPlusInd  1  THENM  D  0)  THENA  Auto)
  THEN  Try  ((RepUR  ``mk\_lambdas``  0  THEN  Complete  (Auto)))
  THEN  (RWO  "mk\_lambdas\_unroll"  0  THENA  Auto)
  THEN  (Subst  \mkleeneopen{}(m  +  1)  -  1  \msim{}  m\mkleeneclose{}  0\mcdot{}  THENA  Auto)
  THEN  MemCD
  THEN  BackThruSomeHyp)

---

Home Index