diff --git a/theories/examples/sort.v b/theories/examples/sort.v
index 66ed64e7bf62ace1875a99523236c4ce7ffab7f2..3e30eb95eb73eb7ea4ff876ea6f2c38c0215ebf1 100644
--- a/theories/examples/sort.v
+++ b/theories/examples/sort.v
@@ -45,8 +45,7 @@ Definition sort_client_func : val := λ: "cmp" "xs",
 Section sort.
   Context `{!heapG Σ, !proto_chanG Σ}.
 
-  Definition sort_protocol {A} (I : A → val → iProp Σ) (R : A → A → Prop)
-      `{!RelDecision R, !Total R} : iProto Σ :=
+  Definition sort_protocol {A} (I : A → val → iProp Σ) (R : A → A → Prop) : iProto Σ :=
     (<!> (xs : list A) (l : loc), MSG #l {{ llist I l xs }};
      <?> (xs' : list A), MSG #() {{ ⌜ Sorted R xs' ⌝ ∗ ⌜ xs' ≡ₚ xs ⌝ ∗ llist I l xs' }};
      END)%proto.