proposition: Lemma eval_make_clause : forall m u cl an (EV: eval_units m u) (HL: Forall (has_literal m) cl) (EC: eval_literal_list cl), Annot.lift eval_clause (make_clause u an cl).
proof: Proof. unfold has_conflict_clause. induction cl; simpl; auto. intros. destruct (find_lit a u) eqn:FD. - inv HL. apply eval_units_find_lit with (m:=m) in FD; auto. destruct (Annot.elt t0) ; simpl ; auto. + unfold Annot.lift ; simpl ; auto. + destruct a ; simpl in *. apply IHcl ; auto. tauto. apply IHcl ; auto. - inv HL. eapply eval_reduce ; eauto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause