{-# OPTIONS --without-K --safe #-}

module Data.Util where

open import Data.List using (List)
open import Data.List.Membership.Propositional using (_∉_)
open import Data.Nat using (ℕ)

record IsFresh (mkFresh : List ℕ → ℕ) : Set where
  field
    distinct : ∀ αs → mkFresh αs ∉ αs

open IsFresh public