proposition: Lemma notin_all_remove_notin : forall x ys E, x ∉ E -> x ∉ (E ∖ ys).
proof: Proof. induction ys as [ | y ]; simpl; auto. intros. assert (x ∉ E ∖ {y}) by (apply notin_remove_notin; auto). auto. Qed.
imports: Utf8 Equalities