proposition: Lemma all_notin_single_inv : forall xs y v, xs ⊄ (y ∶ v) -> ¬ List.In y xs.
proof: Proof. unfold all_notin. intros xs y v Hnotincl. intro Hin. apply Hnotincl in Hin. apply Hin. apply belongs_single; auto. Qed.
imports: Utf8 Equalities