English
Similarly, tails(l) = reverse (map reverse (inits (reverse l))).
Русский
Аналогично, tails(l) = reverse (map reverse (inits (reverse l))).
LaTeX
$$$\forall l : \text{List}(\alpha),\; l.tails = (\text{reverse} \circ \text{map} \circ \text{reverse})(\text{inits} (\text{reverse} \; l)).$$$
Lean4
theorem tails_eq_inits : ∀ l : List α, l.tails = (reverse <| map reverse <| inits <| reverse l)
| [] => by simp
| a :: l => by simp [tails_eq_inits l]