proposition: Lemma eval_reduce : forall m u cl w an (EV : eval_units m u) (HW : has_literal m w) (HL : Forall (has_literal m) cl) (EC : eval_literal_rec w (eval_literal_list cl)), Annot.lift eval_clause (reduce u an w cl).
proof: Proof. induction cl; simpl. - destruct w ; simpl; tauto. - intros. inv HL. destruct_in_goal SL. + apply IHcl; auto. replace a with w in *. apply eval_literal_same; auto. symmetry. eapply has_literal_eq; eauto. + destruct (find_lit a u) eqn:FD. * apply eval_units_find_lit with (m:=m) in FD; auto. destruct (Annot.elt t0). exact I. apply IHcl; auto. apply eval_literal_rec_swap in EC ; auto. * simpl. unfold eval_watched_clause. simpl. auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause