proposition: Lemma all_notin_belongs_neq : forall x ys E, x ∈ E -> ys ⊄ E -> ¬ List.In x ys.
proof: Proof. intros x ys E Hin Hnotincl. unfold all_notin in *. intro Hin2. apply Hnotincl in Hin2. contradiction. Qed.
imports: Utf8 Equalities