diff --git a/proof/crefine/RISCV64/Finalise_C.thy b/proof/crefine/RISCV64/Finalise_C.thy
index 27fd49c1c4..6110bdc7f7 100644
--- a/proof/crefine/RISCV64/Finalise_C.thy
+++ b/proof/crefine/RISCV64/Finalise_C.thy
@@ -1459,15 +1459,10 @@ lemma suspend_ccorres:
     apply clarsimp
     apply (rule conseqPre, vcg)
     apply (rule subset_refl)
-   apply (rule hoare_strengthen_post)
-    apply (rule hoare_vcg_conj_lift)
-     apply (rule hoare_vcg_conj_lift)
-      apply (rule hoare_vcg_conj_lift)
-       apply (rule cancelIPC_sch_act_simple)
-      apply (rule cancelIPC_tcb_at'_better[where P=id, simplified, where p=thread])
-     apply (rule cancelIPC_invs')
-    apply (rule cancelIPC_weak_sch_act_wf)
-   apply (fastforce simp: invs_valid_objs' valid_tcb_state'_def)
+   apply (rule_tac Q="\<lambda>_ s. invs' s \<and> tcb_at' thread s \<and> sch_act_simple s
+                            \<and> weak_sch_act_wf (ksSchedulerAction s) s" in hoare_post_imp)
+    apply fastforce
+   apply (wpsimp wp: hoare_vcg_all_lift)
   apply (auto simp: ThreadState_defs)
   done