proposition: Lemma xexists_spec: forall f s i, xexists f s i = true <-> Exists (fun x => f (i@x) = true) s.
proof: Proof. unfold Exists, In. intro f. induction s as [|l IHl o r IHr]; intros i; simpl. - split; [ discriminate | now intros [ _ [? _]]]. - rewrite <- 2orb_lazy_alt, 2orb_true_iff, <- andb_lazy_alt, andb_true_iff. rewrite IHl, IHr. clear IHl IHr. split. + intros [[Hi|[x Hr]]|[x Hl]]. * exists 1. exact Hi. * exists x~1. exact Hr. * exists x~0. exact Hl. + intros [[x|x|] H]; eauto. Qed.
imports: Bool PeanoNat BinPos OrderedType OrderedTypeEx FSetInterface