diff --git a/.gitignore b/.gitignore
index ecdc2641c856c3f94f1daa3e1fb9d99b9c8c9fa1..cd6fdacb0d8b7af215f0c57008ceb0cd21566552 100644
--- a/.gitignore
+++ b/.gitignore
@@ -9,6 +9,6 @@
 *~
 *.bak
 .coq-native/
-iris-enabled
-Makefile.coq*
-opamroot
+build-dep/
+Makefile.coq
+Makefile.coq.conf
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 28d985125fb44ac8f61e385a9f19237fb2699fd0..e2fd9f2485a1c052bbec4afa786289c34d874fb2 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -16,7 +16,7 @@ variables:
   - 'cat build-log.txt | egrep "[a-zA-Z0-9_/-]+ \((real|user): [0-9]" | tee build-time.txt'
   - 'if test -n "$VALIDATE" && (( RANDOM % 10 == 0 )); then make validate; fi'
   cache:
-    key: "coq$COQ_VERSION-ssr$SSR_VERSION"
+    key: "coq.$COQ_VERSION-ssr.$SSR_VERSION"
     paths:
     - opamroot/
   only:
@@ -34,7 +34,7 @@ lrust-coq8.6.1:
   variables:
     COQ_VERSION: "8.6.1"
     SSR_VERSION: "1.6.1"
-    VALIDATE: 1
+  #  VALIDATE: "1" # coqchk on lambdaRust is currently broken
   artifacts:
     paths:
     - build-time.txt
diff --git a/Makefile b/Makefile
index 7bfa06f89a5c19f9b279f65875196f870b6f88c7..cff640c1c72131e62f2d5b838970ec5e131c2a22 100644
--- a/Makefile
+++ b/Makefile
@@ -1,38 +1,48 @@
-# Process flags
-ifeq ($(Y), 1)
-	YFLAG=-y
-endif
-
 # Forward most targets to Coq makefile (with some trick to make this phony)
 %: Makefile.coq phony
 	+@make -f Makefile.coq $@
 
 all: Makefile.coq
 	+@make -f Makefile.coq all
