{α : Type u_1} →
  {β : Type u_2} →
    (r : Setoid α) →
      (s : Setoid β) →
        (motive : Quotient r × Quotient s → Sort u_3) →
          (x : Quotient r × Quotient s) → ((x : Quotient r) → (y : Quotient s) → motive (x, y)) → motive x