---

Step * 1 2 of Lemma seq-add_wf_consistent


1. T : Type
2. R : n:ℕ ⟶ (ℕn ⟶ T) ⟶ T ⟶ ℙ
3. n : ℕ
4. s : ℕn ⟶ T
5. ∀x:ℕn. (R x s (s x))
6. t : T
7. R n s t
8. x : ℕn + 1
9. ¬(x = n ∈ ℤ)
⊢ R x s.t@n (s.t@n x)
BY
{ ((Assert s.t@n = s ∈ (ℕx ⟶ T) BY
          (FunExt THEN Auto THEN RepUR ``seq-add`` 0 THEN AutoSplit))
   THEN (Subst ⌜s.t@n x ~ s x⌝ 0⋅ THENA (RepUR ``seq-add`` 0 THEN Auto))
   ) }

1
1. T : Type
2. R : n:ℕ ⟶ (ℕn ⟶ T) ⟶ T ⟶ ℙ
3. n : ℕ
4. s : ℕn ⟶ T
5. ∀x:ℕn. (R x s (s x))
6. t : T
7. R n s t
8. x : ℕn + 1
9. ¬(x = n ∈ ℤ)
10. s.t@n = s ∈ (ℕx ⟶ T)
⊢ R x s.t@n (s x)

---

Latex:

---

Latex:

1.  T  :  Type
2.  R  :  n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  T)  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
3.  n  :  \mBbbN{}
4.  s  :  \mBbbN{}n  {}\mrightarrow{}  T
5.  \mforall{}x:\mBbbN{}n.  (R  x  s  (s  x))
6.  t  :  T
7.  R  n  s  t
8.  x  :  \mBbbN{}n  +  1
9.  \mneg{}(x  =  n)
\mvdash{}  R  x  s.t@n  (s.t@n  x)


By

---

Latex:
((Assert  s.t@n  =  s  BY
                (FunExt  THEN  Auto  THEN  RepUR  ``seq-add``  0  THEN  AutoSplit))
  THEN  (Subst  \mkleeneopen{}s.t@n  x  \msim{}  s  x\mkleeneclose{}  0\mcdot{}  THENA  (RepUR  ``seq-add``  0  THEN  Auto))
  )

---

Home Index