{R : Type u} →
  {S : Type v} →
    {ι : Type w} →
      {inst : CommRing R} →
        {inst_1 : CommRing S} →
          {inst_2 : Algebra R S} →
            {P : Sort u_1} →
              {val : ι → S} →
                {σ' : S → MvPolynomial ι R} →
                  {aeval_val_σ' : ∀ (s : S), (MvPolynomial.aeval val) (σ' s) = s} →
                    {algebra : Algebra (MvPolynomial ι R) S} →
                      {algebraMap_eq :
                          autoParam (algebraMap (MvPolynomial ι R) S = ↑(MvPolynomial.aeval val))
                            Algebra.Generators.algebraMap_eq._autoParam} →
                        {val' : ι → S} →
                          {σ'' : S → MvPolynomial ι R} →
                            {aeval_val_σ'' : ∀ (s : S), (MvPolynomial.aeval val') (σ'' s) = s} →
                              {algebra' : Algebra (MvPolynomial ι R) S} →
                                {algebraMap_eq' :
                                    autoParam (algebraMap (MvPolynomial ι R) S = ↑(MvPolynomial.aeval val'))
                                      Algebra.Generators.algebraMap_eq._autoParam} →
                                  { val := val, σ' := σ', aeval_val_σ' := aeval_val_σ', algebra := algebra,
                                        algebraMap_eq := algebraMap_eq } =
                                      { val := val', σ' := σ'', aeval_val_σ' := aeval_val_σ'', algebra := algebra',
                                        algebraMap_eq := algebraMap_eq' } →
                                    (val ≍ val' → σ' ≍ σ'' → algebra ≍ algebra' → P) → P