proposition: Fact In_list_assoc x l : In x (map fst l) -> { y | list_assoc x l = Some y /\ In (x,y) l }.
proof: Proof. intros H. generalize (list_assoc_In x l). destruct (list_assoc x l) as [ y | ]. exists y; auto. tauto. Qed.
imports: List Arith Lia Permutation Undecidability.Shared.Libs.DLW.Utils(list_focus utils_tac)