{P : Sort u} →
  {R : Type u_1} →
    {inst : CommRing R} →
      {I : Ideal R} →
        {M : Type u_3} →
          {inst_1 : AddCommGroup M} →
            {inst_2 : Module R M} →
              {t : I.Filtration M} →
                {R' : Type u_1} →
                  {inst' : CommRing R'} →
                    {I' : Ideal R'} →
                      {M' : Type u_3} →
                        {inst'_1 : AddCommGroup M'} →
                          {inst'_2 : Module R' M'} →
                            {t' : I'.Filtration M'} →
                              R = R' →
                                inst ≍ inst' →
                                  I ≍ I' →
                                    M = M' →
                                      inst_1 ≍ inst'_1 →
                                        inst_2 ≍ inst'_2 → t ≍ t' → Ideal.Filtration.noConfusionType P t t'