proposition: Theorem In_list_in_map_inv l f y : In y (list_in_map l f) -> exists x Hx, y = f x Hx.
proof: Proof. revert f y; induction l as [ | x l IHl ]; intros f y; simpl; try tauto. intros [ H | H ]. + now exists x, (or_introl eq_refl). + destruct IHl with (1 := H) as (z & Hz & E). now exists z, (or_intror Hz). Qed.
imports: List Arith Lia Permutation Undecidability.Shared.Libs.DLW.Utils(list_focus utils_tac)