---

Step * of Lemma apply_larger_list

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

1
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

2
1. B : Type
2. n : ℕ
3. A : ℕn ⟶ Type
4. p : ℤ
5. 0 < p
6. 0 ≤ n - p - 1 < n + 1
⇒ (∀q:ℕ(n - p - 1) + 1. ∀lst:k:{q..n-} ⟶ (A k). ∀r:ℕn - p - 1. ∀a:A r. ∀f:funtype(n - n - p - 1;λx.(A 
                                                                                                      (x
                                                                                                      + (n - p 
                                                                                                        - 1)));B).
      ((apply_gen(n;λx.if (x =z r) then a else lst x fi ) (n - p - 1) f) = (apply_gen(n;lst) (n - p - 1) f) ∈ B))
7. 0 ≤ n - p < n + 1
8. q : ℕ(n - p) + 1
9. lst : k:{q..n-} ⟶ (A k)
10. r : ℕn - p
11. a : A r
12. f : funtype(n - n - p;λx.(A (x + (n - p)));B)
⊢ (apply_gen(n;λx.if (x =z r) then a else lst x fi ) (n - p) f) = (apply_gen(n;lst) (n - p) f) ∈ 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{}[lst:k:\{q..n\msupminus{}\}  {}\mrightarrow{}  (A  k)].  \mforall{}[r:\mBbbN{}m].
\mforall{}[a:A  r].  \mforall{}[f:funtype(n  -  m;\mlambda{}x.(A  (x  +  m));B)].
    ((apply\_gen(n;\mlambda{}x.if  (x  =\msubz{}  r)  then  a  else  lst  x  fi  )  m  f)  =  (apply\_gen(n;lst)  m  f))


By

---

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

---

Home Index