proposition: Fact list_assoc_app x ll mm : list_assoc x (ll++mm) = match list_assoc x ll with | None => list_assoc x mm | Some y => Some y end.
proof: Proof. induction ll as [ | (x',?) ]; simpl; auto. destruct (eq_X_dec x x'); auto. Qed.
imports: List Arith Lia Permutation Undecidability.Shared.Libs.DLW.Utils(list_focus utils_tac)