proposition: Lemma wf_set : forall i t1 t2 cls (WF: wf_map cls) (WF1: wf_map t1) (WF2: wf_map t2) (WFW: wf cls) , wf (IntMap.set' i (t1,t2) cls).
proof: Proof. unfold WMap.wf. split. apply wf_map_add; auto. repeat intro. rewrite gsspec in H; auto. destruct (eqs k i). inv H ; simpl ; auto. apply WFW in H. auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause