λ A x y H₁ H₂, eq.rec H₁ H₂