proposition: Lemma list_exists_option_is_complete_false : forall (A : Type) f l, (forall a, In a l -> f a = Some false) -> @list_exists_option A f l = Some false.
proof: Proof. intros A f l; induction l as [ | a l]. intros; simpl; trivial. intros H; simpl. rewrite (H _ (or_introl _ (eq_refl _))); apply IHl; intros; apply H; right; trivial. Qed.
imports: Coq(Bool List Arith Setoid Relations FunInd) CoLoR(closure)