proposition: Lemma eval_annot_insert_normalised_clause : forall i cl st (HCL : Annot.lift (has_clause (hconsmap st)) cl) (WF : wf_state st) (ES : eval_annot_state st) (EC : eval_annot eval_clause (hconsmap st) cl), eval_annot_result_state (insert_normalised_clause i cl st).
proof: Proof. unfold insert_normalised_clause. intros. unfold eval_annot in EC. destruct (Annot.elt cl) ; simpl ; auto. - intros; apply eval_annot_insert_unit;auto. - intros. apply eval_annot_add_watched_clause; auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause