diff --git a/tests/vect.lp b/tests/vect.lp
new file mode 100644
index 0000000000000000000000000000000000000000..865eee4da027d42143bc41b75245a2a054b9806d
--- /dev/null
+++ b/tests/vect.lp
@@ -0,0 +1,8 @@
+require open personoj.encodings.lhol
+require open personoj.encodings.pvs_cert
+require open personoj.encodings.deptype
+require open personoj.encodings.prenex
+
+symbol nat: θ {|set|}
+symbol vect: ϕ (∀K (λ_, scheme_k (nat *> {|set|})))
+assert vect: Set → η nat → Set