Returning a smaller sized list

Smaller.agda

open import Agda.Builtin.Size
open import Data.Maybe.Base

data List {n} (T : Set n) (i : Size) : Set n where
  [] : List T i
  _∷_ : ∀ {j : Size< i} → T → List T j → List T i

data Smaller {n} (T : Size → Set n) (i : Size) : Set n where
  [_] : {j : Size< i} → T j → Smaller T i

f : ∀ {n} {T : Set n} {i} → List T i → Maybe (Smaller (List T) i)
f [] = nothing
f (x ∷ xs) = just [ xs ]

g : ∀ {n} {T : Set n} {i} → List T i → Maybe (Smaller (List T) i)
g [] = nothing
g (_ ∷ []) = nothing
g (_ ∷ (_ ∷ xs)) = just [ xs ]