proposition: Lemma hconsmap_insert_defs : forall m l, hconsmap_eq (insert_defs m l).
proof: Proof. unfold insert_defs. unfold hconsmap_eq. simpl. reflexivity. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause