{R : Type u_1} →
  {inst : CommRing R} →
    {I : Ideal R} →
      {M : Type u_3} →
        {inst_1 : AddCommGroup M} →
          {inst_2 : Module R M} →
            {P : Sort u} →
              {N : ℕ → Submodule R M} →
                {mono : ∀ (i : ℕ), N (i + 1) ≤ N i} →
                  {smul_le : ∀ (i : ℕ), I • N i ≤ N (i + 1)} →
                    {N' : ℕ → Submodule R M} →
                      {mono' : ∀ (i : ℕ), N' (i + 1) ≤ N' i} →
                        {smul_le' : ∀ (i : ℕ), I • N' i ≤ N' (i + 1)} →
                          { N := N, mono := mono, smul_le := smul_le } =
                              { N := N', mono := mono', smul_le := smul_le' } →
                            (N ≍ N' → P) → P