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