diff --git a/tests/lean/run/pred_to_subtype_coercion.lean b/tests/lean/run/pred_to_subtype_coercion.lean
new file mode 100644
index 0000000000..9d4f80676b
--- /dev/null
+++ b/tests/lean/run/pred_to_subtype_coercion.lean
@@ -0,0 +1,18 @@
+universe variables u
+
+attribute [instance]
+definition pred2subtype {A : Type u} : has_coe_to_sort (A → Prop) :=
+⟨Type (max 1 u), λ p : A → Prop, subtype p⟩
+
+definition below (n : nat) : nat → Prop :=
+λ i, i < n
+
+check λ x : below 10, x
+
+definition f : below 10 → nat
+| ⟨a, h⟩ := a
+
+lemma zlt10 : 0 < 10 :=
+sorry
+
+check f ⟨0, zlt10⟩