proposition: Lemma IntMapForallRemove : forall {A:Type} (P: A -> Prop) m x (WF: wf_map m), IntMapForall P m -> IntMapForall P (IntMap.remove' x m).
proof: Proof. intros. repeat intro. rewrite grspec in H0; auto. destruct (eqs k x); try discriminate. eapply H ;eauto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause