diff --git a/opam.pins b/opam.pins
index 425ba64cb669d5c45b9a499cfeaadde7c340aaf4..16be4581cba6108c7f210c4b9dcdfa4bc215620f 100644
--- a/opam.pins
+++ b/opam.pins
@@ -1 +1 @@
-coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 05b530001f48a4544a9aaee7b8ff1a2abbe14e14
+coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 587cde167492b4b25f1d11ca7797c2087527abd6
diff --git a/theories/typing/function.v b/theories/typing/function.v
index 16d30054df04f7742471f8081a2be643d3de55cb..9a63ce18d8227f60115d28e7ae54364547415b29 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -117,8 +117,8 @@ Section typing.
   Proof.
     intros tys1 tys2 Htys ty1 ty2 Hty. apply fn_subtype_ty.
     - intros. eapply Forall2_impl; first eapply Htys. intros ??.
-      eapply subtype_weaken; last done. by apply contains_inserts_r.
-    - intros. eapply subtype_weaken, Hty; last done. by apply contains_inserts_r.
+      eapply subtype_weaken; last done. by apply submseteq_inserts_r.
+    - intros. eapply subtype_weaken, Hty; last done. by apply submseteq_inserts_r.
   Qed.
 
   Global Instance fn_eqtype_ty' {A n} E0 L0 E :
