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

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