Run on the at.alkalam.org runner (the site's own Rocq tool), 2026-09-30 $ rocq --version The Rocq Prover, version 9.3.0 compiled with OCaml 4.14.2 $ shasum -a 256 ImkanComplete.v 701576250d40f4b314bd5431f550517394cb27eb8f566a26ca6dd97dc12b0222 ImkanComplete.v $ rocq compile -q ImkanComplete.v Axioms: classic : forall P : Prop, P \/ ~ P Closed under the global context Closed under the global context Closed under the global context Closed under the global context Closed under the global context Closed under the global context Closed under the global context Closed under the global context Closed under the global context Closed under the global context Closed under the global context Closed under the global context Closed under the global context Closed under the global context Closed under the global context Closed under the global context Closed under the global context Closed under the global context Closed under the global context Closed under the global context Closed under the global context Closed under the global context Closed under the global context Closed under the global context Closed under the global context Closed under the global context Closed under the global context Closed under the global context Closed under the global context Axioms: classic : forall P : Prop, P \/ ~ P Closed under the global context Axioms: classic : forall P : Prop, P \/ ~ P Closed under the global context Closed under the global context Closed under the global context Closed under the global context Closed under the global context Closed under the global context Axioms: classic : forall P : Prop, P \/ ~ P Closed under the global context Closed under the global context Closed under the global context Closed under the global context Closed under the global context Axioms: classic : forall P : Prop, P \/ ~ P Axioms: classic : forall P : Prop, P \/ ~ P Closed under the global context Closed under the global context Closed under the global context Closed under the global context Closed under the global context Closed under the global context Closed under the global context Closed under the global context Closed under the global context Closed under the global context Axioms: classic : forall P : Prop, P \/ ~ P Axioms: classic : forall P : Prop, P \/ ~ P Closed under the global context Closed under the global context Closed under the global context Axioms: classic : forall P : Prop, P \/ ~ P Axioms: classic : forall P : Prop, P \/ ~ P Closed under the global context Closed under the global context Closed under the global context Axioms: classic : forall P : Prop, P \/ ~ P Closed under the global context Closed under the global context exit code: 0