diff --git a/theories/proofmode/environments.v b/theories/proofmode/environments.v
index 25b78819cd32805502b1bcac3f7b29eb8bfa3e2b..78a8d28ca7ca2732b8b3712dc85f53573ada2408 100644
--- a/theories/proofmode/environments.v
+++ b/theories/proofmode/environments.v
@@ -258,7 +258,7 @@ Instance: Params (@of_envs) 1 := {}.
 Arguments of_envs : simpl never.
 
 Definition envs_entails_aux :
-  seal (λ {PROP : bi} (Γp Γs : env PROP) (Q : PROP), of_envs' Γp Γs ⊢ Q).
+  seal (λ (PROP : bi) (Γp Γs : env PROP) (Q : PROP), of_envs' Γp Γs ⊢ Q).
 Proof. by eexists. Qed.
 Definition envs_entails {PROP : bi} (Δ : envs PROP) (Q : PROP) : Prop :=
   envs_entails_aux.(unseal) PROP (env_intuitionistic Δ) (env_spatial Δ) Q.