rename variables for rsubst2 squash

Signed-off-by: Michael McInerney <[email protected]>
seL4 · Apr 8, 2024 · 455faf5 · 455faf5
1 parent 01c6bd0
commit 455faf5
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/lib/Lib.thy b/lib/Lib.thy
@@ -2536,7 +2536,7 @@ qed
 lemmas rsubst = back_subst[where a=s and b=t for s t]
 
 lemma rsubst2:
-  "\<lbrakk>P s x; s = t; x = y\<rbrakk> \<Longrightarrow> P t y"
+  "\<lbrakk>P a b; a = s; b = t\<rbrakk> \<Longrightarrow> P s t"
   by simp
 
 lemma rsubst3: