proposition: Lemma wf_insert_fresh_watched_clause : forall cl st (ES : wf_state st) (HS : has_watched_clause (hconsmap st) cl), wf_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 wf_insert_normalised_clause;auto. { destruct ES. apply check_annot_normalise_watched_clause;auto. simpl. auto. apply wf_pset_empty. } apply wf_get_fresh_clause_id;auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause