proposition: Lemma wf_map_add : forall {A: Type} x v (cls : IntMap.ptrie A) (WF : wf_map cls), wf_map (IntMap.set' x v cls).
proof: Proof. intros. eapply IntMap.wf_set'; eauto. constructor. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause