diff --git a/program_logic/auth.v b/program_logic/auth.v
index 148c4b2789088815b6b9ad6d0663cb8e995d6ae7..b7fdd572c35188bee0a66d3792ae3f983816af38 100644
--- a/program_logic/auth.v
+++ b/program_logic/auth.v
@@ -1,4 +1,4 @@
-From algebra Require Export auth functor.
+From algebra Require Export auth.
 From program_logic Require Export invariants ghost_ownership.
 Import uPred.
 
diff --git a/program_logic/saved_prop.v b/program_logic/saved_prop.v
new file mode 100644
index 0000000000000000000000000000000000000000..6e3c60b24fe0a81d4a7683b857cd54583d2c1b9b
--- /dev/null
+++ b/program_logic/saved_prop.v
@@ -0,0 +1,31 @@
+From algebra Require Export agree.
+From program_logic Require Export ghost_ownership.
+Import uPred.
+
+Class SavedPropInG Λ Σ (i : gid) :=
+  saved_prop_inG :> InG Λ Σ i (agreeRA (laterC (iPreProp Λ (globalF Σ)))).
+
+Definition saved_prop_own {Λ Σ} (i : gid) `{SavedPropInG Λ Σ i}
+    (γ : gname) (P : iPropG Λ Σ) : iPropG Λ Σ :=
+  own i γ (to_agree (Next (iProp_unfold P))).
+Instance: Params (@saved_prop_own) 5.
+
+Section stored_prop.
+  Context `{SavedPropInG Λ Σ SPI}.
+  Implicit Types P Q : iPropG Λ Σ.
+  Implicit Types γ : gname.
+
+  Lemma saved_prop_alloc N P :
+    True ⊑ pvs N N (∃ γ, saved_prop_own SPI γ P).
+  Proof. by apply own_alloc. Qed.
+
+  Lemma saved_prop_twice γ P Q :
+    (saved_prop_own SPI γ P ★ saved_prop_own SPI γ Q) ⊑ ▷ (P ↔ Q).
+  Proof.
+    rewrite /saved_prop_own -own_op own_valid agree_validI.
+    rewrite agree_equivI later_equivI /=; apply later_mono.
+    rewrite -{2}(iProp_fold_unfold P) -{2}(iProp_fold_unfold Q).
+    apply (eq_rewrite (iProp_unfold P) (iProp_unfold Q) (λ Q' : iPreProp Λ _,
+      iProp_fold (iProp_unfold P) ↔ iProp_fold Q')%I); solve_ne || auto with I.
+  Qed.
+End stored_prop.