proposition: Lemma IntMapForallAdd : forall {A:Type} (P: A -> Prop) m i v (WF: wf_map m), IntMapForall P m -> P v -> IntMapForall P (IntMap.set' i v m).
proof: Proof. unfold IntMapForall. repeat intro. rewrite gsspec in H1;auto. destruct (eqs k i); auto. inv H1. auto. eapply H ; eauto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause