proposition: Lemma notin_singles_inv : forall x xs vs, length xs = length vs -> x ∉ (xs ∷ vs) -> ¬ List.In x xs.
proof: Proof. intros x xs vs Heq Hnotin Hin. elim Hnotin. unfold belongs. rewrite dom_singles; auto. Qed.
imports: Utf8 Equalities