{P : Sort u} →
  {R : Type u_2} →
    {inst : CommRing R} →
      {n : ℕ} →
        {t : ChevalleyThm.PolynomialC.InductionObj✝ R n} →
          {R' : Type u_2} →
            {inst' : CommRing R'} →
              {n' : ℕ} →
                {t' : ChevalleyThm.PolynomialC.InductionObj✝¹ R' n'} →
                  R = R' →
                    inst ≍ inst' → n = n' → t ≍ t' → ChevalleyThm.PolynomialC.InductionObj.noConfusionType✝ P t t'