A bit of comments on the demonic choice

theories/examples/or.v

-(* We can simulate non-determinism with concurrency.
-   In this file we derive the algebraic laws for parallel "or"/demonic choice  combinator. *)
+(* (In)equational theory of erratic choice.
+
+   We can simulate (binary) non-determinism with concurrency. In this
+   file we derive the algebraic laws for parallel "or"/demonic choice
+   combinator. In particular, we show the following (≤ stands for
+   contextual refinement and ≃ stands for contextual equivalence):
+
+   - v or v ≃ v ()           idempotency
+   - v1 or v2 ≃ v2 or v1     commutativity
+   - v or (λ_, ⊥) ≃ v ()     ⊥ is a unit
+   - v1 or (λ_, v2 or v3)     associativity
+     ≃ (λ_, v1 or v2) or v3
+   - v1 () ≤ v1 or v2        choice on the RHS
+*)
 From iris.proofmode Require Import tactics.
-From iris_logrel Require Export logrel examples.various.
+From iris_logrel Require Export logrel examples.various (* for bot *).
 
 Definition or : val := λ: "e1" "e2",
   let: "x" := ref #0 in