∀ {ι : Type u_1} {β : ι → Type u_2} [inst : (i : ι) → PartialOrder (β i)] (a : Lex ((i : ι) → β i))
  (motive : (∃ b, b < ofLex a) → Prop) (x : ∃ b, b < ofLex a),
  (∀ (w : (i : ι) → β i) (hb : w < ofLex a), motive ⋯) → motive x