In `aesop`, this seems to be handled by [`traceScript`](https://github.com/leanprover-community/aesop/blob/c51fa8ea4de8b203f64929cba19d139e555f9f6b/Aesop/Search/Main.lean#L152) Related files: - [`Script.lean`](https://github.com/leanprover-community/aesop/blob/master/Aesop/Script.lean) - [`Tree/ExtractScript.lean`](https://github.com/leanprover-community/aesop/blob/master/Aesop/Tree/ExtractScript.lean)
