@[simp]

theorem Std.HashMap.Imp.empty_buckets {α : Type u_1} {β : Type u_2} : Std.HashMap.Imp.empty.buckets = { val := mkArray 8 Std.AssocList.nil, property := ⋯ }

@[simp]

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

@[simp]

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