---

Step * of Lemma replace-seq-from-succ

∀T:Type. ∀f:ℕ ⟶ T. ∀m:ℕ. ∀k:T.
  (0 < m ⇒ (replace-seq-from(f;m;k) = (λx.if x=m - 1  then f x  else (replace-seq-from(f;m - 1;k) x)) ∈ (ℕ ⟶ T)))
BY
{ (((UnivCD THENA Auto) THEN RepUR ``replace-seq-from`` 0) THEN (FunExt THENA Auto) THEN Reduce 0 THEN AutoSplit) }

---

Latex:

---

Latex:
\mforall{}T:Type.  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  T.  \mforall{}m:\mBbbN{}.  \mforall{}k:T.
    (0  <  m
    {}\mRightarrow{}  (replace-seq-from(f;m;k)  =  (\mlambda{}x.if  x=m  -  1    then  f  x    else  (replace-seq-from(f;m  -  1;k)  x))))


By

---

Latex:
(((UnivCD  THENA  Auto)  THEN  RepUR  ``replace-seq-from``  0)
  THEN  (FunExt  THENA  Auto)
  THEN  Reduce  0
  THEN  AutoSplit)

---

Home Index