proposition: Lemma list_map {A B} (f: A → B) (l: L A): to_list (map f l) = List.map f (to_list l).
proof: Proof. induction l. reflexivity. simpl. congruence. Qed.
imports: Coq.Unicode.Utf8 Coq.Lists.List Coq.Setoids.Setoid Coq.Classes.Morphisms Coq.Sorting.Permutation