proposition: Lemma filter_spec f m `(!Ok m) : bindings (filter f m) = List.filter (fun '(k,e) => f k e) (bindings m).
proof: Proof. induction m; simpl; auto; invok. rewrite bindings_node, !filter_app. simpl. destruct f. - rewrite join_bindings, create_bindings. f_equal; auto. f_equal; auto. apply create_ok; autok; intros y Hy; apply filter_in_inv in Hy; eauto. - rewrite concat_bindings; autok. f_equal; auto. intros y Hy z Hz. apply filter_in_inv in Hy; apply filter_in_inv in Hz. transitivity t1; eauto. Qed.
imports: Coq(Bool PeanoNat BinInt FunInd Int) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)