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