diff --git a/tests/lean/interactive/533.lean.expected.out b/tests/lean/interactive/533.lean.expected.out
index 277babe388..bde72f33e9 100644
--- a/tests/lean/interactive/533.lean.expected.out
+++ b/tests/lean/interactive/533.lean.expected.out
@@ -11,6 +11,10 @@
    "kind": 7,
    "detail":
    "(Type u₁ → Type u₂) → Type u → outParam (Type v) → Type (max (max (max u (u₁ + 1)) u₂) v)"},
+  {"label": "ForIn'",
+   "kind": 7,
+   "detail":
+   "(Type u₁ → Type u₂) →\n  (ρ : Type u) → (α : outParam (Type v)) → [d : outParam (Membership α ρ)] → Type (max (max (max u (u₁ + 1)) u₂) v)"},
   {"label": "ForInStep", "kind": 22, "detail": "Type u → Type u"},
   {"label": "ForM",
    "kind": 7,