proposition: Lemma hconsmap_insert_fresh_watched_clause : forall a st, hconsmap_progress (insert_fresh_watched_clause a) st.
proof: Proof. unfold insert_fresh_watched_clause. repeat intro. simpl in *. rewrite hconsmap_insert_watched_clause; simpl ; auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause