Add test for `unseal` of `siProp`.

tests/siprop.ref

+"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))

tests/siprop.v

+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.