Lean4
/-- Recursion on two `Quotient` arguments `a` and `b`, result type depends on `⟦a⟧` and `⟦b⟧`. -/
protected def hrecOn₂ (qa : Quot ra) (qb : Quot rb) (f : ∀ a b, φ ⟦a⟧ ⟦b⟧)
(ca : ∀ {b a₁ a₂}, ra a₁ a₂ → f a₁ b ≍ f a₂ b) (cb : ∀ {a b₁ b₂}, rb b₁ b₂ → f a b₁ ≍ f a b₂) : φ qa qb :=
Quot.hrecOn (motive := fun qa ↦ φ qa qb) qa (fun a ↦ Quot.hrecOn qb (f a) (fun _ _ pb ↦ cb pb)) fun a₁ a₂ pa ↦
Quot.induction_on qb fun b ↦
have h₁ : @Quot.hrecOn _ _ (φ _) ⟦b⟧ (f a₁) (@cb _) ≍ f a₁ b := by simp
have h₂ : f a₂ b ≍ @Quot.hrecOn _ _ (φ _) ⟦b⟧ (f a₂) (@cb _) := by simp
(h₁.trans (ca pa)).trans h₂
