∀ {α : Sort u_2} {β : Sort u_3} {ra : α → α → Prop} {rb : β → β → Prop} {φ : Quot ra → Quot rb → Sort u_1}
  (f : (a : α) → (b : β) → φ (Quot.mk ra a) (Quot.mk rb b)) (cb : ∀ {a : α} {b₁ b₂ : β}, rb b₁ b₂ → f a b₁ ≍ f a b₂)
  (a₂ : α) (b : β), f a₂ b ≍ Quot.hrecOn (Quot.mk rb b) (f a₂) ⋯