proposition: Lemma wf_insert_watched_clause : forall diff i cl st (WF: wf_state st) (CD : ohold (check_annot has_literal (hconsmap st)) diff) (WFA: check_annot has_watched_clause (hconsmap st) cl), wf_result_state (insert_watched_clause diff i cl st).
proof: Proof. unfold insert_watched_clause. intros. apply wf_insert_normalised_clause; auto. destruct WF. destruct WFA. apply check_annot_normalise_watched_clause; auto. destruct diff;simpl in CD;auto. destruct CD;auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause