---

Step * of Lemma seq-adjoin-is-seq-add

∀[n:ℕ]. ∀[s:ℕn ⟶ ℕ]. ∀[m:ℕ].  (s.m@n = s++m ∈ (ℕn + 1 ⟶ ℕ))
BY
{ ((UnivCD THENA Auto) THEN RepUR ``seq-adjoin seq-add seq-append`` 0 THEN (EqCD THENA Auto) THEN AutoSplit) }

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[s:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}].  \mforall{}[m:\mBbbN{}].    (s.m@n  =  s++m)


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  RepUR  ``seq-adjoin  seq-add  seq-append``  0
  THEN  (EqCD  THENA  Auto)
  THEN  AutoSplit)

---

Home Index