{R : Type u_2} →
  {M : Type u_3} →
    {inst : Semiring R} →
      {inst_1 : AddCommMonoid M} →
        {inst_2 : TopologicalSpace M} →
          {inst_3 : Module R M} →
            {P : Sort u} →
              {toSubmodule : Submodule R M} →
                {isClosed' : IsClosed toSubmodule.carrier} →
                  {toSubmodule' : Submodule R M} →
                    {isClosed'' : IsClosed toSubmodule'.carrier} →
                      { toSubmodule := toSubmodule, isClosed' := isClosed' } =
                          { toSubmodule := toSubmodule', isClosed' := isClosed'' } →
                        (toSubmodule ≍ toSubmodule' → P) → P