src/HOL/Combinatorics/Permutations.thy

--- a/src/HOL/Combinatorics/Permutations.thy	Mon May 17 13:57:19 2021 +1000
+++ b/src/HOL/Combinatorics/Permutations.thy	Mon May 17 09:07:30 2021 +0000
@@ -1150,6 +1150,11 @@
     by (induct xs) (auto simp: inv_f_f surj_f_inv_f)
 qed
 
+lemma list_all2_permute_list_iff:
+  \<open>list_all2 P (permute_list p xs) (permute_list p ys) \<longleftrightarrow> list_all2 P xs ys\<close>
+  if \<open>p permutes {..<length xs}\<close>
+  using that by (auto simp add: list_all2_iff simp flip: permute_list_zip)
+
 
 subsection \<open>More lemmas about permutations\<close>