proposition: Lemma wf_map_empty : forall {A: Type}, wf_map (IntMap.empty A).
proof: Proof. unfold wf_map. intros. constructor. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause