ch:proof-tactics: proof-producing tactic replay

Problem and invariant. Represent each open goal exactly once and store a validation that consumes one proof for each listed goal. A successful empty state must contain a closed proof of the original proposition.

Representation and construction. Use finite proposition and proof-term datatypes, a goal list, and a validation syntax rather than a host-language closure. Implement introduction, splitting, assumption, sequencing, and left-biased choice. Sequencing recursively runs the second tactic on every first-stage goal and builds the matching validation tree; replay checks each constructor before evaluating the validation.

Observable result and mutation. The exact four-line run is the corresponding transcript in Appendix E. Then change sequencing to return after its first generated goal. The mutant still checks, but bad-drop becomes accepted: invalid-drop and the test fails.

Acceptance and boundary. Run check, test, run, and audit; require the recorded transcript and the accepted source record in Appendix E. Require audit []. Restore and rerun after mutation. The program checks finite validation bookkeeping and proves no tactic or kernel theorem.