proposition: Lemma wf_insert_normalised_clause : forall i cl st (HCL : check_annot has_clause (hconsmap st) cl) (WF : wf_state st), wf_result_state (insert_normalised_clause i cl st).
proof: Proof. unfold insert_normalised_clause. intros. unfold Annot.lift in HCL. destruct (Annot.elt cl) eqn:EQ; simpl ; auto. - destruct HCL ; auto. - apply wf_insert_unit;auto. eapply check_annot_set_UNIT; eauto. - apply wf_add_watched_clause; auto. eapply check_annot_set_CLAUSE; eauto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause