Definitely.

map_can_fuse.v

Require Import List.

Definition compose (A B C : Set) (f : B -> C) (g : A -> B) : (A -> C) :=
  fun x => f (g x).

Notation "f @ g"  := (compose _ _ _ f g) (at level 50).

Fixpoint map (A B : Set) (f : A -> B) (az : list A) : list B :=
  match az with
  | nil    => nil
  | h :: t => f h :: map _ _ f t
  end.

Implicit Arguments map [A B].

Lemma map_can_fuse
  : forall A B C : Set
  , forall lst   : list A
  , forall f     : B -> C
  , forall g     : A -> B,
    
    (map f @ map g) lst = map (f @ g) lst.

Proof.
  intros. 
  unfold compose.
  induction lst.
    (* assume list is nil *)
    simpl.
    trivial.
    
    (* assume hypothesis IHlst that prop holds for list "l",
       set goal to prove that it holds for e :: l
    *)
    simpl.
    rewrite IHlst.
    trivial.
Qed.

(* just a concretized version of the map_can_fuse *)
Lemma test1 : 
  let lst : list nat := 1 :: 2 :: 3 :: 4 :: nil in
  let inc (x : nat) : nat := x + 1 in
  let x2  (x : nat) : nat := x * 2 in

    (map inc @ map x2) lst = map (inc @ x2) lst.

Proof.
  unfold compose.
  unfold map.
  reflexivity.
Qed.

Lemma compose_is_associative
  : forall A B C D : Set
  , forall f       : C -> D
  , forall g       : B -> C
  , forall h       : A -> B,

    (f @ g) @ h = f @ (g @ h).

Proof.
  unfold compose. trivial.
Qed.