proposition: Lemma lem_rev_rev {A} : forall l : list A, rev (rev l) = l.
proof: Proof. unfold rev. induction l as [| x l IH]. - reflexivity. - simpl. rewrite (lem_itrev l [x]). generalize (lem_rev_app (itrev l []) [x]). unfold rev. intro H. rewrite H. rewrite IH. reflexivity. Qed.
imports: Hammer(Tactics) Hammer(Hints)