proposition: Lemma eval_annot_insert_fresh_watched_clause : forall cl st (WF : wf_state st) (ES : eval_annot_state st) (EC : eval_watched_clause cl) (HS : has_watched_clause (hconsmap st) cl) , eval_annot_result_state (insert_fresh_watched_clause cl st).
proof: Proof. unfold insert_fresh_watched_clause. intros. destruct (get_fresh_clause_id st) eqn:EQ. change s with (snd (i,s)). rewrite <- EQ. unfold insert_watched_clause. - apply eval_annot_insert_normalised_clause; auto. destruct WF,ES. apply check_annot_normalise_watched_clause;simpl;auto. apply wf_pset_empty. apply wf_get_fresh_clause_id;auto. apply eval_annot_get_fresh_clause; auto. destruct WF,ES. eapply eval_annot_normalise_watched_clause; eauto. apply wf_pset_empty. simpl. auto. simpl. auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause