diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index 63b55ce515bfd7d1c19e9c7a571e9ba2103d934d..2c2581979e881121cef445cc56b3933bd1e41414 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -130,3 +130,11 @@ Proof. iIntros. iAssert False%I with ">[-]" as "[]". done. Qed.
 
 Lemma demo_14 (M : ucmraT) (P : uPred M) : False -∗ P.
 Proof. iIntros "H". done. Qed.
+
+(* Check instantiation and dependent types *)
+Lemma demo_15 (M : ucmraT) (P : ∀ n, vec nat n → uPred M) :
+  (∀ n v, P n v) -∗ ∃ n v, P n v.
+Proof.
+  iIntros "H". iExists _, [#10].
+  iSpecialize ("H" $! _ [#10]). done.
+Qed.