proposition: Lemma eval_units_find_lit : forall m h u b (EV : eval_units m u) (HAS : has_literal m h) (FD : find_lit h u = Some b), (if Annot.elt b then eval_literal h else eval_literal (neg_literal h)).
proof: Proof. unfold eval_units ; intros. rewrite has_form_of_literal in HAS. unfold find_lit in FD. destruct h; simpl in *. - apply units_has_literal_of_form with (m:=m) in FD ; auto. apply EV in FD. unfold Annot.lift, Annot.map in FD. simpl in *. destruct (Annot.elt b) ; auto. - apply neg_bool_some in FD. apply units_has_literal_of_form with (m:=m) in FD ; auto. apply EV in FD. unfold Annot.lift, Annot.map in FD. simpl in *. destruct (Annot.elt b) ; auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause