---

Step * of Lemma seq-add-same

∀[f:ℕ ⟶ ℕ]. ∀[n:ℕ].  (f.f n@n = f ∈ (ℕ ⟶ ℕ))
BY
{ ((UnivCD THENA Auto) THEN RepUR ``seq-add`` 0 THEN (Ext THENA Auto) THEN Reduce 0 THEN AutoSplit) }

---

Latex:

---

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


By

---

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

---

Home Index