proposition: Lemma exists_spec s f : Proper (X.eq==>eq) f -> (exists_ f s = true <-> Exists (fun x => f x = true) s).
proof: Proof. intros Hf; unfold Exists. induction s as [|i l IHl x r IHr]; simpl; auto. - split. * discriminate. * intros (y,(H,_)); inv. - rewrite <- !orb_lazy_alt, !orb_true_iff, IHl, IHr. clear IHl IHr. split; [intros [[H|(y,(H,H'))]|(y,(H,H'))]|intros (y,(H,H'))]. * exists x; auto. * exists y; auto. * exists y; auto. * inv; [left;left|left;right|right]; try (exists y); eauto. Qed.
imports: Orders OrdersFacts MSetInterface PeanoNat