diff --git a/CHANGELOG.md b/CHANGELOG.md
index cfd5f40d65b455f251f9fc76133d5e60b5c2dce3..928f2ae5bd844d48ceaa8ac255e949d482ae376c 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,7 +1,14 @@
 In this changelog, we document "large-ish" changes to Iris that affect even the
 way the logic is used on paper.  We also mention some significant changes in the
 Coq development, but not every API-breaking change is listed.  Changes marked
-[#] still need to be ported to the Iris Documentation LaTeX file.
+[#] still need to be ported to the Iris Documentation LaTeX file(s).
+
+## Iris 3.0
+
+* [#] View shifts are radically simplified to just internalize frame-preserving
+  updates.  Weakestpre is defined inside the logic, and invariants and view
+  shifts with masks are also coded up inside Iris.
+* [#] The language can now fork off multiple threads at once.
 
 ## Iris 2.0
 
diff --git a/_CoqProject b/_CoqProject
index 5f647349c44d2b4554b2c0822bb10089bf6cde9a..8aa83107ec4579662380fa3e2c003f7c45ffe432 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -76,7 +76,6 @@ program_logic/ectx_language.v
 program_logic/ectxi_language.v
 program_logic/ectx_lifting.v
 program_logic/ghost_ownership.v
-program_logic/global_functor.v
 program_logic/saved_prop.v
 program_logic/auth.v
 program_logic/sts.v
@@ -110,6 +109,7 @@ tests/proofmode.v
 tests/barrier_client.v
 tests/list_reverse.v
 tests/tree_sum.v
+tests/counter.v
 proofmode/coq_tactics.v
 proofmode/pviewshifts.v
 proofmode/environments.v
diff --git a/algebra/cofe_solver.v b/algebra/cofe_solver.v
index 515028163eaa79d7aa529cfeb42c6c6b8e0ffe08..20a9ff0f01bfb9788a0525f29c873d107950da65 100644
--- a/algebra/cofe_solver.v
+++ b/algebra/cofe_solver.v
@@ -106,17 +106,17 @@ Proof. by assert (k = j) by lia; subst; rewrite !coerce_id. Qed.
 Lemma coerce_f {k j} (H : S k = S j) (x : A k) :
   coerce H (f k x) = f j (coerce (Nat.succ_inj _ _ H) x).
 Proof. by assert (k = j) by lia; subst; rewrite !coerce_id. Qed.
-Lemma gg_gg {k i i1 i2 j} (H1 : k = i + j) (H2 : k = i2 + (i1 + j)) (x : A k) :
+Lemma gg_gg {k i i1 i2 j} : âˆ€ (H1: k = i + j) (H2: k = i2 + (i1 + j)) (x: A k),
   gg i (coerce H1 x) = gg i1 (gg i2 (coerce H2 x)).
 Proof.
-  assert (i = i2 + i1) by lia; simplify_eq/=. revert j x H1.
+  intros ? -> x. assert (i = i2 + i1) as -> by lia. revert j x H1.
   induction i2 as [|i2 IH]; intros j X H1; simplify_eq/=;
     [by rewrite coerce_id|by rewrite g_coerce IH].
 Qed.
-Lemma ff_ff {k i i1 i2 j} (H1 : i + k = j) (H2 : i1 + (i2 + k) = j) (x : A k) :
+Lemma ff_ff {k i i1 i2 j} : âˆ€ (H1: i + k = j) (H2: i1 + (i2 + k) = j) (x: A k),
   coerce H1 (ff i x) = coerce H2 (ff i1 (ff i2 x)).
 Proof.
-  assert (i = i1 + i2) by lia; simplify_eq/=.
+  intros ? <- x. assert (i = i1 + i2) as -> by lia.
   induction i1 as [|i1 IH]; simplify_eq/=;
     [by rewrite coerce_id|by rewrite coerce_f IH].
 Qed.
diff --git a/algebra/list.v b/algebra/list.v
index 3ab4d27c259f3b75a130ae1163f0814ff01d522b..1c4389ac50e450291e50931b7bbc47d1d118aa64 100644
--- a/algebra/list.v
+++ b/algebra/list.v
@@ -81,13 +81,16 @@ End cofe.
 Arguments listC : clear implicits.
 
 (** Functor *)
+Lemma list_fmap_ext_ne {A} {B : cofeT} (f g : A â†’ B) (l : list A) n :
+  (âˆ€ x, f x â‰¡{n}â‰¡ g x) â†’ f <$> l â‰¡{n}â‰¡ g <$> l.
+Proof. intros Hf. by apply Forall2_fmap, Forall_Forall2, Forall_true. Qed.
 Instance list_fmap_ne {A B : cofeT} (f : A â†’ B) n:
   Proper (dist n ==> dist n) f â†’ Proper (dist n ==> dist n) (fmap (M:=list) f).
-Proof. intros Hf l k ?; by eapply Forall2_fmap, Forall2_impl; eauto. Qed. 
+Proof. intros Hf l k ?; by eapply Forall2_fmap, Forall2_impl; eauto. Qed.
 Definition listC_map {A B} (f : A -n> B) : listC A -n> listC B :=
   CofeMor (fmap f : listC A â†’ listC B).
 Instance listC_map_ne A B n : Proper (dist n ==> dist n) (@listC_map A B).
-Proof. intros f f' ? l; by apply Forall2_fmap, Forall_Forall2, Forall_true. Qed.
+Proof. intros f g ? l. by apply list_fmap_ext_ne. Qed.
 
 Program Definition listCF (F : cFunctor) : cFunctor := {|
   cFunctor_car A B := listC (cFunctor_car F A B);
diff --git a/algebra/upred.v b/algebra/upred.v
index 1bd35b4c9de6550b762a3a002cc779ce8a72e960..37cc9c626a24d14998c45c601c19f6aba8cf5c52 100644
--- a/algebra/upred.v
+++ b/algebra/upred.v
@@ -328,13 +328,6 @@ Arguments uPred_always_if _ !_ _/.
 Notation "â–¡? p P" := (uPred_always_if p P)
   (at level 20, p at level 0, P at level 20, format "â–¡? p  P").
 
-Definition uPred_laterN {M} (n : nat) (P : uPred M) : uPred M :=
-  Nat.iter n uPred_later P.
-Instance: Params (@uPred_laterN) 2.
-Notation "â–·^ n P" := (uPred_laterN n P)
-  (at level 20, n at level 9, right associativity,
-   format "â–·^ n  P") : uPred_scope.
-
 Definition uPred_now_True {M} (P : uPred M) : uPred M := â–· False âˆ¨ P.
 Notation "â—‡ P" := (uPred_now_True P)
   (at level 20, right associativity) : uPred_scope.
@@ -987,8 +980,6 @@ Lemma always_entails_l' P Q : (P âŠ¢ â–¡ Q) â†’ P âŠ¢ â–¡ Q â˜… P.
 Proof. intros; rewrite -always_and_sep_l'; auto. Qed.
 Lemma always_entails_r' P Q : (P âŠ¢ â–¡ Q) â†’ P âŠ¢ P â˜… â–¡ Q.
 Proof. intros; rewrite -always_and_sep_r'; auto. Qed.
-Lemma always_laterN n P : â–¡ â–·^n P âŠ£âŠ¢ â–·^n â–¡ P.
-Proof. induction n as [|n IH]; simpl; auto. by rewrite always_later IH. Qed.
 
 (* Conditional always *)
 Global Instance always_if_ne n p : Proper (dist n ==> dist n) (@uPred_always_if M p).
@@ -1071,60 +1062,6 @@ Proof. apply wand_intro_r;rewrite -later_sep; eauto using wand_elim_l. Qed.
 Lemma later_iff P Q : â–· (P â†” Q) âŠ¢ â–· P â†” â–· Q.
 Proof. by rewrite /uPred_iff later_and !later_impl. Qed.
 
-(* n-times later *)
-Global Instance laterN_ne n m : Proper (dist n ==> dist n) (@uPred_laterN M m).
-Proof. induction m; simpl. by intros ???. solve_proper. Qed.
-Global Instance laterN_proper m :
-  Proper ((âŠ£âŠ¢) ==> (âŠ£âŠ¢)) (@uPred_laterN M m) := ne_proper _.
-
-Lemma later_laterN n P : â–·^(S n) P âŠ£âŠ¢ â–· â–·^n P.
-Proof. done. Qed.
-Lemma laterN_later n P : â–·^(S n) P âŠ£âŠ¢ â–·^n â–· P.
-Proof. induction n; simpl; auto. Qed.
-Lemma laterN_plus n1 n2 P : â–·^(n1 + n2) P âŠ£âŠ¢ â–·^n1 â–·^n2 P.
-Proof. induction n1; simpl; auto. Qed.
-Lemma laterN_le n1 n2 P : n1 â‰¤ n2 â†’ â–·^n1 P âŠ¢ â–·^n2 P.
-Proof. induction 1; simpl; by rewrite -?later_intro. Qed.
-
-Lemma laterN_mono n P Q : (P âŠ¢ Q) â†’ â–·^n P âŠ¢ â–·^n Q.
-Proof. induction n; simpl; auto. Qed.
-Lemma laterN_intro n P : P âŠ¢ â–·^n P.
-Proof. induction n as [|n IH]; simpl; by rewrite -?later_intro. Qed.
-Lemma laterN_and n P Q : â–·^n (P âˆ§ Q) âŠ£âŠ¢ â–·^n P âˆ§ â–·^n Q.
-Proof. induction n as [|n IH]; simpl; rewrite -?later_and; auto. Qed.
-Lemma laterN_or n P Q : â–·^n (P âˆ¨ Q) âŠ£âŠ¢ â–·^n P âˆ¨ â–·^n Q.
-Proof. induction n as [|n IH]; simpl; rewrite -?later_or; auto. Qed.
-Lemma laterN_forall {A} n (Î¦ : A â†’ uPred M) : (â–·^n âˆ€ a, Î¦ a) âŠ£âŠ¢ (âˆ€ a, â–·^n Î¦ a).
-Proof. induction n as [|n IH]; simpl; rewrite -?later_forall; auto. Qed.
-Lemma laterN_exist_1 {A} n (Î¦ : A â†’ uPred M) : (âˆƒ a, â–·^n Î¦ a) âŠ¢ (â–·^n âˆƒ a, Î¦ a).
-Proof. induction n as [|n IH]; simpl; rewrite ?later_exist_1; auto. Qed.
-Lemma laterN_exist_2 `{Inhabited A} n (Î¦ : A â†’ uPred M) :
-  (â–·^n âˆƒ a, Î¦ a) âŠ¢ âˆƒ a, â–·^n Î¦ a.
-Proof. induction n as [|n IH]; simpl; rewrite -?later_exist_2; auto. Qed.
-Lemma laterN_sep n P Q : â–·^n (P â˜… Q) âŠ£âŠ¢ â–·^n P â˜… â–·^n Q.
-Proof. induction n as [|n IH]; simpl; rewrite -?later_sep; auto. Qed.
-
-Global Instance laterN_mono' n : Proper ((âŠ¢) ==> (âŠ¢)) (@uPred_laterN M n).
-Proof. intros P Q; apply laterN_mono. Qed.
-Global Instance laterN_flip_mono' n :
-  Proper (flip (âŠ¢) ==> flip (âŠ¢)) (@uPred_laterN M n).
-Proof. intros P Q; apply laterN_mono. Qed.
-Lemma laterN_True n : â–·^n True âŠ£âŠ¢ True.
-Proof. apply (anti_symm (âŠ¢)); auto using laterN_intro. Qed.
-Lemma laterN_impl n P Q : â–·^n (P â†’ Q) âŠ¢ â–·^n P â†’ â–·^n Q.
-Proof.
-  apply impl_intro_l; rewrite -laterN_and; eauto using impl_elim, laterN_mono.
-Qed.
-Lemma laterN_exist n `{Inhabited A} (Î¦ : A â†’ uPred M) :
-  â–·^n (âˆƒ a, Î¦ a) âŠ£âŠ¢ (âˆƒ a, â–·^n Î¦ a).
-Proof. apply: anti_symm; eauto using laterN_exist_2, laterN_exist_1. Qed.
-Lemma laterN_wand n P Q : â–·^n (P -â˜… Q) âŠ¢ â–·^n P -â˜… â–·^n Q.
-Proof.
-  apply wand_intro_r; rewrite -laterN_sep; eauto using wand_elim_l,laterN_mono.
-Qed.
-Lemma laterN_iff n P Q : â–·^n (P â†” Q) âŠ¢ â–·^n P â†” â–·^n Q.
-Proof. by rewrite /uPred_iff laterN_and !laterN_impl. Qed.
-
 (* True now *)
 Global Instance now_True_ne n : Proper (dist n ==> dist n) (@uPred_now_True M).
 Proof. solve_proper. Qed.
@@ -1244,7 +1181,7 @@ Proof.
   exists (y â‹… x3); split; first by rewrite -assoc.
   exists y; eauto using cmra_includedN_l.
 Qed.
-Lemma now_True_rvs P : â—‡ (|=r=> â—‡ P) âŠ¢ (|=r=> â—‡ P).
+Lemma now_True_rvs P : â—‡ (|=r=> P) âŠ¢ (|=r=> â—‡ P).
 Proof.
   rewrite /uPred_now_True. apply or_elim; auto using rvs_mono.
   by rewrite -rvs_intro -or_intro_l.
@@ -1390,8 +1327,6 @@ Global Instance valid_persistent {A : cmraT} (a : A) :
 Proof. by intros; rewrite /PersistentP always_valid. Qed.
 Global Instance later_persistent P : PersistentP P â†’ PersistentP (â–· P).
 Proof. by intros; rewrite /PersistentP always_later; apply later_mono. Qed.
-Global Instance laterN_persistent n P : PersistentP P â†’ PersistentP (â–·^n P).
-Proof. induction n; apply _. Qed.
 Global Instance ownM_persistent : Persistent a â†’ PersistentP (@uPred_ownM M a).
 Proof. intros. by rewrite /PersistentP always_ownM. Qed.
 Global Instance from_option_persistent {A} P (Î¨ : A â†’ uPred M) (mx : option A) :
@@ -1427,14 +1362,8 @@ Proof.
   eapply IH with x'; eauto using cmra_validN_S, cmra_validN_op_l.
 Qed.
 
-Lemma soundness_laterN n : Â¬(True âŠ¢ â–·^n False).
-Proof.
-  intros H. apply (adequacy False n). rewrite H {H}.
-  induction n as [|n IH]; rewrite /= ?IH; auto using rvs_intro.
-Qed.
-
 Theorem soundness : Â¬ (True âŠ¢ False).
-Proof. exact (soundness_laterN 0). Qed.
+Proof. exact (adequacy False 0). Qed.
 End uPred_logic.
 
 (* Hint DB for the logic *)
diff --git a/heap_lang/adequacy.v b/heap_lang/adequacy.v
index 174a73cb320bb4bd3b51361267029ad9fb7e79d5..89990989d5a81b261b795a6498c9819173e489dd 100644
--- a/heap_lang/adequacy.v
+++ b/heap_lang/adequacy.v
@@ -4,7 +4,7 @@ From iris.program_logic Require Import auth ownership.
 From iris.heap_lang Require Import proofmode notation.
 From iris.proofmode Require Import tactics weakestpre.
 
-Definition heapGF : gFunctorList := [authGF heapUR; irisGF heap_lang].
+Definition heapÎ£ : gFunctors := #[authÎ£ heapUR; irisÎ£ heap_lang].
 
 Definition heap_adequacy Î£ `{irisPreG heap_lang Î£, authG Î£ heapUR} e Ïƒ Ï† :
   (âˆ€ `{heapG Î£}, heap_ctx âŠ¢ WP e {{ v, â–  Ï† v }}) â†’
diff --git a/heap_lang/lang.v b/heap_lang/lang.v
index 881e486cc2d0b59fc0da2ec654792352496b8ab6..186439910c6b4597a37d46727aaa9cd6cb197f7c 100644
--- a/heap_lang/lang.v
+++ b/heap_lang/lang.v
@@ -225,53 +225,53 @@ Definition bin_op_eval (op : bin_op) (l1 l2 : base_lit) : option base_lit :=
   | _, _, _ => None
   end.
 
-Inductive head_step : expr â†’ state â†’ expr â†’ state â†’ option (expr) â†’ Prop :=
+Inductive head_step : expr â†’ state â†’ expr â†’ state â†’ list (expr) â†’ Prop :=
   | BetaS f x e1 e2 v2 e' Ïƒ :
      to_val e2 = Some v2 â†’
      Closed (f :b: x :b: []) e1 â†’
      e' = subst' x (of_val v2) (subst' f (Rec f x e1) e1) â†’
-     head_step (App (Rec f x e1) e2) Ïƒ e' Ïƒ None
+     head_step (App (Rec f x e1) e2) Ïƒ e' Ïƒ []
   | UnOpS op l l' Ïƒ :
      un_op_eval op l = Some l' â†’ 
-     head_step (UnOp op (Lit l)) Ïƒ (Lit l') Ïƒ None
+     head_step (UnOp op (Lit l)) Ïƒ (Lit l') Ïƒ []
   | BinOpS op l1 l2 l' Ïƒ :
      bin_op_eval op l1 l2 = Some l' â†’ 
-     head_step (BinOp op (Lit l1) (Lit l2)) Ïƒ (Lit l') Ïƒ None
+     head_step (BinOp op (Lit l1) (Lit l2)) Ïƒ (Lit l') Ïƒ []
   | IfTrueS e1 e2 Ïƒ :
-     head_step (If (Lit $ LitBool true) e1 e2) Ïƒ e1 Ïƒ None
+     head_step (If (Lit $ LitBool true) e1 e2) Ïƒ e1 Ïƒ []
   | IfFalseS e1 e2 Ïƒ :
-     head_step (If (Lit $ LitBool false) e1 e2) Ïƒ e2 Ïƒ None
+     head_step (If (Lit $ LitBool false) e1 e2) Ïƒ e2 Ïƒ []
   | FstS e1 v1 e2 v2 Ïƒ :
      to_val e1 = Some v1 â†’ to_val e2 = Some v2 â†’
-     head_step (Fst (Pair e1 e2)) Ïƒ e1 Ïƒ None
+     head_step (Fst (Pair e1 e2)) Ïƒ e1 Ïƒ []
   | SndS e1 v1 e2 v2 Ïƒ :
      to_val e1 = Some v1 â†’ to_val e2 = Some v2 â†’
-     head_step (Snd (Pair e1 e2)) Ïƒ e2 Ïƒ None
+     head_step (Snd (Pair e1 e2)) Ïƒ e2 Ïƒ []
   | CaseLS e0 v0 e1 e2 Ïƒ :
      to_val e0 = Some v0 â†’
-     head_step (Case (InjL e0) e1 e2) Ïƒ (App e1 e0) Ïƒ None
+     head_step (Case (InjL e0) e1 e2) Ïƒ (App e1 e0) Ïƒ []
   | CaseRS e0 v0 e1 e2 Ïƒ :
      to_val e0 = Some v0 â†’
-     head_step (Case (InjR e0) e1 e2) Ïƒ (App e2 e0) Ïƒ None
+     head_step (Case (InjR e0) e1 e2) Ïƒ (App e2 e0) Ïƒ []
   | ForkS e Ïƒ:
-     head_step (Fork e) Ïƒ (Lit LitUnit) Ïƒ (Some e)
+     head_step (Fork e) Ïƒ (Lit LitUnit) Ïƒ [e]
   | AllocS e v Ïƒ l :
      to_val e = Some v â†’ Ïƒ !! l = None â†’
-     head_step (Alloc e) Ïƒ (Lit $ LitLoc l) (<[l:=v]>Ïƒ) None
+     head_step (Alloc e) Ïƒ (Lit $ LitLoc l) (<[l:=v]>Ïƒ) []
   | LoadS l v Ïƒ :
      Ïƒ !! l = Some v â†’
-     head_step (Load (Lit $ LitLoc l)) Ïƒ (of_val v) Ïƒ None
+     head_step (Load (Lit $ LitLoc l)) Ïƒ (of_val v) Ïƒ []
   | StoreS l e v Ïƒ :
      to_val e = Some v â†’ is_Some (Ïƒ !! l) â†’
-     head_step (Store (Lit $ LitLoc l) e) Ïƒ (Lit LitUnit) (<[l:=v]>Ïƒ) None
+     head_step (Store (Lit $ LitLoc l) e) Ïƒ (Lit LitUnit) (<[l:=v]>Ïƒ) []
   | CasFailS l e1 v1 e2 v2 vl Ïƒ :
      to_val e1 = Some v1 â†’ to_val e2 = Some v2 â†’
      Ïƒ !! l = Some vl â†’ vl â‰  v1 â†’
-     head_step (CAS (Lit $ LitLoc l) e1 e2) Ïƒ (Lit $ LitBool false) Ïƒ None
+     head_step (CAS (Lit $ LitLoc l) e1 e2) Ïƒ (Lit $ LitBool false) Ïƒ []
   | CasSucS l e1 v1 e2 v2 Ïƒ :
      to_val e1 = Some v1 â†’ to_val e2 = Some v2 â†’
      Ïƒ !! l = Some v1 â†’
-     head_step (CAS (Lit $ LitLoc l) e1 e2) Ïƒ (Lit $ LitBool true) (<[l:=v2]>Ïƒ) None.
+     head_step (CAS (Lit $ LitLoc l) e1 e2) Ïƒ (Lit $ LitBool true) (<[l:=v2]>Ïƒ) [].
 
 (** Basic properties about the language *)
 Lemma to_of_val v : to_val (of_val v) = Some v.
@@ -294,11 +294,11 @@ Lemma fill_item_val Ki e :
   is_Some (to_val (fill_item Ki e)) â†’ is_Some (to_val e).
 Proof. intros [v ?]. destruct Ki; simplify_option_eq; eauto. Qed.
 
-Lemma val_stuck e1 Ïƒ1 e2 Ïƒ2 ef : head_step e1 Ïƒ1 e2 Ïƒ2 ef â†’ to_val e1 = None.
+Lemma val_stuck e1 Ïƒ1 e2 Ïƒ2 efs : head_step e1 Ïƒ1 e2 Ïƒ2 efs â†’ to_val e1 = None.
 Proof. destruct 1; naive_solver. Qed.
 
-Lemma head_ctx_step_val Ki e Ïƒ1 e2 Ïƒ2 ef :
-  head_step (fill_item Ki e) Ïƒ1 e2 Ïƒ2 ef â†’ is_Some (to_val e).
+Lemma head_ctx_step_val Ki e Ïƒ1 e2 Ïƒ2 efs :
+  head_step (fill_item Ki e) Ïƒ1 e2 Ïƒ2 efs â†’ is_Some (to_val e).
 Proof. destruct Ki; inversion_clear 1; simplify_option_eq; by eauto. Qed.
 
 Lemma fill_item_no_val_inj Ki1 Ki2 e1 e2 :
@@ -313,7 +313,7 @@ Qed.
 
 Lemma alloc_fresh e v Ïƒ :
   let l := fresh (dom _ Ïƒ) in
-  to_val e = Some v â†’ head_step (Alloc e) Ïƒ (Lit (LitLoc l)) (<[l:=v]>Ïƒ) None.
+  to_val e = Some v â†’ head_step (Alloc e) Ïƒ (Lit (LitLoc l)) (<[l:=v]>Ïƒ) [].
 Proof. by intros; apply AllocS, (not_elem_of_dom (D:=gset _)), is_fresh. Qed.
 
 (** Closed expressions *)
diff --git a/heap_lang/lib/barrier/proof.v b/heap_lang/lib/barrier/proof.v
index 69df1e7bbac23ef6e57fdaf95b757cb20cae0149..3a101a9417c884490c95b2ec4d04f30193f84ad3 100644
--- a/heap_lang/lib/barrier/proof.v
+++ b/heap_lang/lib/barrier/proof.v
@@ -14,10 +14,10 @@ Class barrierG Î£ := BarrierG {
   barrier_savedPropG :> savedPropG Î£ idCF;
 }.
 (** The Functors we need. *)
-Definition barrierGF : gFunctorList := [stsGF sts; savedPropGF idCF].
+Definition barrierÎ£ : gFunctors := #[stsÎ£ sts; savedPropÎ£ idCF].
 (* Show and register that they match. *)
-Instance inGF_barrierG `{H : inGFs Î£ barrierGF} : barrierG Î£.
-Proof. destruct H as (?&?&?). split; apply _. Qed.
+Instance subG_barrierÎ£ {Î£} : subG barrierÎ£ Î£ â†’ barrierG Î£.
+Proof. intros [? [? _]%subG_inv]%subG_inv. split; apply _. Qed.
 
 (** Now we come to the Iris part of the proof. *)
 Section proof.
diff --git a/heap_lang/lib/counter.v b/heap_lang/lib/counter.v
index c2816d4c2995140a79d82b46d6e6b3ae62052677..d67c547f00d3fda8a7cd957d8d0840f9cedd8bcc 100644
--- a/heap_lang/lib/counter.v
+++ b/heap_lang/lib/counter.v
@@ -14,9 +14,10 @@ Global Opaque newcounter inc get.
 
 (** The CMRA we need. *)
 Class counterG Î£ := CounterG { counter_tokG :> authG Î£ mnatUR }.
-Definition counterGF : gFunctorList := [authGF mnatUR].
-Instance inGF_counterG `{H : inGFs Î£ counterGF} : counterG Î£.
-Proof. destruct H; split; apply _. Qed.
+
+Definition counterÎ£ : gFunctors := #[authÎ£ mnatUR].
+Instance subG_counterÎ£ {Î£} : subG counterÎ£ Î£ â†’ counterG Î£.
+Proof. intros [? _]%subG_inv. split; apply _. Qed.
 
 Section proof.
 Context `{!heapG Î£, !counterG Î£} (N : namespace).
diff --git a/heap_lang/lib/lock.v b/heap_lang/lib/lock.v
index 1723fa38ddc9f8ddc5863896a19993cb599f8138..11be5e4ac98a34b55a31aeac1ac540f4c35a5d8d 100644
--- a/heap_lang/lib/lock.v
+++ b/heap_lang/lib/lock.v
@@ -14,9 +14,10 @@ Global Opaque newlock acquire release.
 (** The CMRA we need. *)
 (* Not bundling heapG, as it may be shared with other users. *)
 Class lockG Î£ := LockG { lock_tokG :> inG Î£ (exclR unitC) }.
-Definition lockGF : gFunctorList := [GFunctor (constRF (exclR unitC))].
-Instance inGF_lockG `{H : inGFs Î£ lockGF} : lockG Î£.
-Proof. destruct H. split. apply: inGF_inG. Qed.
+
+Definition lockÎ£ : gFunctors := #[GFunctor (constRF (exclR unitC))].
+Instance subG_lockÎ£ {Î£} : subG lockÎ£ Î£ â†’ lockG Î£.
+Proof. intros [?%subG_inG _]%subG_inv. split; apply _. Qed.
 
 Section proof.
 Context `{!heapG Î£, !lockG Î£} (N : namespace).
diff --git a/heap_lang/lib/spawn.v b/heap_lang/lib/spawn.v
index dc89e4b0ea7ae51205ce00733763e016df6ac43d..c1d7ea66a9129e208b3b1bf9eb7e2d3ee446784c 100644
--- a/heap_lang/lib/spawn.v
+++ b/heap_lang/lib/spawn.v
@@ -19,11 +19,11 @@ Global Opaque spawn join.
 (** The CMRA we need. *)
 (* Not bundling heapG, as it may be shared with other users. *)
 Class spawnG Î£ := SpawnG { spawn_tokG :> inG Î£ (exclR unitC) }.
-(** The functor we need. *)
-Definition spawnGF : gFunctorList := [GFunctor (constRF (exclR unitC))].
-(* Show and register that they match. *)
-Instance inGF_spawnG `{H : inGFs Î£ spawnGF} : spawnG Î£.
-Proof. destruct H as (?&?). split. apply: inGF_inG. Qed.
+
+(** The functor we need and register that they match. *)
+Definition spawnÎ£ : gFunctors := #[GFunctor (constRF (exclR unitC))].
+Instance subG_spawnÎ£ {Î£} : subG spawnÎ£ Î£ â†’ spawnG Î£.
+Proof. intros [?%subG_inG _]%subG_inv. split; apply _. Qed.
 
 (** Now we come to the Iris part of the proof. *)
 Section proof.
diff --git a/heap_lang/lib/ticket_lock.v b/heap_lang/lib/ticket_lock.v
index 331631cc21477baf32bddfb1d50491c120e17ae4..cf3e4add51221ecaa03c9c8afc8414c48ad5e764 100644
--- a/heap_lang/lib/ticket_lock.v
+++ b/heap_lang/lib/ticket_lock.v
@@ -36,10 +36,10 @@ Class tlockG Î£ := TlockG {
    tlock_exclG  :> inG Î£ (exclR unitC)
 }.
 
-Definition tlockGF : gFunctorList :=
-  [authGF (gset_disjUR nat); GFunctor (constRF (exclR unitC))].
-Instance inGF_tlockG `{H : inGFs Î£ tlockGF} : tlockG Î£.
-Proof. destruct H as (? & ? & ?). split. apply _. apply: inGF_inG. Qed.
+Definition tlockÎ£ : gFunctors :=
+  #[authÎ£ (gset_disjUR nat); GFunctor (constRF (exclR unitC))].
+Instance subG_tlockÎ£ {Î£} : subG tlockÎ£ Î£ â†’ tlockG Î£.
+Proof. intros [? [?%subG_inG _]%subG_inv]%subG_inv. split; apply _. Qed.
 
 Section proof.
 Context `{!heapG Î£, !tlockG Î£} (N : namespace).
diff --git a/heap_lang/lifting.v b/heap_lang/lifting.v
index 6926c97bace4eeca96642454e1961ef153fb16a3..44a1dec2630e7d647a41161a2e31273a366e4606 100644
--- a/heap_lang/lifting.v
+++ b/heap_lang/lifting.v
@@ -10,7 +10,7 @@ Section lifting.
 Context `{irisG heap_lang Î£}.
 Implicit Types P Q : iProp Î£.
 Implicit Types Î¦ : val â†’ iProp Î£.
-Implicit Types ef : option expr.
+Implicit Types efs : list expr.
 
 (** Bind. This bundles some arguments that wp_ectx_bind leaves as indices. *)
 Lemma wp_bind {E e} K Î¦ :
@@ -38,7 +38,7 @@ Lemma wp_load_pst E Ïƒ l v Î¦ :
   Ïƒ !! l = Some v â†’
   â–· ownP Ïƒ â˜… â–· (ownP Ïƒ ={E}=â˜… Î¦ v) âŠ¢ WP Load (Lit (LitLoc l)) @ E {{ Î¦ }}.
 Proof.
-  intros. rewrite -(wp_lift_atomic_det_head_step Ïƒ v Ïƒ None) ?right_id //;
+  intros. rewrite -(wp_lift_atomic_det_head_step Ïƒ v Ïƒ []) ?right_id //;
     last (by intros; inv_head_step; eauto using to_of_val). solve_atomic.
 Qed.
 
@@ -48,7 +48,7 @@ Lemma wp_store_pst E Ïƒ l v v' Î¦ :
   âŠ¢ WP Store (Lit (LitLoc l)) (of_val v) @ E {{ Î¦ }}.
 Proof.
   intros ?.
-  rewrite-(wp_lift_atomic_det_head_step Ïƒ (LitV LitUnit) (<[l:=v]>Ïƒ) None)
+  rewrite-(wp_lift_atomic_det_head_step Ïƒ (LitV LitUnit) (<[l:=v]>Ïƒ) [])
     ?right_id //; last (by intros; inv_head_step; eauto). solve_atomic.
 Qed.
 
@@ -58,7 +58,7 @@ Lemma wp_cas_fail_pst E Ïƒ l v1 v2 v' Î¦ :
   âŠ¢ WP CAS (Lit (LitLoc l)) (of_val v1) (of_val v2) @ E {{ Î¦ }}.
 Proof.
   intros ??.
-  rewrite -(wp_lift_atomic_det_head_step Ïƒ (LitV $ LitBool false) Ïƒ None)
+  rewrite -(wp_lift_atomic_det_head_step Ïƒ (LitV $ LitBool false) Ïƒ [])
     ?right_id //; last (by intros; inv_head_step; eauto). solve_atomic.
 Qed.
 
@@ -68,7 +68,7 @@ Lemma wp_cas_suc_pst E Ïƒ l v1 v2 Î¦ :
   âŠ¢ WP CAS (Lit (LitLoc l)) (of_val v1) (of_val v2) @ E {{ Î¦ }}.
 Proof.
   intros ?. rewrite -(wp_lift_atomic_det_head_step Ïƒ (LitV $ LitBool true)
-    (<[l:=v2]>Ïƒ) None) ?right_id //; last (by intros; inv_head_step; eauto).
+    (<[l:=v2]>Ïƒ) []) ?right_id //; last (by intros; inv_head_step; eauto).
   solve_atomic.
 Qed.
 
@@ -76,9 +76,9 @@ Qed.
 Lemma wp_fork E e Î¦ :
   â–· (|={E}=> Î¦ (LitV LitUnit)) â˜… â–· WP e {{ _, True }} âŠ¢ WP Fork e @ E {{ Î¦ }}.
 Proof.
-  rewrite -(wp_lift_pure_det_head_step (Fork e) (Lit LitUnit) (Some e)) //=;
+  rewrite -(wp_lift_pure_det_head_step (Fork e) (Lit LitUnit) [e]) //=;
     last by intros; inv_head_step; eauto.
-  rewrite later_sep -(wp_value_pvs _ _ (Lit _)) //.
+  by rewrite later_sep -(wp_value_pvs _ _ (Lit _)) // right_id.
 Qed.
 
 Lemma wp_rec E f x erec e1 e2 Î¦ :
@@ -88,7 +88,7 @@ Lemma wp_rec E f x erec e1 e2 Î¦ :
   â–· WP subst' x e2 (subst' f e1 erec) @ E {{ Î¦ }} âŠ¢ WP App e1 e2 @ E {{ Î¦ }}.
 Proof.
   intros -> [v2 ?] ?. rewrite -(wp_lift_pure_det_head_step (App _ _)
-    (subst' x e2 (subst' f (Rec f x erec) erec)) None) //= ?right_id;
+    (subst' x e2 (subst' f (Rec f x erec) erec)) []) //= ?right_id;
     intros; inv_head_step; eauto.
 Qed.
 
@@ -96,7 +96,7 @@ Lemma wp_un_op E op l l' Î¦ :
   un_op_eval op l = Some l' â†’
   â–· (|={E}=> Î¦ (LitV l')) âŠ¢ WP UnOp op (Lit l) @ E {{ Î¦ }}.
 Proof.
-  intros. rewrite -(wp_lift_pure_det_head_step (UnOp op _) (Lit l') None)
+  intros. rewrite -(wp_lift_pure_det_head_step (UnOp op _) (Lit l') [])
     ?right_id -?wp_value_pvs //; intros; inv_head_step; eauto.
 Qed.
 
@@ -104,21 +104,21 @@ Lemma wp_bin_op E op l1 l2 l' Î¦ :
   bin_op_eval op l1 l2 = Some l' â†’
   â–· (|={E}=> Î¦ (LitV l')) âŠ¢ WP BinOp op (Lit l1) (Lit l2) @ E {{ Î¦ }}.
 Proof.
-  intros Heval. rewrite -(wp_lift_pure_det_head_step (BinOp op _ _) (Lit l') None)
+  intros Heval. rewrite -(wp_lift_pure_det_head_step (BinOp op _ _) (Lit l') [])
     ?right_id -?wp_value_pvs //; intros; inv_head_step; eauto.
 Qed.
 
 Lemma wp_if_true E e1 e2 Î¦ :
   â–· WP e1 @ E {{ Î¦ }} âŠ¢ WP If (Lit (LitBool true)) e1 e2 @ E {{ Î¦ }}.
 Proof.
-  rewrite -(wp_lift_pure_det_head_step (If _ _ _) e1 None)
+  rewrite -(wp_lift_pure_det_head_step (If _ _ _) e1 [])
     ?right_id //; intros; inv_head_step; eauto.
 Qed.
 
 Lemma wp_if_false E e1 e2 Î¦ :
   â–· WP e2 @ E {{ Î¦ }} âŠ¢ WP If (Lit (LitBool false)) e1 e2 @ E {{ Î¦ }}.
 Proof.
-  rewrite -(wp_lift_pure_det_head_step (If _ _ _) e2 None)
+  rewrite -(wp_lift_pure_det_head_step (If _ _ _) e2 [])
     ?right_id //; intros; inv_head_step; eauto.
 Qed.
 
@@ -126,7 +126,7 @@ Lemma wp_fst E e1 v1 e2 Î¦ :
   to_val e1 = Some v1 â†’ is_Some (to_val e2) â†’
   â–· (|={E}=> Î¦ v1) âŠ¢ WP Fst (Pair e1 e2) @ E {{ Î¦ }}.
 Proof.
-  intros ? [v2 ?]. rewrite -(wp_lift_pure_det_head_step (Fst _) e1 None)
+  intros ? [v2 ?]. rewrite -(wp_lift_pure_det_head_step (Fst _) e1 [])
     ?right_id -?wp_value_pvs //; intros; inv_head_step; eauto.
 Qed.
 
@@ -134,7 +134,7 @@ Lemma wp_snd E e1 e2 v2 Î¦ :
   is_Some (to_val e1) â†’ to_val e2 = Some v2 â†’
   â–· (|={E}=> Î¦ v2) âŠ¢ WP Snd (Pair e1 e2) @ E {{ Î¦ }}.
 Proof.
-  intros [v1 ?] ?. rewrite -(wp_lift_pure_det_head_step (Snd _) e2 None)
+  intros [v1 ?] ?. rewrite -(wp_lift_pure_det_head_step (Snd _) e2 [])
     ?right_id -?wp_value_pvs //; intros; inv_head_step; eauto.
 Qed.
 
@@ -143,7 +143,7 @@ Lemma wp_case_inl E e0 e1 e2 Î¦ :
   â–· WP App e1 e0 @ E {{ Î¦ }} âŠ¢ WP Case (InjL e0) e1 e2 @ E {{ Î¦ }}.
 Proof.
   intros [v0 ?]. rewrite -(wp_lift_pure_det_head_step (Case _ _ _)
-    (App e1 e0) None) ?right_id //; intros; inv_head_step; eauto.
+    (App e1 e0) []) ?right_id //; intros; inv_head_step; eauto.
 Qed.
 
 Lemma wp_case_inr E e0 e1 e2 Î¦ :
@@ -151,6 +151,6 @@ Lemma wp_case_inr E e0 e1 e2 Î¦ :
   â–· WP App e2 e0 @ E {{ Î¦ }} âŠ¢ WP Case (InjR e0) e1 e2 @ E {{ Î¦ }}.
 Proof.
   intros [v0 ?]. rewrite -(wp_lift_pure_det_head_step (Case _ _ _)
-    (App e2 e0) None) ?right_id //; intros; inv_head_step; eauto.
+    (App e2 e0) []) ?right_id //; intros; inv_head_step; eauto.
 Qed.
 End lifting.
diff --git a/heap_lang/tactics.v b/heap_lang/tactics.v
index dbe50971a7de1be0598f64ece4dc4490c5799e76..7118b4af2fb2cda83003b4384c9a18dff2c5ebe9 100644
--- a/heap_lang/tactics.v
+++ b/heap_lang/tactics.v
@@ -312,7 +312,7 @@ Tactic Notation "do_head_step" tactic3(tac) :=
   try match goal with |- head_reducible _ _ => eexists _, _, _ end;
   simpl;
   match goal with
-  | |- head_step ?e1 ?Ïƒ1 ?e2 ?Ïƒ2 ?ef =>
+  | |- head_step ?e1 ?Ïƒ1 ?e2 ?Ïƒ2 ?efs =>
      first [apply alloc_fresh|econstructor];
        (* solve [to_val] side-conditions *)
        first [rewrite ?to_of_val; reflexivity|simpl_subst; tac; fast_done]
diff --git a/heap_lang/wp_tactics.v b/heap_lang/wp_tactics.v
index ff18e12dac2eaf43a8554f61988c610ed84623e8..08a4c4c4391ab4bc137f14e7801469f5215675fb 100644
--- a/heap_lang/wp_tactics.v
+++ b/heap_lang/wp_tactics.v
@@ -1,4 +1,3 @@
-From iris.algebra Require Export upred_tactics.
 From iris.heap_lang Require Export tactics derived.
 Import uPred.
 
diff --git a/prelude/collections.v b/prelude/collections.v
index 850226e1571c4a65910ed62910d035490568c18c..ef7383d529cf25477858fe854a4fb7bbf46bfc2f 100644
--- a/prelude/collections.v
+++ b/prelude/collections.v
@@ -390,7 +390,7 @@ Section simple_collection.
     split.
     - induction Xs; simpl; intros HXs; [by apply elem_of_empty in HXs|].
       setoid_rewrite elem_of_cons. apply elem_of_union in HXs. naive_solver.
-    - intros [X []]. induction 1; simpl; [by apply elem_of_union_l |].
+    - intros [X [Hx]]. induction Hx; simpl; [by apply elem_of_union_l |].
       intros. apply elem_of_union_r; auto.
   Qed.
 
diff --git a/prelude/list.v b/prelude/list.v
index 59b26331813bf82dc7cd243e88f8721e7b9fd82e..9a384897ea4fdf4aa708d14ac60121cd48fbd247 100644
--- a/prelude/list.v
+++ b/prelude/list.v
@@ -926,7 +926,7 @@ Proof. by destruct n. Qed.
 Lemma drop_length l n : length (drop n l) = length l - n.
 Proof. revert n. by induction l; intros [|i]; f_equal/=. Qed.
 Lemma drop_ge l n : length l â‰¤ n â†’ drop n l = [].
-Proof. revert n. induction l; intros [|??]; simpl in *; auto with lia. Qed.
+Proof. revert n. induction l; intros [|?]; simpl in *; auto with lia. Qed.
 Lemma drop_all l : drop (length l) l = [].
 Proof. by apply drop_ge. Qed.
 Lemma drop_drop l n1 n2 : drop n1 (drop n2 l) = drop (n2 + n1) l.
@@ -2828,7 +2828,7 @@ Section fmap.
     (âˆ€ x, f x = y) â†’ f <$> l = replicate (length l) y.
   Proof. intros; induction l; f_equal/=; auto. Qed.
   Lemma list_lookup_fmap l i : (f <$> l) !! i = f <$> (l !! i).
-  Proof. revert i. induction l; by intros [|]. Qed.
+  Proof. revert i. induction l; intros [|n]; by try revert n. Qed.
   Lemma list_lookup_fmap_inv l i x :
     (f <$> l) !! i = Some x â†’ âˆƒ y, x = f y âˆ§ l !! i = Some y.
   Proof.
diff --git a/prelude/vector.v b/prelude/vector.v
index 26f78e9451e419fb4f04d05a9365e2f3addbbe12..9253a797f7b162ac3f5681259f1284d682564851 100644
--- a/prelude/vector.v
+++ b/prelude/vector.v
@@ -69,12 +69,13 @@ Ltac inv_fin i :=
     revert dependent i; match goal with |- âˆ€ i, @?P i => apply (fin_S_inv P) end
   end.
 
-Instance: Inj (=) (=) (@FS n).
+Instance FS_inj: Inj (=) (=) (@FS n).
 Proof. intros n i j. apply Fin.FS_inj. Qed.
-Instance: Inj (=) (=) (@fin_to_nat n).
+Instance fin_to_nat_inj : Inj (=) (=) (@fin_to_nat n).
 Proof.
   intros n i. induction i; intros j; inv_fin j; intros; f_equal/=; auto with lia.
 Qed.
+
 Lemma fin_to_nat_lt {n} (i : fin n) : fin_to_nat i < n.
 Proof. induction i; simpl; lia. Qed.
 Lemma fin_to_of_nat n m (H : n < m) : fin_to_nat (Fin.of_nat_lt H) = n.
@@ -82,6 +83,31 @@ Proof.
   revert m H. induction n; intros [|?]; simpl; auto; intros; exfalso; lia.
 Qed.
 
+Fixpoint fin_plus_inv {n1 n2} : âˆ€ (P : fin (n1 + n2) â†’ Type)
+    (H1 : âˆ€ i1 : fin n1, P (Fin.L n2 i1))
+    (H2 : âˆ€ i2, P (Fin.R n1 i2)) (i : fin (n1 + n2)), P i :=
+  match n1 with
+  | 0 => Î» P H1 H2 i, H2 i
+  | S n => Î» P H1 H2, fin_S_inv P (H1 0%fin) (fin_plus_inv _ (Î» i, H1 (FS i)) H2)
+  end.
+
+Lemma fin_plus_inv_L {n1 n2} (P : fin (n1 + n2) â†’ Type)
+    (H1: âˆ€ i1 : fin n1, P (Fin.L _ i1)) (H2: âˆ€ i2, P (Fin.R _ i2)) (i: fin n1) :
+  fin_plus_inv P H1 H2 (Fin.L n2 i) = H1 i.
+Proof.
+  revert P H1 H2 i.
+  induction n1 as [|n1 IH]; intros P H1 H2 i; inv_fin i; simpl; auto.
+  intros i. apply (IH (Î» i, P (FS i))).
+Qed.
+
+Lemma fin_plus_inv_R {n1 n2} (P : fin (n1 + n2) â†’ Type)
+    (H1: âˆ€ i1 : fin n1, P (Fin.L _ i1)) (H2: âˆ€ i2, P (Fin.R _ i2)) (i: fin n2) :
+  fin_plus_inv P H1 H2 (Fin.R n1 i) = H2 i.
+Proof.
+  revert P H1 H2 i; induction n1 as [|n1 IH]; intros P H1 H2 i; simpl; auto.
+  apply (IH (Î» i, P (FS i))).
+Qed.
+
 (** * Vectors *)
 (** The type [vec n] represents lists of consisting of exactly [n] elements.
 Whereas the standard library declares exactly the same notations for vectors as
diff --git a/program_logic/adequacy.v b/program_logic/adequacy.v
index f8927d9da446175989f5900fb741667fc6f45441..b7d729a87dbf07ab59c644ba47c2426c5abe8bbd 100644
--- a/program_logic/adequacy.v
+++ b/program_logic/adequacy.v
@@ -20,11 +20,11 @@ Proof.
   intros Had ?.
   destruct (decide (Forall (Î» e, is_Some (to_val e)) t2)) as [|Ht2]; [by left|].
   apply (not_Forall_Exists _), Exists_exists in Ht2; destruct Ht2 as (e2&?&He2).
-  destruct (adequate_safe e1 Ïƒ1 Ï† Had t2 Ïƒ2 e2) as [?|(e3&Ïƒ3&ef&?)];
+  destruct (adequate_safe e1 Ïƒ1 Ï† Had t2 Ïƒ2 e2) as [?|(e3&Ïƒ3&efs&?)];
     rewrite ?eq_None_not_Some; auto.
   { exfalso. eauto. }
   destruct (elem_of_list_split t2 e2) as (t2'&t2''&->); auto.
-  right; exists (t2' ++ e3 :: t2'' ++ option_list ef), Ïƒ3; econstructor; eauto.
+  right; exists (t2' ++ e3 :: t2'' ++ efs), Ïƒ3; econstructor; eauto.
 Qed.
 
 Section adequacy.
@@ -42,19 +42,17 @@ Lemma wptp_cons e t : wptp (e :: t) âŠ£âŠ¢ WP e {{ _, True }} â˜… wptp t.
 Proof. done. Qed.
 Lemma wptp_app t1 t2 : wptp (t1 ++ t2) âŠ£âŠ¢ wptp t1 â˜… wptp t2.
 Proof. by rewrite /wptp fmap_app big_sep_app. Qed.
-Lemma wptp_fork ef : wptp (option_list ef) âŠ£âŠ¢ wp_fork ef.
-Proof. destruct ef; by rewrite /wptp /= ?right_id. Qed.
 
-Lemma wp_step e1 Ïƒ1 e2 Ïƒ2 ef Î¦ :
-  prim_step e1 Ïƒ1 e2 Ïƒ2 ef â†’
-  world Ïƒ1 â˜… WP e1 {{ Î¦ }} =r=> â–· |=r=> â—‡ (world Ïƒ2 â˜… WP e2 {{ Î¦ }} â˜… wp_fork ef).
+Lemma wp_step e1 Ïƒ1 e2 Ïƒ2 efs Î¦ :
+  prim_step e1 Ïƒ1 e2 Ïƒ2 efs â†’
+  world Ïƒ1 â˜… WP e1 {{ Î¦ }} =r=> â–· |=r=> â—‡ (world Ïƒ2 â˜… WP e2 {{ Î¦ }} â˜… wp_fork efs).
 Proof.
   rewrite {1}wp_unfold /wp_pre. iIntros (Hstep) "[(Hw & HE & HÏƒ) [H|[_ H]]]".
   { iDestruct "H" as (v) "[% _]". apply val_stuck in Hstep; simplify_eq. }
   rewrite pvs_eq /pvs_def.
   iVs ("H" $! Ïƒ1 with "HÏƒ [Hw HE]") as ">(Hw & HE & _ & H)"; first by iFrame.
   iVsIntro; iNext.
-  iVs ("H" $! e2 Ïƒ2 ef with "[%] [Hw HE]")
+  iVs ("H" $! e2 Ïƒ2 efs with "[%] [Hw HE]")
     as ">($ & $ & $ & $)"; try iFrame; eauto.
 Qed.
 
@@ -64,11 +62,11 @@ Lemma wptp_step e1 t1 t2 Ïƒ1 Ïƒ2 Î¦ :
   =r=> âˆƒ e2 t2', t2 = e2 :: t2' â˜… â–· |=r=> â—‡ (world Ïƒ2 â˜… WP e2 {{ Î¦ }} â˜… wptp t2').
 Proof.
   iIntros (Hstep) "(HW & He & Ht)".
-  destruct Hstep as [e1' Ïƒ1' e2' Ïƒ2' ef [|? t1'] t2' ?? Hstep]; simplify_eq/=.
-  - iExists e2', (t2' ++ option_list ef); iSplitR; first eauto.
-    rewrite wptp_app wptp_fork. iFrame "Ht". iApply wp_step; try iFrame; eauto.
-  - iExists e, (t1' ++ e2' :: t2' ++ option_list ef); iSplitR; first eauto.
-    rewrite !wptp_app !wptp_cons wptp_app wptp_fork.
+  destruct Hstep as [e1' Ïƒ1' e2' Ïƒ2' efs [|? t1'] t2' ?? Hstep]; simplify_eq/=.
+  - iExists e2', (t2' ++ efs); iSplitR; first eauto.
+    rewrite wptp_app. iFrame "Ht". iApply wp_step; try iFrame; eauto.
+  - iExists e, (t1' ++ e2' :: t2' ++ efs); iSplitR; first eauto.
+    rewrite !wptp_app !wptp_cons wptp_app.
     iDestruct "Ht" as "($ & He' & $)"; iFrame "He".
     iApply wp_step; try iFrame; eauto.
 Qed.
@@ -94,7 +92,8 @@ Lemma wptp_result n e1 t1 v2 t2 Ïƒ1 Ïƒ2 Ï† :
   world Ïƒ1 â˜… WP e1 {{ v, â–  Ï† v }} â˜… wptp t1 âŠ¢
   Nat.iter (S (S n)) (Î» P, |=r=> â–· P) (â–  Ï† v2).
 Proof.
-  intros. rewrite wptp_steps // (Nat_iter_S_r (S n)); []. apply: rvs_iter_mono.
+  intros. rewrite wptp_steps //.
+  rewrite (Nat_iter_S_r (S n)). apply rvs_iter_mono.
   iDestruct 1 as (e2 t2') "(% & (Hw & HE & _) & H & _)"; simplify_eq.
   iDestruct (wp_value_inv with "H") as "H". rewrite pvs_eq /pvs_def.
   iVs ("H" with "[Hw HE]") as ">(_ & _ & $)"; iFrame; auto.
@@ -114,7 +113,7 @@ Lemma wptp_safe n e1 e2 t1 t2 Ïƒ1 Ïƒ2 Î¦ :
   world Ïƒ1 â˜… WP e1 {{ Î¦ }} â˜… wptp t1 âŠ¢
   Nat.iter (S (S n)) (Î» P, |=r=> â–· P) (â–  (is_Some (to_val e2) âˆ¨ reducible e2 Ïƒ2)).
 Proof.
-  intros ? He2. rewrite wptp_steps // (Nat_iter_S_r (S n)); apply: rvs_iter_mono.
+  intros ? He2. rewrite wptp_steps //; rewrite (Nat_iter_S_r (S n)). apply rvs_iter_mono.
   iDestruct 1 as (e2' t2') "(% & Hw & H & Htp)"; simplify_eq.
   apply elem_of_cons in He2 as [<-|?]; first (iApply wp_safe; by iFrame "Hw H").
   iApply wp_safe. iFrame "Hw".
diff --git a/program_logic/auth.v b/program_logic/auth.v
index 996e74578b4ed46460c14dac9fc0869ddfa7e4ec..4dcdf9c7e38fd56214de988ad0a03a43790b64d0 100644
--- a/program_logic/auth.v
+++ b/program_logic/auth.v
@@ -7,13 +7,13 @@ Import uPred.
 (* The CMRA we need. *)
 Class authG Î£ (A : ucmraT) := AuthG {
   auth_inG :> inG Î£ (authR A);
-  auth_timeless :> CMRADiscrete A;
+  auth_discrete :> CMRADiscrete A;
 }.
-(* The Functor we need. *)
-Definition authGF (A : ucmraT) : gFunctor := GFunctor (constRF (authR A)).
-(* Show and register that they match. *)
-Instance authGF_inGF `{inGF Î£ (authGF A), CMRADiscrete A} : authG Î£ A.
-Proof. split; try apply _. apply: inGF_inG. Qed.
+
+(* The global functor we need and register that they match. *)
+Definition authÎ£ (A : ucmraT) : gFunctors := #[ GFunctor (constRF (authR A)) ].
+Instance subG_authÎ£ Î£ A : subG (authÎ£ A) Î£ â†’ CMRADiscrete A â†’ authG Î£ A.
+Proof. intros ?%subG_inG ?. by split. Qed.
 
 Section definitions.
   Context `{irisG Î› Î£, authG Î£ A} (Î³ : gname).
diff --git a/program_logic/counter_examples.v b/program_logic/counter_examples.v
index 3b1751aa91a61a0cdf01eedb0cf9f6b3f9d9f141..f44df277bad5e83078284c5d2ce47d7b72e48c55 100644
--- a/program_logic/counter_examples.v
+++ b/program_logic/counter_examples.v
@@ -2,7 +2,7 @@ From iris.algebra Require Import upred.
 From iris.proofmode Require Import tactics.
 
 (** This proves that we need the â–· in a "Saved Proposition" construction with
-name-dependend allocation. *)
+name-dependent allocation. *)
 Module savedprop. Section savedprop.
   Context (M : ucmraT).
   Notation iProp := (uPred M).
@@ -87,6 +87,12 @@ Module inv. Section inv.
   (* We have tokens for a little "two-state STS": [start] -> [finish].
      state. [start] also asserts the exact state; it is only ever owned by the
      invariant.  [finished] is duplicable. *)
+  (* Posssible implementations of these axioms:
+     * Using the STS monoid of a two-state STS, where [start] is the
+       authoritative saying the state is exactly [start], and [finish]
+       is the "we are at least in state [finish]" typically owned by threads.
+     * Ex () +_âŠ¥ ()
+  *)
   Context (gname : Type).
   Context (start finished : gname â†’ iProp).
 
@@ -133,7 +139,7 @@ Module inv. Section inv.
     apply pvs_mono. by rewrite -HP -(uPred.exist_intro a).
   Qed.
 
-  (** Now to the actual counterexample. We start with a weird for of saved propositions. *)
+  (** Now to the actual counterexample. We start with a weird form of saved propositions. *)
   Definition saved (Î³ : gname) (P : iProp) : iProp :=
     âˆƒ i, inv i (start Î³ âˆ¨ (finished Î³ â˜… â–¡ P)).
   Global Instance saved_persistent Î³ P : PersistentP (saved Î³ P) := _.
@@ -150,12 +156,11 @@ Module inv. Section inv.
   Proof.
     iIntros "(#HsP & #HsQ & #HP)". iDestruct "HsP" as (i) "HiP".
     iApply (inv_open' i). iSplit; first done.
-    (* Can I state a view-shift and immediately run it? *)
-    iIntros "HaP". iAssert (pvs M0 (finished Î³)) with "[HaP]" as "Hf".
+    iIntros "HaP". iAssert (pvs M0 (finished Î³)) with "[HaP]" as "==> Hf".
     { iDestruct "HaP" as "[Hs | [Hf _]]".
       - by iApply start_finish.
       - by iApply pvs_intro. }
-    iVs "Hf" as "Hf". iDestruct (finished_dup with "Hf") as "[Hf Hf']".
+    iDestruct (finished_dup with "Hf") as "[Hf Hf']".
     iApply pvs_intro. iSplitL "Hf'"; first by eauto.
     (* Step 2: Open the Q-invariant. *)
     iClear "HiP". clear i. iDestruct "HsQ" as (i) "HiQ".
diff --git a/program_logic/ectx_language.v b/program_logic/ectx_language.v
index d7b58df92eac2bd6fbc9ce115420f19454bfd68b..28657bbaeef74d8fde127f87f0c3df8fe2bae3fa 100644
--- a/program_logic/ectx_language.v
+++ b/program_logic/ectx_language.v
@@ -11,11 +11,11 @@ Class EctxLanguage (expr val ectx state : Type) := {
   empty_ectx : ectx;
   comp_ectx : ectx â†’ ectx â†’ ectx;
   fill : ectx â†’ expr â†’ expr;
-  head_step : expr â†’ state â†’ expr â†’ state â†’ option expr â†’ Prop;
+  head_step : expr â†’ state â†’ expr â†’ state â†’ list expr â†’ Prop;
 
   to_of_val v : to_val (of_val v) = Some v;
   of_to_val e v : to_val e = Some v â†’ of_val v = e;
-  val_stuck e1 Ïƒ1 e2 Ïƒ2 ef : head_step e1 Ïƒ1 e2 Ïƒ2 ef â†’ to_val e1 = None;
+  val_stuck e1 Ïƒ1 e2 Ïƒ2 efs : head_step e1 Ïƒ1 e2 Ïƒ2 efs â†’ to_val e1 = None;
 
   fill_empty e : fill empty_ectx e = e;
   fill_comp K1 K2 e : fill K1 (fill K2 e) = fill (comp_ectx K1 K2) e;
@@ -28,10 +28,10 @@ Class EctxLanguage (expr val ectx state : Type) := {
   ectx_positive K1 K2 :
     comp_ectx K1 K2 = empty_ectx â†’ K1 = empty_ectx âˆ§ K2 = empty_ectx;
 
-  step_by_val K K' e1 e1' Ïƒ1 e2 Ïƒ2 ef :
+  step_by_val K K' e1 e1' Ïƒ1 e2 Ïƒ2 efs :
     fill K e1 = fill K' e1' â†’
     to_val e1 = None â†’
-    head_step e1' Ïƒ1 e2 Ïƒ2 ef â†’
+    head_step e1' Ïƒ1 e2 Ïƒ2 efs â†’
     exists K'', K' = comp_ectx K K'';
 }.
 
@@ -57,16 +57,16 @@ Section ectx_language.
   Implicit Types (e : expr) (K : ectx).
 
   Definition head_reducible (e : expr) (Ïƒ : state) :=
-    âˆƒ e' Ïƒ' ef, head_step e Ïƒ e' Ïƒ' ef.
+    âˆƒ e' Ïƒ' efs, head_step e Ïƒ e' Ïƒ' efs.
 
   Inductive prim_step (e1 : expr) (Ïƒ1 : state)
-      (e2 : expr) (Ïƒ2 : state) (ef : option expr) : Prop :=
+      (e2 : expr) (Ïƒ2 : state) (efs : list expr) : Prop :=
     Ectx_step K e1' e2' :
       e1 = fill K e1' â†’ e2 = fill K e2' â†’
-      head_step e1' Ïƒ1 e2' Ïƒ2 ef â†’ prim_step e1 Ïƒ1 e2 Ïƒ2 ef.
+      head_step e1' Ïƒ1 e2' Ïƒ2 efs â†’ prim_step e1 Ïƒ1 e2 Ïƒ2 efs.
 
-  Lemma val_prim_stuck e1 Ïƒ1 e2 Ïƒ2 ef :
-    prim_step e1 Ïƒ1 e2 Ïƒ2 ef â†’ to_val e1 = None.
+  Lemma val_prim_stuck e1 Ïƒ1 e2 Ïƒ2 efs :
+    prim_step e1 Ïƒ1 e2 Ïƒ2 efs â†’ to_val e1 = None.
   Proof. intros [??? -> -> ?]; eauto using fill_not_val, val_stuck. Qed.
 
   Canonical Structure ectx_lang : language := {|
@@ -78,29 +78,29 @@ Section ectx_language.
   |}.
 
   (* Some lemmas about this language *)
-  Lemma head_prim_step e1 Ïƒ1 e2 Ïƒ2 ef :
-    head_step e1 Ïƒ1 e2 Ïƒ2 ef â†’ prim_step e1 Ïƒ1 e2 Ïƒ2 ef.
+  Lemma head_prim_step e1 Ïƒ1 e2 Ïƒ2 efs :
+    head_step e1 Ïƒ1 e2 Ïƒ2 efs â†’ prim_step e1 Ïƒ1 e2 Ïƒ2 efs.
   Proof. apply Ectx_step with empty_ectx; by rewrite ?fill_empty. Qed.
 
   Lemma head_prim_reducible e Ïƒ : head_reducible e Ïƒ â†’ reducible e Ïƒ.
-  Proof. intros (e'&Ïƒ'&ef&?). eexists e', Ïƒ', ef. by apply head_prim_step. Qed.
+  Proof. intros (e'&Ïƒ'&efs&?). eexists e', Ïƒ', efs. by apply head_prim_step. Qed.
 
   Lemma ectx_language_atomic e :
-    (âˆ€ Ïƒ e' Ïƒ' ef, head_step e Ïƒ e' Ïƒ' ef â†’ is_Some (to_val e')) â†’
+    (âˆ€ Ïƒ e' Ïƒ' efs, head_step e Ïƒ e' Ïƒ' efs â†’ is_Some (to_val e')) â†’
     (âˆ€ K e', e = fill K e' â†’ to_val e' = None â†’ K = empty_ectx) â†’
     atomic e.
   Proof.
-    intros Hatomic_step Hatomic_fill Ïƒ e' Ïƒ' ef [K e1' e2' -> -> Hstep].
+    intros Hatomic_step Hatomic_fill Ïƒ e' Ïƒ' efs [K e1' e2' -> -> Hstep].
     assert (K = empty_ectx) as -> by eauto 10 using val_stuck.
     rewrite fill_empty. eapply Hatomic_step. by rewrite fill_empty.
   Qed.
 
-  Lemma head_reducible_prim_step e1 Ïƒ1 e2 Ïƒ2 ef :
-    head_reducible e1 Ïƒ1 â†’ prim_step e1 Ïƒ1 e2 Ïƒ2 ef â†’
-    head_step e1 Ïƒ1 e2 Ïƒ2 ef.
+  Lemma head_reducible_prim_step e1 Ïƒ1 e2 Ïƒ2 efs :
+    head_reducible e1 Ïƒ1 â†’ prim_step e1 Ïƒ1 e2 Ïƒ2 efs â†’
+    head_step e1 Ïƒ1 e2 Ïƒ2 efs.
   Proof.
-    intros (e2''&Ïƒ2''&ef''&?) [K e1' e2' -> -> Hstep].
-    destruct (step_by_val K empty_ectx e1' (fill K e1') Ïƒ1 e2'' Ïƒ2'' ef'')
+    intros (e2''&Ïƒ2''&efs''&?) [K e1' e2' -> -> Hstep].
+    destruct (step_by_val K empty_ectx e1' (fill K e1') Ïƒ1 e2'' Ïƒ2'' efs'')
       as [K' [-> _]%symmetry%ectx_positive];
       eauto using fill_empty, fill_not_val, val_stuck.
     by rewrite !fill_empty.
@@ -114,7 +114,7 @@ Section ectx_language.
     - intros ????? [K' e1' e2' Heq1 Heq2 Hstep].
       by exists (comp_ectx K K') e1' e2'; rewrite ?Heq1 ?Heq2 ?fill_comp.
     - intros e1 Ïƒ1 e2 Ïƒ2 ? Hnval [K'' e1'' e2'' Heq1 -> Hstep].
-      destruct (step_by_val K K'' e1 e1'' Ïƒ1 e2'' Ïƒ2 ef) as [K' ->]; eauto.
+      destruct (step_by_val K K'' e1 e1'' Ïƒ1 e2'' Ïƒ2 efs) as [K' ->]; eauto.
       rewrite -fill_comp in Heq1; apply (inj (fill _)) in Heq1.
       exists (fill K' e2''); rewrite -fill_comp; split; auto.
       econstructor; eauto.
diff --git a/program_logic/ectx_lifting.v b/program_logic/ectx_lifting.v
index d298f34b219caf202f24e7bebbbc444f9b5a9df1..cff6e639645aadd5e153db00174185e585733062 100644
--- a/program_logic/ectx_lifting.v
+++ b/program_logic/ectx_lifting.v
@@ -19,21 +19,21 @@ Proof. apply: weakestpre.wp_bind. Qed.
 Lemma wp_lift_head_step E Î¦ e1 :
   to_val e1 = None â†’
   (|={E,âˆ…}=> âˆƒ Ïƒ1, â–  head_reducible e1 Ïƒ1 â˜… â–· ownP Ïƒ1 â˜…
-     â–· âˆ€ e2 Ïƒ2 ef, â–  head_step e1 Ïƒ1 e2 Ïƒ2 ef â˜… ownP Ïƒ2
-          ={âˆ…,E}=â˜… WP e2 @ E {{ Î¦ }} â˜… wp_fork ef)
+    â–· âˆ€ e2 Ïƒ2 efs, â–  head_step e1 Ïƒ1 e2 Ïƒ2 efs â˜… ownP Ïƒ2
+          ={âˆ…,E}=â˜… WP e2 @ E {{ Î¦ }} â˜… wp_fork efs)
   âŠ¢ WP e1 @ E {{ Î¦ }}.
 Proof.
   iIntros (?) "H". iApply (wp_lift_step E); try done.
   iVs "H" as (Ïƒ1) "(%&HÏƒ1&Hwp)". iVsIntro. iExists Ïƒ1.
-  iSplit; first by eauto. iFrame. iNext. iIntros (e2 Ïƒ2 ef) "[% ?]".
+  iSplit; first by eauto. iFrame. iNext. iIntros (e2 Ïƒ2 efs) "[% ?]".
   iApply "Hwp". by eauto.
 Qed.
 
 Lemma wp_lift_pure_head_step E Î¦ e1 :
   to_val e1 = None â†’
   (âˆ€ Ïƒ1, head_reducible e1 Ïƒ1) â†’
-  (âˆ€ Ïƒ1 e2 Ïƒ2 ef, head_step e1 Ïƒ1 e2 Ïƒ2 ef â†’ Ïƒ1 = Ïƒ2) â†’
-  (â–· âˆ€ e2 ef Ïƒ, â–  head_step e1 Ïƒ e2 Ïƒ ef â†’ WP e2 @ E {{ Î¦ }} â˜… wp_fork ef)
+  (âˆ€ Ïƒ1 e2 Ïƒ2 efs, head_step e1 Ïƒ1 e2 Ïƒ2 efs â†’ Ïƒ1 = Ïƒ2) â†’
+  (â–· âˆ€ e2 efs Ïƒ, â–  head_step e1 Ïƒ e2 Ïƒ efs â†’ WP e2 @ E {{ Î¦ }} â˜… wp_fork efs)
   âŠ¢ WP e1 @ E {{ Î¦ }}.
 Proof.
   iIntros (???) "H". iApply wp_lift_pure_step; eauto. iNext.
@@ -43,26 +43,26 @@ Qed.
 Lemma wp_lift_atomic_head_step {E Î¦} e1 Ïƒ1 :
   atomic e1 â†’
   head_reducible e1 Ïƒ1 â†’
-  â–· ownP Ïƒ1 â˜… â–· (âˆ€ v2 Ïƒ2 ef,
-  â–  head_step e1 Ïƒ1 (of_val v2) Ïƒ2 ef âˆ§ ownP Ïƒ2 -â˜… (|={E}=> Î¦ v2) â˜… wp_fork ef)
+  â–· ownP Ïƒ1 â˜… â–· (âˆ€ v2 Ïƒ2 efs,
+  â–  head_step e1 Ïƒ1 (of_val v2) Ïƒ2 efs âˆ§ ownP Ïƒ2 -â˜… (|={E}=> Î¦ v2) â˜… wp_fork efs)
   âŠ¢ WP e1 @ E {{ Î¦ }}.
 Proof.
   iIntros (??) "[? H]". iApply wp_lift_atomic_step; eauto. iFrame. iNext.
   iIntros (???) "[% ?]". iApply "H". eauto.
 Qed.
 
-Lemma wp_lift_atomic_det_head_step {E Î¦ e1} Ïƒ1 v2 Ïƒ2 ef :
+Lemma wp_lift_atomic_det_head_step {E Î¦ e1} Ïƒ1 v2 Ïƒ2 efs :
   atomic e1 â†’
   head_reducible e1 Ïƒ1 â†’
-  (âˆ€ e2' Ïƒ2' ef', head_step e1 Ïƒ1 e2' Ïƒ2' ef' â†’
-    Ïƒ2 = Ïƒ2' âˆ§ to_val e2' = Some v2 âˆ§ ef = ef') â†’
-  â–· ownP Ïƒ1 â˜… â–· (ownP Ïƒ2 -â˜… (|={E}=> Î¦ v2) â˜… wp_fork ef) âŠ¢ WP e1 @ E {{ Î¦ }}.
+  (âˆ€ e2' Ïƒ2' efs', head_step e1 Ïƒ1 e2' Ïƒ2' efs' â†’
+    Ïƒ2 = Ïƒ2' âˆ§ to_val e2' = Some v2 âˆ§ efs = efs') â†’
+  â–· ownP Ïƒ1 â˜… â–· (ownP Ïƒ2 -â˜… (|={E}=> Î¦ v2) â˜… wp_fork efs) âŠ¢ WP e1 @ E {{ Î¦ }}.
 Proof. eauto using wp_lift_atomic_det_step. Qed.
 
-Lemma wp_lift_pure_det_head_step {E Î¦} e1 e2 ef :
+Lemma wp_lift_pure_det_head_step {E Î¦} e1 e2 efs :
   to_val e1 = None â†’
   (âˆ€ Ïƒ1, head_reducible e1 Ïƒ1) â†’
-  (âˆ€ Ïƒ1 e2' Ïƒ2 ef', head_step e1 Ïƒ1 e2' Ïƒ2 ef' â†’ Ïƒ1 = Ïƒ2 âˆ§ e2 = e2' âˆ§ ef = ef')â†’
-  â–· (WP e2 @ E {{ Î¦ }} â˜… wp_fork ef) âŠ¢ WP e1 @ E {{ Î¦ }}.
+  (âˆ€ Ïƒ1 e2' Ïƒ2 efs', head_step e1 Ïƒ1 e2' Ïƒ2 efs' â†’ Ïƒ1 = Ïƒ2 âˆ§ e2 = e2' âˆ§ efs = efs')â†’
+  â–· (WP e2 @ E {{ Î¦ }} â˜… wp_fork efs) âŠ¢ WP e1 @ E {{ Î¦ }}.
 Proof. eauto using wp_lift_pure_det_step. Qed.
 End wp.
diff --git a/program_logic/ectxi_language.v b/program_logic/ectxi_language.v
index 4a8f62fd85863f80c4946907b42602a29e98fc3d..cbc159d2dbebcd221087794cb87a4c7f2deb8afa 100644
--- a/program_logic/ectxi_language.v
+++ b/program_logic/ectxi_language.v
@@ -9,11 +9,11 @@ Class EctxiLanguage (expr val ectx_item state : Type) := {
   of_val : val â†’ expr;
   to_val : expr â†’ option val;
   fill_item : ectx_item â†’ expr â†’ expr;
-  head_step : expr â†’ state â†’ expr â†’ state â†’ option expr â†’ Prop;
+  head_step : expr â†’ state â†’ expr â†’ state â†’ list expr â†’ Prop;
 
   to_of_val v : to_val (of_val v) = Some v;
   of_to_val e v : to_val e = Some v â†’ of_val v = e;
-  val_stuck e1 Ïƒ1 e2 Ïƒ2 ef : head_step e1 Ïƒ1 e2 Ïƒ2 ef â†’ to_val e1 = None;
+  val_stuck e1 Ïƒ1 e2 Ïƒ2 efs : head_step e1 Ïƒ1 e2 Ïƒ2 efs â†’ to_val e1 = None;
 
   fill_item_inj Ki :> Inj (=) (=) (fill_item Ki);
   fill_item_val Ki e : is_Some (to_val (fill_item Ki e)) â†’ is_Some (to_val e);
@@ -21,8 +21,8 @@ Class EctxiLanguage (expr val ectx_item state : Type) := {
     to_val e1 = None â†’ to_val e2 = None â†’
     fill_item Ki1 e1 = fill_item Ki2 e2 â†’ Ki1 = Ki2;
 
-  head_ctx_step_val Ki e Ïƒ1 e2 Ïƒ2 ef :
-    head_step (fill_item Ki e) Ïƒ1 e2 Ïƒ2 ef â†’ is_Some (to_val e);
+  head_ctx_step_val Ki e Ïƒ1 e2 Ïƒ2 efs :
+    head_step (fill_item Ki e) Ïƒ1 e2 Ïƒ2 efs â†’ is_Some (to_val e);
 }.
 
 Arguments of_val {_ _ _ _ _} _.
@@ -60,8 +60,8 @@ Section ectxi_language.
   (* When something does a step, and another decomposition of the same expression
   has a non-val [e] in the hole, then [K] is a left sub-context of [K'] - in
   other words, [e] also contains the reducible expression *)
-  Lemma step_by_val K K' e1 e1' Ïƒ1 e2 Ïƒ2 ef :
-    fill K e1 = fill K' e1' â†’ to_val e1 = None â†’ head_step e1' Ïƒ1 e2 Ïƒ2 ef â†’
+  Lemma step_by_val K K' e1 e1' Ïƒ1 e2 Ïƒ2 efs :
+    fill K e1 = fill K' e1' â†’ to_val e1 = None â†’ head_step e1' Ïƒ1 e2 Ïƒ2 efs â†’
     exists K'', K' = K ++ K''. (* K `prefix_of` K' *)
   Proof.
     intros Hfill Hred Hnval; revert K' Hfill.
diff --git a/program_logic/ghost_ownership.v b/program_logic/ghost_ownership.v
index 3706f39fc3424def05dc1baecb13910e5ae178e4..0bbd38a5ea1583626d83949376bc03e025a6e474 100644
--- a/program_logic/ghost_ownership.v
+++ b/program_logic/ghost_ownership.v
@@ -1,33 +1,60 @@
-From iris.program_logic Require Export global_functor.
+From iris.program_logic Require Export model.
 From iris.algebra Require Import iprod gmap.
 Import uPred.
 
+(** The class [inG Î£ A] expresses that the CMRA [A] is in the list of functors
+[Î£]. This class is similar to the [subG] class, but written down in terms of
+individual CMRAs instead of lists of CMRA functors. This additional class is
+needed because Coq is otherwise unable to solve type class constraints due to
+higher-order unification problems. *)
+Class inG (Î£ : gFunctors) (A : cmraT) :=
+  InG { inG_id : gid Î£; inG_prf : A = Î£ inG_id (iPreProp Î£) }.
+Arguments inG_id {_ _} _.
+
+Lemma subG_inG Î£ (F : gFunctor) : subG F Î£ â†’ inG Î£ (F (iPreProp Î£)).
+Proof. move=> /(_ 0%fin) /= [j ->]. by exists j. Qed.
+
+(** * Definition of the connective [own] *)
+Definition iRes_singleton `{i : inG Î£ A} (Î³ : gname) (a : A) : iResUR Î£ :=
+  iprod_singleton (inG_id i) {[ Î³ := cmra_transport inG_prf a ]}.
+Instance: Params (@iRes_singleton) 4.
+
 Definition own_def `{inG Î£ A} (Î³ : gname) (a : A) : iProp Î£ :=
-  uPred_ownM (to_iRes Î³ a).
+  uPred_ownM (iRes_singleton Î³ a).
 Definition own_aux : { x | x = @own_def }. by eexists. Qed.
 Definition own {Î£ A i} := proj1_sig own_aux Î£ A i.
 Definition own_eq : @own = @own_def := proj2_sig own_aux.
 Instance: Params (@own) 4.
 Typeclasses Opaque own.
 
-(** Properties about ghost ownership *)
+(** * Properties about ghost ownership *)
 Section global.
 Context `{i : inG Î£ A}.
 Implicit Types a : A.
 
-(** * Properties of own *)
+(** ** Properties of [iRes_singleton] *)
+Global Instance iRes_singleton_ne Î³ n :
+  Proper (dist n ==> dist n) (@iRes_singleton Î£ A _ Î³).
+Proof. by intros a a' Ha; apply iprod_singleton_ne; rewrite Ha. Qed.
+Lemma iRes_singleton_op Î³ a1 a2 :
+  iRes_singleton Î³ (a1 â‹… a2) â‰¡ iRes_singleton Î³ a1 â‹… iRes_singleton Î³ a2.
+Proof.
+  by rewrite /iRes_singleton iprod_op_singleton op_singleton cmra_transport_op.
+Qed.
+
+(** ** Properties of [own] *)
 Global Instance own_ne Î³ n : Proper (dist n ==> dist n) (@own Î£ A _ Î³).
 Proof. rewrite !own_eq. solve_proper. Qed.
 Global Instance own_proper Î³ :
   Proper ((â‰¡) ==> (âŠ£âŠ¢)) (@own Î£ A _ Î³) := ne_proper _.
 
 Lemma own_op Î³ a1 a2 : own Î³ (a1 â‹… a2) âŠ£âŠ¢ own Î³ a1 â˜… own Î³ a2.
-Proof. by rewrite !own_eq /own_def -ownM_op to_iRes_op. Qed.
+Proof. by rewrite !own_eq /own_def -ownM_op iRes_singleton_op. Qed.
 Global Instance own_mono Î³ : Proper (flip (â‰¼) ==> (âŠ¢)) (@own Î£ A _ Î³).
 Proof. move=>a b [c ->]. rewrite own_op. eauto with I. Qed.
 Lemma own_valid Î³ a : own Î³ a âŠ¢ âœ“ a.
 Proof.
-  rewrite !own_eq /own_def ownM_valid /to_iRes.
+  rewrite !own_eq /own_def ownM_valid /iRes_singleton.
   rewrite iprod_validI (forall_elim (inG_id i)) iprod_lookup_singleton.
   rewrite gmap_validI (forall_elim Î³) lookup_singleton option_validI.
   (* implicit arguments differ a bit *)
@@ -42,13 +69,14 @@ Proof. rewrite !own_eq /own_def; apply _. Qed.
 Global Instance own_core_persistent Î³ a : Persistent a â†’ PersistentP (own Î³ a).
 Proof. rewrite !own_eq /own_def; apply _. Qed.
 
+(** ** Allocation *)
 (* TODO: This also holds if we just have âœ“ a at the current step-idx, as Iris
    assertion. However, the map_updateP_alloc does not suffice to show this. *)
 Lemma own_alloc_strong a (G : gset gname) :
   âœ“ a â†’ True =r=> âˆƒ Î³, â–  (Î³ âˆ‰ G) âˆ§ own Î³ a.
 Proof.
   intros Ha.
-  rewrite -(rvs_mono (âˆƒ m, â–  (âˆƒ Î³, Î³ âˆ‰ G âˆ§ m = to_iRes Î³ a) âˆ§ uPred_ownM m)%I).
+  rewrite -(rvs_mono (âˆƒ m, â–  (âˆƒ Î³, Î³ âˆ‰ G âˆ§ m = iRes_singleton Î³ a) âˆ§ uPred_ownM m)%I).
   - rewrite ownM_empty.
     eapply rvs_ownM_updateP, (iprod_singleton_updateP_empty (inG_id i));
       first (eapply alloc_updateP_strong', cmra_transport_valid, Ha);
@@ -62,10 +90,11 @@ Proof.
   apply rvs_mono, exist_mono=>?. eauto with I.
 Qed.
 
+(** ** Frame preserving updates *)
 Lemma own_updateP P Î³ a : a ~~>: P â†’ own Î³ a =r=> âˆƒ a', â–  P a' âˆ§ own Î³ a'.
 Proof.
   intros Ha. rewrite !own_eq.
-  rewrite -(rvs_mono (âˆƒ m, â–  (âˆƒ a', m = to_iRes Î³ a' âˆ§ P a') âˆ§ uPred_ownM m)%I).
+  rewrite -(rvs_mono (âˆƒ m, â–  (âˆƒ a', m = iRes_singleton Î³ a' âˆ§ P a') âˆ§ uPred_ownM m)%I).
   - eapply rvs_ownM_updateP, iprod_singleton_updateP;
       first by (eapply singleton_updateP', cmra_transport_updateP', Ha).
     naive_solver.
diff --git a/program_logic/global_functor.v b/program_logic/global_functor.v
deleted file mode 100644
index 489f415870b6983ea287a398ee7a4bd6057c8b1d..0000000000000000000000000000000000000000
--- a/program_logic/global_functor.v
+++ /dev/null
@@ -1,120 +0,0 @@
-From iris.program_logic Require Export model.
-From iris.algebra Require Import iprod gmap.
-
-Class inG (Î£ : gFunctors) (A : cmraT) := InG {
-  inG_id : gid Î£;
-  inG_prf : A = projT2 Î£ inG_id (iPreProp Î£)
-}.
-Arguments inG_id {_ _} _.
-
-Definition to_iRes `{i : inG Î£ A} (Î³ : gname) (a : A) : iResUR Î£ :=
-  iprod_singleton (inG_id i) {[ Î³ := cmra_transport inG_prf a ]}.
-Instance: Params (@to_iRes) 4.
-Typeclasses Opaque to_iRes.
-
-(** * Properties of [to_iRes] *)
-Section to_iRes.
-Context `{inG Î£ A}.
-Implicit Types a : A.
-
-Global Instance to_iRes_ne Î³ n :
-  Proper (dist n ==> dist n) (@to_iRes Î£ A _ Î³).
-Proof. by intros a a' Ha; apply iprod_singleton_ne; rewrite Ha. Qed.
-Lemma to_iRes_op Î³ a1 a2 :
-  to_iRes Î³ (a1 â‹… a2) â‰¡ to_iRes Î³ a1 â‹… to_iRes Î³ a2.
-Proof.
-  by rewrite /to_iRes iprod_op_singleton op_singleton cmra_transport_op.
-Qed.
-Global Instance to_iRes_timeless Î³ a : Timeless a â†’ Timeless (to_iRes Î³ a).
-Proof. rewrite /to_iRes; apply _. Qed.
-Global Instance to_iRes_persistent Î³ a :
-  Persistent a â†’ Persistent (to_iRes Î³ a).
-Proof. rewrite /to_iRes; apply _. Qed.
-End to_iRes.
-
-(** When instantiating the logic, we want to just plug together the
-    requirements exported by the modules we use. To this end, we construct
-    the "gFunctors" from a "list gFunctor", and have some typeclass magic
-    to infer the inG. *)
-Module gFunctorList.
-  Inductive T :=
-    | nil  : T
-    | cons : gFunctor â†’ T â†’ T.
-  Coercion singleton (F : gFunctor) : T := cons F nil.
-
-  Fixpoint app (Fs1 Fs2 : T) : T :=
-    match Fs1 with nil => Fs2 | cons F Fs1 => cons F (app Fs1 Fs2) end.
-
-  Fixpoint fold_right {A} (f : gFunctor â†’ A â†’ A) (a : A) (Fs : T) : A :=
-    match Fs with
-    | nil => a
-    | cons F Fs => f F (fold_right f a Fs)
-    end.
-End gFunctorList.
-Notation gFunctorList := gFunctorList.T.
-
-Delimit Scope gFunctor_scope with gFunctor.
-Bind Scope gFunctor_scope with gFunctorList.
-Arguments gFunctorList.cons _ _%gFunctor.
-
-Notation "[ ]" := gFunctorList.nil (format "[ ]") : gFunctor_scope.
-Notation "[ F ]" := (gFunctorList.app F gFunctorList.nil) : gFunctor_scope.
-Notation "[ F1 ; F2 ; .. ; Fn ]" :=
-  (gFunctorList.app F1 (gFunctorList.app F2 ..
-    (gFunctorList.app Fn gFunctorList.nil) ..)) : gFunctor_scope.
-
-Module gFunctors.
-  Definition nil : gFunctors := existT 0 (fin_0_inv _).
-
-  Definition cons (F : gFunctor) (Î£ : gFunctors) : gFunctors :=
-    existT (S (projT1 Î£)) (fin_S_inv _ F (projT2 Î£)).
-
-  Fixpoint app (Fs : gFunctorList) (Î£ : gFunctors) : gFunctors :=
-    match Fs with
-    | gFunctorList.nil => Î£
-    | gFunctorList.cons F Fs => cons F (app Fs Î£)
-    end.
-End gFunctors.
-
-(** Cannot bind this scope with the [gFunctorG] since [gFunctorG] is a
-notation hiding a more complex type. *)
-Notation "#[ ]" := gFunctors.nil (format "#[ ]").
-Notation "#[ Fs ]" := (gFunctors.app Fs gFunctors.nil).
-Notation "#[ Fs1 ; Fs2 ; .. ; Fsn ]" :=
-  (gFunctors.app Fs1 (gFunctors.app Fs2 ..
-    (gFunctors.app Fsn gFunctors.nil) ..)).
-
-(** We need another typeclass to identify the *functor* in the Î£. Basing inG on
-   the functor breaks badly because Coq is unable to infer the correct
-   typeclasses, it does not unfold the functor. *)
-Class inGF (Î£ : gFunctors) (F : gFunctor) := InGF {
-  inGF_id : gid Î£;
-  inGF_prf : F = projT2 Î£ inGF_id;
-}.
-(* Avoid eager type class search: this line ensures that type class search
-is only triggered if the first two arguments of inGF do not contain evars. Since
-instance search for [inGF] is restrained, instances should always have [inGF] as
-their first argument to avoid loops. For example, the instances [authGF_inGF]
-and [auth_identity] otherwise create a cycle that pops up arbitrarily. *)
-Hint Mode inGF + - : typeclass_instances.
-
-Lemma inGF_inG {Î£ F} : inGF Î£ F â†’ inG Î£ (F (iPreProp Î£)).
-Proof. intros. exists inGF_id. by rewrite -inGF_prf. Qed.
-Instance inGF_here {Î£} (F: gFunctor) : inGF (gFunctors.cons F Î£) F.
-Proof. by exists 0%fin. Qed.
-Instance inGF_further {Î£} (F F': gFunctor) :
-  inGF Î£ F â†’ inGF (gFunctors.cons F' Î£) F.
-Proof. intros [i ?]. by exists (FS i). Qed.
-
-(** For modules that need more than one functor, we offer a typeclass
-    [inGFs] to demand a list of rFunctor to be available. We do
-    *not* register any instances that go from there to [inGF], to
-    avoid cycles. *)
-Class inGFs (Î£ : gFunctors) (Fs : gFunctorList) :=
-  InGFs : (gFunctorList.fold_right (Î» F T, inGF Î£ F * T) () Fs)%type.
-
-Instance inGFs_nil {Î£} : inGFs Î£ [].
-Proof. exact tt. Qed.
-Instance inGFs_cons {Î£} F Fs :
-  inGF Î£ F â†’ inGFs Î£ Fs â†’ inGFs Î£ (gFunctorList.cons F Fs).
-Proof. by split. Qed.
diff --git a/program_logic/iris.v b/program_logic/iris.v
index 5153818ac1217f63c405dc2f4d2830a03b18d9b2..b32b16f073864c36a099365719db9410c4b9be96 100644
--- a/program_logic/iris.v
+++ b/program_logic/iris.v
@@ -17,13 +17,14 @@ Class irisG (Î› : language) (Î£ : gFunctors) : Set := IrisG {
   disabled_name : gname;
 }.
 
-Definition irisGF (Î› : language) : gFunctorList :=
-  [GFunctor (constRF (authUR (optionUR (exclR (stateC Î›)))));
-   GFunctor (authRF (gmapURF positive (agreeRF (laterCF idCF))));
-   GFunctor (constRF coPset_disjUR);
-   GFunctor (constRF (gset_disjUR positive))].
+Definition irisÎ£ (Î› : language) : gFunctors :=
+  #[GFunctor (constRF (authUR (optionUR (exclR (stateC Î›)))));
+    GFunctor (authRF (gmapURF positive (agreeRF (laterCF idCF))));
+    GFunctor (constRF coPset_disjUR);
+    GFunctor (constRF (gset_disjUR positive))].
 
-Instance inGF_barrierG `{H : inGFs Î£ (irisGF Î›)} : irisPreG Î› Î£.
+Instance subG_irisÎ£ {Î£ Î›} : subG (irisÎ£ Î›) Î£ â†’ irisPreG Î› Î£.
 Proof.
-  by destruct H as (?%inGF_inG & ?%inGF_inG & ?%inGF_inG & ?%inGF_inG & _).
-Qed.
+  intros [?%subG_inG [?%subG_inG
+    [?%subG_inG ?%subG_inG]%subG_inv]%subG_inv]%subG_inv; by constructor.
+Qed.
\ No newline at end of file
diff --git a/program_logic/language.v b/program_logic/language.v
index 33600f6dfce705774c1a66d601f6bfcb7c46e4ae..04bba2a4a4dc635d74a676aebd8b8f650c327afe 100644
--- a/program_logic/language.v
+++ b/program_logic/language.v
@@ -6,10 +6,10 @@ Structure language := Language {
   state : Type;
   of_val : val â†’ expr;
   to_val : expr â†’ option val;
-  prim_step : expr â†’ state â†’ expr â†’ state â†’ option expr â†’ Prop;
+  prim_step : expr â†’ state â†’ expr â†’ state â†’ list expr â†’ Prop;
   to_of_val v : to_val (of_val v) = Some v;
   of_to_val e v : to_val e = Some v â†’ of_val v = e;
-  val_stuck e Ïƒ e' Ïƒ' ef : prim_step e Ïƒ e' Ïƒ' ef â†’ to_val e = None
+  val_stuck e Ïƒ e' Ïƒ' efs : prim_step e Ïƒ e' Ïƒ' efs â†’ to_val e = None
 }.
 Arguments of_val {_} _.
 Arguments to_val {_} _.
@@ -29,31 +29,31 @@ Section language.
   Implicit Types v : val Î›.
 
   Definition reducible (e : expr Î›) (Ïƒ : state Î›) :=
-    âˆƒ e' Ïƒ' ef, prim_step e Ïƒ e' Ïƒ' ef.
+    âˆƒ e' Ïƒ' efs, prim_step e Ïƒ e' Ïƒ' efs.
   Definition atomic (e : expr Î›) : Prop :=
-    âˆ€ Ïƒ e' Ïƒ' ef, prim_step e Ïƒ e' Ïƒ' ef â†’ is_Some (to_val e').
+    âˆ€ Ïƒ e' Ïƒ' efs, prim_step e Ïƒ e' Ïƒ' efs â†’ is_Some (to_val e').
   Inductive step (Ï1 Ï2 : cfg Î›) : Prop :=
-    | step_atomic e1 Ïƒ1 e2 Ïƒ2 ef t1 t2 :
+    | step_atomic e1 Ïƒ1 e2 Ïƒ2 efs t1 t2 :
        Ï1 = (t1 ++ e1 :: t2, Ïƒ1) â†’
-       Ï2 = (t1 ++ e2 :: t2 ++ option_list ef, Ïƒ2) â†’
-       prim_step e1 Ïƒ1 e2 Ïƒ2 ef â†’
+       Ï2 = (t1 ++ e2 :: t2 ++ efs, Ïƒ2) â†’
+       prim_step e1 Ïƒ1 e2 Ïƒ2 efs â†’
        step Ï1 Ï2.
 
   Lemma of_to_val_flip v e : of_val v = e â†’ to_val e = Some v.
   Proof. intros <-. by rewrite to_of_val. Qed.
   Lemma reducible_not_val e Ïƒ : reducible e Ïƒ â†’ to_val e = None.
   Proof. intros (?&?&?&?); eauto using val_stuck. Qed.
-  Global Instance: Inj (=) (=) (@of_val Î›).
+  Global Instance of_val_inj : Inj (=) (=) (@of_val Î›).
   Proof. by intros v v' Hv; apply (inj Some); rewrite -!to_of_val Hv. Qed.
 End language.
 
 Class LanguageCtx (Î› : language) (K : expr Î› â†’ expr Î›) := {
   fill_not_val e :
     to_val e = None â†’ to_val (K e) = None;
-  fill_step e1 Ïƒ1 e2 Ïƒ2 ef :
-    prim_step e1 Ïƒ1 e2 Ïƒ2 ef â†’
-    prim_step (K e1) Ïƒ1 (K e2) Ïƒ2 ef;
-  fill_step_inv e1' Ïƒ1 e2 Ïƒ2 ef :
-    to_val e1' = None â†’ prim_step (K e1') Ïƒ1 e2 Ïƒ2 ef â†’
-    âˆƒ e2', e2 = K e2' âˆ§ prim_step e1' Ïƒ1 e2' Ïƒ2 ef
+  fill_step e1 Ïƒ1 e2 Ïƒ2 efs :
+    prim_step e1 Ïƒ1 e2 Ïƒ2 efs â†’
+    prim_step (K e1) Ïƒ1 (K e2) Ïƒ2 efs;
+  fill_step_inv e1' Ïƒ1 e2 Ïƒ2 efs :
+    to_val e1' = None â†’ prim_step (K e1') Ïƒ1 e2 Ïƒ2 efs â†’
+    âˆƒ e2', e2 = K e2' âˆ§ prim_step e1' Ïƒ1 e2' Ïƒ2 efs
 }.
diff --git a/program_logic/lifting.v b/program_logic/lifting.v
index 6fd4ecc6b6d390eab610602f999a1819ab18e1cd..12584487babb9284de89af4a80f59d601c839a03 100644
--- a/program_logic/lifting.v
+++ b/program_logic/lifting.v
@@ -13,14 +13,14 @@ Implicit Types Î¦ : val Î› â†’ iProp Î£.
 Lemma wp_lift_step E Î¦ e1 :
   to_val e1 = None â†’
   (|={E,âˆ…}=> âˆƒ Ïƒ1, â–  reducible e1 Ïƒ1 â˜… â–· ownP Ïƒ1 â˜…
-     â–· âˆ€ e2 Ïƒ2 ef, â–  prim_step e1 Ïƒ1 e2 Ïƒ2 ef â˜… ownP Ïƒ2
-          ={âˆ…,E}=â˜… WP e2 @ E {{ Î¦ }} â˜… wp_fork ef)
+    â–· âˆ€ e2 Ïƒ2 efs, â–  prim_step e1 Ïƒ1 e2 Ïƒ2 efs â˜… ownP Ïƒ2
+          ={âˆ…,E}=â˜… WP e2 @ E {{ Î¦ }} â˜… wp_fork efs)
   âŠ¢ WP e1 @ E {{ Î¦ }}.
 Proof.
   iIntros (?) "H". rewrite wp_unfold /wp_pre; iRight; iSplit; auto.
   iIntros (Ïƒ1) "HÏƒ". iVs "H" as (Ïƒ1') "(% & >HÏƒf & H)".
   iDestruct (ownP_agree Ïƒ1 Ïƒ1' with "[#]") as %<-; first by iFrame.
-  iVsIntro; iSplit; [done|]; iNext; iIntros (e2 Ïƒ2 ef Hstep).
+  iVsIntro; iSplit; [done|]; iNext; iIntros (e2 Ïƒ2 efs Hstep).
   iVs (ownP_update Ïƒ1 Ïƒ2 with "[-H]") as "[$ ?]"; first by iFrame.
   iApply "H"; eauto.
 Qed.
@@ -28,14 +28,14 @@ Qed.
 Lemma wp_lift_pure_step E Î¦ e1 :
   to_val e1 = None â†’
   (âˆ€ Ïƒ1, reducible e1 Ïƒ1) â†’
-  (âˆ€ Ïƒ1 e2 Ïƒ2 ef, prim_step e1 Ïƒ1 e2 Ïƒ2 ef â†’ Ïƒ1 = Ïƒ2) â†’
-  (â–· âˆ€ e2 ef Ïƒ, â–  prim_step e1 Ïƒ e2 Ïƒ ef â†’ WP e2 @ E {{ Î¦ }} â˜… wp_fork ef)
+  (âˆ€ Ïƒ1 e2 Ïƒ2 efs, prim_step e1 Ïƒ1 e2 Ïƒ2 efs â†’ Ïƒ1 = Ïƒ2) â†’
+  (â–· âˆ€ e2 efs Ïƒ, â–  prim_step e1 Ïƒ e2 Ïƒ efs â†’ WP e2 @ E {{ Î¦ }} â˜… wp_fork efs)
   âŠ¢ WP e1 @ E {{ Î¦ }}.
 Proof.
   iIntros (He Hsafe Hstep) "H". rewrite wp_unfold /wp_pre; iRight; iSplit; auto.
   iIntros (Ïƒ1) "HÏƒ". iApply pvs_intro'; [set_solver|iIntros "Hclose"].
-  iSplit; [done|]; iNext; iIntros (e2 Ïƒ2 ef ?).
-  destruct (Hstep Ïƒ1 e2 Ïƒ2 ef); auto; subst.
+  iSplit; [done|]; iNext; iIntros (e2 Ïƒ2 efs ?).
+  destruct (Hstep Ïƒ1 e2 Ïƒ2 efs); auto; subst.
   iVs "Hclose"; iVsIntro. iFrame "HÏƒ". iApply "H"; auto.
 Qed.
 
@@ -43,39 +43,39 @@ Qed.
 Lemma wp_lift_atomic_step {E Î¦} e1 Ïƒ1 :
   atomic e1 â†’
   reducible e1 Ïƒ1 â†’
-  â–· ownP Ïƒ1 â˜… â–· (âˆ€ v2 Ïƒ2 ef,
-    â–  prim_step e1 Ïƒ1 (of_val v2) Ïƒ2 ef âˆ§ ownP Ïƒ2 -â˜… (|={E}=> Î¦ v2) â˜… wp_fork ef)
+  â–· ownP Ïƒ1 â˜… â–· (âˆ€ v2 Ïƒ2 efs,
+    â–  prim_step e1 Ïƒ1 (of_val v2) Ïƒ2 efs âˆ§ ownP Ïƒ2 -â˜… (|={E}=> Î¦ v2) â˜… wp_fork efs)
   âŠ¢ WP e1 @ E {{ Î¦ }}.
 Proof.
   iIntros (Hatomic ?) "[HÏƒ H]".
   iApply (wp_lift_step E _ e1); eauto using reducible_not_val.
   iApply pvs_intro'; [set_solver|iIntros "Hclose"].
   iExists Ïƒ1. iFrame "HÏƒ"; iSplit; eauto.
-  iNext; iIntros (e2 Ïƒ2 ef) "[% HÏƒ]".
-  edestruct (Hatomic Ïƒ1 e2 Ïƒ2 ef) as [v2 <-%of_to_val]; eauto.
-  iDestruct ("H" $! v2 Ïƒ2 ef with "[HÏƒ]") as "[HÎ¦ $]"; first by eauto.
+  iNext; iIntros (e2 Ïƒ2 efs) "[% HÏƒ]".
+  edestruct (Hatomic Ïƒ1 e2 Ïƒ2 efs) as [v2 <-%of_to_val]; eauto.
+  iDestruct ("H" $! v2 Ïƒ2 efs with "[HÏƒ]") as "[HÎ¦ $]"; first by eauto.
   iVs "Hclose". iVs "HÎ¦". iApply wp_value; auto using to_of_val.
 Qed.
 
-Lemma wp_lift_atomic_det_step {E Î¦ e1} Ïƒ1 v2 Ïƒ2 ef :
+Lemma wp_lift_atomic_det_step {E Î¦ e1} Ïƒ1 v2 Ïƒ2 efs :
   atomic e1 â†’
   reducible e1 Ïƒ1 â†’
-  (âˆ€ e2' Ïƒ2' ef', prim_step e1 Ïƒ1 e2' Ïƒ2' ef' â†’
-                  Ïƒ2 = Ïƒ2' âˆ§ to_val e2' = Some v2 âˆ§ ef = ef') â†’
-  â–· ownP Ïƒ1 â˜… â–· (ownP Ïƒ2 -â˜… (|={E}=> Î¦ v2) â˜… wp_fork ef) âŠ¢ WP e1 @ E {{ Î¦ }}.
+  (âˆ€ e2' Ïƒ2' efs', prim_step e1 Ïƒ1 e2' Ïƒ2' efs' â†’
+                   Ïƒ2 = Ïƒ2' âˆ§ to_val e2' = Some v2 âˆ§ efs = efs') â†’
+  â–· ownP Ïƒ1 â˜… â–· (ownP Ïƒ2 -â˜… (|={E}=> Î¦ v2) â˜… wp_fork efs) âŠ¢ WP e1 @ E {{ Î¦ }}.
 Proof.
   iIntros (?? Hdet) "[HÏƒ1 HÏƒ2]". iApply (wp_lift_atomic_step _ Ïƒ1); try done.
-  iFrame. iNext. iIntros (v2' Ïƒ2' ef') "[% HÏƒ2']".
+  iFrame. iNext. iIntros (v2' Ïƒ2' efs') "[% HÏƒ2']".
   edestruct Hdet as (->&->%of_to_val%(inj of_val)&->). done. by iApply "HÏƒ2".
 Qed.
 
-Lemma wp_lift_pure_det_step {E Î¦} e1 e2 ef :
+Lemma wp_lift_pure_det_step {E Î¦} e1 e2 efs :
   to_val e1 = None â†’
   (âˆ€ Ïƒ1, reducible e1 Ïƒ1) â†’
-  (âˆ€ Ïƒ1 e2' Ïƒ2 ef', prim_step e1 Ïƒ1 e2' Ïƒ2 ef' â†’ Ïƒ1 = Ïƒ2 âˆ§ e2 = e2' âˆ§ ef = ef')â†’
-  â–· (WP e2 @ E {{ Î¦ }} â˜… wp_fork ef) âŠ¢ WP e1 @ E {{ Î¦ }}.
+  (âˆ€ Ïƒ1 e2' Ïƒ2 efs', prim_step e1 Ïƒ1 e2' Ïƒ2 efs' â†’ Ïƒ1 = Ïƒ2 âˆ§ e2 = e2' âˆ§ efs = efs')â†’
+  â–· (WP e2 @ E {{ Î¦ }} â˜… wp_fork efs) âŠ¢ WP e1 @ E {{ Î¦ }}.
 Proof.
   iIntros (?? Hpuredet) "?". iApply (wp_lift_pure_step E); try done.
-  by intros; eapply Hpuredet. iNext. by iIntros (e' ef' Ïƒ (_&->&->)%Hpuredet).
+  by intros; eapply Hpuredet. iNext. by iIntros (e' efs' Ïƒ (_&->&->)%Hpuredet).
 Qed.
 End lifting.
diff --git a/program_logic/model.v b/program_logic/model.v
index 6603df4d70964ea1556376fb778f77ef81365186..789c57a5beddd20183283ec8795cedd263767bce 100644
--- a/program_logic/model.v
+++ b/program_logic/model.v
@@ -2,11 +2,27 @@ From iris.algebra Require Export upred.
 From iris.algebra Require Import iprod gmap.
 From iris.algebra Require cofe_solver.
 
-(* The Iris program logic is parametrized by a dependent product of a bunch of
-[gFunctor]s, which are locally contractive functor from the category of COFEs to
-the category of CMRAs. These functors are instantiated with [iProp], the type
-of Iris propositions, which allows one to construct impredicate CMRAs, such as
-invariants and stored propositions using the agreement CMRA. *)
+(** In this file we construct the type [iProp] of propositions of the Iris
+logic. This is done by solving the following recursive domain equation:
+
+  iProp â‰ˆ uPred { i : gid  &  gname -fin-> (Î£ i) iProp }
+
+where:
+
+  Î£ : gFunctors  := lists of locally constractive functors
+  i : gid        := indexes addressing individual functors in [Î£]
+  Î³ : gname      := ghost variable names
+
+The Iris logic is parametrized by a list of locally contractive functors [Î£]
+from the category of COFEs to the category of CMRAs. These functors are
+instantiated with [iProp], the type of Iris propositions, which allows one to
+construct impredicate CMRAs, such as invariants and stored propositions using
+the agreement CMRA. *)
+
+
+(** * Locally contractive functors *)
+(** The type [gFunctor] bundles a functor from the category of COFEs to the
+category of CMRAs with a proof that it is locally contractive. *)
 Structure gFunctor := GFunctor {
   gFunctor_F :> rFunctor;
   gFunctor_contractive : rFunctorContractive gFunctor_F;
@@ -14,51 +30,125 @@ Structure gFunctor := GFunctor {
 Arguments GFunctor _ {_}.
 Existing Instance gFunctor_contractive.
 
-(** The global CMRA: Indexed product over a gid i to (gname --fin--> Î£ i) *)
+(** The type [gFunctors] describes the parameters [Î£] of the Iris logic: lists
+of [gFunctor]s.
+
+Note that [gFunctors] is isomorphic to [list gFunctor], but defined in an
+alternative way to avoid universe inconsistencies with respect to the universe
+monomorphic [list] type. *)
 Definition gFunctors := { n : nat & fin n â†’ gFunctor }.
+
 Definition gid (Î£ : gFunctors) := fin (projT1 Î£).
+Definition gFunctors_lookup (Î£ : gFunctors) : gid Î£ â†’ gFunctor := projT2 Î£.
+Coercion gFunctors_lookup : gFunctors >-> Funclass.
 
-(** Name of one instance of a particular CMRA in the ghost state. *)
 Definition gname := positive.
 
-(** Solution of the recursive domain equation *)
+(** The resources functor [iResF Î£ A := { i : gid & gname -fin-> (Î£ i) A }]. *)
+Definition iResF (Î£ : gFunctors) : urFunctor :=
+  iprodURF (Î» i, gmapURF gname (Î£ i)).
+
+
+(** We define functions for the empty list of functors, the singleton list of
+functors, and the append operator on lists of functors. These are used to
+compose [gFunctors] out of smaller pieces. *)
+Module gFunctors.
+  Definition nil : gFunctors := existT 0 (fin_0_inv _).
+
+  Definition singleton (F : gFunctor) : gFunctors :=
+    existT 1 (fin_S_inv (Î» _, gFunctor) F (fin_0_inv _)).
+
+  Definition app (Î£1 Î£2 : gFunctors) : gFunctors :=
+    existT (projT1 Î£1 + projT1 Î£2) (fin_plus_inv _ (projT2 Î£1) (projT2 Î£2)).
+End gFunctors.
+
+Coercion gFunctors.singleton : gFunctor >-> gFunctors.
+Notation "#[ ]" := gFunctors.nil (format "#[ ]").
+Notation "#[ Î£1 ; .. ; Î£n ]" :=
+  (gFunctors.app Î£1 .. (gFunctors.app Î£n gFunctors.nil) ..).
+
+
+(** * Subfunctors *)
+(** In order to make proofs in the Iris logic modular, they are not done with
+respect to some concrete list of functors [Î£], but are instead parametrized by
+an arbitrary list of functors [Î£] that contains atleast certain functors. For
+example, the lock library is parametrized by a functor [Î£] that should have:
+the functors corresponding to: the heap and the exclusive monoid to manage to
+lock invariant.
+
+The contraints to can be expressed using the type class [subG Î£1 Î£2], which
+expresses that the functors [Î£1] are contained in [Î£2]. *)
+Class subG (Î£1 Î£2 : gFunctors) := in_subG i : { j | Î£1 i = Î£2 j }.
+
+(** Avoid trigger happy type class search: this line ensures that type class
+search is only triggered if the arguments of [subG] do not contain evars. Since
+instance search for [subG] is restrained, instances should always have [subG] as
+their first parameter to avoid loops. For example, the instances [subG_authÎ£]
+and [auth_discrete] otherwise create a cycle that pops up arbitrarily. *)
+Hint Mode subG + + : typeclass_instances.
+
+Lemma subG_inv Î£1 Î£2 Î£ : subG (gFunctors.app Î£1 Î£2) Î£ â†’ subG Î£1 Î£ * subG Î£2 Î£.
+Proof.
+  move=> H; split.
+  - move=> i; move: H=> /(_ (Fin.L _ i)) [j] /=. rewrite fin_plus_inv_L; eauto.
+  - move=> i; move: H=> /(_ (Fin.R _ i)) [j] /=. rewrite fin_plus_inv_R; eauto.
+Qed.
+
+Instance subG_refl Î£ : subG Î£ Î£.
+Proof. move=> i; by exists i. Qed.
+Instance subG_app_l Î£ Î£1 Î£2 : subG Î£ Î£1 â†’ subG Î£ (gFunctors.app Î£1 Î£2).
+Proof.
+  move=> H i; move: H=> /(_ i) [j ?].
+  exists (Fin.L _ j). by rewrite /= fin_plus_inv_L.
+Qed.
+Instance inGF_app_r Î£ Î£1 Î£2 : subG Î£ Î£2 â†’ subG Î£ (gFunctors.app Î£1 Î£2).
+Proof.
+  move=> H i; move: H=> /(_ i) [j ?].
+  exists (Fin.R _ j). by rewrite /= fin_plus_inv_R.
+Qed.
+
+
+(** * Solution of the recursive domain equation *)
+(** We first declare a module type and then an instance of it so as to seall of
+the construction, this way we are sure we do not use any properties of the
+construction, and also avoid Coq from blindly unfolding it. *)
 Module Type iProp_solution_sig.
-Parameter iPreProp : gFunctors â†’ cofeT.
-Definition iResUR (Î£ : gFunctors) : ucmraT :=
-  iprodUR (Î» i, gmapUR gname (projT2 Î£ i (iPreProp Î£))).
-Definition iProp (Î£ : gFunctors) : cofeT := uPredC (iResUR Î£).
-
-Parameter iProp_unfold: âˆ€ {Î£}, iProp Î£ -n> iPreProp Î£.
-Parameter iProp_fold: âˆ€ {Î£}, iPreProp Î£ -n> iProp Î£.
-Parameter iProp_fold_unfold: âˆ€ {Î£} (P : iProp Î£),
-  iProp_fold (iProp_unfold P) â‰¡ P.
-Parameter iProp_unfold_fold: âˆ€ {Î£} (P : iPreProp Î£),
-  iProp_unfold (iProp_fold P) â‰¡ P.
+  Parameter iPreProp : gFunctors â†’ cofeT.
+  Definition iResUR (Î£ : gFunctors) : ucmraT :=
+    iprodUR (Î» i, gmapUR gname (Î£ i (iPreProp Î£))).
+  Definition iProp (Î£ : gFunctors) : cofeT := uPredC (iResUR Î£).
+
+  Parameter iProp_unfold: âˆ€ {Î£}, iProp Î£ -n> iPreProp Î£.
+  Parameter iProp_fold: âˆ€ {Î£}, iPreProp Î£ -n> iProp Î£.
+  Parameter iProp_fold_unfold: âˆ€ {Î£} (P : iProp Î£),
+    iProp_fold (iProp_unfold P) â‰¡ P.
+  Parameter iProp_unfold_fold: âˆ€ {Î£} (P : iPreProp Î£),
+    iProp_unfold (iProp_fold P) â‰¡ P.
 End iProp_solution_sig.
 
 Module Export iProp_solution : iProp_solution_sig.
-Import cofe_solver.
-Definition iResF (Î£ : gFunctors) : urFunctor :=
-  iprodURF (Î» i, gmapURF gname (projT2 Î£ i)).
-Definition iProp_result (Î£ : gFunctors) :
-  solution (uPredCF (iResF Î£)) := solver.result _.
-
-Definition iPreProp (Î£ : gFunctors) : cofeT := iProp_result Î£.
-Definition iResUR (Î£ : gFunctors) : ucmraT :=
-  iprodUR (Î» i, gmapUR gname (projT2 Î£ i (iPreProp Î£))).
-Definition iProp (Î£ : gFunctors) : cofeT := uPredC (iResUR Î£).
-
-Definition iProp_unfold {Î£} : iProp Î£ -n> iPreProp Î£ :=
-  solution_fold (iProp_result Î£).
-Definition iProp_fold {Î£} : iPreProp Î£ -n> iProp Î£ := solution_unfold _.
-Lemma iProp_fold_unfold {Î£} (P : iProp Î£) : iProp_fold (iProp_unfold P) â‰¡ P.
-Proof. apply solution_unfold_fold. Qed.
-Lemma iProp_unfold_fold {Î£} (P : iPreProp Î£) : iProp_unfold (iProp_fold P) â‰¡ P.
-Proof. apply solution_fold_unfold. Qed.
+  Import cofe_solver.
+  Definition iProp_result (Î£ : gFunctors) :
+    solution (uPredCF (iResF Î£)) := solver.result _.
+
+  Definition iPreProp (Î£ : gFunctors) : cofeT := iProp_result Î£.
+  Definition iResUR (Î£ : gFunctors) : ucmraT :=
+    iprodUR (Î» i, gmapUR gname (Î£ i (iPreProp Î£))).
+  Definition iProp (Î£ : gFunctors) : cofeT := uPredC (iResUR Î£).
+
+  Definition iProp_unfold {Î£} : iProp Î£ -n> iPreProp Î£ :=
+    solution_fold (iProp_result Î£).
+  Definition iProp_fold {Î£} : iPreProp Î£ -n> iProp Î£ := solution_unfold _.
+  Lemma iProp_fold_unfold {Î£} (P : iProp Î£) : iProp_fold (iProp_unfold P) â‰¡ P.
+  Proof. apply solution_unfold_fold. Qed.
+  Lemma iProp_unfold_fold {Î£} (P : iPreProp Î£) : iProp_unfold (iProp_fold P) â‰¡ P.
+  Proof. apply solution_fold_unfold. Qed.
 End iProp_solution.
 
 Bind Scope uPred_scope with iProp.
 
+
+(** * Properties of the solution to the recursive domain equation *)
 Lemma iProp_unfold_equivI {Î£} (P Q : iProp Î£) :
   iProp_unfold P â‰¡ iProp_unfold Q âŠ¢ (P â‰¡ Q : iProp Î£).
 Proof.
diff --git a/program_logic/saved_prop.v b/program_logic/saved_prop.v
index c27e0c886281c94f6507b7c09bad80c860de15d7..4e2888615d0577ea6b4b0151189dfa5edb5b6a7f 100644
--- a/program_logic/saved_prop.v
+++ b/program_logic/saved_prop.v
@@ -5,10 +5,11 @@ Import uPred.
 
 Class savedPropG (Î£ : gFunctors) (F : cFunctor) :=
   saved_prop_inG :> inG Î£ (agreeR (laterC (F (iPreProp Î£)))).
-Definition savedPropGF (F : cFunctor) : gFunctor :=
-  GFunctor (agreeRF (â–¶ F)).
-Instance inGF_savedPropG  `{inGF Î£ (savedPropGF F)} : savedPropG Î£ F.
-Proof. apply: inGF_inG. Qed.
+
+Definition savedPropÎ£ (F : cFunctor) : gFunctors :=
+  #[ GFunctor (agreeRF (â–¶ F)) ].
+Instance subG_savedPropÎ£  {Î£ F} : subG (savedPropÎ£ F) Î£ â†’ savedPropG Î£ F.
+Proof. apply subG_inG. Qed.
 
 Definition saved_prop_own `{savedPropG Î£ F}
     (Î³ : gname) (x : F (iProp Î£)) : iProp Î£ :=
diff --git a/program_logic/sts.v b/program_logic/sts.v
index e331e34c978d75f172783a60c0aa96ac2278dc53..527780b55fdcd0a56dde76b7cf6a56ed05c86bb0 100644
--- a/program_logic/sts.v
+++ b/program_logic/sts.v
@@ -8,13 +8,12 @@ Class stsG Î£ (sts : stsT) := StsG {
   sts_inG :> inG Î£ (stsR sts);
   sts_inhabited :> Inhabited (sts.state sts);
 }.
-Coercion sts_inG : stsG >-> inG.
-(** The Functor we need. *)
-Definition stsGF (sts : stsT) : gFunctor := GFunctor (constRF (stsR sts)).
-(* Show and register that they match. *)
-Instance inGF_stsG sts `{inGF Î› (stsGF sts)}
-  `{Inhabited (sts.state sts)} : stsG Î› sts.
-Proof. split; try apply _. apply: inGF_inG. Qed.
+
+(* The global functor we need and register that they match. *)
+Definition stsÎ£ (sts : stsT) : gFunctors := #[ GFunctor (constRF (stsR sts)) ].
+Instance subG_stsÎ£ Î£ sts :
+  subG (stsÎ£ sts) Î£ â†’ Inhabited (sts.state sts) â†’ stsG Î£ sts.
+Proof. intros ?%subG_inG ?. by split. Qed.
 
 Section definitions.
   Context `{irisG Î› Î£, stsG Î£ sts} (Î³ : gname).
diff --git a/program_logic/weakestpre.v b/program_logic/weakestpre.v
index b1ddc167952b3c1ba765f977c90648876109500c..3026e7e71e16e0f04f8f1d957b565270c67c9d90 100644
--- a/program_logic/weakestpre.v
+++ b/program_logic/weakestpre.v
@@ -1,5 +1,6 @@
 From iris.program_logic Require Export pviewshifts.
 From iris.program_logic Require Import ownership.
+From iris.algebra Require Import upred_big_op.
 From iris.prelude Require Export coPset.
 From iris.proofmode Require Import tactics pviewshifts.
 Import uPred.
@@ -12,18 +13,18 @@ Definition wp_pre `{irisG Î› Î£}
   (* step case *)
   (to_val e1 = None âˆ§ âˆ€ Ïƒ1,
      ownP_auth Ïƒ1 ={E,âˆ…}=â˜… â–  reducible e1 Ïƒ1 â˜…
-     â–· âˆ€ e2 Ïƒ2 ef, â–  prim_step e1 Ïƒ1 e2 Ïƒ2 ef ={âˆ…,E}=â˜…
+     â–· âˆ€ e2 Ïƒ2 efs, â–  prim_step e1 Ïƒ1 e2 Ïƒ2 efs ={âˆ…,E}=â˜…
        ownP_auth Ïƒ2 â˜… wp E e2 Î¦ â˜…
-       from_option (flip (wp âŠ¤) (Î» _, True)) True ef))%I.
+       [â˜…] (flip (wp âŠ¤) (Î» _, True) <$> efs)))%I.
 
 Local Instance wp_pre_contractive `{irisG Î› Î£} : Contractive wp_pre.
 Proof.
   rewrite /wp_pre=> n wp wp' Hwp E e1 Î¦.
   apply or_ne, and_ne, forall_ne; auto=> Ïƒ1; apply wand_ne; auto.
   apply pvs_ne, sep_ne, later_contractive; auto=> i ?.
-  apply forall_ne=> e2; apply forall_ne=> Ïƒ2; apply forall_ne=> ef.
+  apply forall_ne=> e2; apply forall_ne=> Ïƒ2; apply forall_ne=> efs.
   apply wand_ne, pvs_ne, sep_ne, sep_ne; auto; first by apply Hwp.
-  destruct ef; first apply Hwp; auto.
+  eapply big_sep_ne, list_fmap_ext_ne=> ef. by apply Hwp.
 Qed.
 
 Definition wp_def `{irisG Î› Î£} :
@@ -49,7 +50,7 @@ Notation "'WP' e {{ v , Q } }" := (wp âŠ¤ e (Î» v, Q))
   (at level 20, e, Q at level 200,
    format "'WP'  e  {{  v ,  Q  } }") : uPred_scope.
 
-Notation wp_fork ef := (from_option (flip (wp âŠ¤) (Î» _, True)) True ef)%I.
+Notation wp_fork efs := ([â˜…] (flip (wp âŠ¤) (Î» _, True) <$> efs))%I.
 
 Section wp.
 Context `{irisG Î› Î£}.
@@ -99,8 +100,8 @@ Proof.
   iSplit; [done|]; iIntros (Ïƒ1) "HÏƒ".
   iApply (pvs_trans _ E1); iApply pvs_intro'; auto. iIntros "Hclose".
   iVs ("H" $! Ïƒ1 with "HÏƒ") as "[$ H]".
-  iVsIntro. iNext. iIntros (e2 Ïƒ2 ef Hstep).
-  iVs ("H" $! _ Ïƒ2 ef with "[#]") as "($ & H & $)"; auto.
+  iVsIntro. iNext. iIntros (e2 Ïƒ2 efs Hstep).
+  iVs ("H" $! _ Ïƒ2 efs with "[#]") as "($ & H & $)"; auto.
   iVs "Hclose" as "_". by iApply ("IH" with "HÎ¦").
 Qed.
 
@@ -127,9 +128,9 @@ Proof.
   iIntros (Ïƒ1) "HÏƒ". iVs "H" as "[H|[_ H]]".
   { iDestruct "H" as (v') "[% ?]"; simplify_eq. }
   iVs ("H" $! Ïƒ1 with "HÏƒ") as "[$ H]".
-  iVsIntro. iNext. iIntros (e2 Ïƒ2 ef Hstep).
+  iVsIntro. iNext. iIntros (e2 Ïƒ2 efs Hstep).
   destruct (Hatomic _ _ _ _ Hstep) as [v <-%of_to_val].
-  iVs ("H" $! _ Ïƒ2 ef with "[#]") as "($ & H & $)"; auto.
+  iVs ("H" $! _ Ïƒ2 efs with "[#]") as "($ & H & $)"; auto.
   iVs (wp_value_inv with "H") as "==> H". by iApply wp_value'.
 Qed.
 
@@ -141,8 +142,8 @@ Proof.
   { iDestruct "Hv" as (v) "[% Hv]"; simplify_eq. }
   iRight; iSplit; [done|]. iIntros (Ïƒ1) "HÏƒ".
   iVs "HR". iVs ("H" $! _ with "HÏƒ") as "[$ H]".
-  iVsIntro; iNext; iIntros (e2 Ïƒ2 ef Hstep).
-  iVs ("H" $! e2 Ïƒ2 ef with "[%]") as "($ & H & $)"; auto.
+  iVsIntro; iNext; iIntros (e2 Ïƒ2 efs Hstep).
+  iVs ("H" $! e2 Ïƒ2 efs with "[%]") as "($ & H & $)"; auto.
   iVs "HR". iVsIntro. iApply (wp_strong_mono E2 _ _ Î¦); try iFrame; eauto.
 Qed.
 
@@ -157,9 +158,9 @@ Proof.
   iIntros (Ïƒ1) "HÏƒ". iVs ("H" $! _ with "HÏƒ") as "[% H]".
   iVsIntro; iSplit.
   { iPureIntro. unfold reducible in *. naive_solver eauto using fill_step. }
-  iNext; iIntros (e2 Ïƒ2 ef Hstep).
-  destruct (fill_step_inv e Ïƒ1 e2 Ïƒ2 ef) as (e2'&->&?); auto.
-  iVs ("H" $! e2' Ïƒ2 ef with "[%]") as "($ & H & $)"; auto.
+  iNext; iIntros (e2 Ïƒ2 efs Hstep).
+  destruct (fill_step_inv e Ïƒ1 e2 Ïƒ2 efs) as (e2'&->&?); auto.
+  iVs ("H" $! e2' Ïƒ2 efs with "[%]") as "($ & H & $)"; auto.
   by iApply "IH".
 Qed.
 
diff --git a/proofmode/class_instances.v b/proofmode/class_instances.v
index 988f337544dccec7128349279b1a7fc6eb0587a5..ff5944225792146a045b8c4607efb0ef7ac45e6d 100644
--- a/proofmode/class_instances.v
+++ b/proofmode/class_instances.v
@@ -1,5 +1,5 @@
 From iris.proofmode Require Export classes.
-From iris.algebra Require Import upred_big_op gmap upred_tactics.
+From iris.algebra Require Import upred_big_op gmap.
 Import uPred.
 
 Section classes.
@@ -225,7 +225,7 @@ Global Instance frame_sep_l R P1 P2 Q Q' :
 Proof. rewrite /Frame /MakeSep => <- <-. by rewrite assoc. Qed.
 Global Instance frame_sep_r R P1 P2 Q Q' :
   Frame R P2 Q â†’ MakeSep P1 Q Q' â†’ Frame R (P1 â˜… P2) Q' | 10.
-Proof. rewrite /Frame /MakeSep => <- <-. solve_sep_entails. Qed.
+Proof. rewrite /Frame /MakeSep => <- <-. by rewrite assoc (comm _ R) assoc. Qed.
 
 Class MakeAnd (P Q PQ : uPred M) := make_and : P âˆ§ Q âŠ£âŠ¢ PQ.
 Global Instance make_and_true_l P : MakeAnd True P P.
@@ -340,7 +340,8 @@ Global Instance is_now_True_later P : IsNowTrue (â–· P).
 Proof. by rewrite /IsNowTrue now_True_later. Qed.
 Global Instance is_now_True_rvs P : IsNowTrue P â†’ IsNowTrue (|=r=> P).
 Proof.
-  rewrite /IsNowTrue=> HP. by rewrite -{2}HP -now_True_rvs -(now_True_intro P).
+  rewrite /IsNowTrue=> HP.
+  by rewrite -{2}HP -(now_True_idemp P) -now_True_rvs -(now_True_intro P).
 Qed.
 
 (* FromViewShift *)
diff --git a/proofmode/tactics.v b/proofmode/tactics.v
index c3044b80fdd1f73b70d21983a6858bbd2519cdbd..0ffe83c1739c4a70109d6f8fb99fc56d1f356ed5 100644
--- a/proofmode/tactics.v
+++ b/proofmode/tactics.v
@@ -107,14 +107,14 @@ Local Tactic Notation "iPersistent" constr(H) :=
   eapply tac_persistent with _ H _ _ _; (* (i:=H) *)
     [env_cbv; reflexivity || fail "iPersistent:" H "not found"
     |let Q := match goal with |- IntoPersistentP ?Q _ => Q end in
-     apply _ || fail "iPersistent:" H ":" Q "not persistent"
+     apply _ || fail "iPersistent:" Q "not persistent"
     |env_cbv; reflexivity|].
 
 Local Tactic Notation "iPure" constr(H) "as" simple_intropattern(pat) :=
   eapply tac_pure with _ H _ _ _; (* (i:=H1) *)
     [env_cbv; reflexivity || fail "iPure:" H "not found"
     |let P := match goal with |- IntoPure ?P _ => P end in
-     apply _ || fail "iPure:" H ":" P "not pure"
+     apply _ || fail "iPure:" P "not pure"
     |intros pat].
 
 Tactic Notation "iPureIntro" :=
@@ -139,14 +139,15 @@ Local Tactic Notation "iSpecializeArgs" constr(H) open_constr(xs) :=
   | _ =>
     eapply tac_forall_specialize with _ H _ _ _ xs; (* (i:=H) (a:=x) *)
       [env_cbv; reflexivity || fail 1 "iSpecialize:" H "not found"
-      |apply _ || fail 1 "iSpecialize:" H "not a forall of the right arity or type"
+      |let P := match goal with |- ForallSpecialize _ ?P _ => P end in
+       apply _ || fail 1 "iSpecialize:" P "not a forall of the right arity or type"
       |cbn [himpl hcurry]; reflexivity|]
   end.
 
 Local Tactic Notation "iSpecializePat" constr(H) constr(pat) :=
   let solve_to_wand H1 :=
     let P := match goal with |- IntoWand ?P _ _ => P end in
-    apply _ || fail "iSpecialize:" H1 ":" P "not an implication/wand" in
+    apply _ || fail "iSpecialize:" P "not an implication/wand" in
   let rec go H1 pats :=
     lazymatch pats with
     | [] => idtac
@@ -157,7 +158,7 @@ Local Tactic Notation "iSpecializePat" constr(H) constr(pat) :=
          |env_cbv; reflexivity || fail "iSpecialize:" H1 "not found"
          |let P := match goal with |- IntoWand ?P ?Q _ => P end in
           let Q := match goal with |- IntoWand ?P ?Q _ => Q end in
-          apply _ || fail "iSpecialize: cannot instantiate" H1 ":" P "with" H2 ":" Q
+          apply _ || fail "iSpecialize: cannot instantiate" P "with" Q
          |env_cbv; reflexivity|go H1 pats]
     | SName true ?H2 :: ?pats =>
        eapply tac_specialize_persistent with _ _ H1 _ _ _ _;
@@ -270,7 +271,7 @@ Tactic Notation "iApply" open_constr(lem) :=
     |eapply tac_apply with _ H _ _ _;
        [env_cbv; reflexivity || fail 1 "iApply:" H "not found"
        |let P := match goal with |- IntoWand ?P _ _ => P end in
-        apply _ || fail 1 "iApply: cannot apply" H ":" P
+        apply _ || fail 1 "iApply: cannot apply" P
        |lazy beta (* reduce betas created by instantiation *)]] in
   lazymatch lem with
   | ITrm ?t ?xs ?pat =>
@@ -362,7 +363,7 @@ Local Tactic Notation "iOrDestruct" constr(H) "as" constr(H1) constr(H2) :=
   eapply tac_or_destruct with _ _ H _ H1 H2 _ _ _; (* (i:=H) (j1:=H1) (j2:=H2) *)
     [env_cbv; reflexivity || fail "iOrDestruct:" H "not found"
     |let P := match goal with |- IntoOr ?P _ _ => P end in
-     apply _ || fail "iOrDestruct:" H ":" P "not a disjunction"
+     apply _ || fail "iOrDestruct:" P "not a disjunction"
     |env_cbv; reflexivity || fail "iOrDestruct:" H1 "not fresh"
     |env_cbv; reflexivity || fail "iOrDestruct:" H2 "not fresh"| |].
 
@@ -398,7 +399,7 @@ Local Tactic Notation "iSepDestruct" constr(H) "as" constr(H1) constr(H2) :=
   eapply tac_sep_destruct with _ H _ H1 H2 _ _ _; (* (i:=H) (j1:=H1) (j2:=H2) *)
     [env_cbv; reflexivity || fail "iSepDestruct:" H "not found"
     |let P := match goal with |- IntoSep _ ?P _ _ => P end in
-     apply _ || fail "iSepDestruct:" H ":" P "not separating destructable"
+     apply _ || fail "iSepDestruct:" P "not separating destructable"
     |env_cbv; reflexivity || fail "iSepDestruct:" H1 "or" H2 " not fresh"|].
 
 Tactic Notation "iCombine" constr(H1) constr(H2) "as" constr(H) :=
@@ -407,7 +408,7 @@ Tactic Notation "iCombine" constr(H1) constr(H2) "as" constr(H) :=
     |env_cbv; reflexivity || fail "iCombine:" H2 "not found"
     |let P1 := match goal with |- FromSep _ ?P1 _ => P1 end in
      let P2 := match goal with |- FromSep _ _ ?P2 => P2 end in
-     apply _ || fail "iCombine: cannot combine" H1 ":" P1 "and" H2 ":" P2
+     apply _ || fail "iCombine: cannot combine" P1 "and" P2
     |env_cbv; reflexivity || fail "iCombine:" H "not fresh"|].
 
 (** Framing *)
@@ -479,7 +480,7 @@ Local Tactic Notation "iExistDestruct" constr(H)
   eapply tac_exist_destruct with H _ Hx _ _; (* (i:=H) (j:=Hx) *)
     [env_cbv; reflexivity || fail "iExistDestruct:" H "not found"
     |let P := match goal with |- IntoExist ?P _ => P end in
-     apply _ || fail "iExistDestruct:" H ":" P "not an existential"|];
+     apply _ || fail "iExistDestruct:" P "not an existential"|];
   let y := fresh in
   intros y; eexists; split;
     [env_cbv; reflexivity || fail "iExistDestruct:" Hx "not fresh"
@@ -517,7 +518,7 @@ Tactic Notation "iVsCore" constr(H) :=
     [env_cbv; reflexivity || fail "iVs:" H "not found"
     |let P := match goal with |- ElimVs ?P _ _ _ => P end in
      let Q := match goal with |- ElimVs _ _ ?Q _ => Q end in
-     apply _ || fail "iVs: cannot run" H ":" P "in" Q
+     apply _ || fail "iVs: cannot run" P "in" Q
                      "because the goal or hypothesis is not a view shift"
     |env_cbv; reflexivity|].
 
@@ -849,7 +850,7 @@ Local Tactic Notation "iRewriteCore" constr(lr) open_constr(lem) :=
     eapply (tac_rewrite _ Heq _ _ lr);
       [env_cbv; reflexivity || fail "iRewrite:" Heq "not found"
       |let P := match goal with |- ?P âŠ¢ _ => P end in
-       reflexivity || fail "iRewrite:" Heq ":" P "not an equality"
+       reflexivity || fail "iRewrite:" P "not an equality"
       |iRewriteFindPred
       |intros ??? ->; reflexivity|lazy beta; iClear Heq]).
 
@@ -862,7 +863,7 @@ Local Tactic Notation "iRewriteCore" constr(lr) open_constr(lem) "in" constr(H)
       [env_cbv; reflexivity || fail "iRewrite:" Heq "not found"
       |env_cbv; reflexivity || fail "iRewrite:" H "not found"
       |let P := match goal with |- ?P âŠ¢ _ => P end in
-       reflexivity || fail "iRewrite:" Heq ":" P "not an equality"
+       reflexivity || fail "iRewrite:" P "not an equality"
       |iRewriteFindPred
       |intros ??? ->; reflexivity
       |env_cbv; reflexivity|lazy beta; iClear Heq]).
diff --git a/tests/barrier_client.v b/tests/barrier_client.v
index e9680779b6b618d4a32e4c09d79b9f596503df92..686c3810d736561623d70d39253d274157bdfa76 100644
--- a/tests/barrier_client.v
+++ b/tests/barrier_client.v
@@ -59,7 +59,7 @@ End client.
 
 Lemma client_adequate Ïƒ : adequate client Ïƒ (Î» _, True).
 Proof.
-  apply (heap_adequacy #[ heapGF ; barrierGF ; spawnGF ])=> ?.
+  apply (heap_adequacy #[ heapÎ£ ; barrierÎ£ ; spawnÎ£ ])=> ?.
   apply (client_safe (nroot .@ "barrier")); auto with ndisj.
 Qed.
 
diff --git a/tests/counter.v b/tests/counter.v
new file mode 100644
index 0000000000000000000000000000000000000000..1a6f6c753ec4c0d8319fae3ac4b03d3e1776e7fc
--- /dev/null
+++ b/tests/counter.v
@@ -0,0 +1,138 @@
+(* This file contains a formalization of the monotone counter, but with an
+explicit contruction of the monoid, as we have also done in the proof mode
+paper. A version that uses the authoritative monoid and natural number monoid
+under max can be found in `heap_lang/lib/counter.v`. *)
+From iris.program_logic Require Export weakestpre.
+From iris.heap_lang Require Export lang.
+From iris.program_logic Require Export hoare.
+From iris.proofmode Require Import invariants tactics.
+From iris.heap_lang Require Import proofmode notation.
+Import uPred.
+
+Definition newcounter : val := Î»: <>, ref #0.
+Definition inc : val :=
+  rec: "inc" "l" :=
+    let: "n" := !"l" in
+    if: CAS "l" "n" (#1 + "n") then #() else "inc" "l".
+Definition read : val := Î»: "l", !"l".
+Global Opaque newcounter inc read.
+
+(** The CMRA we need. *)
+Inductive M := Auth : nat â†’ M | Frag : nat â†’ M | Bot.
+
+Section M.
+  Arguments cmra_op _ !_ !_/.
+  Arguments op _ _ !_ !_/.
+  Arguments core _ _ !_/.
+
+  Canonical Structure M_C : cofeT := leibnizC M.
+
+  Instance M_valid : Valid M := Î» x, x â‰  Bot.
+  Instance M_op : Op M := Î» x y,
+    match x, y with
+    | Auth n, Frag j | Frag j, Auth n => if decide (j â‰¤ n)%nat then Auth n else Bot
+    | Frag i, Frag j => Frag (max i j)
+    | _, _ => Bot
+    end.
+  Instance M_pcore : PCore M := Î» x,
+    Some match x with Auth j | Frag j => Frag j | _ => Bot end.
+  Instance M_empty : Empty M := Frag 0.
+
+  Definition M_ra_mixin : RAMixin M.
+  Proof.
+    apply ra_total_mixin; try solve_proper || eauto.
+    - intros [n1|i1|] [n2|i2|] [n3|i3|];
+        repeat (simpl; case_decide); f_equal/=; lia.
+    - intros [n1|i1|] [n2|i2|]; repeat (simpl; case_decide); f_equal/=; lia.
+    - intros [n|i|]; repeat (simpl; case_decide); f_equal/=; lia.
+    - by intros [n|i|].
+    - intros [n1|i1|] y [[n2|i2|] ?]; exists (core y); simplify_eq/=;
+        repeat (simpl; case_decide); f_equal/=; lia.
+    - intros [n1|i1|] [n2|i2|]; simpl; by try case_decide.
+  Qed.
+  Canonical Structure M_R : cmraT := discreteR M M_ra_mixin.
+  Definition M_ucmra_mixin : UCMRAMixin M.
+  Proof.
+    split; try (done || apply _).
+    intros [?|?|]; simpl; try case_decide; f_equal/=; lia.
+  Qed.
+  Canonical Structure M_UR : ucmraT := discreteUR M M_ra_mixin M_ucmra_mixin.
+
+  Global Instance frag_persistent n : Persistent (Frag n).
+  Proof. by constructor. Qed.
+  Lemma auth_frag_valid j n : âœ“ (Auth n â‹… Frag j) â†’ (j â‰¤ n)%nat.
+  Proof. simpl. case_decide. done. by intros []. Qed.
+  Lemma auth_frag_op (j n : nat) : (j â‰¤ n)%nat â†’ Auth n = Auth n â‹… Frag j.
+  Proof. intros. by rewrite /= decide_True. Qed.
+
+  Lemma M_update n : Auth n ~~> Auth (S n).
+  Proof.
+    apply cmra_discrete_update=>-[m|j|] /= ?; repeat case_decide; done || lia.
+  Qed.
+End M.
+
+Class counterG Î£ := CounterG { counter_tokG :> inG Î£ M_UR }.
+Definition counterÎ£ : gFunctors := #[GFunctor (constRF M_UR)].
+Instance subG_counterÎ£ {Î£} : subG counterÎ£ Î£ â†’ counterG Î£.
+Proof. intros [?%subG_inG _]%subG_inv. split; apply _. Qed.
+
+Section proof.
+Context `{!heapG Î£, !counterG Î£}.
+Implicit Types l : loc.
+
+Definition I (Î³ : gname) (l : loc) : iProp Î£ :=
+  (âˆƒ c : nat, l â†¦ #c â˜… own Î³ (Auth c))%I.
+
+Definition C (l : loc) (n : nat) : iProp Î£ :=
+  (âˆƒ N Î³, heapN âŠ¥ N âˆ§ heap_ctx âˆ§ inv N (I Î³ l) âˆ§ own Î³ (Frag n))%I.
+
+(** The main proofs. *)
+Global Instance C_persistent l n : PersistentP (C l n).
+Proof. apply _. Qed.
+
+Lemma newcounter_spec N :
+  heapN âŠ¥ N â†’
+  heap_ctx âŠ¢ {{ True }} newcounter #() {{ v, âˆƒ l, v = #l âˆ§ C l 0 }}.
+Proof.
+  iIntros (?) "#Hh !# _ /=". rewrite /newcounter. wp_seq. wp_alloc l as "Hl".
+  iVs (own_alloc (Auth 0)) as (Î³) "HÎ³"; first done.
+  rewrite (auth_frag_op 0 0) //; iDestruct "HÎ³" as "[HÎ³ HÎ³f]".
+  iVs (inv_alloc N _ (I Î³ l) with "[Hl HÎ³]") as "#?".
+  { iIntros "!>". iExists 0%nat. by iFrame. }
+  iVsIntro. rewrite /C; eauto 10.
+Qed.
+
+Lemma inc_spec l n :
+  {{ C l n }} inc #l {{ v, v = #() âˆ§ C l (S n) }}.
+Proof.
+  iIntros "!# Hl /=". iLÃ¶b as "IH". wp_rec.
+  iDestruct "Hl" as (N Î³) "(% & #Hh & #Hinv & HÎ³f)".
+  wp_bind (! _)%E; iInv N as (c) "[Hl HÎ³]" "Hclose".
+  wp_load. iVs ("Hclose" with "[Hl HÎ³]"); [iNext; iExists c; by iFrame|].
+  iVsIntro. wp_let. wp_op.
+  wp_bind (CAS _ _ _). iInv N as (c') ">[Hl HÎ³]" "Hclose".
+  destruct (decide (c' = c)) as [->|].
+  - iCombine "HÎ³" "HÎ³f" as "HÎ³".
+    iDestruct (own_valid with "#HÎ³") as %?%auth_frag_valid; rewrite -auth_frag_op //.
+    iVs (own_update with "HÎ³") as "HÎ³"; first apply M_update.
+    rewrite (auth_frag_op (S n) (S c)); last lia; iDestruct "HÎ³" as "[HÎ³ HÎ³f]".
+    wp_cas_suc. iVs ("Hclose" with "[Hl HÎ³]").
+    { iNext. iExists (S c). rewrite Nat2Z.inj_succ Z.add_1_l. by iFrame. }
+    iVsIntro. wp_if. iVsIntro; rewrite {3}/C; eauto 10.
+  - wp_cas_fail; first (intros [=]; abstract omega).
+    iVs ("Hclose" with "[Hl HÎ³]"); [iNext; iExists c'; by iFrame|].
+    iVsIntro. wp_if. iApply ("IH" with "[HÎ³f]"). rewrite {3}/C; eauto 10.
+Qed.
+
+Lemma read_spec l n :
+  {{ C l n }} read #l {{ v, âˆƒ m : nat, â–  (v = #m âˆ§ n â‰¤ m) âˆ§ C l m }}.
+Proof.
+  iIntros "!# Hl /=". iDestruct "Hl" as (N Î³) "(% & #Hh & #Hinv & HÎ³f)".
+  rewrite /read. wp_let. iInv N as (c) "[Hl HÎ³]" "Hclose". wp_load.
+  iDestruct (own_valid Î³ (Frag n â‹… Auth c) with "[#]") as % ?%auth_frag_valid.
+  { iApply own_op. by iFrame. }
+  rewrite (auth_frag_op c c); last lia; iDestruct "HÎ³" as "[HÎ³ HÎ³f']".
+  iVs ("Hclose" with "[Hl HÎ³]"); [iNext; iExists c; by iFrame|].
+  iVsIntro; rewrite /C; eauto 10 with omega.
+Qed.
+End proof.
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index 429e401a7941e7605e323489db579d112620e9ae..fecf44a345180c76daf1c3495833886b485e3d09 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -7,13 +7,13 @@ From iris.heap_lang Require Import proofmode notation.
 
 Section LangTests.
   Definition add : expr := #21 + #21.
-  Goal âˆ€ Ïƒ, head_step add Ïƒ (#42) Ïƒ None.
+  Goal âˆ€ Ïƒ, head_step add Ïƒ (#42) Ïƒ [].
   Proof. intros; do_head_step done. Qed.
   Definition rec_app : expr := (rec: "f" "x" := "f" "x") #0.
-  Goal âˆ€ Ïƒ, head_step rec_app Ïƒ rec_app Ïƒ None.
+  Goal âˆ€ Ïƒ, head_step rec_app Ïƒ rec_app Ïƒ [].
   Proof. intros. rewrite /rec_app. do_head_step done. Qed.
   Definition lam : expr := Î»: "x", "x" + #21.
-  Goal âˆ€ Ïƒ, head_step (lam #21)%E Ïƒ add Ïƒ None.
+  Goal âˆ€ Ïƒ, head_step (lam #21)%E Ïƒ add Ïƒ [].
   Proof. intros. rewrite /lam. do_head_step done. Qed.
 End LangTests.
 
@@ -77,4 +77,4 @@ Section LiftingTests.
 End LiftingTests.
 
 Lemma heap_e_adequate Ïƒ : adequate heap_e Ïƒ (Î» v, v = #2).
-Proof. eapply (heap_adequacy #[ heapGF ])=> ?. by apply heap_e_spec. Qed.
+Proof. eapply (heap_adequacy heapÎ£)=> ?. by apply heap_e_spec. Qed.
diff --git a/tests/joining_existentials.v b/tests/joining_existentials.v
index af329f00932c261017a1c8cbd03b7437c8d9d766..b9a7a6ca2bc13d997d361c11837dd1284e0ec935 100644
--- a/tests/joining_existentials.v
+++ b/tests/joining_existentials.v
@@ -13,10 +13,10 @@ Definition Shot {Î£} {F : cFunctor} (x : F (iProp Î£)) : one_shotR Î£ F :=
 
 Class oneShotG (Î£ : gFunctors) (F : cFunctor) :=
   one_shot_inG :> inG Î£ (one_shotR Î£ F).
-Definition oneShotGF (F : cFunctor) : gFunctor :=
-  GFunctor (csumRF (exclRF unitC) (agreeRF (â–¶ F))).
-Instance inGF_oneShotG  `{inGF Î£ (oneShotGF F)} : oneShotG Î£ F.
-Proof. apply: inGF_inG. Qed.
+Definition oneShotÎ£ (F : cFunctor) : gFunctors :=
+  #[ GFunctor (csumRF (exclRF unitC) (agreeRF (â–¶ F))) ].
+Instance subG_oneShotÎ£ {Î£ F} : subG (oneShotÎ£ F) Î£ â†’ oneShotG Î£ F.
+Proof. apply subG_inG. Qed.
 
 Definition client eM eW1 eW2 : expr :=
   let: "b" := newbarrier #() in
diff --git a/tests/one_shot.v b/tests/one_shot.v
index e5cec89dc3c618eff94efe7cfcbd8dad7f41cd9e..111a9f5542819951476e5268ba0fd8e45ada0d14 100644
--- a/tests/one_shot.v
+++ b/tests/one_shot.v
@@ -24,10 +24,10 @@ Definition one_shotR := csumR (exclR unitC) (dec_agreeR Z).
 Definition Pending : one_shotR := (Cinl (Excl ()) : one_shotR).
 Definition Shot (n : Z) : one_shotR := (Cinr (DecAgree n) : one_shotR).
 
-Class one_shotG Î£ := one_shot_inG :> inG Î£ one_shotR.
-Definition one_shotGF : gFunctorList := [GFunctor (constRF one_shotR)].
-Instance inGF_one_shotG Î£ : inGFs Î£ one_shotGF â†’ one_shotG Î£.
-Proof. intros [? _]; apply: inGF_inG. Qed.
+Class one_shotG Î£ := { one_shot_inG :> inG Î£ one_shotR }.
+Definition one_shotÎ£ : gFunctors := #[GFunctor (constRF one_shotR)].
+Instance subG_one_shotÎ£ {Î£} : subG one_shotÎ£ Î£ â†’ one_shotG Î£.
+Proof. intros [?%subG_inG _]%subG_inv. split; apply _. Qed.
 
 Section proof.
 Context `{!heapG Î£, !one_shotG Î£} (N : namespace) (HN : heapN âŠ¥ N).