proposition: Lemma sublists_map {A B} (f : A -> B) l : sublists (map f l) = map (map f) (sublists l).
proof: Proof. induction l as [| a l IHl]. reflexivity. simpl. rewrite map_app, IHl. f_equal. clear. induction (sublists l) as [| x xs IHxs]. reflexivity. simpl. f_equal. auto. Qed.
imports: Lists.List ZArith Setoid Coq.Classes.Morphisms Lia