proposition: Lemma dom_map : forall A B (IB:Inhab B) C (f:A->B->C) M, dom (map_ f M) = dom M.
proof: Proof. Proof using. intros. simpl. unfold dom_impl, map_. rew_set. intros x. rew_set. destruct (M x); iff*. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibOption LibRelation LibLogic LibOperation LibEpsilon LibMonoid LibSet)