1 files changed, 13 insertions, 0 deletions
diff --git a/src/Data/Util.agda b/src/Data/Util.agda
new file mode 100644
index 0000000..4d9ec33
--- /dev/null
+++ b/src/Data/Util.agda
@@ -0,0 +1,13 @@
+{-# 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