∀ {ι : Type u_1} {R : Type u_2} {S : Type u_3} [inst : SetLike S R] {A : ι → S} {a b : R}
  (motive : SetLike.IsHomogeneousElem A a → SetLike.IsHomogeneousElem A b → Prop) (x : SetLike.IsHomogeneousElem A a)
  (x_1 : SetLike.IsHomogeneousElem A b), (∀ (i : ι) (hi : a ∈ A i) (j : ι) (hj : b ∈ A j), motive ⋯ ⋯) → motive x x_1