From a8915795c109980285e11ed53d453987c0917069 Mon Sep 17 00:00:00 2001 From: Hannes Schulze Date: Tue, 2 Dec 2025 11:52:15 +0100 Subject: minor cleanup --- Nominal/Helpers/CountableString.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'Nominal/Helpers/CountableString.lean') diff --git a/Nominal/Helpers/CountableString.lean b/Nominal/Helpers/CountableString.lean index 7d94516..b6f59f8 100644 --- a/Nominal/Helpers/CountableString.lean +++ b/Nominal/Helpers/CountableString.lean @@ -2,7 +2,7 @@ import Mathlib instance : Countable Char where exists_injective_nat' := by - exists Char.toNat + use Char.toNat intro c₁ c₂ hc rw [Char.toNat, Char.toNat, UInt32.toNat_inj] at hc exact Char.eq_of_val_eq hc -- cgit v1.3.1