proposition: Lemma lem_itrev_perm {A} : forall l l' : list A, Permutation (itrev l l') (l ++ l').
proof: Proof. induction l as [| x l IH]; simpl. - eauto using Permutation. - intro l'. enough (Permutation (l ++ (x :: l')) (x :: l ++ l')). { eauto using Permutation. } eauto using Permutation_middle, Permutation_sym. Qed.
imports: Hammer(Tactics) Hammer(Hints) Sorting.Permutation