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

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