@[simp]

theorem Batteries.HashMap.Imp.empty_buckets {α : Type u_1} {β : Type u_2} : Batteries.HashMap.Imp.empty.buckets = ⟨mkArray 8 Batteries.AssocList.nil, ⋯⟩

@[simp]

theorem Batteries.HashMap.Imp.empty_val {α : Type u_1} {β : Type u_2} [BEq α] [Hashable α] : ∅.val = Batteries.HashMap.Imp.empty

@[simp]

theorem Batteries.HashMap.empty_find? {α : Type u_1} {β : Type u_2} [BEq α] [Hashable α] {a : α} : ∅.find? a = none