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