---

Step * 1 1 1 of Lemma seq-append_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 seq-append(n;1;s;λi.t) t
BY
{ (NthHypEq (-3) THEN RepeatFor 2 (EqCD)) }

1
.....subterm..... T:t
1:n
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) = (R n) ∈ ((ℕx ⟶ T) ⟶ T ⟶ ℙ)

2
.....subterm..... T:t
2:n
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 ∈ ℤ
⊢ seq-append(n;1;s;λi.t) = s ∈ (ℕx ⟶ T)

---

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.  x  =  n
\mvdash{}  R  x  seq-append(n;1;s;\mlambda{}i.t)  t


By

---

Latex:
(NthHypEq  (-3)  THEN  RepeatFor  2  (EqCD))

---

Home Index