proposition: Lemma eval_annot_reduce : forall m u cl w an (WF : wf_units_lit u m) (WA : wf_pset m an) (EV : eval_annot_units u m) (HW : has_literal m w) (HL : Forall (has_literal m) cl) (EC : eval_pset m an -> eval_literal_rec w (eval_literal_list cl)), eval_annot eval_clause m (reduce u an w cl).
proof: Proof. induction cl; simpl. - repeat intro ; simpl in *. destruct w; simpl in *. tauto. tauto. - intros. inv HL. destruct_in_goal SL. { apply IHcl; auto. intro. specialize (EC H). replace a with w in *. apply eval_literal_same; auto. symmetry. eapply has_literal_eq;eauto. } destruct (find_lit a u) eqn:FD. + assert (FD':=FD). apply check_annot_find_lit with (hm:=m) in FD'; auto. apply eval_annot_units_find_lit with (m:=m) in FD; auto. unfold Annot.map in FD. destruct (Annot.elt t0). apply eval_annot_TRUE. apply IHcl; auto. apply wf_pset_union;auto. intro U. destruct FD'. destruct WA. apply eval_pset_union in U as (ET &EA); auto. specialize (EC EA). apply eval_literal_rec_swap in EC ; auto. + unfold eval_annot. simpl. auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause