proposition: Lemma has_form_find_lit : forall m f lit (HL : has_form m f) (EU : eval_units m lit), match IntMap.get' (id f) lit with | None => True | Some b => eval_literal (Annot.lift literal_of_bool b f) end.
proof: Proof. intros. unfold eval_units in EU. unfold forall_units in EU. destruct (IntMap.get' (id f) lit) eqn:EQ; auto. assert (units_has_literal m lit (Annot.mk ((Annot.lift literal_of_bool t0 f)) (Annot.deps t0))). { unfold units_has_literal; intros. unfold Annot.lift,Annot.map. simpl. rewrite id_of_literal_of_bool. rewrite is_positive_literal_of_bool. rewrite EQ. destruct t0 ; simpl ; split ; auto. destruct elt0 ; auto. } apply EU in H. auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause