The Rocq Prover, version 9.3.0
command: coqc -q pr004_no_two_step_giving.v
exit code: 0
sha256(pr004_no_two_step_giving.v): 9355af1975a36a48a559be62b6825cbc8084e4cc430b8b1b0b80c1381a1c2e9b
date: 2026-10-01

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