diff --git a/actris/examples/map_reduce.v b/actris/examples/map_reduce.v
index 479401be9e970403a1543384d60cc69eaeec72b1..5da7132fce93da68332a964ecc174876ea4f6b5a 100644
--- a/actris/examples/map_reduce.v
+++ b/actris/examples/map_reduce.v
@@ -211,7 +211,7 @@ Section mapper.
       inversion 1 as [|?? [? _]]; discriminate_list || simplify_list_eq.
       assert (RZB (j',y') (i,y'')) as [??]; last (simpl in *; lia).
       apply (Sorted_StronglySorted _) in Hsort.
-      eapply elem_of_StronglySorted_app; set_solver.
+      eapply StronglySorted_app; set_solver.
   Qed.
 
   Lemma par_map_reduce_reduce_spec n iys iys_sorted miy zs l Y csort cred :