+.PHONY: all
 
 clean: Makefile.coq
 	+@make -f Makefile.coq clean
 	find theories \( -name "*.v.d" -o -name "*.vo" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete
 	rm -f Makefile.coq
+.PHONY: clean
 
-# Create Coq Makefile. POSIX awk can't do in-place editing, but coq_makefile wants the real filename, so we do some file gymnastics.
+# Create Coq Makefile. POSIX awk can't do in-place editing, but coq_makefile wants the real
+# filename, so we do some file gymnastics.
 Makefile.coq: _CoqProject Makefile awk.Makefile
 	coq_makefile -f _CoqProject -o Makefile.coq
 	mv Makefile.coq Makefile.coq.tmp && awk -f awk.Makefile Makefile.coq.tmp > Makefile.coq && rm Makefile.coq.tmp
 
 # Install build-dependencies
-build-dep:
-	build/opam-pins.sh < opam.pins
-	opam upgrade $(YFLAG) # it is not nice that we upgrade *all* packages here, but I found no nice way to upgrade only those that we pinned
-	opam pin add opam-builddep-temp "$$(pwd)#HEAD" -k git -n -y
-	opam install opam-builddep-temp --deps-only $(YFLAG)
-	opam pin remove opam-builddep-temp
+build-dep/opam: opam
+	# Create the build-dep package.
+	@mkdir -p build-dep
+	@sed <opam 's/^\(build\|install\|remove\):.*/\1: []/; s/^name: *"\(.*\)" */name: "\1-builddep"/' > build-dep/opam
+	@fgrep builddep build-dep/opam >/dev/null || (echo "sed failed to fix the package name" && exit 1) # sanity check
+
+build-dep: build-dep/opam phony
+	@# We want opam to not just instal the build-deps now, but to also keep satisfying these
+	@# constraints.  Otherwise, `opam upgrade` may well update some packages to versions
+	@# that are incompatible with our build requirements.
+	@# To achieve this, we create a fake opam package that has our build-dependencies as
+	@# dependencies, but does not actually install anything.
+	# Add the pin and (re)install build-dep package.
+	@# Reinstallation is needed in case the pin already exists, but the builddep package changed.
+	@BUILD_DEP_PACKAGE="$$(egrep "^name:" build-dep/opam | sed 's/^name: *"\(.*\)" */\1/')"; \
+	  opam pin add "$$BUILD_DEP_PACKAGE".dev "$$(pwd)/build-dep" -k path $(OPAMFLAGS) && \
+	  opam reinstall "$$BUILD_DEP_PACKAGE"
 
 # Some files that do *not* need to be forwarded to Makefile.coq
 Makefile: ;
 _CoqProject: ;
 awk.Makefile: ;
+opam: ;
 
-# Phony targets (i.e. targets that should be run no matter the timestamps of the involved files)
+# Phony wildcard targets
 phony: ;
-.PHONY: all clean phony
+.PHONY: phony
diff --git a/Makefile.coq.local b/Makefile.coq.local
new file mode 100644
index 0000000000000000000000000000000000000000..b261de990be8a8d16d2d8e690b4bb18809ad8696
--- /dev/null
+++ b/Makefile.coq.local
@@ -0,0 +1,5 @@
+uninstall::
+	@# This makes sure we also delete stale files in the destination directory
+	$(HIDE)df="$(COQLIBINSTALL)/`$(COQMKFILE) -destination-of "theories/base.v" $(COQLIBS)`" &&\
+	echo "RM in $$df" &&\
+	if [ -d "$$df" ]; then find "$$df" \( -name "*.vo" -o -name "*.v" -o -name "*.glob" -o \( -type d -empty \) \) -print -delete; fi
diff --git a/README.md b/README.md
index 2fec6cd768e10747083aa8fff82ec69029dd47b7..80b0f882cab5407ff5a073a1343997cacaae88a5 100644
--- a/README.md
+++ b/README.md
@@ -6,19 +6,19 @@ This is the Coq development accompanying lambda-Rust.
 
 This version is known to compile with:
 
- - Coq 8.6
+ - Coq 8.6.1
  - Ssreflect 1.6.1
  - A development version of [Iris](https://gitlab.mpi-sws.org/FP/iris-coq/)
 
 The easiest way to install the correct versions of the dependencies is through
-opam.  Coq packages are available on the coq-released repository, set up by the
-command:
+opam.  You will need the Coq and Iris opam repositories:
 
     opam repo add coq-released https://coq.inria.fr/opam/released
+    opam repo add iris-dev https://gitlab.mpi-sws.org/FP/opam-dev.git
 
-Once you got opam set up, just run `make build-dep` to install the right
-versions of the dependencies.  When the dependencies change, just run `make
-build-dep` again.
+Once you got opam set up, run `make build-dep` to install the right versions
+of the dependencies.  When the dependencies change, just run `make build-dep`
+again.
 
 ## Building Instructions
 
diff --git a/awk.Makefile b/awk.Makefile
index 09ded0aa64f3a85ee4a55668d21ee17bb9a362f0..91f7d7374d1fd76f61ef2f9404ba4e1b1ac3dfb7 100644
--- a/awk.Makefile
+++ b/awk.Makefile
@@ -11,24 +11,24 @@
 
 # Patch the uninstall target to work properly, and to also uninstall stale files.
 # Also see <https://coq.inria.fr/bugs/show_bug.cgi?id=4907>.
-/^uninstall:/ {
+# This (and the section above) can be removed once we no longer support Coq 8.6.
+/^uninstall: / {
 	print "uninstall:";
 	print "\tif [ -d \"$(DSTROOT)\"$(COQLIBINSTALL)/"PROJECT"/ ]; then find \"$(DSTROOT)\"$(COQLIBINSTALL)/"PROJECT"/ \\( -name \"*.vo\" -o -name \"*.v\" -o -name \"*.glob\" -o \\( -type d -empty \\) \\) -print -delete; fi";
 	getline;
 	next
 }
 
-# Patch vio2vo to (a) run "make quick" with the same number of jobs, ensuring
+# Add new target quick2vo to (a) run "make quick" with the same number of jobs, ensuring
 # that the .vio files are up-to-date, and (b) only schedule vio2vo for those
 # files where the .vo is *older* than the .vio.
 /^vio2vo:/ {
-	print "vio2vo:";
+	print "quick2vo:";
 	print "\t@make -j $(J) quick"
-	print "\t@VIOFILES=$$(for file in $(VOFILES:%.vo=%.vio); do vofile=\"$$(echo \"$$file\" | sed \"s/\\.vio/.vo/\")\"; if [ \"$$vofile\" -ot \"$$file\" -o ! -e \"$$vofile\" ]; then echo -n \"$$file \"; fi; done); \\"
+	print "\t@VIOFILES=$$(for vofile in $(VOFILES); do viofile=\"$$(echo \"$$vofile\" | sed \"s/\\.vo/.vio/\")\"; if [ \"$$vofile\" -ot \"$$viofile\" -o ! -e \"$$vofile\" ]; then echo -n \"$$viofile \"; fi; done); \\"
 	print "\t echo \"VIO2VO: $$VIOFILES\"; \\"
-	print "\t if [ -n \"$$VIOFILES\" ]; then $(COQC) $(COQDEBUG) $(COQFLAGS) -schedule-vio2vo $(J) $$VIOFILES; fi"
-	getline;
-	next
+	print "\t if [ -n \"$$VIOFILES\" ]; then $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) -schedule-vio2vo $(J) $$VIOFILES; fi"
+	print ".PHONY: quick2vo"
 }
 
 # This forwards all unchanged lines
diff --git a/build/opam-ci.sh b/build/opam-ci.sh
index 20d87f9d4da508096531227791ccce63da17bd6f..27ae623d2f580b2d2b898d674cd6229bf74425e1 100755
--- a/build/opam-ci.sh
+++ b/build/opam-ci.sh
@@ -1,42 +1,66 @@
 #!/bin/bash
 set -e
-# This script installs the build dependencies for CI builds.
+## This script installs the build dependencies for CI builds.
+function run_and_print() {
+    echo "$ $@"
+    "$@"
+}
 
 # Prepare OPAM configuration
 export OPAMROOT="$(pwd)/opamroot"
 export OPAMJOBS="$((2*$CPU_CORES))"
 export OPAM_EDITOR="$(which false)"
 
-# Make sure we got a good OPAM
-test -d "$OPAMROOT" || (mkdir "$OPAMROOT" && opam init --no-setup -y)
+# Make sure we got a good OPAM.
+test -d "$OPAMROOT" || (mkdir "$OPAMROOT" && run_and_print opam init --no-setup -y)
 eval `opam conf env`
+# Delete old pins from opam.pins times.
+run_and_print opam pin remove coq-stdpp -n
+run_and_print opam pin remove coq-iris -n
+# Make sure the pin for the builddep package is not stale.
+run_and_print make build-dep/opam
+
+# Get us all the latest repositories
 if test $(find "$OPAMROOT/repo/package-index" -mtime +0); then
     # last update was more than a day ago
-    opam update
+    run_and_print opam update
 else
-    echo "[opam-ci] Not updating opam."
+    # only update iris-dev
+    if test -d "$OPAMROOT/repo/iris-dev"; then run_and_print opam update iris-dev; fi
 fi
-test -d "$OPAMROOT/repo/coq-extra-dev" || opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev -p 5
-test -d "$OPAMROOT/repo/coq-core-dev" || opam repo add coq-core-dev https://coq.inria.fr/opam/core-dev -p 5
-test -d "$OPAMROOT/repo/coq-released" || opam repo add coq-released https://coq.inria.fr/opam/released -p 10
+test -d "$OPAMROOT/repo/coq-extra-dev" && run_and_print opam repo remove coq-extra-dev
+test -d "$OPAMROOT/repo/coq-core-dev" || run_and_print opam repo add coq-core-dev https://coq.inria.fr/opam/core-dev -p 5
+test -d "$OPAMROOT/repo/coq-released" || run_and_print opam repo add coq-released https://coq.inria.fr/opam/released -p 10
+test -d "$OPAMROOT/repo/iris-dev" || run_and_print opam repo add iris-dev https://gitlab.mpi-sws.org/FP/opam-dev.git -p 20
+echo
+
+# We really want to run all of the following in one opam transaction, but due to opam limitations,
+# that is not currently possible.
 
-# Install fixed versions of some dependencies
+# Install fixed versions of some dependencies.
 echo
 while (( "$#" )); do # while there are arguments left
     PACKAGE="$1" ; shift
     VERSION="$1" ; shift
+
     # Check if the pin is already set
     if opam pin list | fgrep "$PACKAGE.$VERSION " > /dev/null; then
         echo "[opam-ci] $PACKAGE already pinned to $VERSION"
     else
         echo "[opam-ci] Pinning $PACKAGE to $VERSION"
-        opam pin add "$PACKAGE" "$VERSION" -k version -y
+        run_and_print opam pin add "$PACKAGE" "$VERSION" -k version -y
     fi
 done
 
-# Install build-dependencies
+# Upgrade cached things.
+echo
+echo "[opam-ci] Upgrading opam"
+run_and_print opam upgrade -y
+
+# Install build-dependencies.
 echo
-make build-dep Y=1
+echo "[opam-ci] Installing build-dependencies"
+make build-dep OPAMFLAGS=-y
 
 # done
 echo
diff --git a/build/opam-pins.sh b/build/opam-pins.sh
deleted file mode 100755
index 5291cb234701dbaba66e19717a4ef242fc9e83e8..0000000000000000000000000000000000000000
--- a/build/opam-pins.sh
+++ /dev/null
@@ -1,26 +0,0 @@
-#!/bin/bash
-set -e
-## Process an opam.pins file from stdin: Add all the given pins, but don't install anything.
-## Usage:
-##   ./opam-pins.sh < opam.pins
-
-if ! which curl >/dev/null; then
-    echo "opam-pins needs curl. Please install curl and try again."
-    exit 1
-fi
-
-# Process stdin
-while read PACKAGE URL HASH; do
-    if echo "$URL" | egrep '^https://gitlab\.mpi-sws\.org' > /dev/null; then
-        echo "[opam-pins] Recursing into $URL"
-        # an MPI URL -- try doing recursive pin processing
-        curl -f "$URL/raw/$HASH/opam.pins" 2>/dev/null | "$0"
-    fi
-    if opam pin list | fgrep "$PACKAGE.dev.$HASH " > /dev/null; then
-        echo "[opam-pins] $PACKAGE already at commit $HASH"
-    else
-        echo "[opam-pins] Applying pin: $PACKAGE -> $URL#$HASH"
-        opam pin add "$PACKAGE.dev.$HASH" "$URL#$HASH" -k git -y -n
-        echo
-    fi
-done
diff --git a/opam b/opam
index e92373cb126232c8841c7145fa57abb823e116bd..e09ae8787b6bb4dd85da880b67a36e7839f5ce0e 100644
--- a/opam
+++ b/opam
@@ -6,11 +6,9 @@ authors: "The RustBelt Team"
 homepage: "http://plv.mpi-sws.org/rustbelt/"
 bug-reports: "https://gitlab.mpi-sws.org/FP/lambdaRust-coq/issues"
 dev-repo: "https://gitlab.mpi-sws.org/FP/lambdaRust-coq.git"
-build: [
-  [make "-j%{jobs}%"]
-]
+build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/lrust'" ]
 depends: [
-  "coq-iris"
+  "coq-iris" { (= "dev.2017-09-25.0") | (= "dev") }
 ]
diff --git a/opam.pins b/opam.pins
deleted file mode 100644
index 2c200453f67a9f2301754445d21ca0e7403bc5a6..0000000000000000000000000000000000000000
--- a/opam.pins
+++ /dev/null
@@ -1 +0,0 @@
-coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 2e2c5c25aea886acc7d0925d435fe856ffa6ac14
diff --git a/theories/lang/lang.v b/theories/lang/lang.v
index b7abe7f678e8492149cc635690fb515d1cced230..3e86445f120c4248aa3be5147947b8938cc04706 100644
--- a/theories/lang/lang.v
+++ b/theories/lang/lang.v
@@ -216,6 +216,13 @@ Fixpoint free_mem (l:loc) (n:nat) (σ:state) : state :=
 Inductive lit_eq (σ : state) : base_lit → base_lit → Prop :=
 | IntRefl z : lit_eq σ (LitInt z) (LitInt z)
 | LocRefl l : lit_eq σ (LitLoc l) (LitLoc l)
+(* Comparing unallocated pointers can non-deterministically say they are equal
+   even if they are not.  Given that our `free` actually makes addresses
+   re-usable, this may not be strictly necessary, but it is the most
+   conservative choice that avoids UB (and we cannot use UB as this operation is
+   possible in safe Rust).  See
+   <https://internals.rust-lang.org/t/comparing-dangling-pointers/3019> for some
+   more background. *)
 | LocUnallocL l1 l2 :
     σ !! l1 = None →
     lit_eq σ (LitLoc l1) (LitLoc l2)
@@ -443,7 +450,7 @@ Proof.
   assert (∀ (l : loc) ls (X : gset block),
     l ∈ ls → l.1 ∈ foldr (λ l, ({[l.1]} ∪)) X ls) as help.
   { induction 1; set_solver. }
-  rewrite /fresh_block /shift_loc /= -not_elem_of_dom -elem_of_elements.
+  rewrite /fresh_block /shift_loc /= -(not_elem_of_dom (D := gset loc)) -elem_of_elements.
   move=> /(help _ _ ∅) /=. apply is_fresh.
 Qed.
 
diff --git a/theories/lang/lib/arc.v b/theories/lang/lib/arc.v
index 166130461bcf6fb15192e93f21872af20dcb247d..10ec7bbe63547e04116f929cda07c5c16e195299 100644
--- a/theories/lang/lib/arc.v
+++ b/theories/lang/lib/arc.v
@@ -452,20 +452,20 @@ Section arc.
         + iMod ("Hclose1" with "[>-]") as "_"; last iLeft; auto with lia.
           iExists _. iMod (own_update_2 with "H● Hown") as "$".
           { apply auth_update_dealloc, prod_local_update_2,
-                  (cancel_local_update_empty 1%nat), _. }
+                  (cancel_local_update_unit 1%nat), _. }
           iExists _. iFrame. by replace (S (S weak) - 1) with (S weak:Z) by lia.
         + iFrame. iApply "Hclose1". iExists _. auto with iFrame.
       - iDestruct "H" as "[? >$]". iIntros "!>"; iSplit; iIntros "Hl1".
         + iMod ("Hclose1" with "[>-]") as "_"; last iLeft; auto with lia.
           iExists _. iMod (own_update_2 with "H● Hown") as "$".
           { apply auth_update_dealloc, prod_local_update_2,
-                  (cancel_local_update_empty 1%nat), _. }
+                  (cancel_local_update_unit 1%nat), _. }
           iFrame. by replace (S (S weak) - 1) with (S weak:Z) by lia.
         + iFrame. iApply "Hclose1". iExists _. auto with iFrame.
       - iDestruct "H" as "(>? & >$ & HP2)". iIntros "!>"; iSplit; iIntros "Hl1".
         + iMod (own_update_2 with "H● Hown") as "H●".
           { apply auth_update_dealloc, prod_local_update_2,
-                  (cancel_local_update_empty 1%nat), _. }
+                  (cancel_local_update_unit 1%nat), _. }
           destruct weak as [|weak].
           * iMod ("Hclose1" with "[H●]") as "_"; last by auto with iFrame.
             iExists _. iFrame.
