From ca0c7d5e75a631d0e6689ee21d017404046f3f12 Mon Sep 17 00:00:00 2001
From: Hannes Schulze <haschu0103@outlook.de>
Date: Thu, 30 Oct 2025 11:29:19 +0100
Subject: implement lambda preterms

---
 Nominal/Helpers/CountableString.lean | 12 ++++++++++++
 1 file changed, 12 insertions(+)
 create mode 100644 Nominal/Helpers/CountableString.lean

(limited to 'Nominal/Helpers/CountableString.lean')

diff --git a/Nominal/Helpers/CountableString.lean b/Nominal/Helpers/CountableString.lean
new file mode 100644
index 0000000..7d2fcb7
--- /dev/null
+++ b/Nominal/Helpers/CountableString.lean
@@ -0,0 +1,12 @@
+import Mathlib
+
+instance : Countable Char where
+  exists_injective_nat' := by
+    exists Char.toNat
+    intro c₁ c₂ hc
+    rw [Char.toNat, Char.toNat, UInt32.toNat_inj] at hc
+    exact Char.eq_of_val_eq hc
+
+instance : Countable String := Countable.of_equiv (List Char)
+  { toFun := String.mk
+    invFun := String.data }
-- 
cgit v1.3.1