proposition: Lemma hconsmap_insert_watched_clause : forall diff i cl st, hconsmap_progress (insert_watched_clause diff i cl) st.
proof: Proof. unfold insert_watched_clause; intros. unfold hconsmap_progress. intros. eapply hconsmap_insert_normalised_clause;auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause