diff --git a/theories/finite.v b/theories/finite.v
index 60b3961a2e565a6d34983afe6c98470f74a9acbc..c1a0ebc65d58ecfa408324f2e77392aba329e816 100644
--- a/theories/finite.v
+++ b/theories/finite.v
@@ -237,7 +237,7 @@ Section bijective_finite.
   Context `{Finite A, EqDecision B} (f : A → B) (g : B → A).
   Context `{!Inj (=) (=) f, !Cancel (=) f g}.
 
-  Local Instance bijective_finite: Finite B :=
+  Definition bijective_finite : Finite B :=
     let _ := cancel_surj (f:=f) (g:=g) in
     surjective_finite f.
 End bijective_finite.