Address Gerwin's PR comment squash

Signed-off-by: Michael McInerney <[email protected]>

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