proposition: Lemma check_annot_normalise_watched_clause : forall diff hm u wc d (WF : wf_units_lit u hm) (HCL : has_watched_clause hm wc) (HL : ohold (Annot.lift_deps (wf_pset hm)) diff) (HA : wf_pset hm d), check_annot has_clause hm (normalise_watched_clause diff u d wc).
proof: Proof. unfold normalise_watched_clause. intros. destruct diff. - apply check_annot_shorten_clause; auto. - eapply check_annot_reduce_lits in HCL;eauto. destruct_in_goal R. + simpl in HCL. destruct HCL. split. simpl. auto. apply has_no_dup_clause;auto. + apply check_annot_TRUE. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause