{aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit} →
  {P : Sort u} →
    {map : Std.DHashMap Std.Tactic.BVDecide.BVExpr.Cache.Key fun k => Vector Std.Sat.AIG.Fanin k.w} →
      {hbound :
          ∀ {i : ℕ} (k : Std.Tactic.BVDecide.BVExpr.Cache.Key) (h1 : k ∈ map) (h2 : i < k.w),
            (map.get k h1)[i].gate < aig.decls.size} →
        {map' : Std.DHashMap Std.Tactic.BVDecide.BVExpr.Cache.Key fun k => Vector Std.Sat.AIG.Fanin k.w} →
          {hbound' :
              ∀ {i : ℕ} (k : Std.Tactic.BVDecide.BVExpr.Cache.Key) (h1 : k ∈ map') (h2 : i < k.w),
                (map'.get k h1)[i].gate < aig.decls.size} →
            { map := map, hbound := hbound } = { map := map', hbound := hbound' } → (map = map' → P) → P