[STATEMENT]
lemma subindex_permutation2:
  assumes "distinct ss" "set ss \<subseteq> {..<length ls}"
  obtains f where "f permutes {..<length ls}"
    "ls = permute_list f (map ((!) ls) (filter (\<lambda>i. i \<notin> set ss) [0..<length ls]) @ map ((!) ls) ss)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>f. \<lbrakk>f permutes {..<length ls}; ls = permute_list f (map ((!) ls) (filter (\<lambda>i. i \<notin> set ss) [0..<length ls]) @ map ((!) ls) ss)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using subindex_permutation
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>distinct ?ss; set ?ss \<subseteq> {..<length ?ls}; \<And>f. \<lbrakk>f permutes {..<length ?ls}; permute_list f ?ls = map ((!) ?ls) (filter (\<lambda>i. i \<notin> set ?ss) [0..<length ?ls]) @ map ((!) ?ls) ?ss\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>f. \<lbrakk>f permutes {..<length ls}; ls = permute_list f (map ((!) ls) (filter (\<lambda>i. i \<notin> set ss) [0..<length ls]) @ map ((!) ls) ss)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis assms(1) assms(2) length_permute_list mset_eq_permutation mset_permute_list)