proposition: Lemma hconsmap_shorten_clauses : forall d l st, hconsmap_progress (shorten_clauses d l) st.
proof: Proof. unfold shorten_clauses. intros. apply hconsmap_fold. - intros. apply hconsmap_update_watched_clause. - destruct st0 ; simpl in *; try tauto. intros. apply not_fail_insert_watched_clause. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause