proposition: Lemma dom_singles_incl : forall xs vs, List.incl (dom (xs ∷ vs)) xs.
proof: Proof. induction xs; induction vs; intros; simpl; auto. apply incl_refl. unfold List.incl; intros x Hin; inversion Hin. apply List.incl_cons. simpl; auto. apply List.incl_tl. auto. Qed.
imports: Utf8 Equalities