diff --git a/tests/lean/extra/bag.661.20.expected.out b/tests/lean/extra/bag.661.20.expected.out
index be03a4bc1..e3315427e 100644
--- a/tests/lean/extra/bag.661.20.expected.out
+++ b/tests/lean/extra/bag.661.20.expected.out
@@ -2,15 +2,13 @@ LEAN_INFORMATION
 position 661:20
 A : Type,
 decA : decidable_eq A,
-all_of_subcount_eq_tt :
-  ∀ {l₁ l₂ : list A},
-    subcount l₁ l₂ = tt → (∀ (a : A), list.count a l₁ ≤ list.count a l₂),
+all_of_subcount_eq_tt : ∀ {l₁ l₂}, subcount l₁ l₂ = tt → (∀ a, list.count a l₁ ≤ list.count a l₂),
 a : A,
 l₁ l₂ : list A,
 h : subcount (a :: l₁) l₂ = tt,
 x : A,
 this : subcount l₁ l₂ = tt,
-ih : ∀ (a : A), list.count a l₁ ≤ list.count a l₂,
+ih : ∀ a, list.count a l₁ ≤ list.count a l₂,
 i : list.count a (a :: l₁) ≤ list.count a l₂,
 this : x = a
 ⊢ list.count x (a :: l₁) ≤ list.count x l₂