diff --git a/algebra/sts.v b/algebra/sts.v
index 6d7346321eb8b5dac2caa05409bff2163b7fb5d4..290cbc225b6ff762fe237f43ee21033025a997d4 100644
--- a/algebra/sts.v
+++ b/algebra/sts.v
@@ -376,6 +376,11 @@ Proof.
     eapply closed_steps, Hsup; first done. set_solver +Hs'.
 Qed.
 
+Global Instance sts_frag_peristent S : Persistent (sts_frag S ∅).
+Proof.
+  constructor; split=> //= [[??]]. by rewrite /dra.dra_core /= sts.up_closed.
+Qed.
+
 (** Inclusion *)
 (* This is surprisingly different from to_validity_included. I am not sure
    whether this is because to_validity_included is non-canonical, or this
diff --git a/program_logic/sts.v b/program_logic/sts.v
index 5163df44663199104b91bb16ebdcc632b71df6c6..06c1f37ad88f582df92338d4bd02de4e4be037f8 100644
--- a/program_logic/sts.v
+++ b/program_logic/sts.v
@@ -44,6 +44,10 @@ Section definitions.
   Proof. solve_proper. Qed.
   Global Instance sts_ctx_persistent N φ : PersistentP (sts_ctx N φ).
   Proof. apply _. Qed.
+  Global Instance sts_own_peristent s : PersistentP (sts_own s ∅).
+  Proof. apply _. Qed.
+  Global Instance sts_ownS_peristent S : PersistentP (sts_ownS S ∅).
+  Proof. apply _. Qed.
 End definitions.
 
 Typeclasses Opaque sts_own sts_ownS sts_inv sts_ctx.