---

Step * of Lemma apply_gen_wf2

∀[B:Type]. ∀[n:ℕ]. ∀[m:ℕn + 1]. ∀[q:ℕm + 1]. ∀[A:ℕn ⟶ Type]. ∀[f:funtype(n - q;λx.(A (x + q));B)].
∀[lst:k:{q..n-} ⟶ (A k)].
  (apply_gen(m;lst) q f ∈ funtype(n - m;λx.(A (x + m));B))
BY
{ ((UnivCD THEN Auto')
   THEN (D (-4) THENA Auto)
   THEN (D (-6) THENA Auto)
   THEN (Assert ⌜∃p:ℕ. (q = (m - p) ∈ ℤ)⌝⋅ THENA (InstConcl [⌜m - q⌝]⋅ THEN Auto'))
   THEN D (-1)
   THEN (HypSubst' (-1) 0
         THEN MoveToConcl (-4)
         THEN (D 0 THENA Auto')
         THEN HypSubst' (-2) (-1)
         THEN MoveToConcl (-6)
         THEN (D 0 THENA Auto)
         THEN HypSubst' (-3) (-1)⋅
         THEN MoveToConcl (-5)
         THEN (D 0 THENA Auto)
         THEN HypSubst' (-4) (-1)
         THEN Thin (-4)
         THEN Thin (-6)
         THEN MoveToConcl (-3)
         THEN (D 0 THENA Auto'))⋅) }

1
1. B : Type
2. n : ℕ
3. m : ℤ
4. 0 ≤ m < n + 1
5. A : ℕn ⟶ Type
6. p : ℕ
7. 0 ≤ m - p < m + 1
8. lst : k:{m - p..n-} ⟶ (A k)
9. f : funtype(n - m - p;λx.(A (x + (m - p)));B)
⊢ apply_gen(m;lst) (m - p) f ∈ funtype(n - m;λx.(A (x + m));B)

---

Latex:

---

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


By

---

Latex:
((UnivCD  THEN  Auto')
  THEN  (D  (-4)  THENA  Auto)
  THEN  (D  (-6)  THENA  Auto)
  THEN  (Assert  \mkleeneopen{}\mexists{}p:\mBbbN{}.  (q  =  (m  -  p))\mkleeneclose{}\mcdot{}  THENA  (InstConcl  [\mkleeneopen{}m  -  q\mkleeneclose{}]\mcdot{}  THEN  Auto'))
  THEN  D  (-1)
  THEN  (HypSubst'  (-1)  0
              THEN  MoveToConcl  (-4)
              THEN  (D  0  THENA  Auto')
              THEN  HypSubst'  (-2)  (-1)
              THEN  MoveToConcl  (-6)
              THEN  (D  0  THENA  Auto)
              THEN  HypSubst'  (-3)  (-1)\mcdot{}
              THEN  MoveToConcl  (-5)
              THEN  (D  0  THENA  Auto)
              THEN  HypSubst'  (-4)  (-1)
              THEN  Thin  (-4)
              THEN  Thin  (-6)
              THEN  MoveToConcl  (-3)
              THEN  (D  0  THENA  Auto'))\mcdot{})

---

Home Index