∀ {α : Type u_1} {r : α → α → Prop} [inst : DecidableRel r] [inst_1 : DecidableEq α] [Std.Refl r] (x head : α)
  (tail : List α),
  (List.orderedInsert r x tail).erase x = tail → (List.orderedInsert r x (head :: tail)).erase x = head :: tail