How to get `termination_by` to target param in pattern match

Stream: new members

[nrs]

inductive Tree (a : Type) : Type where
  | node : (val: a) -> List (Tree a) -> Tree a

namespace Tree

  def all (p : α -> Bool) : Tree α -> Bool
  | node val [] => p val
  | node val treeList => p val && treeList.all (all p)

I'm trying to prove termination for the above function. I know I need to use termination_by followed by decreasing_by, but the argument I'm trying to make is that treeList will be smaller each call. How do I pass treeList.length to termination_by to even begin my argument?

[nrs]

update:

you can use this:

  termination_by t => let extList : Tree a -> List (Tree a)
    | node val treeList => treeList
  (extList t).length

update2:

this is also nice:

termination_by t => t |> (fun | node val treeList => treeList.length)

update3:
turns out there's no way to prove this, using this particular definition of Tree

edit: I was wrong, there is a way to prove this by virtue of lean's type theory implying that Tree must be wellfounded, thanks to Mario Carneiro