fix normalise_through_run_stage wix new return

src/verification/FPSProp.v

@@ -738,6 +738,15 @@ Module FPS_PROP (EVAL_Def: EVAL_ENV)
         by rewrite <- (normalise_through_goto_valid _ Hderoute).
       }
 
+      { (* return *)
+        intros e1 b1.
+        rewrite /return_sem.
+        intros H. inversion H. clear H. clear H1. clear H2.
+        rewrite /break /app_trace /full_normalise /mk_fp_env //=.
+        rewrite /FPE_BS.fp /Common.on_enter /Common.on_exit.
+        by repeat rewrite -get_block_get_normalise.
+      }
+
       {
         (* nav_sem *)
         intros e1 b1.