The Rocq Prover, version 9.2, with coq-hammer-tactics 1.3.3+9.2
command: rocq compile -q pr004_no_two_step_giving.v
exit code: 0
sha256(pr004_no_two_step_giving.v): 3686a27bf55cb5323395ad2c07629e61301dd6839f2aba82c38a6e62e5b7c6c9
date: 2026-10-02

--- output ---
Closed under the global context