proposition: Lemma list_exists_is_complete_false : forall (A : Type) (f : A -> bool) (l : list A), list_exists f l = false -> forall a, In a l -> f a = false.
proof: Proof. intros A f l; induction l as [ | a l]; simpl. intros; contradiction. intros H b [a_eq_b | b_in_l]. subst b; destruct (f a); [simpl in H; discriminate | reflexivity]. destruct (f a); [simpl in H; discriminate | apply IHl; trivial]. Qed.
imports: Coq(Bool List Arith Setoid Relations FunInd) CoLoR(closure)