proposition: Lemma xfilter_spec: forall f s x i, In x (xfilter f s i) <-> In x s /\ f (i@x) = true.
proof: Proof. intro f. unfold In. induction s as [|l IHl o r IHr]; intros x i; simpl xfilter. - rewrite mem_Leaf. intuition discriminate. - rewrite mem_node. destruct x; simpl. + rewrite IHr. reflexivity. + rewrite IHl. reflexivity. + rewrite <- andb_lazy_alt. apply andb_true_iff. Qed.
imports: Bool PeanoNat BinPos Orders OrdersEx MSetInterface