proposition: Fact map_cons_inv ll y m : map f ll = y::m -> { x : _ & { l | ll = x::l /\ f x = y /\ map f l = m } }.
proof: Proof. destruct ll as [ | x l ]; try discriminate; simpl. intros H; inversion H; subst; exists x, l; auto. Qed.
imports: List Arith Lia Permutation Undecidability.Shared.Libs.DLW.Utils(list_focus utils_tac)