diff --git a/iris/bi/big_op.v b/iris/bi/big_op.v
index 5e7d97371d532915f0e487405628d40578a2c80b..739f41e56993e930163ede5511b4bebb1cbb78ce 100644
--- a/iris/bi/big_op.v
+++ b/iris/bi/big_op.v
@@ -2497,7 +2497,7 @@ Section gset.
   (** No need to declare instances for non-expansiveness and properness, we
   get both from the generic [big_opS] instances. *)
   Global Instance big_sepS_mono' :
-     Proper (pointwise_relation _ (⊢) ==> (=) ==> (⊢)) (big_opS (@bi_sep PROP) (A:=A)).
+    Proper (pointwise_relation _ (⊢) ==> (=) ==> (⊢)) (big_opS (@bi_sep PROP) (A:=A)).
   Proof. intros f g Hf m ? <-. by apply big_sepS_mono. Qed.
 
   Global Instance big_sepS_empty_persistent Φ :