Apply Robbert's suggestions

theories/finite.v

@@ -224,11 +224,12 @@ Section surjective_finite.
   Context `{Finite A, EqDecision B} (f : A → B).
   Context `{!Surj (=) f}.
 
-  Program Instance surjective_finite: Finite B := {| enum := remove_dups (f <$> enum A) |}.
+  Program Instance surjective_finite: Finite B :=
+    {| enum := remove_dups (f <$> enum A) |}.
   Next Obligation. apply NoDup_remove_dups. Qed.
   Next Obligation.
     intros y. rewrite elem_of_remove_dups, elem_of_list_fmap.
-    destruct (Surj0 y). eauto using elem_of_enum.
+    destruct (surj f y). eauto using elem_of_enum.
   Qed.
 End surjective_finite.
 
@@ -236,9 +237,9 @@ Section bijective_finite.
   Context `{Finite A, EqDecision B} (f : A → B) (g : B → A).
   Context `{!Inj (=) (=) f, !Cancel (=) f g}.
 
-  Program Instance bijective_finite: Finite B := _.
-  Next Obligation. eapply surjective_finite. eapply cancel_surj.
-                   Unshelve. all: eapply _. Qed.
+  Global Instance bijective_finite: Finite B :=
+    let _ := cancel_surj (f:=f) (g:=g) in
+    surjective_finite f.
 End bijective_finite.
 
 Program Instance option_finite `{Finite A} : Finite (option A) :=