proposition: Lemma hconsmap_update_watched_clause : forall d i cl st, hconsmap_progress_r (update_watched_clause d i cl) st.
proof: Proof. intros. unfold update_watched_clause. apply hconsmap_map_dresult. apply hconsmap_comp;auto. apply hconsmap_remove_watched_clause;auto. apply hconsmap_insert_watched_clause;auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause