proposition: Fact not_In_list_assoc x l : ~ In x (map fst l) -> list_assoc x l = None.
proof: Proof. intros H. generalize (list_assoc_In x l). destruct (list_assoc x l) as [ y | ]; auto. intros H1; contradict H. apply in_map_iff. exists (x,y); simpl; auto. Qed.
imports: List Arith Lia Permutation Undecidability.Shared.Libs.DLW.Utils(list_focus utils_tac)