diff --git a/opam b/opam
index a7596e47609ada642c06f74fa27ff130664b7eb3..aa6cda0deaa5b013d3b2796cbe6a734f6ec266c5 100644
--- a/opam
+++ b/opam
@@ -14,7 +14,7 @@ the type system, and safety proof for some Rust libraries.
 """
 
 depends: [
-  "coq-iris" { (= "dev.2020-04-02.2.df3450a6") | (= "dev") }
+  "coq-iris" { (= "dev.2020-04-04.3.9b2ad256") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/lang/heap.v b/theories/lang/heap.v
index 4abef3c1c3b1c079964dd2f5428eb0e3c7309f85..2cc7ebc31f92dfde9c04fbae3da2528095825a4e 100644
--- a/theories/lang/heap.v
+++ b/theories/lang/heap.v
@@ -407,7 +407,7 @@ Section heap.
     iDestruct 1 as (hF) "(Hvalσ & HhF & REL)"; iDestruct "REL" as %REL.
     iIntros "Hmt Hf". rewrite heap_freeable_eq /heap_freeable_def.
     iDestruct (own_valid_2 with "HhF Hf") as % [Hl Hv]%auth_both_valid.
-    move: Hl=> /singleton_included [[q qs] [/leibniz_equiv_iff Hl Hq]].
+    move: Hl=> /singleton_included_l [[q qs] [/leibniz_equiv_iff Hl Hq]].
     apply (Some_included_exclusive _ _) in Hq as [=<-<-]%leibniz_equiv; last first.
     { move: (Hv (l.1)). rewrite Hl. by intros [??]. }
     assert (vl ≠ []).
@@ -430,7 +430,7 @@ Section heap.
   Proof.
     iIntros "H● H◯".
     iDestruct (own_valid_2 with "H● H◯") as %[Hl?]%auth_both_valid.
-    iPureIntro. move: Hl=> /singleton_included [[[q' ls'] dv]].
+    iPureIntro. move: Hl=> /singleton_included_l [[[q' ls'] dv]].
     rewrite /to_heap lookup_fmap fmap_Some_equiv.
     move=> [[[ls'' v'] [?[[/=??]->]]]]; simplify_eq.
     move=> /Some_pair_included_total_2
@@ -447,7 +447,7 @@ Section heap.
   Proof.
     iIntros "H● H◯".
     iDestruct (own_valid_2 with "H● H◯") as %[Hl?]%auth_both_valid.
-    iPureIntro. move: Hl=> /singleton_included [[[q' ls'] dv]].
+    iPureIntro. move: Hl=> /singleton_included_l [[[q' ls'] dv]].
     rewrite /to_heap lookup_fmap fmap_Some_equiv.
     move=> [[[ls'' v'] [?[[/=??]->]]] Hincl]; simplify_eq.
     apply (Some_included_exclusive _ _) in Hincl as [? Hval]; last by destruct ls''.
diff --git a/theories/lifetime/model/accessors.v b/theories/lifetime/model/accessors.v
index 7a17291da13bbc7a82576b6fa270641228555ee6..82e47fa94c9ebe1b6798afcaecc3de08899c1c2b 100644
--- a/theories/lifetime/model/accessors.v
+++ b/theories/lifetime/model/accessors.v
@@ -100,7 +100,7 @@ Proof.
       iLeft. iFrame "%". iExists _, _. iFrame.
     + iDestruct "Hinv" as (?) "[Hinv _]". iDestruct "Hinv" as (B ?) "[>Hinv _]".
       iDestruct (own_bor_valid_2 with "Hinv Hf")
-        as %[(_ & <- & INCL%option_included)%singleton_included _]%auth_both_valid.
+        as %[(_ & <- & INCL%option_included)%singleton_included_l _]%auth_both_valid.
       by destruct INCL as [[=]|(? & ? & [=<-] &
         [[_<-]%lookup_gset_to_gmap_Some [[_ ?%(inj to_agree)]|[]%(exclusive_included _)]])].
   - iMod (lft_dead_in_tok with "HA") as "[_ H†]". done.
@@ -204,7 +204,7 @@ Proof.
       iExists Q. rewrite -bi.iff_refl. eauto.
     + iDestruct "Hinv" as (?) "[Hinv _]". iDestruct "Hinv" as (B ?) "[>Hinv _]".
       iDestruct (own_bor_valid_2 with "Hinv Hbor")
-        as %[(_ & <- & INCL%option_included)%singleton_included _]%auth_both_valid.
+        as %[(_ & <- & INCL%option_included)%singleton_included_l _]%auth_both_valid.
       by destruct INCL as [[=]|(? & ? & [=<-] &
         [[_<-]%lookup_gset_to_gmap_Some [[_?%(inj to_agree)]|[]%(exclusive_included _)]])].
   - iMod (lft_dead_in_tok with "HA") as "[_ H†]". done.
diff --git a/theories/lifetime/model/creation.v b/theories/lifetime/model/creation.v
index 5e3902e67fbcd8019f402183e0468f7467370a5e..622f63e97a559795e3817a575b83ac756d324ecb 100644
--- a/theories/lifetime/model/creation.v
+++ b/theories/lifetime/model/creation.v
@@ -132,7 +132,7 @@ Proof.
   iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose".
   rewrite /lft_tok big_sepMS_singleton.
   iDestruct (own_valid_2 with "HA HΛ")
-    as %[[s [?%leibniz_equiv ?]]%singleton_included _]%auth_both_valid.
+    as %[[s [?%leibniz_equiv ?]]%singleton_included_l _]%auth_both_valid.
   iMod (own_update_2 with "HA HΛ") as "[HA HΛ]".
   { by eapply auth_update, singleton_local_update,
       (exclusive_local_update _ (Cinr ())). }
diff --git a/theories/lifetime/model/primitive.v b/theories/lifetime/model/primitive.v
index b4f16f1cf81849a80e0da8ee80b9741f126d84e0..56fc8a6f19ff481f548e74b0b21b89ab973944e7 100644
--- a/theories/lifetime/model/primitive.v
+++ b/theories/lifetime/model/primitive.v
@@ -13,7 +13,7 @@ Implicit Types κ : lft.
 Lemma to_borUR_included (B : gmap slice_name bor_state) i s q :
   {[i := (q%Qp, to_agree s)]} ≼ to_borUR B → B !! i = Some s.
 Proof.
-  rewrite singleton_included=> -[qs []]. unfold_leibniz.
+  rewrite singleton_included_l=> -[qs []]. unfold_leibniz.
   rewrite lookup_fmap fmap_Some_equiv=> -[s' [-> ->]].
   by move=> /Some_pair_included [_] /Some_included_total /to_agree_included=>->.
 Qed.
@@ -37,7 +37,7 @@ Lemma own_ilft_auth_agree (I : gmap lft lft_names) κ γs :
     own ilft_name (◯ {[κ := to_agree γs]}) -∗ ⌜is_Some (I !! κ)⌝.
 Proof.
   iIntros "HI Hκ". iDestruct (own_valid_2 with "HI Hκ")
-    as %[[? [Hl ?]]%singleton_included _]%auth_both_valid.
+    as %[[? [Hl ?]]%singleton_included_l _]%auth_both_valid.
   unfold to_ilftUR in *. simplify_map_eq.
   destruct (fmap_Some_equiv_1 _ _ _ Hl) as (?&?&?). eauto.
 Qed.
@@ -48,7 +48,7 @@ Lemma own_alft_auth_agree (A : gmap atomic_lft bool) Λ b :
 Proof.
   iIntros "HA HΛ".
   iDestruct (own_valid_2 with "HA HΛ") as %[HA _]%auth_both_valid.
-  iPureIntro. move: HA=> /singleton_included [qs [/leibniz_equiv_iff]].
+  iPureIntro. move: HA=> /singleton_included_l [qs [/leibniz_equiv_iff]].
   rewrite lookup_fmap fmap_Some=> -[b' [? ->]] /Some_included.
   move=> [/leibniz_equiv_iff|/csum_included]; destruct b, b'; naive_solver.
 Qed.