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

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