From the list chapter in the Coq book.

app_ass4

(* There is a short solution to the next exercise. 
If you find yourself getting tangled up, step back and try to look for a simpler way. *)

Theorem app_ass4 :  forall l1 l2 l3 l4 : natlist,
  l1 ++ (l2 ++ (l3 ++ l4)) = ((l1 ++ l2) ++ l3) ++ l4.
Proof.
  intros l1 l2 l3 l4.
  Theorem app_right : forall l1 l2 l3 : natlist,
  l1 ++ (l2 ++ l3) = (l1 ++ l2) ++ l3.
  Proof. 
    intros l1 l2 l3.
    induction l1 as [|h1 t1]. reflexivity. 
    simpl. rewrite -> IHt1. reflexivity.
  Qed. 
  rewrite <- app_right. rewrite app_right. reflexivity. 
Qed.