How can I write an Existential version of a Universally quantified function?

I've got a Dependent Type problem I'm trying to solve, and I've shrunk it down to the following caricature, of removing an index from a sized vector:

TL;DR Given rmIx, how can I write someRmIx?

rmIx     :: forall ix n a. Vector (n+1) a -> Vector n a
someRmIx :: forall ix   a. SomeVector   a -> SomeVector a

In the someRmIx version, I need to get a witness of the constraints in the rmIx function, and, if I can't meet those constraints (eg you can't remove from Vector 0 a), then return the SomeVector unchanged.

module SomeVector where

import qualified Data.Vector.Sized as V
import Data.Vector.Sized
import GHC.TypeNats
import Data.Proxy
import Type.Reflection
import Data.Type.Equality
import Unsafe.Coerce (unsafeCoerce)
import Data.Data (eqT)

data SomeVector a = forall n. KnownNat n => SomeVector (Vector n a)

-- | Remove an index from an existentially sized 'Vector'.
someRmIx :: forall (ix :: Nat) a m. KnownNat ix => SomeVector a -> SomeVector a
someRmIx (SomeVector (v :: Vector n a)) =

  --------------------------------------------------
  --------------------------------------------------
  --------------------------------------------------
  -- WHAT DO I DO HERE???
  --------------------------------------------------
  --------------------------------------------------
  --------------------------------------------------
  case  ???????  of
    Nothing -> SomeVector v
    Just Refl -> SomeVector $ rmIx @ix v


-- | Remove an index of a 'Vector'.
rmIx :: forall (ix :: Nat) n a (m :: Nat).
  (ix <= n,  -- in my actual code I clean this up with GHC.TypeLits.Normalise
  KnownNat ix,
  (ix + m) ~ n,
  ((n - ix) + 1) ~ (1 + m),
  (n + 1) ~ (ix + (1 + m))
  )
  => Vector (n+1) a -> Vector n a
rmIx v = l  V.++ r
  where (l :: Vector ix a, r' :: Vector (n-ix+1) a) = V.splitAt' (Proxy @ix) v
        (r :: Vector m a) = V.drop' (Proxy @1) r'


----------
-- * Tests

myV :: Vector 5 Int
myV = let Just v = V.fromList [1,2,3,4,5]
      in v

test1 :: Vector 4 Int
test1 = rmIx @2 myV

test2 :: SomeVector Int
test2 = someRmIx @2 $ SomeVector myV

The necessary fanfare to compile the above:

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}