∀ {α : Sort uA} {β : Sort uB} {s₁ : Setoid α} {s₂ : Setoid β} {motive : Quotient s₁ → Quotient s₂ → Sort uC}
  [s : ∀ (a : α) (b : β), Subsingleton (motive ⟦a⟧ ⟦b⟧)] (q₁ : Quotient s₁) (q₂ : Quotient s₂)
  (g g_1 : (a : α) → (b : β) → motive ⟦a⟧ ⟦b⟧),
  g = g_1 → Quotient.recOnSubsingleton₂ q₁ q₂ g = Quotient.recOnSubsingleton₂ q₁ q₂ g_1