∀ {R : Type uR} {M : Type uM} {ι : Type uι} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {inst_3 : DecidableEq ι} [inst_4 : DecidableEq ι] (b b_1 : Module.Basis ι R M), b = b_1 → b.toDual = b_1.toDual