∀ {R : Type u_1} [inst : Monoid R] [inst_1 : StarMul R] (x : Rˣ),
  star ↑{ val := star ↑x, inv := star ↑x⁻¹, val_inv := ⋯, inv_val := ⋯ }⁻¹ *
      star ↑{ val := star ↑x, inv := star ↑x⁻¹, val_inv := ⋯, inv_val := ⋯ } =
    1