1. 1
2. 2
3. 3
4. 4
5. 5
6. 6
7. 7

From Stdlib Require Import List.
From Hammer Require Import Hammer.
Import ListNotations.

Goal (forall A (l : list A), rev (rev l) = l).
  hammer.
Qed.