diff --git a/opam b/opam
index 3cde3f37e58ecc5ae23204fad6671df5447664ca..5d8b8295ee5c19ab7409bde9f5b8f2578bfc3e6e 100644
--- a/opam
+++ b/opam
@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/actris" ]
 depends: [
-  "coq-iris-heap-lang" { (= "dev.2021-07-28.0.3424ace5") | (= "dev") }
+  "coq-iris-heap-lang" { (= "dev.2021-10-01.0.b9315f85") | (= "dev") }
 ]
diff --git a/theories/channel/proofmode.v b/theories/channel/proofmode.v
index 4c55908cca608ea8b1bd0bd413c449c0be34f79a..e55928cd8547fb0703768cbc5026bc38e9ab2838 100644
--- a/theories/channel/proofmode.v
+++ b/theories/channel/proofmode.v
@@ -389,7 +389,7 @@ Proof.
   rewrite envs_entails_eq /ProtoNormalize /= right_id=> ? Hp HΦ.
   rewrite envs_lookup_sound //; simpl.
   rewrite (iProto_mapsto_le _ _ (p1 <{P1}&{P2}> p2)%proto) -bi.later_intro -Hp left_id.
-  rewrite -wp_bind. eapply bi.wand_apply; [by eapply branch_spec|f_equiv].
+  rewrite -wp_bind. eapply bi.wand_apply; [by eapply branch_spec|f_equiv; first done].
   rewrite -bi.later_intro; apply bi.forall_intro=> b.
   specialize (HΦ b). destruct (envs_app _ _) as [Δ'|] eqn:HΔ'=> //.
   rewrite envs_app_sound //; simpl. by rewrite right_id HΦ.
@@ -443,7 +443,7 @@ Proof.
   rewrite envs_lookup_sound //; simpl.
   rewrite (iProto_mapsto_le _ _ (p1 <{P1}+{P2}> p2)%proto) -bi.later_intro -Hp left_id.
   rewrite -wp_bind. eapply bi.wand_apply; [by eapply select_spec|].
-  rewrite -assoc; f_equiv.
+  rewrite -assoc; f_equiv; first done.
   destruct (envs_split _ _ _) as [[Δ1 Δ2]|] eqn:? => //.
   destruct (envs_app _ _ _) as [Δ2'|] eqn:? => //.
   rewrite envs_split_sound //; rewrite (envs_app_sound Δ2) //; simpl.