[Agda] Termination checking (perhaps could be smarter)

[flicky frans]

> And what may be here a proof for that  []  is sorted?

You can write

    sort : ∀ ns -> OList (minimum ns)

and no proving is needed. Or you can define `OList' as

    data OList : ℕ -> List ℕ -> Set where
      o[] : ∀ {n} -> OList n []
      _o∷_  : ∀ {n' n ns} -> n' ≤ n -> OList n ns -> OList n' (n' ∷ ns)

I've just tried this encoding [1], but my attempt looks awkward. Maybe
it's better to just extend `ℕ' with `ω':

    data ℕω : Set where
      ω : ℕω
      liftω : ℕ -> ℕω

    postulate
      _≤ω_ : ℕ -> ℕω -> Set

    data OList : ℕω -> List ℕ -> Set where
      o[]  : OList ω []
      _o∷_ : ∀ {n' n ns} -> n' ≤ω n -> OList n ns -> OList (liftω n') (n' ∷ ns)

[1] http://lpaste.net/118588