proposition: Lemma notin_singles : forall x xs vs, ¬ List.In x xs -> x ∉ (xs ∷ vs).
proof: Proof. intros x xs vs Hnotin Hin. elim Hnotin. unfold belongs in Hin. assert (forall x l l', List.In x l -> List.incl l l' -> List.In x l') as Hincl by auto. apply Hincl with (dom (xs ∷ vs)); auto. apply dom_singles_incl. Qed.
imports: Utf8 Equalities