proposition: Lemma ok_singles_inv : forall xs vs, length xs = length vs -> ok (xs ∷ vs) -> List.NoDup xs.
proof: Proof. induction xs as [ | x xs IHxs ]; induction vs as [ | v vs IHvs ]; intros Hlen Hok; auto. apply List.NoDup_nil. apply List.NoDup_nil. inversion Hlen. inversion Hlen as [ Hlen2 ]. inversion Hok as [ | y w F Hok2 ]; subst. destruct Hok2 as [ Hok3 Hnotin ]. apply (IHxs vs) in Hok3; auto. unfold notin, belongs in Hnotin. rewrite dom_singles in Hnotin; auto. apply List.NoDup_cons; auto. Qed.
imports: Utf8 Equalities