diff --git a/theories/logrel/examples/pair.v b/theories/logrel/examples/pair.v
index 77074ab3da3e301548da9ff8b1199d37d6ca6c44..427c357259b1aa52a5bf5388582bef2970348695 100644
--- a/theories/logrel/examples/pair.v
+++ b/theories/logrel/examples/pair.v
@@ -11,6 +11,8 @@ Section pair.
   Proof.
     rewrite /prog.
     iApply ltyped_lam. iApply ltyped_pair.
-    iApply ltyped_recv. iApply ltyped_recv.
+    iApply ltyped_recv.
+    2:{ iApply ltyped_recv. by rewrite /binder_insert lookup_insert. }
+    by rewrite lookup_insert.
   Qed.
 End pair.