proposition: Lemma all_notin_map_inv : forall xs E f, xs ⊄ (map f E) -> xs ⊄ E.
proof: Proof. intros xs E f Hnotincl. unfold all_notin in *; intros x Hin. apply Hnotincl in Hin. apply notin_map_inv with f; auto. Qed.
imports: Utf8 Equalities