diff --git a/golden-tests/tests/isprop-subsing/expected b/golden-tests/tests/isprop-subsing/expected
new file mode 100644
index 0000000..8fbea7a
--- /dev/null
+++ b/golden-tests/tests/isprop-subsing/expected
@@ -0,0 +1,2 @@
+0.IsProp : 1.★ → ★
+0.feq : 1.(A : ★) → 1.(f : IsProp A) → 1.(g : IsProp A) → f ≡ g : IsProp A
diff --git a/golden-tests/tests/isprop-subsing/isprop-subsing.quox b/golden-tests/tests/isprop-subsing/isprop-subsing.quox
new file mode 100644
index 0000000..2117d08
--- /dev/null
+++ b/golden-tests/tests/isprop-subsing/isprop-subsing.quox
@@ -0,0 +1,4 @@
+def0 IsProp : ★ → ★ = λ A ⇒ (x y : A) → x ≡ y : A
+
+def0 feq : (A : ★) → (f g : IsProp A) → f ≡ g : IsProp A =
+  λ A f g ⇒ δ _ ⇒ f
diff --git a/golden-tests/tests/isprop-subsing/run b/golden-tests/tests/isprop-subsing/run
new file mode 100644
index 0000000..feb762b
--- /dev/null
+++ b/golden-tests/tests/isprop-subsing/run
@@ -0,0 +1,2 @@
+. ../lib.sh
+check "$1" isprop-subsing.quox