---

Step * of Lemma seq-append0-left

∀[t:Top]. ∀[m:ℕ]. ∀[f:ℕm ⟶ ℕ].  (seq-append(0;m;t;f) = f ∈ (ℕm ⟶ ℕ))
BY
{ ((UnivCD THENA Auto) THEN (Ext THENA Auto) THEN RepUR ``seq-append`` 0 THEN AutoSplit) }

---

Latex:

---

Latex:
\mforall{}[t:Top].  \mforall{}[m:\mBbbN{}].  \mforall{}[f:\mBbbN{}m  {}\mrightarrow{}  \mBbbN{}].    (seq-append(0;m;t;f)  =  f)


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  (Ext  THENA  Auto)  THEN  RepUR  ``seq-append``  0  THEN  AutoSplit)

---

Home Index