diff --git a/tests/lean/hott/tele_eq.hlean b/tests/lean/hott/tele_eq.hlean
new file mode 100644
index 000000000..abc8f602f
--- /dev/null
+++ b/tests/lean/hott/tele_eq.hlean
@@ -0,0 +1,18 @@
+constant A₁ : Type
+constant A₂ : A₁ → Type
+constant A₃ : Π (a₁ : A₁), A₂ a₁ → Type
+
+structure foo :=
+mk :: (a₁ : A₁) (a₂ : A₂ a₁) (a₃ : A₃ a₁ a₂)
+
+theorem foo.eq {a₁ b₁ : A₁} {a₂ : A₂ a₁} {b₂ : A₂ b₁} {a₃ : A₃ a₁ a₂} {b₃ : A₃ b₁ b₂}
+               (H₁ : a₁ = b₁) (H₂ : eq.rec_on H₁ a₂ = b₂) (H₃ : eq.rec_on H₂ (eq.rec_on H₁ a₃) = b₃)
+               : foo.mk a₁ a₂ a₃ = foo.mk b₁ b₂ b₃ :=
+begin
+  cases H₁,
+  cases H₂,
+  cases H₃,
+  apply rfl
+end
+
+print definition foo.eq