∀ {α : Type u_1} [inst : DistribLattice α] (a b : α) (J : Order.Ideal α) (motive : (∃ j ∈ J, b ≤ j ⊔ a) → Prop)
  (x : ∃ j ∈ J, b ≤ j ⊔ a), (∀ (j : α) (hj : j ∈ J) (hbja : b ≤ j ⊔ a), motive ⋯) → motive x