Empty list is right identity for append

import Mathlib

theorem list_append_nil {α : Type} (l : List α) : l ++ [] = l :=
  List.rec rfl (fun x _ => congrArg (List.cons x)) l