English
Given a series p and a new head a with a ~[r] p.head, there is a new r-series consisting of a followed by p, with length increased by one.
Русский
Для серии p и новой головы a, где a ~[r] p.head, существует новая r-серия, состоящая из a в начале, затем p, длина увеличивается на единицу.
LaTeX
$$$ \\text{cons}(p,a,\\,\\text{rel}) : \\text{RelSeries } r$ с длиной $|p|+1$ и Head = a$$
Lean4
/-- Given a series `a₀ -r→ a₁ -r→ ... -r→ aₙ` and an `a` such that `a₀ -r→ a` holds, there is
a series of length `n+1`: `a -r→ a₀ -r→ a₁ -r→ ... -r→ aₙ`.
-/
@[simps! length]
def cons (p : RelSeries r) (newHead : α) (rel : newHead ~[r] p.head) : RelSeries r :=
(singleton r newHead).append p rel
