Proving that list has exactly two sorted elements

I've been trying to use So type to implement SortedTwoElems proof type and function isSortedTwoElems. I'm not sure how to go about implementing proveUnsortedTwoElems case.

Here's the full example:

import Data.So

data SortedTwoElems : List e -> Type where
  MkSortedTwoElems : Ord e => {x : e} -> {y : e} -> (prf : So (x <= y))-> SortedTwoElems [x, y]

proveUnsortedTwoElems : Ord e => {x : e} -> {y : e} -> So (not (x <= y)) -> SortedTwoElems [x, y] -> Void
proveUnsortedTwoElems = ?how_to_implement_this

isSortedTwoElems : Ord e => {x : e} -> {y : e} -> (xs : List e) -> Dec (SortedTwoElems xs)
isSortedTwoElems []                      = No (\(MkSortedTwoElems _)  impossible)
isSortedTwoElems (x :: [])               = No (\(MkSortedTwoElems _)  impossible)
isSortedTwoElems (x :: (y :: (z :: xs))) = No (\(MkSortedTwoElems _)  impossible)
isSortedTwoElems (x :: (y :: [])) =
  case choose (x <= y) of
    (Left prf) => Yes (MkSortedTwoElems prf)
    (Right prfNot) => No (proveUnsortedTwoElems prfNot)

When doing it with:

proveUnsortedTwoElems (MkSortedTwoElems _) impossible

type checker complains with:

proveUnsortedTwoElems (MkSortedTwoElems _) is a valid case

Solution

I started with an intermediate lemma which should allow to conclude whenever you find two contradictory Sos:

soNotTrue : So b -> So (not b) -> Void
soNotTrue {b = True}  prf prf' = absurd prf'
soNotTrue {b = False} prf prf' = absurd prf

You can then try to write:

unsortedTwoElems : Ord e => So (not (x <= y)) -> SortedTwoElems [x, y] -> Void
unsortedTwoElems prf (MkSortedTwoElems prf') = soNotTrue prf' prf

And here the error message should clue you in: the Ord e constraint used in So (not (x <= y)) is the one bound in unsortedTwoElems whilst the one used inside of MkSortedTwoElems is bounded by it.

There is no guarantee that these two Ords are compatible.

My suggested solution: redefine SortedTwoElems so that it is explicit about the Ord it is using.

import Data.So

data SortedTwoElems : Ord e -> List e -> Type where
  MkSortedTwoElems : {o : Ord e} -> So (x <= y) -> SortedTwoElems o [x, y]

soNotTrue : So b -> So (not b) -> Void
soNotTrue {b = True}  prf prf' = absurd prf'
soNotTrue {b = False} prf prf' = absurd prf

unsortedTwoElems : (o : Ord e) => So (not (x <= y)) -> SortedTwoElems o [x, y] -> Void
unsortedTwoElems prf (MkSortedTwoElems prf') = soNotTrue prf' prf