Доказательство теорем о функциях со случаями

Допустим, у нас есть функция merge, которая просто объединяет два списка:

Order : Type -> Type
Order a = a -> a -> Bool

merge : (f : Order a) -> (xs : List a) -> (ys : List a) -> List a
merge f xs [] = xs
merge f [] ys = ys
merge f (x :: xs) (y :: ys) = case x `f` y of
                                   True  => x :: merge f xs (y :: ys)
                                   False => y :: merge f (x :: xs) ys

и мы хотели бы доказать что-то умное в этом отношении, например, что объединение двух непустых списков дает непустой список:

mergePreservesNonEmpty : (f : Order a) ->
                         (xs : List a) -> (ys : List a) ->
                         {auto xsok : NonEmpty xs} -> {auto ysok : NonEmpty ys} ->
                         NonEmpty (merge f xs ys)
mergePreservesNonEmpty f (x :: xs) (y :: ys) = ?wut

Проверка типа отверстия wut дает нам

wut : NonEmpty (case f x y of   True => x :: merge f xs (y :: ys) False => y :: merge f (x :: xs) ys)

Пока имеет смысл! Итак, давайте продолжим и разделим регистр, как предлагает этот тип:

mergePreservesNonEmpty f (x :: xs) (y :: ys) = case x `f` y of
                                                    True => ?wut_1
                                                    False => ?wut_2

Кажется разумным надеяться, что типы wut_1 и wut_2 будут соответствовать соответствующим ветвям выражения case merge (так что wut_1 будет чем-то вроде NonEmpty (x :: merge f xs (y :: ys)), что может быть мгновенно удовлетворено), но наши надежды не оправдались: типы такие же, как и для оригинальный wut.

Действительно, кажется, единственный способ - использовать предложение with:

mergePreservesNonEmpty f (x :: xs) (y :: ys) with (x `f` y)
  mergePreservesNonEmpty f (x :: xs) (y :: ys) | True = ?wut_1
  mergePreservesNonEmpty f (x :: xs) (y :: ys) | False = ?wut_2

В этом случае типы будут такими, как ожидалось, но это приводит к повторению аргументов функции для каждой ветви with (и все становится хуже, когда with становится вложенным), плюс with, похоже, не очень хорошо работает с неявными аргументами (но это, вероятно, того стоит вопрос сам по себе).

Итак, почему здесь не помогает case, есть ли какие-либо причины, помимо чисто практических, которые не соответствуют его поведению с поведением with, и есть ли другие способы написать это доказательство?