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

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