module NotLeqSort where

data Err : Set where
  err : (A : Set) -> Err