One step in the decision of a quantified statement: the statement that was decided, the
rule that decided it, the verdict, and how deep it sits under the statement asked --
the base case of an induction is one below the induction, the identity that settles the
step one below that. The rule is named as the reference names it and as a checker
would: Lemma is the Lean 4 tactic or lemma the step corresponds to, which
is what an export to a proof checker needs and the design constraint of
#746's proof engine.
#1409