proposition: Lemma hconsmap_augment_hyp : forall b a st, hconsmap_progress (augment_hyp b a) st.
proof: Proof. unfold augment_hyp. intros. apply hconsmap_comp. apply hconsmap_insert_unit. intros. apply hconsmap_augment_cnf. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause