proposition: Lemma lem_itrev' {A} : forall l acc : list A, itrev l acc = itrev l [] ++ acc.
proof: Proof. induction l; ssimpl. rewrite IHl. pattern (itrev l [a]). rewrite IHl. sauto db: slist. Restart. induction l as [|x l ?]; simpl. - sauto. - assert (itrev l [x] = itrev l [] ++ [x]) by sauto. sauto db: slist. Qed.
imports: Hammer(Tactics) Hammer(Hints)