proposition: Lemma filter_in_inv f (m:t elt) x : x ∈ filter f m -> x ∈ m.
proof: Proof. induction m as [|h l IHl y d r IHr]; simpl; auto. case (f y d); rewrite ?join_in, ?concat_in; intuition_in. Qed.
imports: Coq(Bool PeanoNat BinInt FunInd Int) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)