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): 76422fec777f15284751d62e06e47cc6e10b84c52be27006c899f7e044ee0f89
date: 2026-10-02

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