syntax_data: {"ast_node_type":"other","tokens":[{"end":74,"kind":"keyword","start":0,"text":"//!"}]}
source_snippet: //! and we discard inference progress via "probes", we cannot mechanically
context_before: //! Because each nested goal in the solver gets [canonicalized] separately
context_after: //! use proof trees without somehow "lifting up" data local to the current