Needing help with call_with_depth_limit/3

@j4n_bur53 , unfortunately, there is a bug in your program:

show((![X]:f(X) => ![Y]:g(Y)) => (?[X]: ![Y]: (f(X) => g(Y)))).
\begin{prooftree}\AxiomC{}
\RightLabel{Ax}\UnaryInfC{
ERROR: Domain error: `variable_name' expected, found `'[''
ERROR: In:
ERROR:   [20] write_term(f(a),[variable_names(...)])
ERROR:   [19] render_list([f(...)],['X'=_842,...|...])

Probably easy to fix for you, but too difficult for me. :frowning: