∀ {α : Type u_1} (x : ℕ) (x_1 : List α),
  List.sym x x_1 =
    match x, x_1 with
    | 0, x => [Sym.nil]
    | x, [] => []
    | n.succ, x :: xs => List.map (fun p => x ::ₛ p) (List.sym n (x :: xs)) ++ List.sym (n + 1) xs