∀ {X : Type u_1} {I : Type u_2} (U : Set X) (motive : ↑(U ×ˢ Set.univ) → Prop) (x : ↑(U ×ˢ Set.univ)),
  (∀ (x : X) (i : I) (hx : (x, i).1 ∈ U) (right : (x, i).2 ∈ Set.univ), motive ⟨(x, i), ⋯⟩) → motive x