∀ {α : Type u_1} {r : α → α → Prop} [inst : DecidableRel r] [IsTrans α r] {as bs : List α} (x : α),
  as.Sublist bs → List.Pairwise r bs → (List.orderedInsert r x as).Sublist (List.orderedInsert r x bs)