List.attach 使用例

Zulip: How to make this recursion (?) work?

mutual
  inductive Value: Type where
  | function: ℕ → Expression → Value

  inductive Expression where
  | fun_apply: Expression → List Expression → Expression
end

def List.Exists {A} (L: List A) (P: A → Prop): Prop :=
  match L with
  | List.nil => False
  | x :: t => P x ∨ t.Exists P

def freeVariable (n: ℕ) (exp: Expression): Prop :=
  match exp with
  | Expression.fun_apply f L => freeVariable n f ∨ List.Exists L.attach (fun ⟨e, _⟩ => freeVariable n e)

Start with the linked Zulip discussion and the Lean snippet in the issue, focusing on List.attach and the recursive freeVariable definition. Determine how this example can be expressed correctly, then document a working List.attach usage example in the repository; done means the recursion and attached-list traversal are accepted by Lean.