proposition: Lemma filter_spec : forall s x f, Proper (X.eq==>Logic.eq) f -> (InT x (filter f s) <-> InT x s /\ f x = true).
proof: Proof. induction s as [ |h l Hl x0 r Hr]; intros x f Hf; simpl. - intuition_in. - case_eq (f x0); intros Hx0. * rewrite join_spec, Hl, Hr; intuition_in. now setoid_replace x with x0. * rewrite concat_spec, Hl, Hr; intuition_in. assert (f x = f x0) by auto. congruence. Qed.
imports: FunInd MSetInterface MSetGenTree BinInt Int