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

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