proposition: Lemma LocSet_fold_orb: forall f s, LocSet.fold (fun e b => (f e) || b) s false = true <-> exists e, LocSet.In e s /\ f e = true.
proof: Proof. intros. rewrite LocSet.fold_1. rewrite <- fold_left_rev_right. rewrite fold_right_orb. split; intros. destruct H as (e, H). rewrite <- in_rev in H. exists e. destruct H. split. apply LocSet.elements_2. unfold LocSet.E.eq. clear H0. induction (LocSet.elements s). inversion H. simpl in H. destruct H. apply InA_cons_hd. auto. apply InA_cons_tl. apply IHl; trivial. trivial. destruct H as (e, H). exists e. split. destruct H. rewrite <- in_rev. apply LocSet.elements_1 in H. unfold LocSet.E.eq in H. induction H. left; auto. right. trivial. tauto. Qed.
imports: Coq(List) JML(Stack) Coq(ListSet) Coq(Bool) Coq(ZArith) Coq(Relation_Operators) JML(ListHelpers) Coq(Classical) Coq(DecidableType) Coq(FSetInterface) Coq(FSetProperties) Coq(FSetEqProperties) Coq(FSetFacts) Coq(Sumbool) Coq(Lia)