proposition: Lemma grspec : forall {A:Type} i j (m: IntMap.ptrie A) (WF: wf_map m), IntMap.get' i (IntMap.remove' j m) = if eqs i j then None else IntMap.get' i m.
proof: Proof. intros. destruct (eqs i j). - subst. eapply IntMap.grs'; eauto. - eapply IntMap.gro'; eauto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause