proposition: Lemma partition_spec {elt} (f:key->elt->bool) m `{!Ok m} : prodmap (@bindings _) (partition f m) = List.partition (fun '(k,e) => f k e) (bindings m).
proof: Proof. unfold bindings, partition. now destruct List.partition. Qed.
imports: Coq(EqualitiesFacts)