fix(library/constructions/injective): use same transparency setting as no_confusion

src/library/constructions/injective.cpp

@@ -58,7 +58,8 @@ static void collect_args(type_context & tctx, expr const & type, unsigned num_pa
 }
 
 expr mk_injective_type(environment const & env, name const & ir_name, expr const & ir_type, unsigned num_params, level_param_names const & lp_names) {
-    type_context tctx(env);
+    // The transparency needs to match the kernel since we need to be consistent with the no_confusion construction.
+    type_context tctx(env, transparency_mode::All);
     buffer<expr> params, args1, args2, new_args;
     collect_args(tctx, ir_type, num_params, params, args1, args2, new_args);
     expr c_ir_params = mk_app(mk_constant(ir_name, param_names_to_levels(lp_names)), params);

tests/lean/run/injection.lean

@@ -0,0 +1,2 @@
+inductive term
+| abs : tt → term → term