proposition: Lemma list_exists_option_is_complete_true : forall (A : Type) f l, (exists a, In a l /\ f a = Some true) -> @list_exists_option A f l = Some true.
proof: Proof. intros A f l; induction l as [ | a l]. simpl; intros [a [a_in_nil fa_eq_true]]; contradiction. intros [b [[b_eq_a | b_in_l] fb_eq_true]]; simpl. subst b; rewrite fb_eq_true; trivial. destruct (f a) as [ [ | ] | ]; trivial. rewrite IHl; trivial; exists b; split; trivial. rewrite IHl; trivial; exists b; split; trivial. Qed.
imports: Coq(Bool List Arith Setoid Relations FunInd) CoLoR(closure)