update expected output
diff --git a/tests/lean/funind_errors.lean.expected.out b/tests/lean/funind_errors.lean.expected.out
index 78c2416..9f2e2aa 100644
--- a/tests/lean/funind_errors.lean.expected.out
+++ b/tests/lean/funind_errors.lean.expected.out
@@ -6,11 +6,11 @@
 takeWhile.foo.induct.{u_1} {α : Type u_1} (p : α → Bool) (as : Array α) (motive : Nat → Array α → Prop)
   (case1 :
     ∀ (i : Nat) (r : Array α) (h : i < as.size),
-      let a := as.get ⟨i, h⟩;
+      let a := as.get i h;
       p a = true → motive (i + 1) (r.push a) → motive i r)
   (case2 :
     ∀ (i : Nat) (r : Array α) (h : i < as.size),
-      let a := as.get ⟨i, h⟩;
+      let a := as.get i h;
       ¬p a = true → motive i r)
   (case3 : ∀ (i : Nat) (r : Array α), ¬i < as.size → motive i r) (i : Nat) (r : Array α) : motive i r
 funind_errors.lean:38:7-38:20: error: invalid field notation, type is not of the form (C ...) where C is a constant