proposition: Lemma filter_aux_bindings f m acc : filter_aux f m acc = List.filter (fun '(k,e) => f k e) (bindings m) ++ acc.
proof: Proof. revert acc. induction m as [|c l IHl x v r IHr]; trivial. intros acc. rewrite <- (List.app_nil_r (bindings _)). rewrite bindings_node, !filter_app. simpl. rewrite List.app_nil_r. destruct (f x v); now rewrite IHl, IHr, <- app_assoc. Qed.
imports: Coq(Bool BinPos Pnat Setoid SetoidList PeanoNat) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)