proposition: Lemma dom_incl : forall A B (M N : map A B), M \c N -> dom M \c dom N.
proof: Proof. Proof using. introv. simpl. unfold dom_impl, incl_inst, incl_impl. rew_set. intros HI x Hx. rew_set in *. specializes HI x. destruct (M x) as [v|]; tryfalse. specializes HI v. destruct (N x) as [v'|]; auto_false*. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibOption LibRelation LibLogic LibOperation LibEpsilon LibMonoid LibSet)