proposition: Lemma eval_literal_list_plus_and : forall l hf, elt hf = LOP LAND l -> eval_literal_list (xrev_map NEG (POS hf :: nil) l).
proof: Proof. intros. rewrite xmap_rev. rewrite eval_literal_list_NEG_app. simpl. rewrite H. simpl. rewrite eval_and_list_rev. rewrite eval_and_list_eq. unfold eval_hformula. tauto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause