---

Step * 1 of Lemma apply_gen_wf2


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)
BY
{ NatInd (-4)⋅ }

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

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

1.  B  :  Type
2.  n  :  \mBbbN{}
3.  m  :  \mBbbZ{}
4.  0  \mleq{}  m  <  n  +  1
5.  A  :  \mBbbN{}n  {}\mrightarrow{}  Type
6.  p  :  \mBbbN{}
7.  0  \mleq{}  m  -  p  <  m  +  1
8.  lst  :  k:\{m  -  p..n\msupminus{}\}  {}\mrightarrow{}  (A  k)
9.  f  :  funtype(n  -  m  -  p;\mlambda{}x.(A  (x  +  (m  -  p)));B)
\mvdash{}  apply\_gen(m;lst)  (m  -  p)  f  \mmember{}  funtype(n  -  m;\mlambda{}x.(A  (x  +  m));B)


By

---

Latex:
NatInd  (-4)\mcdot{}

---

Home Index