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 KalimaComplete.v 6a17293509c82ecc1a4e60040f89ca29bc898cf02654553ed853bbb23dae06af KalimaComplete.v $ rocq compile -q KalimaComplete.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 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 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 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 Axioms: classic : forall P : Prop, P \/ ~ P 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 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 Axioms: classic : forall P : Prop, P \/ ~ P Axioms: classic : forall P : Prop, P \/ ~ P exit code: 0