Agda wrote nub for me (with some prodding)

Nub.agda

module Untitled where

open import Data.Nat
open import Data.Nat.Properties
open import Data.Char hiding (_≟_)
open import Data.Bool hiding (_≟_)
open import Data.List
open import Data.Unit hiding (_≟_)
open import Data.Empty
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality

module FRESHLIST (X : Set) (Xeq? : (x x₁ : X) → Dec (x ≡ x₁)) where
  mutual
    data FreshList : Set where
      [] : FreshList
      _,_ : (x : X)(xs : FreshList) {ok : x ∉ xs} → FreshList

    -- The distinctness (freshness) guarantee says that.
    _∉_ : X → FreshList → Set
    x ∉ [] = ⊤ -- There's nothing to do with an x and the empty list.
    x ∉ (x₁ , xs) with Xeq? x x₁ -- Otherwise destruct a decidable eq on head.
    x ∉ (x₁ , xs) | yes _ = ⊥ -- We have a match!  It isn't fresh.
    x ∉ (x₁ , xs) | no _ = x ∉ xs -- Otherwise try again.


open module UniqueList = FRESHLIST ℕ Data.Nat._≟_

fresh : (x : ℕ) → (xs : FreshList) → Dec (x ∉ xs)
fresh n FRESHLIST.[] = yes tt
fresh n (x FRESHLIST., xs) with (n ≟ x)
fresh n (x FRESHLIST., xs) | yes p = no (λ z → z)
fresh n (x FRESHLIST., xs) | no ¬p = fresh n xs

unique : List ℕ → FreshList
unique [] = []
unique (x ∷ xs) with fresh x (unique xs)
unique (x ∷ xs) | yes p = _,_ x (unique xs) {p}
unique (x ∷ xs) | no ¬p = (unique xs)