proposition: Lemma filter_weak_spec : forall s x f, InT x (filter f s) -> InT x s.
proof: Proof. induction s as [ |h l Hl x0 r Hr]; intros x f; simpl. - trivial. - destruct (f x0). * rewrite join_spec; intuition_in; eauto. * rewrite concat_spec; intuition_in; eauto. Qed.
imports: FunInd MSetInterface MSetGenTree BinInt Int