diff --git a/tests/siprop.ref b/tests/siprop.ref
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..c7ab6a8bf472dcb11e41b51cdfd0ce63b30a292a 100644
--- a/tests/siprop.ref
+++ b/tests/siprop.ref
@@ -0,0 +1,17 @@
+"unseal_test"
+     : string
+1 goal
+  
+  P, Q : siProp
+  Φ : nat → siProp
+  ============================
+  siprop.siProp_and_def P
+    (siprop.siProp_and_def (siprop.siProp_later_def Q)
+       (siprop.siProp_exist_def (λ x : nat, Φ x)))
+  ⊣⊢ siprop.siProp_exist_def
+       (λ x : nat,
+          siprop.siProp_or_def
+            (siprop.siProp_and_def P
+               (siprop.siProp_and_def (siprop.siProp_later_def Q)
+                  (siprop.siProp_pure_def True))) 
+            (Φ x))
diff --git a/tests/siprop.v b/tests/siprop.v
index fc72d0ccce2bfc8f9b98adb2786bcbb09867b22f..9e6c6b7d5e51af448cbaa3eb0c9cf37cb4958869 100644
--- a/tests/siprop.v
+++ b/tests/siprop.v
@@ -1,4 +1,14 @@
+From stdpp Require Import strings.
 From iris.si_logic Require Import bi.
+Unset Mangle Names.
+
+Check "unseal_test".
+Lemma unseal_test (P Q : siProp) (Φ : nat → siProp) :
+  P ∧ ▷ Q ∧ (∃ x, Φ x) ⊣⊢ ∃ x, P ∗ ▷ Q ∧ emp ∨ Φ x.
+Proof.
+  siProp.unseal.
+  Show.
+Abort.
 
 (** Make sure that [siProp]s are parsed in [bi_scope]. *)
 Definition test : siProp := â–· True.