proposition: Lemma hconsmap_cnf_hyps : forall o l st, hconsmap_progress (cnf_hyps (is_classic o) l) st.
proof: Proof. unfold cnf_hyps. intros. apply hconsmap_fold_update. apply hconsmap_augment_hyp. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause