proposition: Lemma restrict_incl : forall A B (M N : map A B), M \c N -> N \| (dom M) = M.
proof: Proof. Proof using. introv HI. applys fun_ext_1. simpls. intros k. unfolds dom_impl, restrict_impl, read_impl, incl_impl. specializes HI k. rew_set. case_if*. { destruct (M k) as [v|]; tryfalse. applys* HI. } Qed.
imports: TLC(LibTactics LibLogic LibReflect LibOption LibRelation LibLogic LibOperation LibEpsilon LibMonoid LibSet)