Results for fold 1 Results for lemma elements_spec1: : forall (s : t) (x : elt), In x (elements s) <-> In x s FAILURE! Tactics applied: 100000 Original Proof: [intuition.] Proof search time: 0 min, 54 sec Results for lemma for_all_spec: : forall (s : t) (f : elt -> bool), Proper (X.eq==>eq) f -> (for_all f s = true <-> For_all (fun x => f x = true) s) FAILURE! Tactics applied: 100000 Original Proof: [unfold For_all; induction s; simpl; intros. split; intros; auto. inv. destruct (f a) eqn:F. rewrite IHs; auto. firstorder. inv; auto. setoid_replace x with a; auto. split; intros H'. discriminate. rewrite H' in F; auto.] Proof search time: 0 min, 49 sec Results for lemma filter_inf: : forall (s : t) (x : elt) (f : elt -> bool) (Hs : Ok s), Inf x s -> Inf x (filter f s) FAILURE! Tactics applied: 100000 Original Proof: [simple induction s; simpl. intuition. intros x l Hrec a f Hs Ha; inv. case (f x); auto. apply Hrec; auto. apply Inf_lt with x; auto.] Proof search time: 0 min, 47 sec Results for lemma max_elt_spec1: : forall (s : t) (x : elt), max_elt s = Some x -> In x s FAILURE! Tactics applied: 100000 Original Proof: [induction s as [ | x s IH]. inversion 1. destruct s as [ | y s]. simpl. inversion 1; subst; auto. right; apply IH; auto.] Proof search time: 0 min, 46 sec Results for lemma add_spec: : forall (s : t) (x y : elt) (Hs : Ok s), In y (add x s) <-> X.eq y x \/ In y s FAILURE! Tactics applied: 100000 Original Proof: [induction s; simpl; intros. intuition. inv; auto. elim_compare x a; inv; rewrite !InA_cons, ?IHs; intuition. left; order.] Proof search time: 0 min, 42 sec