proposition: Lemma list_exists_rest_is_sound : forall (A : Type) (P : A -> Prop) l P_dec, list_exists_rest P l P_dec= true <-> (exists a, In a l /\ P a).
proof: Proof. intros A P l; induction l as [ | a l]; intros P_dec; simpl. split; [intros; discriminate | intros [a [Abs _]]; contradiction]. destruct (P_dec a) as [Pa | not_Pa]. split; trivial. intros _; exists a; split; trivial; left; trivial. split. intro H; rewrite IHl in H. destruct H as [b [b_in_l Pb]]; exists b; split; trivial; right; trivial. intro H; destruct H as [b [[b_eq_a | b_in_l] Pb]]. subst b; absurd (P a); trivial. rewrite IHl; exists b; split; trivial. Qed.
imports: Coq(Bool List Arith Setoid Relations FunInd) CoLoR(closure)