diff --git a/theories/infinite.v b/theories/infinite.v
index 25ecb25fc07766728954989f33c32180bae71850..ef4931b89f739509c31f0d7ef2602f6dec7d813a 100644
--- a/theories/infinite.v
+++ b/theories/infinite.v
@@ -42,8 +42,7 @@ Section Fresh.
   Proof.
     intros relfg i.
     unfold fresh_generic_body.
-    destruct decide.
-    2: done.
+    destruct decide; auto.
     apply relfg.
   Qed.