chore: adaptations for leanprover/lean4#3756

Std/Logic.lean

@@ -81,11 +81,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') :

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2024-04-21
+leanprover/lean4-pr-releases:pr-release-3756