proposition: Lemma ok_singles : forall xs vs, List.NoDup xs -> ok (xs ∷ vs).
proof: Proof. induction xs as [ | x xs IHxs ]; induction vs as [ | v vs IHvs ]; intro Hnodup; simpl in *; auto. apply ok_nil. apply ok_nil. assert (ok ((xs ∷ vs) & (x ∶ v))); auto. apply ok_cons. assert (List.NoDup xs ∧ ¬ List.In x xs) as Hdup by (rewrite <- List.app_nil_l in Hnodup; split; [ apply List.NoDup_remove_1 in Hnodup | apply List.NoDup_remove_2 in Hnodup ]; auto). destruct Hdup as [ Hnodup2 Hnotin ]. apply IHxs with vs in Hnodup2. split; auto. unfold belongs. assert (forall x l l', ¬ List.In x l' -> List.incl l l' -> ¬ List.In x l) as Hincl by auto. apply Hincl with xs; auto. apply dom_singles_incl. Qed.
imports: Utf8 Equalities