prove "bind" function is total

Stream: lean4

[Locria Cyber]

def extract [Pure ε] [Bind ε] : (stacked: Eff [ε] α) -> ε α
| Free.pure x => pure x
| Free.bind val cont => bind (simplify val) (λ a => extract (cont a))

the compiler says

fail to show termination for
  Eff.extract
with errors
argument #5 was not used because its type is an inductive family and indices are not variables
  Free (Union [ε]) α

structural recursion cannot be used

failed to prove termination, use `termination_by` to specify a well-founded relation

[Simon Hudon]

Can you show the definition of Eff?

[Locria Cyber]

I solved it. It cannot be proved.

[Locria Cyber]

(mcont a') should be smaller than val, which is mk (FreeView.bind mval mcont)

[Simon Hudon]

Does the termination_by line fix your issue?