diff --git a/theories/typing/own.v b/theories/typing/own.v
index 4750061072d287242aa040b3be3a51eb8c91e21f..f14a983cad86e5f073e097777be0682c7a7eb257 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -38,7 +38,7 @@ Section own.
     - by rewrite left_id shift_loc_0.
     - by rewrite right_id Nat.add_0_r.
     - iSplit. by iIntros "[[]?]". by iIntros "[]".
-    - rewrite hist_freeable_op_eq. f_equiv.
+    - rewrite hist_freeable_op_eq. f_equiv; [|done..].
       by rewrite -Qp_div_add_distr pos_to_Qp_add -Nat2Pos.inj_add.
   Qed.