diff --git a/tests/lean/eta_bug.lean.expected.out b/tests/lean/eta_bug.lean.expected.out index acdb9c4c2..6ce8ac64d 100644 --- a/tests/lean/eta_bug.lean.expected.out +++ b/tests/lean/eta_bug.lean.expected.out @@ -1 +1 @@ -λ (A : Type) (x y : A) (H₁ : x = y) (H₂ : y = x), eq.trans H₁ H₂ +λ (A : Type) (x y : A) (H₁ : x = y) (H₂ : y = x), eq.rec H₁ H₂