test: avoid testing colliding private inductives

Author: Kha

tests/lean/run/prelude-injectivity.lean

@@ -1,12 +1,12 @@
+module
+
 import Lean
 
 open Lean Meta
 
 -- without this, the catch below does not catch kernel errors
 set_option Elab.async false
 
-#exit -- **TODO**: remove after fixing async panic
-
 /--
 info: Possible candidates for Init/Core.lean (these do not need to be added if they are irrelevant for verification):
 gen_injective_theorems% MacroScopesView
@@ -16,7 +16,6 @@ gen_injective_theorems% TSyntax
 gen_injective_theorems% Macro.Context
 gen_injective_theorems% Macro.Exception
 gen_injective_theorems% Macro.Methods
-gen_injective_theorems% Macro.State
 gen_injective_theorems% Syntax.Preresolved
 gen_injective_theorems% Syntax.SepArray
 gen_injective_theorems% Syntax.TSepArray