diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean
index 403ebb2a59..1e89ef46c3 100644
--- a/src/Lean/Meta/ExprDefEq.lean
+++ b/src/Lean/Meta/ExprDefEq.lean
@@ -905,9 +905,8 @@ private def unfoldReducibeDefEq (tInfo sInfo : ConstantInfo) (t s : Expr) : Meta
 
   Auxiliary method for isDefEqDelta -/
 private def unfoldNonProjFnDefEq (tInfo sInfo : ConstantInfo) (t s : Expr) : MetaM LBool := do
-  let env ← getEnv
-  let tProj? := env.isProjectionFn tInfo.name
-  let sProj? := env.isProjectionFn sInfo.name
+  let tProj? ← isProjectionFn tInfo.name
+  let sProj? ← isProjectionFn sInfo.name
   if tProj? && !sProj? then
     unfold s (unfoldDefEq tInfo sInfo t s) $ fun s => isDefEqRight sInfo.name t s
   else if !tProj? && sProj? then
diff --git a/src/Lean/ProjFns.lean b/src/Lean/ProjFns.lean
index 818f71cee9..9b1eb70762 100644
--- a/src/Lean/ProjFns.lean
+++ b/src/Lean/ProjFns.lean
@@ -62,4 +62,11 @@ def getProjectionStructureName? (env : Environment) (projName : Name) : Option N
     | _ => none
 
 end Environment
+
+def isProjectionFn [MonadEnv m] [Monad m] (declName : Name) : m Bool :=
+  return (← getEnv).isProjectionFn declName
+
+def getProjectionFnInfo? [MonadEnv m] [Monad m] (declName : Name) : m (Option ProjectionFunctionInfo) :=
+  return (← getEnv).getProjectionFnInfo? declName
+
 end Lean