proposition: Lemma lem_itrev {A} : forall l acc : list A, itrev l acc = itrev l [] ++ acc.
proof: Proof. induction l as [| h t IH]. - auto. - intro acc. simpl. rewrite IH. pattern (itrev t [h]). rewrite IH. rewrite <- List.app_assoc. reflexivity. Qed.
imports: Hammer(Tactics) Hammer(Hints)