From 2147acd780ca4586a4fd7b045eb92611cdbb13a0 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Thu, 7 Jul 2022 17:53:24 +0100
Subject: Prove alpha equivalence preserves free variables.

---
 src/Data/Util.agda | 13 +++++++++++++
 1 file changed, 13 insertions(+)
 create mode 100644 src/Data/Util.agda

(limited to 'src/Data/Util.agda')

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
-- 
cgit v1.2.3