proposition: Lemma lem_rev_app {A} : forall l1 l2 : list A, rev (l1 ++ l2) = rev l2 ++ rev l1.
proof: Proof. unfold rev. induction l1 as [| x l1 IH]; intro l2. - simpl. rewrite List.app_nil_r. reflexivity. - simpl. rewrite lem_itrev. rewrite IH. rewrite <- List.app_assoc. rewrite (lem_itrev l1 [x]). reflexivity. Qed.
imports: Hammer(Tactics) Hammer(Hints)