diff --git a/opam b/opam
index 3023744e7dbb86dd1ebdeced08e8a9b304fec14b..4ca4f67904479698624c19a2f67247967e452bb9 100644
--- a/opam
+++ b/opam
@@ -9,6 +9,6 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/reloc"]
 depends: [
-  "coq-iris" { (= "dev.2020-05-26.0.e3f87a95") | (= "dev") }
+  "coq-iris" { (= "dev.2020-05-26.1.d80e7abf") | (= "dev") }
   "coq-autosubst" { = "dev.coq86" }
 ]
diff --git a/theories/examples/coinflip.v b/theories/examples/coinflip.v
index 2631e0a9289dda5e1e71a24f5449b8a92ea39542..eed47d8e853cb5aca1734723eb6f8c7c012ba728 100644
--- a/theories/examples/coinflip.v
+++ b/theories/examples/coinflip.v
@@ -1,4 +1,4 @@
-From iris.heap_lang Require Import lifting.
+From iris.heap_lang Require Import derived_laws.
 From reloc Require Import reloc lib.lock.
 
 (* for rand (), val_to_bool *)
diff --git a/theories/examples/lateearlychoice.v b/theories/examples/lateearlychoice.v
index 80f6394662c6f6475afe887a8fee0322e391a46b..b4eb8d4d875c2cb5c8751a8daeeec9036fba890f 100644
--- a/theories/examples/lateearlychoice.v
+++ b/theories/examples/lateearlychoice.v
@@ -1,4 +1,4 @@
-From iris.heap_lang Require Import lifting.
+From iris.heap_lang Require Import derived_laws.
 From reloc Require Import reloc.
 
 Definition rand: val :=
diff --git a/theories/examples/ticket_lock.v b/theories/examples/ticket_lock.v
index c5a82571854786585101bb672e805a907fb8752d..edecad12d161da8888a2e133241b5d3dbc952f83 100644
--- a/theories/examples/ticket_lock.v
+++ b/theories/examples/ticket_lock.v
@@ -187,7 +187,7 @@ Section refinement.
       iMod (issueNewTicket with "Hissued") as "[Hissued Hm]".
       iMod ("H" with "[-HP Hm]") as "_".
       { iExists _. iFrame.
-        replace (Z.of_nat n + 1) with (Z.of_nat (S n)) by lia.
+        replace (Z.of_nat n + 1)%Z with (Z.of_nat (S n)) by lia.
         done. }
       clear o o'.
       repeat rel_pure_l.
@@ -259,7 +259,7 @@ Section refinement.
       iMod (issueNewTicket with "Hissued") as "[Hissued Hm]".
       iMod ("Hcl" with "[-Hm]") as "_".
       { iNext.
-        replace (Z.of_nat n + 1) with (Z.of_nat (S n)) by lia.
+        replace (Z.of_nat n + 1)%Z with (Z.of_nat (S n)) by lia.
         iExists _,_,_; by iFrame. }
       repeat rel_pure_l.
       by iApply wait_loop_refinement.
@@ -335,7 +335,7 @@ Section refinement.
       iIntros "Hl'".
       iMod ("Hcl" with "[-]") as "_".
       { iNext.
-        replace (o' + 1) with (Z.of_nat (o' + 1))%nat by lia.
+        replace (o' + 1)%Z with (Z.of_nat (o' + 1))%nat by lia.
         iExists (o' + 1)%nat,_,_. by iFrame. }
       rel_values.
   Qed.
diff --git a/theories/logic/model.v b/theories/logic/model.v
index cfc792d2d64fff41b119715d8924ba8b2fb86864..a5b808d2303c1720c5dbd6ccba566861654e453c 100644
--- a/theories/logic/model.v
+++ b/theories/logic/model.v
@@ -3,10 +3,9 @@
     - The model for types and type combinators;
     - Closure under context substitutions;
     - Basic monadic rules *)
-From iris.heap_lang Require Export lifting metatheory.
 From iris.base_logic.lib Require Import invariants.
 From iris.algebra Require Import list gmap.
-From iris.heap_lang Require Export lang notation.
+From iris.heap_lang Require Export lang notation derived_laws metatheory.
 From iris.heap_lang Require Import proofmode.
 From reloc Require Import prelude.properness logic.spec_rules prelude.ctx_subst.
 From reloc Require Export logic.spec_ra.
diff --git a/theories/logic/spec_ra.v b/theories/logic/spec_ra.v
index d9e17548faeba7994b743f1f556348fad29eed83..90dcc44595b3734e548357d9826d0fd9738c2720 100644
--- a/theories/logic/spec_ra.v
+++ b/theories/logic/spec_ra.v
@@ -5,7 +5,7 @@ From iris.bi Require Export fractional.
 From iris.base_logic Require Import gen_heap.
 From iris.base_logic Require Export invariants.
 From iris.proofmode Require Import tactics.
-From iris.heap_lang Require Import lang lifting.
+From iris.heap_lang Require Import lang primitive_laws.
 Import uPred.
 
 Definition relocN := nroot .@ "reloc".