@@ -519,7 +519,7 @@ Section arc.
       + destruct Hqq' as [<- ->].
         iMod (own_update_2 with "H● Hown") as "[H● H◯]".
         { apply auth_update, prod_local_update_1. rewrite -[x in (x, _)]right_id.
-          etrans; first apply cancel_local_update_empty, _.
+          etrans; first apply cancel_local_update_unit, _.
           by apply (op_local_update _ _ (Some (Cinr (Excl ())))). }
         iMod ("Hclose" with "[H● Hs Hw]") as "_"; first by iExists _; do 2 iFrame.
         iModIntro. wp_case. iApply wp_fupd. wp_op=>[_|//].
@@ -528,7 +528,7 @@ Section arc.
         rewrite -[in (_, _)](Pos.succ_pred s) // -[wl in Cinl (_, wl)]left_id
                 -Pos.add_1_l -2!pair_op -Cinl_op Some_op.
         iMod (own_update_2 _ _ _ _ with "H● Hown") as "H●".
-        { apply auth_update_dealloc, prod_local_update_1, @cancel_local_update_empty, _. }
+        { apply auth_update_dealloc, prod_local_update_1, @cancel_local_update_unit, _. }
         iMod ("Hclose" with "[- HΦ]") as "_".
         { iExists _. iFrame. iExists (q + q'')%Qp. iFrame. iSplit; last by destruct s.
           iIntros "!> !%". rewrite assoc -Hq''. f_equal. apply comm, _. }
@@ -552,7 +552,7 @@ Section arc.
     - wp_apply (wp_cas_int_suc with "Hs"); first done. iIntros "Hs".
       destruct Hqq' as [<- ->]. iMod (own_update_2 with "H● Hown") as "[H● H◯]".
       { apply auth_update, prod_local_update_1. rewrite -[x in (x, _)]right_id.
-        etrans; first apply cancel_local_update_empty, _.
+        etrans; first apply cancel_local_update_unit, _.
         by apply (op_local_update _ _ (Some (Cinr (Excl ())))). }
       iMod ("Hclose" with "[H● Hs Hw]") as "_"; first by iExists _; do 2 iFrame.
       iApply ("HΦ" $! true). rewrite -{1}Hq''. iFrame. by iApply close_last_strong.
@@ -615,7 +615,7 @@ Section arc.
       + setoid_subst. iDestruct "H" as (?) "(Hq & ? & ? & >? & >%)". subst. wp_read.
         iMod (own_update_2 with "H● H◯") as "H●".
         { apply auth_update_dealloc. rewrite -{1}[(_, 0%nat)]right_id.
-          apply cancel_local_update_empty, _. }
+          apply cancel_local_update_unit, _. }
         iMod ("Hclose" with "[H●]") as "_"; first by iExists _; iFrame.
         iModIntro. wp_seq. wp_op=>[_|//]. wp_let. wp_op. wp_write. iApply "HΦ".
         iDestruct "Hq" as %<-. iFrame.
@@ -643,7 +643,7 @@ Section arc.
     - wp_apply (wp_cas_int_suc with "Hs")=>//. iIntros "Hs".
       destruct Hqq' as [<- ->]. iMod (own_update_2 with "H● Hown") as "[H● H◯]".
       { apply auth_update, prod_local_update_1. rewrite -[x in (x, _)]right_id.
-        etrans; first apply cancel_local_update_empty, _.
+        etrans; first apply cancel_local_update_unit, _.
         by apply (op_local_update _ _ (Some (Cinr (Excl ())))). }
       iCombine "HP1" "HP1'" as "HP1". rewrite Hq''. clear Hq'' q''.
       iMod ("Hclose" with "[H● Hs Hw]") as "_"; first by iExists _; do 2 iFrame.
@@ -668,4 +668,4 @@ Section arc.
   Qed.
 End arc.
 
-Typeclasses Opaque is_arc arc_tok weak_tok.
\ No newline at end of file
+Typeclasses Opaque is_arc arc_tok weak_tok.
diff --git a/theories/lang/races.v b/theories/lang/races.v
index 5baaf0a70cd1da881274fae33a7745668689dbc9..8fa7a5476eb0d22807e902c4d800012323247bc4 100644
--- a/theories/lang/races.v
+++ b/theories/lang/races.v
@@ -120,17 +120,17 @@ Proof.
   destruct Ha2; simplify_eq; econstructor; eauto; try apply lookup_insert.
   (* Oh my. FIXME. *)
   - eapply lit_neq_state; last done.
-    setoid_rewrite <-not_elem_of_dom. rewrite dom_insert_L.
-    cut (is_Some (σ !! l)); last by eexists. rewrite -elem_of_dom. set_solver+.
+    setoid_rewrite <-(not_elem_of_dom (D:=gset loc)). rewrite dom_insert_L.
+    cut (is_Some (σ !! l)); last by eexists. rewrite -(elem_of_dom (D:=gset loc)). set_solver+.
   - eapply lit_eq_state; last done.
-    setoid_rewrite <-not_elem_of_dom. rewrite dom_insert_L.
-    cut (is_Some (σ !! l)); last by eexists. rewrite -elem_of_dom. set_solver+.
+    setoid_rewrite <-(not_elem_of_dom (D:=gset loc)). rewrite dom_insert_L.
+    cut (is_Some (σ !! l)); last by eexists. rewrite -(elem_of_dom (D:=gset loc)). set_solver+.
   - eapply lit_neq_state; last done.
-    setoid_rewrite <-not_elem_of_dom. rewrite dom_insert_L.
-    cut (is_Some (σ !! l)); last by eexists. rewrite -elem_of_dom. set_solver+.
+    setoid_rewrite <-(not_elem_of_dom (D:=gset loc)). rewrite dom_insert_L.
+    cut (is_Some (σ !! l)); last by eexists. rewrite -(elem_of_dom (D:=gset loc)). set_solver+.
   - eapply lit_eq_state; last done.
-    setoid_rewrite <-not_elem_of_dom. rewrite dom_insert_L.
-    cut (is_Some (σ !! l)); last by eexists. rewrite -elem_of_dom. set_solver+.
+    setoid_rewrite <-(not_elem_of_dom (D:=gset loc)). rewrite dom_insert_L.
+    cut (is_Some (σ !! l)); last by eexists. rewrite -(elem_of_dom (D:=gset loc)). set_solver+.
 Qed.
 
 Lemma next_access_head_Free_concurent_step e1 e1' e2 e'f σ σ' o1 a2 l :
diff --git a/theories/lifetime/model/creation.v b/theories/lifetime/model/creation.v
index befd40f28d4c8ee8d84a3d866cec362051e34427..c0caed9af1cb00aed166a84ad773567715f2c73f 100644
--- a/theories/lifetime/model/creation.v
+++ b/theories/lifetime/model/creation.v
@@ -55,7 +55,7 @@ Proof.
   iModIntro. rewrite /lft_inv_dead. iExists Q. by iFrame.
 Qed.
 
-Lemma lfts_kill A (I : gmap lft lft_names) (K K' : gset lft) :
+Lemma lfts_kill (A : gmap atomic_lft _) (I : gmap lft lft_names) (K K' : gset lft) :
   let Iinv K' := (own_ilft_auth I ∗ [∗ set] κ' ∈ K', lft_inv_alive κ')%I in
   K ⊥ K' →
   (∀ κ κ', κ ∈ K → is_Some (I !! κ') → κ ⊆ κ' → κ' ∈ K) →
@@ -168,12 +168,12 @@ Proof.
     iIntros (κ [[Hκ HκI]%elem_of_filter HκK]%elem_of_difference) "Halive".
     rewrite /lft_inv. iLeft. iFrame "Halive". iPureIntro.
     apply lft_alive_in_insert_false; last done.
-    move: HκK. rewrite elem_of_kill_set -elem_of_dom. set_solver +HκI.
+    move: HκK. rewrite elem_of_kill_set -(elem_of_dom (D:=gset lft)). set_solver +HκI.
   - iApply (@big_sepS_impl with "[$Hinv]"); iIntros "!#".
     rewrite /lft_inv. iIntros (κ Hκ) "[[? %]|[? %]]".
     + iLeft. iFrame. iPureIntro.
       apply lft_alive_in_insert_false; last done. intros ?.
-      assert (κ ∈ K) by (rewrite elem_of_kill_set -elem_of_dom HI elem_of_union; auto).
+      assert (κ ∈ K) by (rewrite elem_of_kill_set -(elem_of_dom (D:=gset lft)) HI elem_of_union; auto).
       eapply HK'', Hκ. rewrite elem_of_union. auto.
     + iRight. iFrame. iPureIntro. by apply lft_dead_in_insert_false.
 Qed.
diff --git a/theories/lifetime/model/faking.v b/theories/lifetime/model/faking.v
index 0714e38e31110531884a34cccb37dd9dbe958245..dfb8359c6aaa9c19a39ef298fe59f4caf736877a 100644
--- a/theories/lifetime/model/faking.v
+++ b/theories/lifetime/model/faking.v
@@ -21,7 +21,7 @@ Proof.
   iMod (own_alloc ((● ∅ ⋅ ◯ ∅) :auth (gmap slice_name
       (frac * agree bor_stateC)))) as (γbor) "[Hbor Hbor']";
     first by apply auth_valid_discrete_2.
-  iMod (own_alloc ((● ∅) :auth (gset_disj slice_name)))
+  iMod (own_alloc ((● ε) :auth (gset_disj slice_name)))
      as (γinh) "Hinh"; first by done.
   set (γs := LftNames γbor γcnt γinh).
   iMod (own_update with "HI") as "[HI Hγs]".
diff --git a/theories/lifetime/model/primitive.v b/theories/lifetime/model/primitive.v
index 54daebe3797c2d929dab3e1c3bc355d7e1066126..a4c995fc218d1baad5adbc8133dc846621f0360d 100644
--- a/theories/lifetime/model/primitive.v
+++ b/theories/lifetime/model/primitive.v
@@ -452,7 +452,7 @@ Proof.
   iModIntro. iSplitL "Hbox HE".
   { iNext. rewrite /lft_inh. iExists ({[γE]} ∪ PE).
     rewrite to_gmap_union_singleton. iFrame. }
-  clear dependent PE. rewrite -(left_id_L ∅ op (◯ GSet {[γE]})).
+  clear dependent PE. rewrite -(left_id_L ε op (◯ GSet {[γE]})).
   iDestruct "HE◯" as "[HE◯' HE◯]". iSplitL "HE◯'".
   { iIntros (I) "HI". iApply (own_inh_auth with "HI HE◯'"). }
   iIntros (Q'). rewrite {1}/lft_inh. iDestruct 1 as (PE) "[>HE Hbox]".
diff --git a/theories/lifetime/model/reborrow.v b/theories/lifetime/model/reborrow.v
index 2e7d4d9af3a6f9a6e70a5b304f89c1706070f168..f73146de35580395f509484fb5a066ab2a5aa2d0 100644
--- a/theories/lifetime/model/reborrow.v
+++ b/theories/lifetime/model/reborrow.v
@@ -70,7 +70,7 @@ Proof.
   iNext. rewrite lft_vs_unfold. iExists (S n). iFrame "Hn●".
   iIntros (I) "Hinv [HP HPb] #Hκ†".
   rewrite {1}lft_vs_inv_unfold; iDestruct "Hinv" as "(Hκdead' & HI & Hinv)".
-  iDestruct (own_bor_auth with "HI Hi") as %?%elem_of_dom.
+  iDestruct (own_bor_auth with "HI Hi") as %?%(elem_of_dom (D:=gset lft)).
   iDestruct (@big_sepS_delete with "Hinv") as "[Hκalive Hinv]"; first done.
   rewrite lft_inv_alive_unfold.
   iDestruct ("Hκalive" with "[//]") as (Pb' Pi') "(Hκalive&Hvs'&Hinh)".
diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index 123029972f8c15f41b31ecf44f6ad81cf3400138..4835e61ec5f6037e1bc4b8abf51fe5ea2efa1c82 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -290,7 +290,7 @@ Section code.
           -- iLeft. iSplit; first done. rewrite Hincls. iFrame "Hl†".
              iMod (own_update_2 with "Hst Htok") as "Hst".
              { apply auth_update_dealloc. rewrite -{1}(right_id (None, 0%nat) _ (_, _)).
-               apply cancel_local_update_empty, _. }
+               apply cancel_local_update_unit, _. }
              rewrite -[in (1).[ν]%I]Hqq' -[(|={∅,⊤}=>_)%I]fupd_trans.
              iApply step_fupd_mask_mono;
                last iMod ("Hνend" with "[$Hν $Hν1]") as "H†"; try done.
@@ -309,7 +309,7 @@ Section code.
                 iModIntro. iNext. iMod "H†". iMod ("Hν†" with "H†") as "Hty". iModIntro.
                 iMod (own_update_2 with "Hst Htok") as "Hst".
                 { apply auth_update_dealloc, prod_local_update_1,
-                        (cancel_local_update_empty (Some _) None). }
+                        (cancel_local_update_unit (Some _) None). }
                 iSplitL "Hty".
                 { iDestruct "Hty" as (vy) "[H Hty]". iExists vy. iFrame.
                   by iApply "Hinclo". }
