proposition: Lemma list_forall_option_is_complete_false : forall (A : Type) f l, (exists a, In a l /\ f a = Some false) -> (forall a, In a l -> f a = None -> False) -> @list_forall_option A f l = Some false.
proof: Proof. intros A f l; induction l as [ | a l]. intros [a [a_in_nil _]] _; contradiction. intros [b [[b_eq_a | b_in_l] fb_eq_false]] H; simpl. subst b; rewrite fb_eq_false. generalize (list_forall_option_is_sound f l); destruct (list_forall_option f l) as [ [ | ] | ]; trivial. intros [c [c_in_l fc_eq_none]]. assert (H' := H c (or_intror _ c_in_l) fc_eq_none); contradiction. generalize (H a (or_introl _ (eq_refl _))); destruct (f a) as [ [ | ] | ]. intros _; apply IHl. exists b; split; trivial. intros c c_in_l; apply H; right; trivial. intros; generalize (list_forall_option_is_sound f l); destruct (list_forall_option f l) as [ [ | ] | ]; trivial. intros [c [c_in_l fc_eq_none]]. assert (H' := H c (or_intror _ c_in_l) fc_eq_none); contradiction. intro H'; generalize (H' (eq_refl _)); contradiction. Qed.
imports: Coq(Bool List Arith Setoid Relations FunInd) CoLoR(closure)