diff --git a/theories/typing/product_split.v b/theories/typing/product_split.v
index 5911d74ce1341b95edb500cd1eaa125065b933ea..0553b61ccb704997e8daf6c67b48c6b37da09252 100644
--- a/theories/typing/product_split.v
+++ b/theories/typing/product_split.v
@@ -293,7 +293,7 @@ Section product_split.
     rewrite !tctx_extract_hasty_unfold=>?. apply (tctx_incl_frame_r _ [_] [_;_]).
     rewrite {1}copy_tctx_incl. apply (tctx_incl_frame_r _ [_] [_]).
     rewrite tctx_split_shr_prod2 -(contains_tctx_incl _ _ [p' ◁ ty]%TC) //.
-    apply contains_skip, contains_nil_l.
+    apply submseteq_skip, submseteq_nil_l.
   Qed.
 
   Lemma tctx_extract_split_own_prod E L p p' n ty tyl T T' :
@@ -319,7 +319,7 @@ Section product_split.
     rewrite !tctx_extract_hasty_unfold=>?. apply (tctx_incl_frame_r _ [_] [_;_]).
     rewrite {1}copy_tctx_incl. apply (tctx_incl_frame_r _ [_] [_]).
     rewrite tctx_split_shr_prod -(contains_tctx_incl _ _ [p' ◁ ty]%TC) //.
-    apply contains_skip, contains_nil_l.
+    apply submseteq_skip, submseteq_nil_l.
   Qed.
 
   (* Merging with [tctx_extract]. *)
diff --git a/theories/typing/programs.v b/theories/typing/programs.v
index 5ba09002b87ce69b7849de69a7e789b36c5acfd9..68b0a6d9f5d22668602c525647d8d9fd9e78f04b 100644
--- a/theories/typing/programs.v
+++ b/theories/typing/programs.v
@@ -130,7 +130,11 @@ Section typing_rules.
     tctx_extract_ctx E L T1 T T' →
     (typed_body E L C (T2 ++ T') e') →
     typed_body E L C T (e ;; e').
-  Proof. intros. by eapply type_let. Qed.
+  Proof.
+    intros ? Hinst ? Hbody. eapply type_let; [done| |done|].
+    (* FIXME: done divergese on the remaining goals. *)
+    exact Hinst. intros. exact Hbody.
+  Qed.
 
   Lemma typed_newlft E L C T κs e :
     Closed [] e →
@@ -265,6 +269,7 @@ Section typing_rules.
     typed_body E L C ((p1 ◁ ty1') :: (p2 ◁ ty2') :: T') e →
     typed_body E L C T (p1 <⋯ !{n}p2;; e).
   Proof.
-    intros. eapply type_seq; [done|by eapply type_memcpy_instr|done|by simpl].
+    intros ?? Hwr Hrd ??. eapply type_seq; [done|eapply type_memcpy_instr| |by simpl]; first done.
+    exact Hwr. exact Hrd. done.
   Qed.
 End typing_rules.
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 5e0d853a9f77ecf4da273a27ebc2699859533f59..89ffb4c61faeb4826c5af1cb7ec3fe6b839cd05b 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -434,13 +434,13 @@ Section weakening.
   Context `{typeG Σ}.
 
   Lemma subtype_weaken E1 E2 L1 L2 ty1 ty2 :
-    E1 `contains` E2 → L1 `contains` L2 →
+    E1 ⊆+ E2 → L1 ⊆+ L2 →
     subtype E1 L1 ty1 ty2 → subtype E2 L2 ty1 ty2.
   Proof.
     (* TODO: There's no lemma relating `contains` to membership (∈)...?? *)
-    iIntros (HE12 [L' HL12]%contains_Permutation Hsub) "#LFT HE HL".
+    iIntros (HE12 [L' HL12]%submseteq_Permutation Hsub) "#LFT HE HL".
     iApply (Hsub with "LFT [HE] [HL]").
-    - rewrite /elctx_interp_0. by iApply big_sepL_contains.
+    - rewrite /elctx_interp_0. by iApply big_sepL_submseteq.
     - iDestruct "HL" as %HL. iPureIntro. intros ??. apply HL.
       rewrite HL12. set_solver.
   Qed.
diff --git a/theories/typing/type_context.v b/theories/typing/type_context.v
index ec4bceff6613164dc1fbccf441b63ddfeb8b9016..bfa53826c49bc651360a543dcee6bf6c401e057d 100644
--- a/theories/typing/type_context.v
+++ b/theories/typing/type_context.v
@@ -197,9 +197,9 @@ Section type_context.
       by iMod (H2 with "LFT HE HL H") as "($ & $ & $)".
   Qed.
 
-  Lemma contains_tctx_incl E L T1 T2 : T1 `contains` T2 → tctx_incl E L T2 T1.
+  Lemma contains_tctx_incl E L T1 T2 : T1 ⊆+ T2 → tctx_incl E L T2 T1.
   Proof.
-    rewrite /tctx_incl. iIntros (Hc ???) "_ $ $ H". by iApply big_sepL_contains.
+    rewrite /tctx_incl. iIntros (Hc ???) "_ $ $ H". by iApply big_sepL_submseteq.
   Qed.
 
   Global Instance tctx_incl_app E L :
@@ -234,7 +234,7 @@ Section type_context.
     remember (p ◁ ty)%TC. induction 1 as [|???? IH]; subst.
     - apply (tctx_incl_frame_r _ [_] [_;_]), copy_tctx_incl, _.
     - etrans. by apply (tctx_incl_frame_l [_]), IH, reflexivity.
-      apply contains_tctx_incl, contains_swap.
+      apply contains_tctx_incl, submseteq_swap.
   Qed.
 
   Lemma subtype_tctx_incl E L p ty1 ty2 :
@@ -258,7 +258,7 @@ Section type_context.
   Lemma tctx_extract_hasty_cons E L p ty T T' x :
     tctx_extract_hasty E L p ty T T' →
     tctx_extract_hasty E L p ty (x::T) (x::T').
-  Proof. unfold tctx_extract_hasty=>->. apply contains_tctx_incl, contains_swap. Qed.
+  Proof. unfold tctx_extract_hasty=>->. apply contains_tctx_incl, submseteq_swap. Qed.
   Lemma tctx_extract_hasty_here_copy E L p ty ty' T `{!Copy ty} :
     subtype E L ty ty' →
     tctx_extract_hasty E L p ty' ((p ◁ ty)::T) ((p ◁ ty)::T).
@@ -281,7 +281,7 @@ Section type_context.
     tctx_extract_blocked E L p κ ty (x::T) (x::T').
   Proof.
     move=> /(tctx_incl_frame_l [x]) /= Hincl. rewrite /tctx_extract_blocked.
-    etrans; first done. apply contains_tctx_incl, contains_swap.
+    etrans; first done. apply contains_tctx_incl, submseteq_swap.
   Qed.
   Lemma tctx_extract_blocked_here E L p κ ty T :
     tctx_extract_blocked E L p κ ty ((p ◁{κ} ty)::T) T.
@@ -309,7 +309,7 @@ Section type_context.
     tctx_incl E L T T'.
   Proof.
     unfold tctx_extract_ctx=>->.
-      by apply contains_tctx_incl, contains_inserts_r.
+      by apply contains_tctx_incl, submseteq_inserts_r.
   Qed.
 
   (* Unblocking a type context. *)