proposition: Lemma rev_map A B (f : A -> B) (l : list A) : rev (map f l) = map f (rev l).
proof: Proof. induction l; ins; rewrite map_app, IHl; ins. Qed.
imports: HahnBase HahnSets Arith Lia Setoid Morphisms Sorted IndefiniteDescription List Permutation