diff --git a/lib/clib/Corres_UL_C.thy b/lib/clib/Corres_UL_C.thy
index bc012b52e..7c552c5c8 100644
--- a/lib/clib/Corres_UL_C.thy
+++ b/lib/clib/Corres_UL_C.thy
@@ -14,6 +14,7 @@ imports
   CParser.LemmaBucket_C
   Lib.LemmaBucket
   SIMPL_Lemmas
+  Monads.OptionMonadWP
 begin
 
 declare word_neq_0_conv [simp del]
@@ -171,6 +172,13 @@ lemma ccorresE:
   apply simp
   done
 
+lemma ccorresE_gets_the:
+  "\<lbrakk>ccorresG srel \<Gamma> rrel xf G G' hs (gets_the c) c'; (s, s') \<in> srel; G s; s' \<in> G'; no_ofail G c;
+    \<Gamma> \<turnstile>\<^sub>h \<langle>c' # hs, s'\<rangle> \<Rightarrow> (n, Normal t')\<rbrakk>
+   \<Longrightarrow> (s, t') \<in> srel \<and> rrel (the (c s)) (xf t')"
+  by (fastforce simp: ccorres_underlying_def no_ofail_def unif_rrel_def gets_the_def gets_def
+                      get_def bind_def return_def)
+
 lemma ccorres_empty_handler_abrupt:
   assumes cc: "ccorres_underlying sr \<Gamma> rrel xf' arrel axf P P' [] a c"
   and   asms: "(s, s') \<in> sr" "P s" "s' \<in> P'" "\<not> snd (a s)"