diff --git a/opam.pins b/opam.pins
index 83c77af52fae50c26d15b272e46451104c6a6f4d..9d0b4a49b0d771649bd7815204bf32cc0cef0036 100644
--- a/opam.pins
+++ b/opam.pins
@@ -1 +1 @@
-coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 7dec931b3ce0674c093a325275976aac96e9c8e6
+coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 0429c257e3088cf77c8852a2cbeff2b02671b8b5
diff --git a/theories/typing/lib/rc.v b/theories/typing/lib/rc.v
index b05eb1fc059462fe38d29926ceb567dfbc6c68e8..4f67aa131ae9459c8549489aa49d081803ea407b 100644
--- a/theories/typing/lib/rc.v
+++ b/theories/typing/lib/rc.v
@@ -154,10 +154,7 @@ Section rc.
   Lemma rc_subtype ty1 ty2 :
     type_incl ty1 ty2 -∗ type_incl (rc ty1) (rc ty2).
   Proof.
-    iIntros "#Hincl". iPoseProof "Hincl" as "Hincl2".
-    iDestruct "Hincl2" as "(#Hsz & #Hoincl & #Hsincl)".
-    (* FIXME: Would be nice to have an easier way to duplicate
-       destructed things.  Maybe iPoseProof with a destruct pattern? *)
+    iIntros "#Hincl". iPoseProof "Hincl" as "(#Hsz & #Hoincl & #Hsincl)".
     iSplit; first done. iSplit; iAlways.
     - iIntros "* Hvl". destruct vl as [|[[|vl|]|] [|]]; try done.
       iDestruct "Hvl" as "[(Hl & H† & Hc) | Hvl]".
diff --git a/theories/typing/sum.v b/theories/typing/sum.v
index d3b4a77c1f92cfb48f363c7163007073f1d2fcb3..1b88e917e6034800cef5044398a47b9d11aebca1 100644
--- a/theories/typing/sum.v
+++ b/theories/typing/sum.v
@@ -141,7 +141,6 @@ Section sum.
     { iInduction Htyl as [|???? Hsub] "IH".
       { iClear "∗". iIntros "!# _". done. }
       iDestruct (Hsub with "HL") as "#Hsub". iDestruct ("IH" with "HL") as "{IH} #IH".
-      (* FIXME: WHy does the previous iDestruvt remove HL? *)
       iAlways. iIntros "#HE". iDestruct ("Hsub" with "HE") as "(% & _ & _)".
       iDestruct ("IH" with "HE") as %IH. iPureIntro. simpl. inversion_clear IH. by f_equal. }
     iDestruct (subtype_Forall2_llctx with "HL") as "#Htyl"; first done.