---

Step * of Lemma seq-append_wf_consistent

∀T:Type. ∀R:n:ℕ ⟶ (ℕn ⟶ T) ⟶ T ⟶ ℙ. ∀n:ℕ. ∀s:R-consistent-seq(n). ∀t:T.
  ((R n s t) ⇒ (seq-append(n;1;s;λi.t) ∈ R-consistent-seq(n + 1)))
BY
{ (Auto THEN DVar `s' THEN MemTypeCD 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
⊢ R x seq-append(n;1;s;λi.t) (seq-append(n;1;s;λi.t) x)

---

Latex:

---

Latex:
\mforall{}T:Type.  \mforall{}R:n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  T)  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}.  \mforall{}n:\mBbbN{}.  \mforall{}s:R-consistent-seq(n).  \mforall{}t:T.
    ((R  n  s  t)  {}\mRightarrow{}  (seq-append(n;1;s;\mlambda{}i.t)  \mmember{}  R-consistent-seq(n  +  1)))


By

---

Latex:
(Auto  THEN  DVar  `s'  THEN  MemTypeCD  THEN  Auto)

---

Home Index