proposition: Lemma all_notin_remove_notin : forall xs y E, xs ⊄ E -> xs ⊄ (E ∖ {y}).
proof: Proof. intros xs y E Hnotincl. induction xs as [ | x xs IHxs ]. unfold all_notin. intros x Hin. inversion Hin. apply all_notin_notin in Hnotincl. destruct Hnotincl as [ Hnotin Hnotincl ]. apply IHxs in Hnotincl. apply notin_all_notin. split; auto. apply notin_remove_notin; auto. Qed.
imports: Utf8 Equalities