proposition: Fact list_assoc_neq x y l x' : x <> x' -> list_assoc x' ((x,y)::l) = list_assoc x' l.
proof: Proof. intros H; simpl. destruct (eq_X_dec x' x) as [ | ]; auto. destruct H; auto. Qed.
imports: List Arith Lia Permutation Undecidability.Shared.Libs.DLW.Utils(list_focus utils_tac)