proposition: Fact list_assoc_In x l : match list_assoc x l with | None => ~ In x (map fst l) | Some y => In (x,y) l end.
proof: Proof. induction l as [ | (x',y) l IHl ]; simpl; auto. destruct (eq_X_dec x x'); subst; auto. destruct (list_assoc x l); auto. intros [ ? | ]; subst; tauto. Qed.
imports: List Arith Lia Permutation Undecidability.Shared.Libs.DLW.Utils(list_focus utils_tac)