proposition: Lemma lem_itrev_perm' {A} : forall l l' : list A, Permutation (itrev l l') (l ++ l').
proof: Proof. induction l; sauto use: Permutation_middle, Permutation_sym. Qed.
imports: Hammer(Tactics) Hammer(Hints) Sorting.Permutation