proposition: Lemma Forall_Exists_neg_neg : forall {A: Type} (P: A -> Prop) l, ((Exists (fun x => not (P x)) l) -> False) -> ((Forall P l -> False) -> False).
proof: Proof. induction l. - intros. rewrite Forall_rew in H0. tauto. - intros. rewrite Forall_rew in H0. rewrite Exists_rew in H. tauto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause