From 91fbc4cdcad15d37d4733e6c2e2ef6607fe9f0cc Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Sat, 29 Mar 2025 15:43:49 -0700
Subject: [PATCH] chore: Remove redundant code

---
 Test/Integration.lean | 2 --
 1 file changed, 2 deletions(-)

diff --git a/Test/Integration.lean b/Test/Integration.lean
index 9c3bc5e..ffb20f3 100644
--- a/Test/Integration.lean
+++ b/Test/Integration.lean
@@ -207,8 +207,6 @@ def test_env_add_inspect : Test :=
       Protocol.EnvInspectResult),
   ]
 
-def f.{u} : (α : Type u) → α → (α × α) := λ (α : Type u) (x : α) => (x, x)
-
 example : ∀ (p: Prop), p → p := by
   intro p h
   exact h