∀ {α : Sort u_1} {ω : Type u_2} {prio : α → Thunk ω} {ε : α → Type} [inst : SizeOf α] [inst_1 : SizeOf ω]
  [inst_2 : (a : α) → SizeOf (ε a)] (key : α) (estimator : ε key),
  sizeOf { key := key, estimator := estimator } = 1 + sizeOf key + sizeOf estimator