---

Step * of Lemma mk_lambdas_compose

∀[F:Top]. ∀[n,m:ℕ].  (mk_lambdas(mk_lambdas(F;n);m) ~ mk_lambdas(F;n + m))
BY
{ ((UnivCD THENA Auto)
   THEN MoveToConcl (-2)
   THEN NatInd (-1)
   THEN (UnivCD THENA Auto)
   THEN Try (Complete ((RepUR ``mk_lambdas`` 0 THEN Subst ⌜n + 0 ~ n⌝ 0⋅ THEN Auto)))
   THEN (RW (AddrC [1] (LemmaC `mk_lambdas_unroll`)) 0 THENA Auto)
   THEN (RW (AddrC [2] (LemmaC `mk_lambdas_unroll`)) 0 THENA Auto')
   THEN MemCD
   THEN (Subst ⌜(n + m) - 1 ~ n + (m - 1)⌝ 0⋅ THENA Auto)
   THEN BackThruSomeHyp) }

---

Latex:

---

Latex:
\mforall{}[F:Top].  \mforall{}[n,m:\mBbbN{}].    (mk\_lambdas(mk\_lambdas(F;n);m)  \msim{}  mk\_lambdas(F;n  +  m))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  MoveToConcl  (-2)
  THEN  NatInd  (-1)
  THEN  (UnivCD  THENA  Auto)
  THEN  Try  (Complete  ((RepUR  ``mk\_lambdas``  0  THEN  Subst  \mkleeneopen{}n  +  0  \msim{}  n\mkleeneclose{}  0\mcdot{}  THEN  Auto)))
  THEN  (RW  (AddrC  [1]  (LemmaC  `mk\_lambdas\_unroll`))  0  THENA  Auto)
  THEN  (RW  (AddrC  [2]  (LemmaC  `mk\_lambdas\_unroll`))  0  THENA  Auto')
  THEN  MemCD
  THEN  (Subst  \mkleeneopen{}(n  +  m)  -  1  \msim{}  n  +  (m  -  1)\mkleeneclose{}  0\mcdot{}  THENA  Auto)
  THEN  BackThruSomeHyp)

---

Home Index