proposition: Lemma hconsmap_augment_clauses : forall prf st, hconsmap_progress (augment_clauses prf) st.
proof: Proof. intros. unfold augment_clauses. apply hconsmap_fold_update. intros. apply hconsmap_augment_with_clause. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause