proposition: Lemma hconsmap_augment_with_clause : forall cl st, hconsmap_progress (augment_with_clause cl) st.
proof: Proof. intros. unfold augment_with_clause. unfold hconsmap_progress. intro. specialize (hconsmap_get_fresh_clause_id st). destruct (get_fresh_clause_id st). intros. simpl in *. rewrite <- H0. apply 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