Improve Equations wf discussing subterm relation

[thomas-lamiaux]

Currently, the subterm relation is not discussed in the tutorial about Equations and well-founded recursion, as at the moment of writing we were lacking a good example. Once, one is found, it would be good to do so.

[thomas-lamiaux]

I was thinking about a simple MLTT like theory

Inductive term : Type := 
| tVar : nat -> term 
| tApp : term -> list term -> term 
| tAbs : string -> term 
| tProd : string -> term -> term 
| tUniv : nat -> term 

and computing sth on it that would require rec call on the args of the app. Sth of the form

Fixpoint foo (t : term) : ??? := 
match t with 
| tApp u lv => fold_right ??? (map foo lv)
end.

EDIT: it didn't work

What do you think @MevenBertrand ?