Lines marked ▸ have a proof. The highlight is the code the current goal is about.
tracer/regen_traces.shGoal-first: start from what we want to show, then pick the one rule whose conclusion has the goal's form
The goal sits at the bottom. Each line is one rule instance: its premises are above the line, its name to the right, its conclusion below. Dashed goals are still open.