Varify Map.v

I've removed some Admitted in Map.v by assuming Hv : Map.Valid.t where necessary.

• filter_map_ss
• merge_ss
• Make_merge_In1
• Make_merge_In2

To prove them, I've added inductive proposition about Make.pick_opt and proved additional some lemmas.

• pick_opt'
• pick_opt_to_ind
• pick_opt_from_ind
• pick_opt_not_In
• In_add
• In_add_intro