I was working on defining formal semantics. I would like to write a function, that computes the list of the variables used in an expression (for the sake of simplicity, in the example code, only empty list, variable and map constructions are present). I’m having problems with the map constructor. When I try to define this function with fmap/map or mutual recursion (as seen in variables2 below) I get an ill-formed recursion error. The only way I was able to construct such a function was with inline fix (as seen in variables).
Inductive Expression : Type := | EEmptyList | EVar (s : string) | EMap (l : list (Expression * Expression)). Fixpoint variables (e : Expression) : list string := match e with | EEmptyList =>  | EVar x => [x] | EMap l => (fix fp l := match l with |  =>  | (a,b)::xs => app (app (variables a) (variables b)) (fp xs) end) l end. Fixpoint variables2 (e : Expression) : list string := match e with | EEmptyList =>  | EVar x => [x] | EMap l => fp l end with fp l := match l with |  =>  | (a, b)::xs => app (app (variables2 a) (variables2 b)) (fp xs) end.
How should I modify the definition of variables2 not to get this error?
Thanks in advance!