---

Step * of Lemma seq-truncate_wf

∀[T:Type]. ∀[s:sequence(T)]. ∀[n:ℕ].  seq-truncate(s;n) ∈ sequence(T) supposing n ≤ ||s||
BY
{ Auto }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[s:sequence(T)].  \mforall{}[n:\mBbbN{}].    seq-truncate(s;n)  \mmember{}  sequence(T)  supposing  n  \mleq{}  ||s||


By

---

Latex:
Auto

---

Home Index