∀ {α : Type u_1} [inst : Preorder α] (p : α → Prop) [inst_1 : DecidablePred p] [inst_2 : LocallyFiniteOrderTop α]
  (a : Subtype p),
  (∀ ⦃a x : α⦄, a ≤ x → p a → p x) → Finset.map (Function.Embedding.subtype p) (Finset.Ici a) = Finset.Ici ↑a