proposition: Lemma remove_remain (x y: X) A: x ∈ A -> x <> y -> x ∈ remove eq_dec y A.
proof: Proof. induction A; cbn; intuition idtac; subst. - destruct (y == x); subst; intuition (auto with datatypes). - destruct (y == a); subst; intuition (auto with datatypes). Qed.
imports: List Arith Lia Undecidability.HOU(std.tactics std.lists.basics std.decidable)