∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] (f : CauSeq α abs)
  (motive : (∃ r, ∀ (i : ℕ), |↑f i| < r) → Prop) (x : ∃ r, ∀ (i : ℕ), |↑f i| < r),
  (∀ (K : α) (H : ∀ (i : ℕ), |↑f i| < K), motive ⋯) → motive x