Function build_proof 

pub fn build_proof(node: &Node, env: &Env) -> Node

Build a derivation tree witnessing how node reduces under env. Returns a Node::List of the form (by <rule> <subderivation>...).

The walker mirrors the structural cases of eval_node: definitions and configuration directives become leaf witnesses, infix and prefix operators become rule applications whose subderivations recurse through build_proof, and equality picks assigned-equality / structural-equality / definitional-equality / numeric-equality (and the negated counterparts) based on the same lookups eval_node performs — delegating to classify_equality_rule so both the proof witness and the per-query provenance agree on which layer fired.