proposition: Lemma lem_rev_rev' {A} : forall l : list A, rev (rev l) = l.
proof: Proof. induction l as [|x l ?]. - reflexivity. - sauto use: (lem_itrev l [x]), (lem_rev_app (itrev l []) [x]) unfold: rev. Qed.
imports: Hammer(Tactics) Hammer(Hints)