diff --git a/proof/refine/RISCV64/IpcCancel_R.thy b/proof/refine/RISCV64/IpcCancel_R.thy
index d7e1f177ea..ed02829345 100644
--- a/proof/refine/RISCV64/IpcCancel_R.thy
+++ b/proof/refine/RISCV64/IpcCancel_R.thy
@@ -1051,8 +1051,7 @@ lemma scReplies_of_scTCB_update[simp]:
 crunch schedContextDonate
   for replies_of': "\<lambda>s. P (replies_of' s)" (* this interfers with list_refs_of_replies' *)
   and scReplies_of[wp]: "\<lambda>s. P' (scReplies_of s)"
-  (simp: crunch_simps wp: crunch_wps
-   rule: schedContextDonate_def[simplified updateSchedContext_def])
+  (simp: crunch_simps wp: crunch_wps updateSchedContext_scReplies_of)
 
 lemma updateReply_replyNext_update_None:
   "\<lbrace> \<top> \<rbrace>
diff --git a/proof/refine/RISCV64/KHeap_R.thy b/proof/refine/RISCV64/KHeap_R.thy
index e1efe240eb..08b9475127 100644
--- a/proof/refine/RISCV64/KHeap_R.thy
+++ b/proof/refine/RISCV64/KHeap_R.thy
@@ -4900,6 +4900,12 @@ lemma setSchedContext_scReplies_of:
   apply (erule back_subst[where P=P], rule ext)
   by (clarsimp simp: opt_map_def)
 
+lemma updateSchedContext_scReplies_of:
+  "(\<And>sc. scReply (f sc) = scReply sc) \<Longrightarrow> updateSchedContext scPtr f \<lbrace>\<lambda>s. P' (scReplies_of s)\<rbrace>"
+  apply (wpsimp simp: updateSchedContext_def wp: setSchedContext_scReplies_of)
+  apply (auto elim!: rsubst[where P=P'] simp: opt_map_def obj_at'_def)
+  done
+
 lemma getObject_tcb_wp:
   "\<lbrace>\<lambda>s. tcb_at' p s \<longrightarrow> (\<exists>t::tcb. ko_at' t p s \<and> Q t s)\<rbrace> getObject p \<lbrace>Q\<rbrace>"
   by (clarsimp simp: getObject_def valid_def in_monad