∀ {α : Type u_1} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} {c : ℕ}
  (motive : m.Equiv (Std.HashSet.emptyWithCapacity c) → Prop) (x_2 : m.Equiv (Std.HashSet.emptyWithCapacity c)),
  (∀ (h : m.inner.Equiv (Std.HashSet.emptyWithCapacity c).inner), motive ⋯) → motive x_2