@@ -319,7 +319,7 @@ Section code.
         * iIntros "Hl1".
           iMod (own_update_2 with "Hst Htok") as "[Hst Htok]".
           { apply auth_update. etrans.
-            - rewrite [(Some _, weak)]pair_split. apply cancel_local_update_empty, _.
+            - rewrite [(Some _, weak)]pair_split. apply cancel_local_update_unit, _.
             - apply (op_local_update _ _ (Some (Cinr (Excl tt)), 0%nat)). auto. }
           rewrite -[(|={∅,⊤}=>_)%I]fupd_trans -[in (1).[ν]%I]Hqq'.
           iApply step_fupd_mask_mono;
@@ -343,14 +343,14 @@ Section code.
              iApply ("Hclose" with "[>- $Hna]"). iExists (None, 0%nat).
              iMod (own_update_2 with "Hst Htok") as "$"; last done.
              apply auth_update_dealloc. rewrite -{1}(right_id (None, 0%nat) _ (_, _)).
-             apply cancel_local_update_empty, _.
+             apply cancel_local_update_unit, _.
           -- iRight. iSplitR; first by auto with lia. iIntros "!> Hl† Hl2 Hvl".
              iApply ("Hclose" with "[>- $Hna]"). iExists (None, S weak).
              rewrite Hincls. iFrame. iSplitR "Hl2"; last first.
              { simpl. destruct Pos.of_succ_nat; rewrite /= ?Pos.pred_double_succ //. }
              iMod (own_update_2 with "Hst Htok") as "$"; last done.
              apply auth_update_dealloc, prod_local_update', reflexivity.
-             rewrite -{1}(right_id None _ (Some _)). apply cancel_local_update_empty, _.
+             rewrite -{1}(right_id None _ (Some _)). apply cancel_local_update_unit, _.
       + apply csum_included in Hincl.
         destruct Hincl as [->|[(?&(?,?)&[=<-]&->&(q',strong)&[]%(inj2 pair))|
                                (?&?&[=]&?)]]; first done. setoid_subst.
@@ -362,7 +362,7 @@ Section code.
         * iMod (own_update_2 with "Hst Htok") as "Hst".
           { apply auth_update_dealloc.
             rewrite -pair_op -Cinl_op Some_op -{1}(left_id 0%nat _ weak) -pair_op.
-            apply (cancel_local_update_empty _ (_, _)). }
+            apply (cancel_local_update_unit _ (_, _)). }
           iApply "Hclose". iFrame. iExists _. iFrame. iExists (q+q'')%Qp. iFrame.
           iSplitL; first last.
           { rewrite [(_+_)%Qp]assoc [(q'+_)%Qp]comm. auto. }
diff --git a/theories/typing/lib/rc/weak.v b/theories/typing/lib/rc/weak.v
index 4e50af06d3d9102ed2c852ca1cfcbfc93ae9d2c5..992f8b234d9172dbeb80055298c31557be1e1771 100644
--- a/theories/typing/lib/rc/weak.v
+++ b/theories/typing/lib/rc/weak.v
@@ -404,7 +404,7 @@ Section code.
       destruct weakc; first by simpl in *; lia.
       iMod (own_update_2 with "Hrc● Hwtok") as "Hrc●".
       { apply auth_update_dealloc, prod_local_update_2,
-              (cancel_local_update_empty 1%nat), _. }
+              (cancel_local_update_unit 1%nat), _. }
       destruct st as [[[q'' strong]| |]|]; try done.
       - iExists _. iDestruct "Hrcst" as (q0) "(Hlw & >$ & Hrcst)". iRight.
         iSplitR; first by auto with lia. iIntros "!>?". iApply "Hclose". iFrame.
diff --git a/theories/typing/lib/refcell/ref_code.v b/theories/typing/lib/refcell/ref_code.v
index 87012a873bb7fa74f639dc196f6e91b4d0766d1f..ca36f8eab0d6cc56facec2e26310d295347f41d1 100644
--- a/theories/typing/lib/refcell/ref_code.v
+++ b/theories/typing/lib/refcell/ref_code.v
@@ -177,7 +177,7 @@ Section ref_functions.
       - destruct Heq as [?%leibniz_equiv ?%leibniz_equiv]. simpl in *. subst.
         iExists None. iFrame. iMod (own_update with "H●◯") as "$".
         { apply auth_update_dealloc. rewrite -(right_id None op (Some _)).
-          apply cancel_local_update_empty, _. }
+          apply cancel_local_update_unit, _. }
         iApply "H†". replace 1%Qp with (q'+q'')%Qp by naive_solver. iFrame.
       - destruct Hincl as [ [=] |[ (?&?&[=]&?) | (?&?&[=<-]&[=<-]&[[q0 n']EQ]) ]].
         destruct EQ as [?%leibniz_equiv ?%leibniz_equiv]. simpl in *. subst.
@@ -186,7 +186,7 @@ Section ref_functions.
         iExists (Some (_, Cinr (q0, n'))). iFrame. iMod (own_update with "H●◯") as "$".
         { apply auth_update_dealloc.
           rewrite -(agree_idemp (to_agree _)) -pair_op -Cinr_op -pair_op Some_op.
-          apply (cancel_local_update_empty (reading_st q ν)), _. }
+          apply (cancel_local_update_unit (reading_st q ν)), _. }
         iExists ν. iFrame. iApply step_fupd_intro; first set_solver. iIntros "!>".
         iSplitR; first done. iExists (q+q'')%Qp. iFrame.
         by rewrite assoc (comm _ q0 q). }
diff --git a/theories/typing/lib/refcell/refmut_code.v b/theories/typing/lib/refcell/refmut_code.v
index acc5cc5b6b0ab94d273889a6b75b1ecccb36c787..396713e73cbecbd762d25fea91f0dd33defd48b6 100644
--- a/theories/typing/lib/refcell/refmut_code.v
+++ b/theories/typing/lib/refcell/refmut_code.v
@@ -138,7 +138,7 @@ Section refmut_functions.
     iMod ("Hcloseβ" with "[> H↦lrc H● H◯ Hb] Hna") as "[Hβ Hna]".
     { iExists None. iFrame. iMod (own_update_2 with "H● H◯") as "$"; last done.
       apply auth_update_dealloc. rewrite -(right_id None _ (Some _)).
-      apply cancel_local_update_empty, _. }
+      apply cancel_local_update_unit, _. }
     iMod ("Hcloseα" with "Hβ") as "Hα". iMod ("Hclose" with "Hα HL") as "HL". wp_seq.
     iApply (type_type _ _ _ [ #lx ◁ box (uninit 2)]
             with "[] LFT HE Hna HL Hk"); last first.
diff --git a/theories/typing/lib/rwlock/rwlockreadguard_code.v b/theories/typing/lib/rwlock/rwlockreadguard_code.v
index 5e3905c02b1e40ffe984b2579285943403b53631..9a6f357382380c9595adce8710acb92bd77be449 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard_code.v
@@ -100,7 +100,7 @@ Section rwlockreadguard_functions.
           iMod ("H†" with "Hν") as "H†". iModIntro. iNext. iMod "H†".
           iMod ("Hh" with "H†") as "Hb". iIntros "!> Hlx". iExists None. iFrame.
           iApply (own_update_2 with "H● H◯"). apply auth_update_dealloc.
-          rewrite -(right_id None op (Some _)). apply cancel_local_update_empty, _.
+          rewrite -(right_id None op (Some _)). apply cancel_local_update_unit, _.
         - iApply step_fupd_intro. set_solver. iNext. iIntros "Hlx".
           apply csum_included in Hle.
           destruct Hle as [|[(?&?&[=]&?)|(?&[[agν q']n]&[=<-]&->&Hle%prod_included)]];
@@ -118,7 +118,7 @@ Section rwlockreadguard_functions.
           assert (n = 1%positive ⋅ Pos.pred n) as EQn.
           { rewrite pos_op_plus -Pplus_one_succ_l Pos.succ_pred // =>?. by subst. }
           rewrite {1}EQn -{1}(agree_idemp (to_agree _)) -2!pair_op -Cinr_op Some_op.
-          apply (cancel_local_update_empty (reading_st q ν)) , _. }
+          apply (cancel_local_update_unit (reading_st q ν)) , _. }
       iApply (wp_step_fupd with "INV"). done. set_solver.
       iApply (wp_cas_int_suc with "Hlx"); try done. iNext. iIntros "Hlx INV !>".
       iMod ("INV" with "Hlx") as "INV". iMod ("Hcloseβ" with "[$INV]") as "Hβ".
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard_code.v b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
index 548fe054bf5a19e9073dcf9fdbbc0ea22c17f6ca..bc97a8042f3cc0efa6cee6937b2152b0e7672184 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
@@ -131,7 +131,7 @@ Section rwlockwriteguard_functions.
       destruct st0 as [[[]|]| |]; try by inversion Heq.
       iExists None. iFrame. iMod (own_update_2 with "H● H◯") as "$"; last done.
       apply auth_update_dealloc. rewrite -(right_id None op (Some _)).
-      apply cancel_local_update_empty, _. }
+      apply cancel_local_update_unit, _. }
     iModIntro. wp_seq. iMod ("Hcloseα" with "Hβ") as "Hα".
     iMod ("Hclose" with "Hα HL") as "HL".
     iApply (type_type _ _ _ [ x ◁ box (uninit 1)]
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 21cefb195c8614ce417505f2cdd6e70b58792d49..73f808382d72df874328e11a006a9e6075b43307 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -13,7 +13,7 @@ Class typeG Σ := TypeG {
   type_frac_borrowG :> frac_borG Σ
 }.
 
-Definition lftE := ↑lftN.
+Definition lftE : coPset := ↑lftN.
 Definition lrustN := nroot .@ "lrust".
 Definition shrN  := lrustN .@ "shr".