{α : Type u_3} →
  [inst : Preorder α] →
    [inst_1 : PredOrder α] →
      {motive : IsPredArchimedean α → Sort u} →
        (t : IsPredArchimedean α) →
          ((exists_pred_iterate_of_le : ∀ {a b : α}, a ≤ b → ∃ n, Order.pred^[n] b = a) → motive ⋯) → motive t