---

Step * of Lemma apply_gen_wf

∀[B:Type]. ∀[n:ℕ]. ∀[m:ℕn + 1]. ∀[A:ℕn ⟶ Type]. ∀[f:funtype(n - m;λx.(A (x + m));B)]. ∀[lst:k:{m..n-} ⟶ (A k)].
  (apply_gen(n;lst) m f ∈ B)
BY
{ xxx(RepeatFor 3 ((D 0 THENA Auto'))
      THEN (Assert ⌜∃p:ℕ. (m = (n - p) ∈ ℤ)⌝⋅ THENA (InstConcl [⌜n - m⌝]⋅ THEN Auto))
      THEN D (-1)
      THEN HypSubst' (-1) 0
      THEN (D (-3) THENA Auto)
      THEN (HypSubst' (-1) (-3) THENA Auto)
      THEN Thin (-2)⋅
      THEN Thin (-3)⋅
      THEN Unfolds ``apply_gen funtype`` 0
      THEN NatInd (-2)⋅
      THEN RW (SweepUpC UnrollRecursionC) 0
      THEN Reduce 0
      THEN (RWO "primrec-unroll" 0 THENA Auto)
      THEN AutoSplit
      THEN Subst ⌜(n - p) + 1 ~ n - p - 1⌝ 0⋅
      THEN Auto
      THEN xxxUsingVars [`A'] (BackThruSomeHyp)xxx
      THEN Reduce 0
      THEN Auto')xxx }

---

Latex:

---

Latex:
\mforall{}[B:Type].  \mforall{}[n:\mBbbN{}].  \mforall{}[m:\mBbbN{}n  +  1].  \mforall{}[A:\mBbbN{}n  {}\mrightarrow{}  Type].  \mforall{}[f:funtype(n  -  m;\mlambda{}x.(A  (x  +  m));B)].
\mforall{}[lst:k:\{m..n\msupminus{}\}  {}\mrightarrow{}  (A  k)].
    (apply\_gen(n;lst)  m  f  \mmember{}  B)


By

---

Latex:
xxx(RepeatFor  3  ((D  0  THENA  Auto'))
        THEN  (Assert  \mkleeneopen{}\mexists{}p:\mBbbN{}.  (m  =  (n  -  p))\mkleeneclose{}\mcdot{}  THENA  (InstConcl  [\mkleeneopen{}n  -  m\mkleeneclose{}]\mcdot{}  THEN  Auto))
        THEN  D  (-1)
        THEN  HypSubst'  (-1)  0
        THEN  (D  (-3)  THENA  Auto)
        THEN  (HypSubst'  (-1)  (-3)  THENA  Auto)
        THEN  Thin  (-2)\mcdot{}
        THEN  Thin  (-3)\mcdot{}
        THEN  Unfolds  ``apply\_gen  funtype``  0
        THEN  NatInd  (-2)\mcdot{}
        THEN  RW  (SweepUpC  UnrollRecursionC)  0
        THEN  Reduce  0
        THEN  (RWO  "primrec-unroll"  0  THENA  Auto)
        THEN  AutoSplit
        THEN  Subst  \mkleeneopen{}(n  -  p)  +  1  \msim{}  n  -  p  -  1\mkleeneclose{}  0\mcdot{}
        THEN  Auto
        THEN  xxxUsingVars  [`A']  (BackThruSomeHyp)xxx
        THEN  Reduce  0
        THEN  Auto')xxx

---

Home Index