proposition: Lemma all_notin_single : forall xs y v, ¬ List.In y xs -> xs ⊄ (y ∶ v).
proof: Proof. intros xs y v Hnotin. unfold all_notin. intros x Hin. apply notin_single. intro; subst. contradiction. Qed.
imports: Utf8 Equalities