∀ {α : Type u_1} (x head : List α) (tail : List (List α)),
  x ++ (List.map (fun x_1 => x_1 ++ x) tail).flatten = (List.map (fun x_1 => x ++ x_1) tail).flatten ++ x →
    x ++ (List.map (fun x_1 => x_1 ++ x) (head :: tail)).flatten =
      (List.map (fun x_1 => x ++ x_1) (head :: tail)).flatten ++ x