Notation "x :: l" := (cons x l) (at level 60, right associativity).
Notation "[ ]" := nil.
Notation "[ x , .. , y ]" := (cons x .. (cons y nil) ..).

Fixpoint map {X Y:Type} (f:X->Y) (l:list X) : (list Y) :=
  match l with
  | [] => []
  | h::t => (f h)::(map f t)
  end.

Fixpoint snoc {X:Type} (l:list X) (v:X) : list X :=
  match l with
  | [] => [v]
  | h::t => h::(snoc t v)
  end.

Fixpoint rev {X:Type} (l:list X) : list X :=
  match l with
  | [] => l
  | h::t => snoc (rev t) h
  end.

Theorem map_rev: forall (X Y:Type) (f:X->Y) (l:list X),
  map f (rev l) = rev (map f l).

(* Enter your proof here. *)