proposition: Lemma eval_units_get : forall m u f b (EVAL : eval_units m u) (HF : has_form m f) (G : IntMap.get' (id f) u = Some b), eval_literal (literal_of_bool (Annot.elt b) f).
proof: Proof. unfold eval_units. intros. unfold forall_units in EVAL. change (Annot.lift eval_literal (Annot.map (fun b => literal_of_bool b f) b)). apply EVAL. unfold units_has_literal. unfold Annot.lift, Annot.map. simpl. rewrite id_of_literal_of_bool. rewrite is_positive_literal_of_bool. destruct b ; simpl ; split; auto. destruct elt0; auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause