diff --git a/Makefile b/Makefile
index 9b16ec0..6c23421 100644
--- a/Makefile
+++ b/Makefile
@@ -1,7 +1,6 @@
 TRILLIUM_DIR := 'trillium'
-FAIRIS_DIR := 'fairis'
 FAIRNERIS_DIR := 'fairneris'
-LOCAL_SRC_DIRS := $(TRILLIUM_DIR) $(FAIRIS_DIR) $(FAIRNERIS_DIR)
+LOCAL_SRC_DIRS := $(TRILLIUM_DIR) $(FAIRNERIS_DIR)
 SRC_DIRS := $(LOCAL_SRC_DIRS) 'external'
 
 ALL_VFILES := $(shell find $(SRC_DIRS) -name "*.v")
@@ -46,7 +45,7 @@ clean:
 # project-specific targets
 .PHONY: build clean-trillium clean-fairis clean-fairneris trillium fairis fairneris
 
-VPATH= $(TRILLIUM_DIR) $(FAIRIS_DIR) $(FAIRNERIS_DIR)
+VPATH= $(TRILLIUM_DIR) $(FAIRNERIS_DIR)
 VPATH_FILES := $(shell find $(VPATH) -name "*.v")
 
 build: $(VPATH_FILES:.v=.vo)
@@ -54,9 +53,6 @@ build: $(VPATH_FILES:.v=.vo)
 fairneris :
 	@$(MAKE) build VPATH=$(FAIRNERIS_DIR)
 
-fairis :
-	@$(MAKE) build VPATH=$(FAIRIS_DIR)
-
 trillium :
 	@$(MAKE) build VPATH=$(TRILLIUM_DIR)
 
@@ -68,8 +64,5 @@ clean-local:
 clean-trillium:
 	@$(MAKE) clean-local LOCAL_SRC_DIRS=$(TRILLIUM_DIR)
 
-clean-fairis:
-	@$(MAKE) clean-local LOCAL_SRC_DIRS=$(FAIRIS_DIR)
-
 clean-fairneris:
 	@$(MAKE) clean-local LOCAL_SRC_DIRS=$(FAIRNERIS_DIR)
diff --git a/_CoqProject b/_CoqProject
index 863644f..9a10a84 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -1,5 +1,4 @@
 -Q trillium trillium
--Q fairis trillium.fairness
 -Q fairneris fairneris
 
 -Q external/stdpp/stdpp stdpp
@@ -9,6 +8,7 @@
 -Q external/iris/iris_unstable iris.unstable
 -Q external/iris/iris_heap_lang iris.heap_lang
 -Q external/paco/src Paco
+-Q external/coq-record-update/src RecordUpdate
 
 -arg -w -arg -notation-overridden
 -arg -w -arg -redundant-canonical-projection
diff --git a/fairneris/examples/retransmit_example_adequacy.v b/fairneris/examples/retransmit_example_adequacy.v
index 4b24ed0..93f9bbd 100644
--- a/fairneris/examples/retransmit_example_adequacy.v
+++ b/fairneris/examples/retransmit_example_adequacy.v
@@ -19,7 +19,7 @@ Definition initial_state shA shB :=
         state_ms := ∅; |}).
 
 Definition initial_model_state : retransmit_state :=
-  (retransmit_model_base.Start, ∅, ∅).
+  (retransmit_model.Start, ∅, ∅).
 
 Lemma retransmit_continued_simulation shA shB :
   fairly_terminating localeB (initial_state shA shB).
diff --git a/fairneris/partial_termination.v b/fairneris/partial_termination.v
index ea6818c..74f9e3b 100644
--- a/fairneris/partial_termination.v
+++ b/fairneris/partial_termination.v
@@ -298,7 +298,7 @@ Qed.
 Lemma not_infinite_terminating_trace {S L} (tr : trace S L) :
   ¬ infinite_trace tr → terminating_trace tr.
 Proof.
-  intros Hinf. epose proof (infinite_or_finite) as [?|?]; done.
+  intros Hinf. epose proof (infinite_or_finite tr) as [?|?]; done.
 Qed.
 
 Lemma trace_always_mono_strong_alt
diff --git a/flake.lock b/flake.lock
index f6ca995..084f496 100644
--- a/flake.lock
+++ b/flake.lock
@@ -5,11 +5,11 @@
         "systems": "systems"
       },
       "locked": {
-        "lastModified": 1692799911,
-        "narHash": "sha256-3eihraek4qL744EvQXsK1Ha6C3CR7nnT8X2qWap4RNk=",
+        "lastModified": 1705309234,
+        "narHash": "sha256-uNRRNRKmJyCRC/8y1RqBkqWBLM034y4qN7EprSdmgyA=",
         "owner": "numtide",
         "repo": "flake-utils",
-        "rev": "f9e7cf818399d17d347f847525c5a5a8032e4e44",
+        "rev": "1ef2e671c3b0c19053962c07dbda38332dcebf26",
         "type": "github"
       },
       "original": {
@@ -20,11 +20,11 @@
     },
     "nixpkgs": {
       "locked": {
-        "lastModified": 1693158576,
-        "narHash": "sha256-aRTTXkYvhXosGx535iAFUaoFboUrZSYb1Ooih/auGp0=",
+        "lastModified": 1708475490,
+        "narHash": "sha256-g1v0TsWBQPX97ziznfJdWhgMyMGtoBFs102xSYO4syU=",
         "owner": "nixos",
         "repo": "nixpkgs",
-        "rev": "a999c1cc0c9eb2095729d5aa03e0d8f7ed256780",
+        "rev": "0e74ca98a74bc7270d28838369593635a5db3260",
         "type": "github"
       },
       "original": {
diff --git a/flake.nix b/flake.nix
index 6c235b3..0820fca 100644
--- a/flake.nix
+++ b/flake.nix
@@ -18,7 +18,7 @@
       with pkgs;
       {
         devShell = mkShell rec {
-          buildInputs = with coqPackages_8_17; [
+          buildInputs = with coqPackages_8_19; [
             coq
 
           # coq-lsp.packages.${system}.coq-lsp