proposition: Lemma list_exists_option_is_complete_none : forall A f l, (exists a, In a l /\ f a = None) -> (forall a, In a l -> f a = Some true -> False) -> @list_exists_option A f l = None.
proof: Proof. intros A f l; induction l as [ | t l]. intros [a [a_in_nil _]]; contradiction. simpl; intros [a [[a_eq_t | a_in_l] fa_eq_none]] H. subst a; rewrite fa_eq_none. generalize (list_exists_option_is_sound f l); destruct (list_exists_option f l) as [ [ | ] | ]; trivial. intros [a [a_in_l fa_eq_true]]; assert False; [idtac | contradiction]. apply (H a); trivial; right; trivial. generalize (H t (or_introl _ (eq_refl _))); destruct (f t) as [ [ | ] | ]. intro H'; assert (H'' := H' (eq_refl _)); contradiction. intros _; apply IHl. exists a; split; trivial. intros b b_in_l; apply H; right; trivial. intros _; generalize (list_exists_option_is_sound f l); destruct (list_exists_option f l) as [ [ | ] | ]. intros [b [b_in_l fb_eq_true]]; assert False; [idtac | contradiction]. apply (H b); trivial; right; trivial. trivial. trivial. Qed.
imports: Coq(Bool List Arith Setoid Relations FunInd) CoLoR(closure)