diff --git a/theories/countable.v b/theories/countable.v
index bd62102163d34420bf0bbaa8b71188b6313cd4bc..6ea4690763cd08e82e314801da7418a0a70bc699 100644
--- a/theories/countable.v
+++ b/theories/countable.v
@@ -68,7 +68,7 @@ Lemma surjective_cancel `{Countable A} `{∀ x y : B, Decision (x = y)}
   (f : A → B) `{!Surjective (=) f} : { g : B → A & Cancel (=) f g }.
 Proof.
   exists (λ y, choose (λ x, f x = y) (surjective f y)).
-  intros y. by rewrite (choose_correct _ (surjective f y)).
+  intros y. by rewrite (choose_correct (λ _, _) (surjective f y)).
 Qed.
 
 (** ** Instances *)