proposition: Lemma map_rev : forall (A B : Type) (f : A -> B) (l : list A), map f (rev l) = rev (map f l).
proof: Proof. intros A B f l; elim l; simpl in |- *; auto. intros a l0 H'; rewrite <- H'; simpl in |- *; auto. apply trans_equal with (y := map f (rev l0) ++ map f (a :: nil)); auto. apply map_app; auto. Qed.
imports: Coq(List)