{α : Type u} →
  {P : Sort u_1} →
    {toNonUnitalNonAssocSemiring : NonUnitalNonAssocSemiring α} →
      {toOne : One α} →
        {one_mul : ∀ (a : α), 1 * a = a} →
          {mul_one : ∀ (a : α), a * 1 = a} →
            {toNatCast : NatCast α} →
              {natCast_zero : autoParam (↑0 = 0) AddMonoidWithOne.natCast_zero._autoParam} →
                {natCast_succ : autoParam (∀ (n : ℕ), ↑(n + 1) = ↑n + 1) AddMonoidWithOne.natCast_succ._autoParam} →
                  {toNonUnitalNonAssocSemiring' : NonUnitalNonAssocSemiring α} →
                    {toOne' : One α} →
                      {one_mul' : ∀ (a : α), 1 * a = a} →
                        {mul_one' : ∀ (a : α), a * 1 = a} →
                          {toNatCast' : NatCast α} →
                            {natCast_zero' : autoParam (↑0 = 0) AddMonoidWithOne.natCast_zero._autoParam} →
                              {natCast_succ' :
                                  autoParam (∀ (n : ℕ), ↑(n + 1) = ↑n + 1) AddMonoidWithOne.natCast_succ._autoParam} →
                                { toNonUnitalNonAssocSemiring := toNonUnitalNonAssocSemiring, toOne := toOne,
                                      one_mul := one_mul, mul_one := mul_one, toNatCast := toNatCast,
                                      natCast_zero := natCast_zero, natCast_succ := natCast_succ } =
                                    { toNonUnitalNonAssocSemiring := toNonUnitalNonAssocSemiring', toOne := toOne',
                                      one_mul := one_mul', mul_one := mul_one', toNatCast := toNatCast',
                                      natCast_zero := natCast_zero', natCast_succ := natCast_succ' } →
                                  (toNonUnitalNonAssocSemiring ≍ toNonUnitalNonAssocSemiring' →
                                      toOne ≍ toOne' → toNatCast ≍ toNatCast' → P) →
                                    P