proposition: Lemma indom_map_inv : forall A B C (IB:Inhab B) (f:A->B->C) M x, x \indom (map_ f M) -> x \indom M.
proof: Proof. Proof using. introv IB H. rewrite* indom_map_eq in H. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibOption LibRelation LibLogic LibOperation LibEpsilon LibMonoid LibSet)