diff --git a/theories/typing/function.v b/theories/typing/function.v
index 7de88219f9a77fd295b3a9905a177eb1fabd19a2..b374b1cefcd2da2735ecafa5d47be9aad2851078 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -357,7 +357,7 @@ Section typing.
     ⊢ typed_body E L C T (call: p ps → k).
   Proof.
     intros Hfn HL HE HTT' HC HT'T''.
-    rewrite -typed_body_mono /flip; last done; first by eapply type_call'.
+    iApply typed_body_mono; [| |done|by iApply type_call']; simpl.
     - etrans.
       + eapply (incl_cctx_incl _ [_]); by intros ? ->%elem_of_list_singleton.
       + apply cctx_incl_cons; first done. intros args. by inv_vec args.