diff --git a/coq-lambda-rust.opam b/coq-lambda-rust.opam
index db0fc708086aba2dbd391fff08f50949ab899886..d8d0d4ed182566e45cfa32d64d4a937253841e9e 100644
--- a/coq-lambda-rust.opam
+++ b/coq-lambda-rust.opam
@@ -13,7 +13,7 @@ the type system, and safety proof for some Rust libraries.
 """
 
 depends: [
-  "coq-iris" { (= "dev.2022-08-03.0.949ab7bc") | (= "dev") }
+  "coq-iris" { (= "dev.2022-08-11.1.c9223a52") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/typing/function.v b/theories/typing/function.v
index 4111d6e4738ba92393b769259a873ee7b74f32ef..7de88219f9a77fd295b3a9905a177eb1fabd19a2 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -95,7 +95,7 @@ Section fn.
       { intros Hprop. apply Hprop, list_fmap_ne; last first.
         - symmetry. eapply Forall2_impl; first apply Hfp. intros.
           apply dist_later_dist, type_dist2_dist_later. done.
-        - apply _. }
+        - solve_proper. }
       clear. intros n tid p i x y. rewrite list_dist_lookup=>/(_ i).
       case _ : (x !! i)=>[tyx|]; case  _ : (y !! i)=>[tyy|];
         inversion_clear 1; [solve_proper|done].
diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index a597e9b3c0a50be09c023f5e0ebcf62ae3cefd5c..b9049edcb6835b20ddaab3179e19414202357362 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -368,7 +368,7 @@ Section code.
                                (?&?&[=]&?)]]; first done. setoid_subst.
         iDestruct "Hproto" as (q'') "(Hl1 & Hl2 & Hl† & >Hqq' & Hν & Hν†)".
         iDestruct "Hqq'" as %Hqq'. wp_read. iApply "HΦ". iFrame "Hl1". iRight.
-        iSplit; first by rewrite !pos_op_plus; auto with lia. iSplit; iIntros "H↦".
+        iSplit; first by rewrite !pos_op_add; auto with lia. iSplit; iIntros "H↦".
         * iMod ("Hclose" with "[- Htok Hν1]") as "$"; last by auto 10 with iFrame.
           iFrame. iExists _. iFrame. auto with iFrame.
         * iMod (own_update_2 with "Hst Htok") as "Hst".
@@ -378,7 +378,7 @@ Section code.
           iApply "Hclose". iFrame. iExists _. iFrame. iExists (q+q'')%Qp. iFrame.
           iSplitL; first last.
           { rewrite [(_+_)%Qp]assoc [(q'+_)%Qp]comm. auto. }
-          rewrite pos_op_plus Z.sub_1_r -Pos2Z.inj_pred; last lia.
+          rewrite pos_op_add Z.sub_1_r -Pos2Z.inj_pred; last lia.
           by rewrite Pos.add_1_l Pos.pred_succ.
   Qed.
 
diff --git a/theories/typing/lib/refcell/ref_code.v b/theories/typing/lib/refcell/ref_code.v
index 88fa78bc88a528a5262fe49e4f83be9c53644d5b..3c1162b31fa1ba8d6a3c37c34362b757bccf3e68 100644
--- a/theories/typing/lib/refcell/ref_code.v
+++ b/theories/typing/lib/refcell/ref_code.v
@@ -173,7 +173,7 @@ Section ref_functions.
         iApply "H†". replace 1%Qp with (q'+q'')%Qp by naive_solver. iFrame.
       - simpl in *. setoid_subst. iExists (Some (ν, false, q0, n')). iFrame.
         iAssert (lrc ↦ #(Z.pos n'))%I with "[H↦lrc]" as "$".
-        { rewrite pos_op_plus Z.sub_1_r -Pos2Z.inj_pred; last lia.
+        { rewrite pos_op_add Z.sub_1_r -Pos2Z.inj_pred; last lia.
           by rewrite Pos.add_1_l Pos.pred_succ. }
         iMod (own_update with "H●◯") as "$".
         { apply auth_update_dealloc.
diff --git a/theories/typing/lib/refcell/refmut_code.v b/theories/typing/lib/refcell/refmut_code.v
index c295c78732667f44e5489896b4fd81ecfc59945b..5fd3f1e59a34d3feda456b9fa045c91cf6af621e 100644
--- a/theories/typing/lib/refcell/refmut_code.v
+++ b/theories/typing/lib/refcell/refmut_code.v
@@ -148,7 +148,7 @@ Section refmut_functions.
           apply (cancel_local_update_unit (writing_stR q _)), _. }
         iDestruct "INV" as "(H† & Hq & _)".
         rewrite /= (_:Z.neg (1%positive â‹… n') + 1 = Z.neg n');
-          last (rewrite pos_op_plus; lia). iFrame.
+          last (rewrite pos_op_add; lia). iFrame.
         iApply step_fupd_intro; [set_solver+|]. iSplitL; [|done].
         iDestruct "Hq" as (q' ?) "?". iExists (q+q')%Qp. iFrame.
         rewrite assoc (comm _ q'' q) //. }
diff --git a/theories/typing/lib/rwlock/rwlockreadguard_code.v b/theories/typing/lib/rwlock/rwlockreadguard_code.v
index 279656a0e93e05440b3861c0cd82b83084cf0bba..5659b7a67faed8d3d21d385422e12e6908c71137 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard_code.v
@@ -117,7 +117,7 @@ Section rwlockreadguard_functions.
           iSplitL "H● H◯"; last by eauto with iFrame.
           iApply (own_update_2 with "H● H◯"). apply auth_update_dealloc.
           assert (n = 1%positive â‹… Pos.pred n) as EQn.
-          { rewrite pos_op_plus -Pplus_one_succ_l Pos.succ_pred // =>?. by subst. }
+          { rewrite pos_op_add -Pplus_one_succ_l Pos.succ_pred // =>?. by subst. }
           rewrite {1}EQn -{1}(agree_idemp (to_agree _)) 2!pair_op Cinr_op Some_op.
           apply (cancel_local_update_unit (reading_st q ν)) , _. }
       iApply (wp_step_fupd with "INV"); first set_solver.