diff --git a/lib/Monads/Fun_Pred_Syntax.thy b/lib/Monads/Fun_Pred_Syntax.thy
index a284367ea5..d733c00f9f 100644
--- a/lib/Monads/Fun_Pred_Syntax.thy
+++ b/lib/Monads/Fun_Pred_Syntax.thy
@@ -187,6 +187,13 @@ lemma bipred_disj_op_eq[simp]:
 lemma bipred_le_true[simp]: "R \<le> \<top>\<top>"
   by clarsimp
 
+lemma bipred_and_or_True[simp]:
+  "(P or \<top>\<top>) = \<top>\<top>"
+  "(\<top>\<top> or P) = \<top>\<top>"
+  "(P and \<top>\<top>) = P"
+  "(\<top>\<top> and P) = P"
+  by auto
+
 
 section \<open>Examples\<close>
 
diff --git a/lib/Monads/trace/Trace_More_RG.thy b/lib/Monads/trace/Trace_More_RG.thy
index b409c3dffe..e868b46f05 100644
--- a/lib/Monads/trace/Trace_More_RG.thy
+++ b/lib/Monads/trace/Trace_More_RG.thy
@@ -177,19 +177,19 @@ lemma list_cases_weak_twp:
   done
 
 lemma rg_vcg_if_lift2:
-  "\<lbrace>R\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv s0 s. (P rv s0 s \<longrightarrow> X rv s0 s) \<and> (\<not> P rv s0 s \<longrightarrow> Y rv s0 s)\<rbrace> \<Longrightarrow>
-   \<lbrace>R\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv s0 s. if P rv s0 s then X rv s0 s else Y rv s0 s\<rbrace>"
+  "\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv s0 s. (Q rv s0 s \<longrightarrow> X rv s0 s) \<and> (\<not> Q rv s0 s \<longrightarrow> Y rv s0 s)\<rbrace> \<Longrightarrow>
+   \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv s0 s. if Q rv s0 s then X rv s0 s else Y rv s0 s\<rbrace>"
 
-  "\<lbrace>R\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv s0 s. (P' rv \<longrightarrow> X rv s0 s) \<and> (\<not> P' rv \<longrightarrow> Y rv s0 s)\<rbrace> \<Longrightarrow>
-   \<lbrace>R\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv. if P' rv then X rv else Y rv\<rbrace>"
+  "\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv s0 s. (Q' rv \<longrightarrow> X rv s0 s) \<and> (\<not> Q' rv \<longrightarrow> Y rv s0 s)\<rbrace> \<Longrightarrow>
+   \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv. if Q' rv then X rv else Y rv\<rbrace>"
   by (auto simp: validI_def)
 
 lemma rg_vcg_if_lift_ER: (* Required because of lack of rv in lifting rules *)
-  "\<lbrace>R\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv s0 s. (P rv s0 s \<longrightarrow> X rv s0 s) \<and> (\<not> P rv s0 s \<longrightarrow> Y rv s0 s)\<rbrace>,\<lbrace>E\<rbrace> \<Longrightarrow>
-   \<lbrace>R\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv s0 s. if P rv s0 s then X rv s0 s else Y rv s0 s\<rbrace>,\<lbrace>E\<rbrace>"
+  "\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv s0 s. (Q rv s0 s \<longrightarrow> X rv s0 s) \<and> (\<not> Q rv s0 s \<longrightarrow> Y rv s0 s)\<rbrace>,\<lbrace>E\<rbrace> \<Longrightarrow>
+   \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv s0 s. if Q rv s0 s then X rv s0 s else Y rv s0 s\<rbrace>,\<lbrace>E\<rbrace>"
 
-  "\<lbrace>R\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv s0 s. (P' rv \<longrightarrow> X rv s0 s) \<and> (\<not> P' rv \<longrightarrow> Y rv s0 s)\<rbrace>,\<lbrace>E\<rbrace> \<Longrightarrow>
-   \<lbrace>R\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv. if P' rv then X rv else Y rv\<rbrace>,\<lbrace>E\<rbrace>"
+  "\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv s0 s. (Q' rv \<longrightarrow> X rv s0 s) \<and> (\<not> Q' rv \<longrightarrow> Y rv s0 s)\<rbrace>,\<lbrace>E\<rbrace> \<Longrightarrow>
+   \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv. if Q' rv then X rv else Y rv\<rbrace>,\<lbrace>E\<rbrace>"
   by (auto simp: validI_def validIE_def)
 
 lemma rg_list_all_lift:
diff --git a/lib/Monads/trace/Trace_RG.thy b/lib/Monads/trace/Trace_RG.thy
index 23d39732cd..baff602f5b 100644
--- a/lib/Monads/trace/Trace_RG.thy
+++ b/lib/Monads/trace/Trace_RG.thy
@@ -86,9 +86,9 @@ lemma rg_empty_conds[simp]:
   by (simp_all add: rely_cond_def guar_cond_def)
 
 lemma rg_conds_True[simp]:
-  "rely_cond \<top>\<top> s0 tr = True"
-  "guar_cond \<top>\<top> s0 tr = True"
-  by (clarsimp simp: rely_cond_def guar_cond_def)+
+  "rely_cond \<top>\<top> = \<top>\<top>"
+  "guar_cond \<top>\<top> = \<top>\<top>"
+  by (clarsimp simp: rely_cond_def guar_cond_def fun_eq_iff)+
 
 text \<open>
   @{text "rely f R s0s"} constructs a new function from @{text f}, where the environment
@@ -335,6 +335,7 @@ lemma rgE_TrueI:
 
 lemmas twp_post_taut = rg_TrueI[where P="\<top>\<top>", THEN iffD2]
 lemmas twp_post_tautE = rgE_TrueI[where P="\<top>\<top>", THEN iffD2]
+lemmas [elim!] = twp_post_taut twp_post_tautE
 
 lemma rg_post_conj[intro]:
   "\<lbrakk>\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>; \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q'\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q and Q'\<rbrace>"