proposition: Lemma hconsmap_insert_unit : forall l, hconsmap_eq (insert_unit l).
proof: Proof. repeat intro. destruct st ; simpl ; auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause