From ec932e389bc0f509069597c094d3feafd129672c Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 29 Apr 2022 12:30:45 -0700
Subject: [PATCH] chore: fix test

---
 tests/lean/rwEqThms.lean.expected.out | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tests/lean/rwEqThms.lean.expected.out b/tests/lean/rwEqThms.lean.expected.out
index b16aade4ee..2a26f39731 100644
--- a/tests/lean/rwEqThms.lean.expected.out
+++ b/tests/lean/rwEqThms.lean.expected.out
@@ -4,7 +4,7 @@ as bs : List α
 h : bs = a :: as
 ⊢ List.length (?a_1 :: as) = List.length bs
 
-case a_1
+case a
 α : Type ?u
 a : α
 as bs : List α