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