diff --git a/theories/list.v b/theories/list.v
index c685c985ba39d9a74876c8574de38870d948d754..5b028f2473149bfb648a1ffbf4df8928b18456d5 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -2175,7 +2175,7 @@ Section Forall_Exists.
     intros [??]; auto using Forall_app_2.
   Qed.
   Lemma Forall_true l : (∀ x, P x) → Forall P l.
-  Proof. induction l; auto. Qed.
+  Proof. intros ?. induction l; auto. Defined.
   Lemma Forall_impl (Q : A → Prop) l :
     Forall P l → (∀ x, P x → Q x) → Forall Q l.
   Proof. intros H ?. induction H; auto. Defined.