diff --git a/program_logic/sts.v b/program_logic/sts.v
index a0807ace1a67b11ff779a7f65eb32146d4b6c139..1a7b45ed1502452ae5d13a571da01f9fa6ef9536 100644
--- a/program_logic/sts.v
+++ b/program_logic/sts.v
@@ -66,10 +66,7 @@ Section sts.
   Lemma sts_ownS_op γ S1 S2 T1 T2 :
     T1 ∪ T2 ⊆ ∅ → sts.closed S1 T1 → sts.closed S2 T2 →
     sts_ownS γ (S1 ∩ S2) (T1 ∪ T2) ≡ (sts_ownS γ S1 T1 ★ sts_ownS γ S2 T2)%I.
-  Proof.
-    intros HT HS1 HS2. rewrite /sts_ownS -own_op.
-      by apply own_proper, sts_op_frag.
-  Qed.
+  Proof. intros. by rewrite /sts_ownS -own_op sts_op_frag. Qed.
 
   Lemma sts_alloc E N s :
     nclose N ⊆ E →