∀ {α : Type u_1} (r : α → α → Prop) [inst : DecidableRel r] [IsTrans α r] [Std.Antisymm r] [Std.Total r]
  (x x_1 : List α),
  (List.isSetoid α) x x_1 → (x.mergeSort fun x1 x2 => decide (r x1 x2)) = x_1.mergeSort fun x1 x2 => decide (r x1 x2)