proposition: Lemma filter_spec0 f m : bindings (filter f m) = List.filter (fun '(k,e) => f k e) (bindings m).
proof: Proof. unfold filter. now rewrite treeify_bindings, filter_aux_bindings, app_nil_r. Qed.
imports: Coq(Bool BinPos Pnat Setoid SetoidList PeanoNat) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)