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

--- output ---
Axioms:
classic : forall P : Prop, P \/ ~ P