∀ {aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit}
  (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),
  sizeOf { map := map, hbound := hbound } = 1 + sizeOf map