∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : PartialOrder β] [inst_2 : LocallyFiniteOrder α]
  [inst_3 : LocallyFiniteOrder β] [inst_4 : DecidableLE (α × β)] (a b : α) (c : β),
  Finset.map (Function.Embedding.sectL α c) (Finset.Icc a b) = Finset.Icc (a, c) (b, c)