diff --git a/program_logic/tests.v b/program_logic/tests.v
index 9d81b5333faf52388a0d6f73088ddd98fa782cf5..ab42402092e21fdd18cb7f47e65382490354eb5e 100644
--- a/program_logic/tests.v
+++ b/program_logic/tests.v
@@ -1,7 +1,21 @@
 (** This file tests a bunch of things. *)
-From program_logic Require Import model.
+From program_logic Require Import model saved_prop.
 
 Module ModelTest. (* Make sure we got the notations right. *)
   Definition iResTest {Λ : language} {Σ : rFunctor}
     (w : iWld Λ Σ) (p : iPst Λ) (g : iGst Λ Σ) : iRes Λ Σ := Res w p (Some g).
 End ModelTest.
+
+Module SavedPropTest.
+  (* Test if we can really go "crazy higher order" *)
+  Section sec.
+    Definition Σ : rFunctorG := #[ agreeRF (cofe_morCF idCF idCF) ].
+    Context {Λ : language}.
+    Notation iProp := (iPropG Λ Σ).
+
+    Local Instance : savedPropG Λ Σ (cofe_morCF idCF idCF) := _.
+
+    Definition own_pred γ (φ : laterC iProp -n> laterC iProp) : iProp :=
+      saved_prop_own γ φ.
+  End sec.
+End SavedPropTest.