proposition: Theorem In_list_in_map l f x (Hx : In x l) : In (f x Hx) (list_in_map l f).
proof: Proof. revert f x Hx. induction l as [ | x l IHl ]; intros f y Hy. + destruct Hy. + destruct Hy as [ -> | Hy ]. * left; auto. * right. apply (IHl (fun z Hz => f z (or_intror Hz))). Qed.
imports: List Arith Lia Permutation Undecidability.Shared.Libs.DLW.Utils(list_focus utils_tac)