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