proposition: Lemma wf_units_def_empty : forall {A: Type} m, wf_units_def (IntMap.empty A) m.
proof: Proof. unfold wf_units_def. intros. rewrite empty_o in H. congruence. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause