diff --git a/Std/Logic.lean b/Std/Logic.lean
index 759164aec1..6b9c9a50b7 100644
--- a/Std/Logic.lean
+++ b/Std/Logic.lean
@@ -94,11 +94,6 @@ theorem heq_of_cast_eq : ∀ (e : α = β) (_ : cast e a = a'), HEq a a'
 theorem cast_eq_iff_heq : cast e a = a' ↔ HEq a a' :=
   ⟨heq_of_cast_eq _, fun h => by cases h; rfl⟩
 
-theorem eqRec_eq_cast {α : Sort _} {a : α} {motive : (a' : α) → a = a' → Sort _}
-    (x : motive a (rfl : a = a)) {a' : α} (e : a = a') :
-    @Eq.rec α a motive x a' e = cast (e ▸ rfl) x := by
-  subst e; rfl
-
 --Porting note: new theorem. More general version of `eqRec_heq`
 theorem eqRec_heq_self {α : Sort _} {a : α} {motive : (a' : α) → a = a' → Sort _}
     (x : motive a (rfl : a = a)) {a' : α} (e : a = a') :
diff --git a/lean-toolchain b/lean-toolchain
index 9ad304042c..179aa76519 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.7.0
+leanprover/lean4-pr-releases:pr-release-3756