From b58eac501340b2d6c56a40c2ce3c888e9dd135ab Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 2 Jun 2016 11:26:53 -0700 Subject: [PATCH] chore(tests/lean/extra): fix test --- tests/lean/extra/bag.661.20.expected.out | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) 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₂