* [args] : stuff to substitute
* [map_arg] : map the argument to obtain a term
* the function is ReductionStrategy.from_env_for_unwind when psubst is
* [args] : stuff to substitute
* [map_arg] : map the argument to obtain a term
* the function is ReductionStrategy.from_env_for_unwind when psubst is