---

Step * of Lemma mk_applies_lambdas1

∀[F,G:Top]. ∀[n:ℕ]. ∀[m:ℕn + 1].  (mk_applies(mk_lambdas(F;m);G;n) ~ mk_applies(F;λk.(G (m + k));n - m))
BY
{ ((UnivCD THENA Auto)
   THEN (Assert ⌜∃i:ℕ. (n = (m + i) ∈ ℤ)⌝⋅ THENA (InstConcl [⌜n - m⌝]⋅ THEN Auto'))
   THEN ExRepD
   THEN HypSubst' (-1) 0
   THEN (Subst ⌜(m + i) - m ~ i⌝ 0⋅ THENA Auto)
   THEN (RWO "mk_applies_split" 0 THENA Auto)
   THEN RWO "mk_applies_lambdas2" 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[F,G:Top].  \mforall{}[n:\mBbbN{}].  \mforall{}[m:\mBbbN{}n  +  1].
    (mk\_applies(mk\_lambdas(F;m);G;n)  \msim{}  mk\_applies(F;\mlambda{}k.(G  (m  +  k));n  -  m))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (Assert  \mkleeneopen{}\mexists{}i:\mBbbN{}.  (n  =  (m  +  i))\mkleeneclose{}\mcdot{}  THENA  (InstConcl  [\mkleeneopen{}n  -  m\mkleeneclose{}]\mcdot{}  THEN  Auto'))
  THEN  ExRepD
  THEN  HypSubst'  (-1)  0
  THEN  (Subst  \mkleeneopen{}(m  +  i)  -  m  \msim{}  i\mkleeneclose{}  0\mcdot{}  THENA  Auto)
  THEN  (RWO  "mk\_applies\_split"  0  THENA  Auto)
  THEN  RWO  "mk\_applies\_lambdas2"  0
  THEN  Auto)

---

Home Index