diff --git a/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean b/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean
index 3cfc7d8d70..312ea2e08b 100644
--- a/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean
@@ -216,7 +216,7 @@ def isFunLike (e : Expr) : MetaM Bool := do
   withTransparency TransparencyMode.all do forallTelescopeReducing (← inferType e) fun xs b => xs.size > 0
 
 def isSubstLike (e : Expr) : Bool :=
-  e.isAppOfArity `Eq.ndrec 6
+  e.isAppOfArity `Eq.ndrec 6 || e.isAppOfArity `Eq.rec 6
 
 def nameNotRoundtrippable (n : Name) : Bool :=
   n.hasMacroScopes || isPrivateName n || containsNum n
diff --git a/tests/lean/ppProofs.lean b/tests/lean/ppProofs.lean
index b730d3b35b..35ce06374f 100644
--- a/tests/lean/ppProofs.lean
+++ b/tests/lean/ppProofs.lean
@@ -1,3 +1,5 @@
+set_option pp.analyze.trustSubst true
+set_option pp.proofs false
 example (h : α = β) : h ▸ (a : α) = (b : β) := _
 example (h : α = β) : id h ▸ (a : α) = (b : β) := _
 example (h : α = β) : id h ▸ (a : α) = (b : β) := by simp