diff --git a/src/Lean/Elab/Deriving/BEq.lean b/src/Lean/Elab/Deriving/BEq.lean
index 7ebe5cbbdf..ab9aca093b 100644
--- a/src/Lean/Elab/Deriving/BEq.lean
+++ b/src/Lean/Elab/Deriving/BEq.lean
@@ -57,7 +57,10 @@ where
             let b := mkIdent (← mkFreshUserName `b)
             ctorArgs1 := ctorArgs1.push a
             ctorArgs2 := ctorArgs2.push b
-            if (← inferType x).isAppOf indVal.name then
+            let xType ← inferType x
+            if (← isProp xType) then
+              continue
+            if xType.isAppOf indVal.name then
               rhs ← `($rhs && $(mkIdent auxFunName):ident $a:ident $b:ident)
             else
               rhs ← `($rhs && $a:ident == $b:ident)
diff --git a/src/Lean/Elab/Deriving/DecEq.lean b/src/Lean/Elab/Deriving/DecEq.lean
index 09b0a83cdf..d2ab52bce9 100644
--- a/src/Lean/Elab/Deriving/DecEq.lean
+++ b/src/Lean/Elab/Deriving/DecEq.lean
@@ -67,11 +67,12 @@ where
                 let b := mkIdent (← mkFreshUserName `b)
                 ctorArgs1 := ctorArgs1.push a
                 ctorArgs2 := ctorArgs2.push b
+                let xType ← inferType x
                 let indValNum :=
                   ctx.typeInfos.findIdx?
-                  ((← inferType x).isAppOf ∘ ConstantVal.name ∘ InductiveVal.toConstantVal)
+                  (xType.isAppOf ∘ ConstantVal.name ∘ InductiveVal.toConstantVal)
                 let recField  := indValNum.map (ctx.auxFunNames[·]!)
-                let isProof   := (← inferType (← inferType x)).isProp
+                let isProof ← isProp xType
                 todo := todo.push (a, b, recField, isProof)
             patterns := patterns.push (← `(@$(mkIdent ctorName₁):ident $ctorArgs1:term*))
             patterns := patterns.push (← `(@$(mkIdent ctorName₁):ident $ctorArgs2:term*))
diff --git a/tests/lean/3140.lean b/tests/lean/3140.lean
new file mode 100644
index 0000000000..6d93a65dda
--- /dev/null
+++ b/tests/lean/3140.lean
@@ -0,0 +1,11 @@
+/- Verify that `deriving BEq` works on structures with `Prop`-fields.-/
+
+structure S where
+  foo : Nat
+  p : True
+  Bar : Nat
+  deriving BEq
+
+#eval (⟨1,⟨⟩,2⟩ : S) == ⟨1,⟨⟩,3⟩ -- false
+#eval (⟨1,⟨⟩,2⟩ : S) == ⟨2,⟨⟩,2⟩ -- false
+#eval (⟨1,⟨⟩,2⟩ : S) == ⟨1,⟨⟩,2⟩ -- true
diff --git a/tests/lean/3140.lean.expected.out b/tests/lean/3140.lean.expected.out
new file mode 100644
index 0000000000..52289c68f9
--- /dev/null
+++ b/tests/lean/3140.lean.expected.out
@@ -0,0 +1,3 @@
+false
+false
+true