proposition: Lemma belongs_singles_inv : forall x xs vs, length xs = length vs -> x ∈ (xs ∷ vs) -> List.In x xs.
proof: Proof. intros x xs vs Hlen Hin; unfold belongs in *; simpl in *; auto. rewrite dom_singles in Hin; auto. Qed.
imports: Utf8 Equalities