diff --git a/lib/MonadicRewrite.thy b/lib/MonadicRewrite.thy
index f08e04fd9..e4fbed648 100644
--- a/lib/MonadicRewrite.thy
+++ b/lib/MonadicRewrite.thy
@@ -10,7 +10,7 @@
 theory MonadicRewrite
 imports
   Monads.Nondet_VCG
-  Corres_UL
+  ExtraCorres
   Monads.Nondet_Empty_Fail
   Rules_Tac
 begin
@@ -744,6 +744,13 @@ lemma monadic_rewrite_corres_r_generic:
    \<Longrightarrow> corres_underlying R nf nf' r P (P' and Q) a c"
   by (fastforce simp: corres_underlying_def monadic_rewrite_def)
 
+lemma monadic_rewrite_corres_r_generic_ex_abs:
+  "\<lbrakk> monadic_rewrite F E (\<lambda>s'. Q s' \<and> ex_abs_underlying sr P s') c' c;
+     corres_underlying sr nf nf'' r P P' a c';
+     F \<longrightarrow> nf''; nf' \<longrightarrow> nf'' \<rbrakk>
+   \<Longrightarrow> corres_underlying sr nf nf' r P (P' and Q) a c"
+  by (fastforce simp: corres_underlying_def monadic_rewrite_def)
+
 lemma monadic_rewrite_corres_r:
   "\<lbrakk> monadic_rewrite False True Q c c';
      corres_underlying R nf nf' r P P' a c' \<rbrakk>