A scope that collects the steps by which the quantified statements decided inside it were
decided, the way RewriteRecording collects rewrites: the proof of
forall n in ZZ+ : sum(k, k, 1, n) = n (n + 1)/2 is the closed form read through
its case, the proof of forall n in ZZ+ : sum(1/(k (k + 1)), k, 1, n) = n/(n + 1) is a base case and a step, each a step here. Nothing is collected outside a scope, and
the ordinary path does not pay for one nobody opened. A decision already made is not
made again: an entity whose Evaled is cached, or a statement parsed
through the parser's cache and evaluated before, records nothing, so a proof is asked of
a fresh entity (FromString(System.String,System.Boolean) with the cache off).

using var proof = ProofRecording.Start();
var verdict = "forall n in ZZ+ : sum(1/(k (k + 1)), k, 1, n) = n/(n + 1)".ToEntity().Evaled;
foreach (var step in proof.Steps)
    Console.WriteLine(step);