---

Step * 1 of Lemma apply_larger_list


1. B : Type
2. n : ℕ
3. A : ℕn ⟶ Type
4. p : ℤ
5. 0 ≤ n - 0 < n + 1
6. q : ℕ(n - 0) + 1
7. lst : k:{q..n-} ⟶ (A k)
8. r : ℕn - 0
9. a : A r
10. f : funtype(n - n - 0;λx.(A (x + (n - 0)));B)
⊢ (apply_gen(n;λx.if (x =z r) then a else lst x fi ) (n - 0) f) = (apply_gen(n;lst) (n - 0) f) ∈ B
BY
{ ((Subst ⌜n - 0 ~ n⌝ 0⋅ THENA Auto)
   THEN (Subst ⌜n - 0 ~ n⌝ (-1)⋅ THENA Auto)
   THEN (Subst ⌜n - n ~ 0⌝ (-1)⋅ THENA Auto)
   THEN RepUR ``funtype`` (-1)
   THEN Auto
   THEN Unfold `apply_gen` 0
   THEN RW (SweepUpC UnrollRecursionC) 0
   THEN Reduce 0
   THEN AutoSplit) }

---

Latex:

---

Latex:

1.  B  :  Type
2.  n  :  \mBbbN{}
3.  A  :  \mBbbN{}n  {}\mrightarrow{}  Type
4.  p  :  \mBbbZ{}
5.  0  \mleq{}  n  -  0  <  n  +  1
6.  q  :  \mBbbN{}(n  -  0)  +  1
7.  lst  :  k:\{q..n\msupminus{}\}  {}\mrightarrow{}  (A  k)
8.  r  :  \mBbbN{}n  -  0
9.  a  :  A  r
10.  f  :  funtype(n  -  n  -  0;\mlambda{}x.(A  (x  +  (n  -  0)));B)
\mvdash{}  (apply\_gen(n;\mlambda{}x.if  (x  =\msubz{}  r)  then  a  else  lst  x  fi  )  (n  -  0)  f)  =  (apply\_gen(n;lst)  (n  -  0)  f)


By

---

Latex:
((Subst  \mkleeneopen{}n  -  0  \msim{}  n\mkleeneclose{}  0\mcdot{}  THENA  Auto)
  THEN  (Subst  \mkleeneopen{}n  -  0  \msim{}  n\mkleeneclose{}  (-1)\mcdot{}  THENA  Auto)
  THEN  (Subst  \mkleeneopen{}n  -  n  \msim{}  0\mkleeneclose{}  (-1)\mcdot{}  THENA  Auto)
  THEN  RepUR  ``funtype``  (-1)
  THEN  Auto
  THEN  Unfold  `apply\_gen`  0
  THEN  RW  (SweepUpC  UnrollRecursionC)  0
  THEN  Reduce  0
  THEN  AutoSplit)

---

Home Index