proposition: Lemma fold_right_orb: forall (A : Type) (l : list A) f, fold_right (fun elem b => (f elem) || b) false l = true <-> (exists elem, In elem l /\ f elem = true).
proof: Proof. split;intros. induction l. simpl in H. discriminate H. simpl in H. apply orb_prop in H. destruct H. exists a. auto with *. apply IHl in H. destruct H. exists x. intuition auto with datatypes. destruct H as (elem, H). destruct H. induction l. inversion H. simpl. apply orb_true_intro. destruct H. left. rewrite H. trivial. right. apply IHl. trivial. 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)