proposition: Lemma partition_spec (f:key->elt->bool) m : prodmap bindings (partition f m) = List.partition (fun '(k,e) => f k e) (bindings m).
proof: Proof. unfold bindings. rewrite <- partition_spec by apply ok. unfold partition; simpl. now destruct R.partition. Qed.