proposition: Lemma all_remove_notin : forall xs E, xs ⊄ E -> E ∖ xs = E.
proof: Proof. intros xs E Hnotincl. induction xs as [ | x ]; simpl; auto. apply all_notin_notin in Hnotincl. destruct Hnotincl. rewrite remove_notin; auto. Qed.
imports: Utf8 Equalities