proposition: Theorem gsspec: forall (A: Type) (i j: int) (x: A) (m: IntMap.ptrie A) (WF : wf_map m), IntMap.get' i (IntMap.set' j x m) = if eqs i j then Some x else IntMap.get' i m.
proof: Proof. intros; destruct (eqs i j). - subst i; eapply IntMap.gss'; eauto. - eapply IntMap.gso'; eauto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause