diff --git a/theories/examples/or.v b/theories/examples/or.v
index 080b9ff173f33e56d3b8d6ba338cc99428f0378e..a794d2abd5e0a938cf1550ccede01f6c654df1f6 100644
--- a/theories/examples/or.v
+++ b/theories/examples/or.v
@@ -96,7 +96,7 @@ Section rules.
   Qed.
 
   (** Choice on the RHS *)
-  Lemma or_choice_1_r (e1 e1' e2 : val) A :
+  Lemma or_choice_1_r (e1 e1' e2 : expr) A :
     (REL e1 << e1' : A) -∗
     REL e1 << (e1' ⊕ e2)%V : A. (* TODO: in the value scope *)
   Proof.