proposition: Lemma eval_literal_list_neg : forall l, (eval_or l -> False) -> eval_literal_list l -> False.
proof: Proof. induction l ; simpl. - tauto. - destruct a ; simpl; tauto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause