∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] {f g : CauSeq α abs}
  (w w_1 : α) (x : ℕ) (motive : w ≤ ↑f x ∧ w_1 ≤ ↑g x → Prop) (x_1 : w ≤ ↑f x ∧ w_1 ≤ ↑g x),
  (∀ (h₁ : w ≤ ↑f x) (h₂ : w_1 ≤ ↑g x), motive ⋯) → motive x_1