proposition: Lemma tl_map {A B} (l: list A) (f: A → B): tl (map f l) = map f (tl l).
proof: Proof. destruct l; reflexivity. Qed.
imports: Coq.Lists.List Coq.Unicode.Utf8 Coq.Setoids.Setoid Coq.Sorting.Permutation Coq.Setoids.Setoid Coq.Classes.Morphisms CoRN.stdlib_omissions.Pair