proposition: Lemma eval_literal_list_NEG_app : forall l r, eval_literal_list (List.map NEG l ++ r) <-> (eval_and_list' eval_hformula l -> eval_literal_list r).
proof: Proof. induction l; simpl. - tauto. - intros. unfold eval_hformula at 1. rewrite IHl. tauto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause