[STATEMENT]
lemma permutations_of_list_impl_aux_correct':
  "permutations_of_list_impl_aux acc xs = 
     map (\<lambda>xs. rev xs @ acc) (permutations_of_list_impl xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. permutations_of_list_impl_aux acc xs = map (\<lambda>xs. rev xs @ acc) (permutations_of_list_impl xs)
[PROOF STEP]
by (induction acc xs rule: permutations_of_list_impl_aux.induct,
      subst permutations_of_list_impl_aux.simps, subst permutations_of_list_impl.simps)
     (auto simp: map_list_bind intro!: list_bind_cong)