diff --git a/src/Lean/Elab/PreDefinition/Structural.lean b/src/Lean/Elab/PreDefinition/Structural.lean
index 379d65fe6c..44dd6cec8c 100644
--- a/src/Lean/Elab/PreDefinition/Structural.lean
+++ b/src/Lean/Elab/PreDefinition/Structural.lean
@@ -212,6 +212,7 @@ withBelowDict below numIndParams fun C belowDict =>
 
 private partial def replaceRecApps (recFnName : Name) (recArgInfo : RecArgInfo) : Expr → Expr → MetaM Expr
 | below, e@(Expr.lam _ _ _ _) => lambdaTelescope e fun xs b => do b ← replaceRecApps below b; mkLambdaFVars xs b
+| below, e@(Expr.forallE _ _ _ _) => forallTelescope e fun xs b => do b ← replaceRecApps below b; mkForallFVars xs b
 | below, Expr.letE n type val body _ => do
   val ← replaceRecApps below val;
   withLetDecl n type val fun x => do
diff --git a/tests/lean/run/def11.lean b/tests/lean/run/def11.lean
new file mode 100644
index 0000000000..1b9edc43e5
--- /dev/null
+++ b/tests/lean/run/def11.lean
@@ -0,0 +1,43 @@
+new_frontend
+
+inductive Formula
+| eqf  : Nat → Nat → Formula
+| andf : Formula → Formula → Formula
+| impf : Formula → Formula → Formula
+| notf : Formula → Formula
+| orf  : Formula → Formula → Formula
+| allf : (Nat → Formula) → Formula
+
+namespace Formula
+def implies (a b : Prop) : Prop := a → b
+
+def denote : Formula → Prop
+| eqf n1 n2  => n1 = n2
+| andf f1 f2 => denote f1 ∧ denote f2
+| impf f1 f2 => implies (denote f1) (denote f2)
+| orf f1 f2  => denote f1 ∨ denote f2
+| notf f     => ¬ denote f
+| allf f     => (n : Nat) → denote (f n)
+
+theorem denote_eqf (n1 n2 : Nat) : denote (eqf n1 n2) = (n1 = n2) :=
+rfl
+
+theorem denote_andf (f1 f2 : Formula) : denote (andf f1 f2) = (denote f1 ∧ denote f2) :=
+rfl
+
+theorem denote_impf (f1 f2 : Formula) : denote (impf f1 f2) = (denote f1 → denote f2) :=
+rfl
+
+theorem denote_orf (f1 f2 : Formula) : denote (orf f1 f2) = (denote f1 ∨ denote f2) :=
+rfl
+
+theorem denote_notf (f : Formula) : denote (notf f) = ¬ denote f :=
+rfl
+
+theorem denote_allf (f : Nat → Formula) : denote (allf f) = (∀ n, denote (f n)) :=
+rfl
+
+theorem ex : denote (allf (fun n₁ => allf (fun n₂ => impf (eqf n₁ n₂) (eqf n₂ n₁)))) = (∀ (n₁ n₂ : Nat), n₁ = n₂ → n₂ = n₁) :=
+rfl
+
+end Formula