diff --git a/CHANGELOG.md b/CHANGELOG.md
index 89bbb9efa0742312eac45297f9f4a7fa9ae78a52..72efeb033f6cd3d9bb35f26d9ee46d1c9e05529e 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -12,11 +12,11 @@ Coq development, but not every API-breaking change is listed.  Changes marked
   updates.  Weakestpre is defined inside the logic, and invariants and view
   shifts with masks are also coded up inside Iris.  Adequacy of weakestpre
   is proven in the logic.
-* [#] Use OFEs instead of COFEs everywhere.  COFEs are only used for solving the
+* Use OFEs instead of COFEs everywhere.  COFEs are only used for solving the
   recursive domain equation.  As a consequence, CMRAs no longer need a proof
   of completeness.
   (The old `cofeT` is provided by `algebra.deprecated`.)
-* [#] Implement a new agreement construction.  Unlike the old one, this one
+* Implement a new agreement construction.  Unlike the old one, this one
   preserves discreteness.
 * Renaming and moving things around: uPred and the rest of the base logic are
   in `base_logic`, while `program_logic` is for everything involving the
diff --git a/algebra/ofe.v b/algebra/ofe.v
index 7b08c03cc6be5dc18fa7ca1abfaace672fcf857b..0419aa3d72ad05e9bceab1cd5e9e115c565ba43d 100644
--- a/algebra/ofe.v
+++ b/algebra/ofe.v
@@ -83,6 +83,11 @@ Record chain (A : ofeT) := {
 Arguments chain_car {_} _ _.
 Arguments chain_cauchy {_} _ _ _ _.
 
+Program Definition chain_map {A B : ofeT} (f : A → B)
+    `{!∀ n, Proper (dist n ==> dist n) f} (c : chain A) : chain B :=
+  {| chain_car n := f (c n) |}.
+Next Obligation. by intros A B f Hf c n i ?; apply Hf, chain_cauchy. Qed.
+
 Notation Compl A := (chain A%type → A).
 Class Cofe (A : ofeT) := {
   compl : Compl A;
@@ -140,8 +145,14 @@ Section cofe.
 End cofe.
 
 (** Contractive functions *)
-Class Contractive {A B : ofeT} (f : A → B) :=
-  contractive n x y : (∀ i, i < n → x ≡{i}≡ y) → f x ≡{n}≡ f y.
+Definition dist_later {A : ofeT} (n : nat) (x y : A) : Prop :=
+  match n with 0 => True | S n => x ≡{n}≡ y end.
+Arguments dist_later _ !_ _ _ /.
+
+Global Instance dist_later_equivalence A n : Equivalence (@dist_later A n).
+Proof. destruct n as [|n]. by split. apply dist_equivalence. Qed.
+
+Notation Contractive f := (∀ n, Proper (dist_later n ==> dist n) f).
 
 Instance const_contractive {A B : ofeT} (x : A) : Contractive (@const A B x).
 Proof. by intros n y1 y2. Qed.
@@ -151,9 +162,9 @@ Section contractive.
   Implicit Types x y : A.
 
   Lemma contractive_0 x y : f x ≡{0}≡ f y.
-  Proof. eauto using contractive with omega. Qed.
+  Proof. by apply (_ : Contractive f). Qed.
   Lemma contractive_S n x y : x ≡{n}≡ y → f x ≡{S n}≡ f y.
-  Proof. eauto using contractive, dist_le with omega. Qed.
+  Proof. intros. by apply (_ : Contractive f). Qed.
 
   Global Instance contractive_ne n : Proper (dist n ==> dist n) f | 100.
   Proof. by intros x y ?; apply dist_S, contractive_S. Qed.
@@ -161,18 +172,27 @@ Section contractive.
   Proof. apply (ne_proper _). Qed.
 End contractive.
 
-(** Mapping a chain *)
-Program Definition chain_map {A B : ofeT} (f : A → B)
-    `{!∀ n, Proper (dist n ==> dist n) f} (c : chain A) : chain B :=
-  {| chain_car n := f (c n) |}.
-Next Obligation. by intros A B f Hf c n i ?; apply Hf, chain_cauchy. Qed.
+Ltac f_contractive :=
+  match goal with
+  | |- ?f _ ≡{_}≡ ?f _ => apply (_ : Proper (dist_later _ ==> _) f)
+  | |- ?f _ _ ≡{_}≡ ?f _ _ => apply (_ : Proper (dist_later _ ==> _ ==> _) f)
+  | |- ?f _ _ ≡{_}≡ ?f _ _ => apply (_ : Proper (_ ==> dist_later _ ==> _) f)
+  end;
+  try match goal with
+  | |- dist_later ?n ?x ?y => destruct n as [|n]; [done|change (x ≡{n}≡ y)]
+  end;
+  try reflexivity.
+
+Ltac solve_contractive :=
+  preprocess_solve_proper;
+  solve [repeat (first [f_contractive|f_equiv]; try eassumption)].
 
 (** Fixpoint *)
 Program Definition fixpoint_chain {A : ofeT} `{Inhabited A} (f : A → A)
   `{!Contractive f} : chain A := {| chain_car i := Nat.iter (S i) f inhabitant |}.
 Next Obligation.
   intros A ? f ? n.
-  induction n as [|n IH]; intros [|i] ?; simpl in *; try reflexivity || omega.
+  induction n as [|n IH]=> -[|i] //= ?; try omega.
   - apply (contractive_0 f).
   - apply (contractive_S f), IH; auto with omega.
 Qed.
@@ -213,6 +233,85 @@ Section fixpoint.
   Proof. setoid_rewrite equiv_dist; naive_solver eauto using fixpoint_ne. Qed.
 End fixpoint.
 
+(** Mutual fixpoints *)
+Section fixpoint2.
+  Context `{Cofe A, Cofe B, !Inhabited A, !Inhabited B}.
+  Context (fA : A → B → A).
+  Context (fB : A → B → B).
+  Context `{∀ n, Proper (dist_later n ==> dist n ==> dist n) fA}.
+  Context `{∀ n, Proper (dist_later n ==> dist_later n ==> dist n) fB}.
+
+  Local Definition fixpoint_AB (x : A) : B := fixpoint (fB x).
+  Local Instance fixpoint_AB_contractive : Contractive fixpoint_AB.
+  Proof.
+    intros n x x' Hx; rewrite /fixpoint_AB.
+    apply fixpoint_ne=> y. by f_contractive.
+  Qed.
+
+  Local Definition fixpoint_AA (x : A) : A := fA x (fixpoint_AB x).
+  Local Instance fixpoint_AA_contractive : Contractive fixpoint_AA.
+  Proof. solve_contractive. Qed.
+
+  Definition fixpoint_A : A := fixpoint fixpoint_AA.
+  Definition fixpoint_B : B := fixpoint_AB fixpoint_A.
+
+  Lemma fixpoint_A_unfold : fA fixpoint_A fixpoint_B ≡ fixpoint_A.
+  Proof. by rewrite {2}/fixpoint_A (fixpoint_unfold _). Qed.
+  Lemma fixpoint_B_unfold : fB fixpoint_A fixpoint_B ≡ fixpoint_B.
+  Proof. by rewrite {2}/fixpoint_B /fixpoint_AB (fixpoint_unfold _). Qed.
+
+  Instance: Proper ((≡) ==> (≡) ==> (≡)) fA.
+  Proof.
+    apply ne_proper_2=> n x x' ? y y' ?. f_contractive; auto using dist_S.
+  Qed.
+  Instance: Proper ((≡) ==> (≡) ==> (≡)) fB.
+  Proof.
+    apply ne_proper_2=> n x x' ? y y' ?. f_contractive; auto using dist_S.
+  Qed.
+
+  Lemma fixpoint_A_unique p q : fA p q ≡ p → fB p q ≡ q → p ≡ fixpoint_A.
+  Proof.
+    intros HfA HfB. rewrite -HfA. apply fixpoint_unique. rewrite /fixpoint_AA.
+    f_equiv=> //. apply fixpoint_unique. by rewrite HfA HfB.
+  Qed.
+  Lemma fixpoint_B_unique p q : fA p q ≡ p → fB p q ≡ q → q ≡ fixpoint_B.
+  Proof. intros. apply fixpoint_unique. by rewrite -fixpoint_A_unique. Qed.
+End fixpoint2.
+
+Section fixpoint2_ne.
+  Context `{Cofe A, Cofe B, !Inhabited A, !Inhabited B}.
+  Context (fA fA' : A → B → A).
+  Context (fB fB' : A → B → B).
+  Context `{∀ n, Proper (dist_later n ==> dist n ==> dist n) fA}.
+  Context `{∀ n, Proper (dist_later n ==> dist n ==> dist n) fA'}.
+  Context `{∀ n, Proper (dist_later n ==> dist_later n ==> dist n) fB}.
+  Context `{∀ n, Proper (dist_later n ==> dist_later n ==> dist n) fB'}.
+
+  Lemma fixpoint_A_ne n :
+    (∀ x y, fA x y ≡{n}≡ fA' x y) → (∀ x y, fB x y ≡{n}≡ fB' x y) →
+    fixpoint_A fA fB ≡{n}≡ fixpoint_A fA' fB'.
+  Proof.
+    intros HfA HfB. apply fixpoint_ne=> z.
+    rewrite /fixpoint_AA /fixpoint_AB HfA. f_equiv. by apply fixpoint_ne.
+  Qed.
+  Lemma fixpoint_B_ne n :
+    (∀ x y, fA x y ≡{n}≡ fA' x y) → (∀ x y, fB x y ≡{n}≡ fB' x y) →
+    fixpoint_B fA fB ≡{n}≡ fixpoint_B fA' fB'.
+  Proof.
+    intros HfA HfB. apply fixpoint_ne=> z. rewrite HfB. f_contractive.
+    apply fixpoint_A_ne; auto using dist_S.
+  Qed.
+
+  Lemma fixpoint_A_proper :
+    (∀ x y, fA x y ≡ fA' x y) → (∀ x y, fB x y ≡ fB' x y) →
+    fixpoint_A fA fB ≡ fixpoint_A fA' fB'.
+  Proof. setoid_rewrite equiv_dist; naive_solver eauto using fixpoint_A_ne. Qed.
+  Lemma fixpoint_B_proper :
+    (∀ x y, fA x y ≡ fA' x y) → (∀ x y, fB x y ≡ fB' x y) →
+    fixpoint_B fA fB ≡ fixpoint_B fA' fB'.
+  Proof. setoid_rewrite equiv_dist; naive_solver eauto using fixpoint_B_ne. Qed.
+End fixpoint2_ne.
+
 (** Function space *)
 (* We make [ofe_fun] a definition so that we can register it as a canonical
 structure. *)
@@ -513,7 +612,7 @@ Instance ofe_morCF_contractive F1 F2 :
   cFunctorContractive (ofe_morCF F1 F2).
 Proof.
   intros ?? A1 A2 B1 B2 n [f g] [f' g'] Hfg; simpl in *.
-  apply ofe_morC_map_ne; apply cFunctor_contractive=>i ?; split; by apply Hfg.
+  apply ofe_morC_map_ne; apply cFunctor_contractive; destruct n, Hfg; by split.
 Qed.
 
 (** Sum *)
@@ -606,6 +705,7 @@ Qed.
 (** Discrete cofe *)
 Section discrete_cofe.
   Context `{Equiv A, @Equivalence A (≡)}.
+
   Instance discrete_dist : Dist A := λ n x y, x ≡ y.
   Definition discrete_ofe_mixin : OfeMixin A.
   Proof.
@@ -614,7 +714,7 @@ Section discrete_cofe.
     - done.
     - done.
   Qed.
-  
+
   Global Program Instance discrete_cofe : Cofe (OfeT A discrete_ofe_mixin) :=
     { compl c := c 0 }.
   Next Obligation.
@@ -743,17 +843,17 @@ Section later.
   Context {A : ofeT}.
   Instance later_equiv : Equiv (later A) := λ x y, later_car x ≡ later_car y.
   Instance later_dist : Dist (later A) := λ n x y,
-    match n with 0 => True | S n => later_car x ≡{n}≡ later_car y end.
+    dist_later n (later_car x) (later_car y).
   Definition later_ofe_mixin : OfeMixin (later A).
   Proof.
     split.
     - intros x y; unfold equiv, later_equiv; rewrite !equiv_dist.
       split. intros Hxy [|n]; [done|apply Hxy]. intros Hxy n; apply (Hxy (S n)).
-    - intros [|n]; [by split|split]; unfold dist, later_dist.
+    - split; rewrite /dist /later_dist.
       + by intros [x].
       + by intros [x] [y].
       + by intros [x] [y] [z] ??; trans y.
-    - intros [|n] [x] [y] ?; [done|]; unfold dist, later_dist; by apply dist_S.
+    - intros [|n] [x] [y] ?; [done|]; rewrite /dist /later_dist; by apply dist_S.
   Qed.
   Canonical Structure laterC : ofeT := OfeT (later A) later_ofe_mixin.
 
@@ -767,15 +867,21 @@ Section later.
   Qed.
 
   Global Instance Next_contractive : Contractive (@Next A).
-  Proof. intros [|n] x y Hxy; [done|]; apply Hxy; lia. Qed.
+  Proof. by intros [|n] x y. Qed.
   Global Instance Later_inj n : Inj (dist n) (dist (S n)) (@Next A).
   Proof. by intros x y. Qed.
 
-  Lemma later_car_compose_ne {B : ofeT} (f : A → B) :
-    (Contractive f) → ∀ n, Proper (dist n ==> dist n) (f ∘ later_car).
+  Instance later_car_anti_contractive n :
+    Proper (dist n ==> dist_later n) later_car.
+  Proof. move=> [x] [y] /= Hxy. done. Qed.
+
+  Lemma contractive_alt {B : ofeT} (f : A → B) :
+    Contractive f ↔ ∃ g : later A → B,
+      (∀ n, Proper (dist n ==> dist n) g) ∧ (∀ x, f x ≡ g (Next x)).
   Proof.
-    move=> Hcont n [x] [y] /= Hxy. apply Hcont. intros m Hmn.
-    destruct n; first by (exfalso; omega). eapply dist_le', Hxy. omega.
+    split.
+    - intros Hf. exists (f ∘ later_car); split=> // n x y ?. by f_equiv.
+    - intros (g&Hg&Hf) n x y Hxy. rewrite !Hf. by apply Hg.
   Qed.
 End later.
 
@@ -819,8 +925,8 @@ Qed.
 
 Instance laterCF_contractive F : cFunctorContractive (laterCF F).
 Proof.
-  intros A1 A2 B1 B2 n fg fg' Hfg.
-  apply laterC_map_contractive => i ?. by apply cFunctor_ne, Hfg.
+  intros A1 A2 B1 B2 n fg fg' Hfg. apply laterC_map_contractive.
+  destruct n as [|n]; simpl in *; first done. apply cFunctor_ne, Hfg.
 Qed.
 
 (** Notation for writing functors *)
diff --git a/algebra/sts.v b/algebra/sts.v
index fd6046d1f67c83aa4ba2cd17b504b04a8caa066f..d19e197490eec334037450f8d55cf673aaff89b8 100644
--- a/algebra/sts.v
+++ b/algebra/sts.v
@@ -78,7 +78,7 @@ Qed.
 Global Instance up_set_preserving : Proper ((⊆) ==> flip (⊆) ==> (⊆)) up_set.
 Proof.
   intros S1 S2 HS T1 T2 HT. rewrite /up_set.
-  f_equiv; last done. move =>s1 s2 Hs. simpl in HT. by apply up_preserving.
+  f_equiv=> // s1 s2 Hs. by apply up_preserving.
 Qed.
 Global Instance up_set_proper : Proper ((≡) ==> (≡) ==> (≡)) up_set.
 Proof.
diff --git a/base_logic/derived.v b/base_logic/derived.v
index 81d2539970b170daa7918ca97b8a84609fb7cc07..7361ad14752e70666af09eaad19906a3e2a13897 100644
--- a/base_logic/derived.v
+++ b/base_logic/derived.v
@@ -290,10 +290,8 @@ Proof. apply (internal_eq_rewrite a b (λ b, b ≡ a)%I); auto. solve_proper. Qe
 Lemma internal_eq_rewrite_contractive {A : ofeT} a b (Ψ : A → uPred M) P
   {HΨ : Contractive Ψ} : (P ⊢ ▷ (a ≡ b)) → (P ⊢ Ψ a) → P ⊢ Ψ b.
 Proof.
-  rewrite -later_equivI. intros Heq.
-  change ((P ⊢ (Ψ ∘ later_car) (Next a)) → P ⊢ (Ψ ∘ later_car) (Next b)).
-  apply internal_eq_rewrite; last done.
-  exact: later_car_compose_ne.
+  move: HΨ=> /contractiveI HΨ Heq ?.
+  apply (internal_eq_rewrite (Ψ a) (Ψ b) id _)=>//=. by rewrite -HΨ.
 Qed.
 
 Lemma pure_impl_forall φ P : (⌜φ⌝ → P) ⊣⊢ (∀ _ : φ, P).
diff --git a/base_logic/lib/boxes.v b/base_logic/lib/boxes.v
index 8e53d5347f5ac51c7facd30edee618d74dd413bd..8c3bc73bdb49edadfe489c4aa202e64bc8c3cdc7 100644
--- a/base_logic/lib/boxes.v
+++ b/base_logic/lib/boxes.v
@@ -47,17 +47,17 @@ Global Instance box_own_prop_ne n γ : Proper (dist n ==> dist n) (box_own_prop
 Proof. solve_proper. Qed.
 Global Instance box_inv_ne n γ : Proper (dist n ==> dist n) (slice_inv γ).
 Proof. solve_proper. Qed.
+
 Global Instance slice_ne n γ : Proper (dist n ==> dist n) (slice N γ).
 Proof. solve_proper. Qed.
-Global Instance box_contractive f : Contractive (box N f).
-Proof.
-  intros n P1 P2 HP1P2. apply exist_ne. intros Φ. f_equiv; last done.
-  apply contractive. intros n' ?. by rewrite HP1P2.
-Qed.
-
 Global Instance slice_persistent γ P : PersistentP (slice N γ P).
 Proof. apply _. Qed.
 
+Global Instance box_contractive f : Contractive (box N f).
+Proof. solve_contractive. Qed.
+Global Instance box_ne n f : Proper (dist n ==> dist n) (box N f).
+Proof. apply (contractive_ne _). Qed.
+
 Lemma box_own_auth_agree γ b1 b2 :
   box_own_auth γ (● Excl' b1) ∗ box_own_auth γ (◯ Excl' b2) ⊢ ⌜b1 = b2⌝.
 Proof.
diff --git a/base_logic/lib/fractional.v b/base_logic/lib/fractional.v
index d00d1af1ae9107dfb7608bc5ed0032c123561798..e4545fded2b7f388c6737de52a3c0ac63d676ecf 100644
--- a/base_logic/lib/fractional.v
+++ b/base_logic/lib/fractional.v
@@ -45,7 +45,7 @@ Section fractional.
     Fractional Φ → Fractional Ψ → Fractional (λ q, Φ q ∗ Ψ q)%I.
   Proof.
     intros ?? q q'. rewrite !fractional -!assoc. f_equiv.
-    rewrite !assoc. f_equiv; last done. by rewrite comm.
+    rewrite !assoc. f_equiv. by rewrite comm.
   Qed.
 
   Global Instance fractional_big_sepL {A} l Ψ :
@@ -98,7 +98,6 @@ Section fractional.
   Proof. done. Qed.
 
   (** Proof mode instances *)
-
   Global Instance from_sep_fractional_fwd P P1 P2 Φ q1 q2 :
     AsFractional P Φ (q1 + q2) → Fractional Φ →
     AsFractional P1 Φ q1 → AsFractional P2 Φ q2 →
@@ -140,12 +139,11 @@ Section fractional.
     AsFractional R Φ r → AsFractional PP' Φ (p + p') → Fractional Φ →
     Frame R (Φ p') Q → MakeSep (Φ p) Q PQ → Frame R PP' PQ.
   Proof.
-    rewrite /Frame=>->->-><-<-. rewrite !assoc. f_equiv. by rewrite comm. done.
+    rewrite /Frame=>->->-><-<-. rewrite !assoc. f_equiv. by rewrite comm.
   Qed.
   Global Instance frame_fractional_half P Q R Φ p:
     AsFractional R Φ (p/2) → AsFractional P Φ p → Fractional Φ →
     AsFractional Q Φ (p/2)%Qp →
     Frame R P Q.
   Proof. by rewrite /Frame -{2}(Qp_div_2 p)=>->->->->. Qed.
-
 End fractional.
diff --git a/base_logic/lib/wsat.v b/base_logic/lib/wsat.v
index 4489034ab5ffbb0b9124f20b85826b7390872168..c456f19f24277e028eaa912739603b7a42ab2035 100644
--- a/base_logic/lib/wsat.v
+++ b/base_logic/lib/wsat.v
@@ -44,11 +44,10 @@ Context `{invG Σ}.
 Implicit Types P : iProp Σ.
 
 (* Invariants *)
+Instance invariant_unfold_contractive : Contractive (@invariant_unfold Σ).
+Proof. solve_contractive. Qed.
 Global Instance ownI_contractive i : Contractive (@ownI Σ _ i).
-Proof.
-  intros n P Q HPQ. rewrite /ownI /invariant_unfold. do 4 f_equiv.
-  apply Next_contractive=> j ?; by rewrite (HPQ j).
-Qed.
+Proof. solve_contractive. Qed.
 Global Instance ownI_persistent i P : PersistentP (ownI i P).
 Proof. rewrite /ownI. apply _. Qed.
 
diff --git a/base_logic/primitive.v b/base_logic/primitive.v
index 033d562e57a48ed670f9544dcfa678d34d3e4581..85dfdb49ea08d8c48d3300a5a6e9090acf0caaa1 100644
--- a/base_logic/primitive.v
+++ b/base_logic/primitive.v
@@ -284,8 +284,8 @@ Proof.
 Qed.
 Global Instance later_contractive : Contractive (@uPred_later M).
 Proof.
-  intros n P Q HPQ; unseal; split=> -[|n'] x ??; simpl; [done|].
-  apply (HPQ n'); eauto using cmra_validN_S.
+  unseal; intros [|n] P Q HPQ; split=> -[|n'] x ?? //=; try omega.
+  apply HPQ; eauto using cmra_validN_S.
 Qed.
 Global Instance later_proper' :
   Proper ((⊣⊢) ==> (⊣⊢)) (@uPred_later M) := ne_proper _.
@@ -581,6 +581,15 @@ Lemma option_validI {A : cmraT} (mx : option A) :
   ✓ mx ⊣⊢ match mx with Some x => ✓ x | None => True end.
 Proof. unseal. by destruct mx. Qed.
 
+(* Contractive functions *)
+Lemma contractiveI {A B : ofeT} (f : A → B) :
+  Contractive f ↔ (∀ a b, ▷ (a ≡ b) ⊢ f a ≡ f b).
+Proof.
+  split; unseal; intros Hf.
+  - intros a b; split=> n x _; apply Hf.
+  - intros i a b; eapply Hf, ucmra_unit_validN.
+Qed.
+
 (* Functions *)
 Lemma cofe_funC_equivI {A B} (f g : A -c> B) : f ≡ g ⊣⊢ ∀ x, f x ≡ g x.
 Proof. by unseal. Qed.
diff --git a/base_logic/upred.v b/base_logic/upred.v
index f943c438818aa3a3ad761839247f08fdc74920be..ac98bdddc617447ec8de647344cce6372a077ca4 100644
--- a/base_logic/upred.v
+++ b/base_logic/upred.v
@@ -118,8 +118,8 @@ Qed.
 Instance uPredCF_contractive F :
   urFunctorContractive F → cFunctorContractive (uPredCF F).
 Proof.
-  intros ? A1 A2 B1 B2 n P Q HPQ.
-  apply uPredC_map_ne, urFunctor_contractive=> i ?; split; by apply HPQ.
+  intros ? A1 A2 B1 B2 n P Q HPQ. apply uPredC_map_ne, urFunctor_contractive.
+  destruct n; split; by apply HPQ.
 Qed.
 
 (** logical entailement *)
diff --git a/docs/constructions.tex b/docs/constructions.tex
index eb72d0c87c0467463e528f9d9580d2ac79280a50..225016c8497075b0615063d5476c3304d2642df5 100644
--- a/docs/constructions.tex
+++ b/docs/constructions.tex
@@ -141,35 +141,28 @@ $K \fpfn (-)$ is a locally non-expansive functor from $\CMRAs$ to $\CMRAs$.
 
 Given some OFE $\cofe$, we define the CMRA $\agm(\cofe)$ as follows:
 \begin{align*}
-  \agm(\cofe) \eqdef{}& \set{(c, V) \in (\nat \to \cofe) \times \SProp}/\ {\sim} \\[-0.2em]
-  \textnormal{where }& \melt \sim \meltB \eqdef{} \melt.V = \meltB.V \land 
-    \All n. n \in \melt.V \Ra \melt.c(n) \nequiv{n} \meltB.c(n)  \\
+  \agm(\cofe) \eqdef{}& \setComp{\melt \in \finpset\cofe}{c \neq \emptyset} /\ {\sim} \\[-0.2em]
+  \melt \nequiv{n} \meltB \eqdef{}& (\All x \in \melt. \Exists y \in \meltB. x \nequiv{n} y) \land (\All y \in \meltB. \Exists x \in \melt. x \nequiv{n} y) \\
+  \textnormal{where }& \melt \sim \meltB \eqdef{} \All n. \melt \nequiv{n} \meltB  \\
+~\\
 %    \All n \in {\melt.V}.\, \melt.x \nequiv{n} \meltB.x \\
-  \melt \nequiv{n} \meltB \eqdef{}& (\All m \leq n. m \in \melt.V \Lra m \in \meltB.V) \land (\All m \leq n. m \in \melt.V \Ra \melt.c(m) \nequiv{m} \meltB.c(m)) \\
-  \mval_n \eqdef{}& \setComp{\melt \in \agm(\cofe)}{ n \in \melt.V \land \All m \leq n. \melt.c(n) \nequiv{m} \melt.c(m) } \\
+  \mval_n \eqdef{}& \setComp{\melt \in \agm(\cofe)}{ \All x, y \in \melt. x \nequiv{n} y } \\
   \mcore\melt \eqdef{}& \melt \\
-  \melt \mtimes \meltB \eqdef{}& \left(\melt.c, \setComp{n}{n \in \melt.V \land n \in \meltB.V \land \melt \nequiv{n} \meltB }\right)
+  \melt \mtimes \meltB \eqdef{}& \melt \cup \meltB
 \end{align*}
 %Note that the carrier $\agm(\cofe)$ is a \emph{record} consisting of the two fields $c$ and $V$.
 
 $\agm(-)$ is a locally non-expansive functor from $\OFEs$ to $\CMRAs$.
 
-You can think of the $c$ as a \emph{chain} of elements of $\cofe$ that has to converge only for $n \in V$ steps.
-The reason we store a chain, rather than a single element, is that $\agm(\cofe)$ needs to be a COFE itself, so we need to be able to give a limit for every chain of $\agm(\cofe)$.
-However, given such a chain, we cannot constructively define its limit: Clearly, the $V$ of the limit is the limit of the $V$ of the chain.
-But what to pick for the actual data, for the element of $\cofe$?
-Only if $V = \nat$ we have a chain of $\cofe$ that we can take a limit of; if the $V$ is smaller, the chain ``cancels'', \ie stops converging as we reach indices $n \notin V$.
-To mitigate this, we apply the usual construction to close a set; we go from elements of $\cofe$ to chains of $\cofe$.
-
-We define an injection $\aginj$ into $\agm(\cofe)$ as follows:
-\[ \aginj(x) \eqdef \record{\mathrm c \eqdef \Lam \any. x, \mathrm V \eqdef \nat} \]
+We define a non-expansive injection $\aginj$ into $\agm(\cofe)$ as follows:
+\[ \aginj(x) \eqdef \set{x} \]
 There are no interesting frame-preserving updates for $\agm(\cofe)$, but we can show the following:
 \begin{mathpar}
   \axiomH{ag-val}{\aginj(x) \in \mval_n}
 
   \axiomH{ag-dup}{\aginj(x) = \aginj(x)\mtimes\aginj(x)}
   
-  \axiomH{ag-agree}{\aginj(x) \mtimes \aginj(y) \in \mval_n \Ra x \nequiv{n} y}
+  \axiomH{ag-agree}{\aginj(x) \mtimes \aginj(y) \in \mval_n \Lra x \nequiv{n} y}
 \end{mathpar}
 
 
diff --git a/prelude/gmultiset.v b/prelude/gmultiset.v
index 84c7be8ee75fb4d73d98052d155ceeccf79e0153..52a77a7aabbef2146ff90a9545a422d83ad160f9 100644
--- a/prelude/gmultiset.v
+++ b/prelude/gmultiset.v
@@ -185,8 +185,8 @@ Proof.
     rewrite !map_to_list_insert, !bind_cons
       by (by rewrite ?lookup_union_with, ?lookup_delete, ?HX).
     rewrite (assoc_L _), <-(comm (++) (f (_,n'))), <-!(assoc_L _), <-IH.
-    rewrite (assoc_L _); f_equiv; [rewrite (comm _); simpl|done].
-    by rewrite replicate_plus, Permutation_middle.
+    rewrite (assoc_L _). f_equiv.
+    rewrite (comm _); simpl. by rewrite replicate_plus, Permutation_middle.
   - rewrite <-insert_union_with_l, !map_to_list_insert, !bind_cons
       by (by rewrite ?lookup_union_with, ?HX, ?HY).
     by rewrite <-(assoc_L (++)), <-IH.
diff --git a/prelude/tactics.v b/prelude/tactics.v
index 381757576dbee9e6ba80d0a3b97307f14a225311..7ca9b524a148ede613bda213d22c21c3d99afe1f 100644
--- a/prelude/tactics.v
+++ b/prelude/tactics.v
@@ -273,6 +273,7 @@ favor the second because the relation (dist) stays the same. *)
 Ltac f_equiv :=
   match goal with
   | _ => reflexivity
+  | |- pointwise_relation _ _ _ _ => intros ?
   (* We support matches on both sides, *if* they concern the same variable, or
      variables in some relation. *)
   | |- ?R (match ?x with _ => _ end) (match ?x with _ => _ end) =>
@@ -301,26 +302,12 @@ Ltac f_equiv :=
    (* In case the function symbol differs, but the arguments are the same,
       maybe we have a pointwise_relation in our context. *)
   | H : pointwise_relation _ ?R ?f ?g |- ?R (?f ?x) (?g ?x) => apply H
-  end.
-
-(** auto_proper solves goals of the form "f _ = f _", for any relation and any
-    number of arguments, by repeatedly applying f_equiv and handling trivial cases.
-    If it cannot solve an equality, it will leave that to the user. *)
-Ltac auto_equiv :=
-  (* Deal with "pointwise_relation" *)
-  repeat lazymatch goal with
-  | |- pointwise_relation _ _ _ _ => intros ?
   end;
-  (* Normalize away equalities. *)
-  simplify_eq;
-  (* repeatedly apply congruence lemmas and use the equalities in the hypotheses. *)
-  try (f_equiv; fast_done || auto_equiv).
-
-(** solve_proper solves goals of the form "Proper (R1 ==> R2)", for any
-    number of relations. All the actual work is done by auto_equiv;
-    solve_proper just introduces the assumptions and unfolds the first
-    head symbol. *)
-Ltac solve_proper :=
+  try reflexivity.
+
+(* The tactic [preprocess_solve_proper] unfolds the first head symbol, so that
+we proceed by repeatedly using [f_equiv]. *)
+Ltac preprocess_solve_proper :=
   (* Introduce everything *)
   intros;
   repeat lazymatch goal with
@@ -340,7 +327,14 @@ Ltac solve_proper :=
   | |- ?R (?f _ _) (?f _ _) => unfold f
   | |- ?R (?f _) (?f _) => unfold f
   end;
-  solve [ auto_equiv ].
+  simplify_eq.
+
+(** The tactic [solve_proper] solves goals of the form "Proper (R1 ==> R2)", for
+any number of relations. The actual work is done by repeatedly applying
+[f_equiv]. *)
+Ltac solve_proper :=
+  preprocess_solve_proper;
+  solve [repeat (f_equiv; try eassumption)].
 
 (** The tactic [intros_revert tac] introduces all foralls/arrows, performs tac,
 and then reverts them. *)
diff --git a/program_logic/weakestpre.v b/program_logic/weakestpre.v
index 9c3070b349866ce43b1a456fe48a06d6b7a3cb8c..6999d2311a34407b6658f10c4619bc27308a31c4 100644
--- a/program_logic/weakestpre.v
+++ b/program_logic/weakestpre.v
@@ -37,11 +37,7 @@ Definition wp_pre `{irisG Λ Σ}
 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 fupd_ne, sep_ne, later_contractive; auto=> i ?.
-  apply forall_ne=> e2; apply forall_ne=> σ2; apply forall_ne=> efs.
-  apply wand_ne, fupd_ne, sep_ne, sep_ne; auto; first by apply Hwp.
-  apply big_opL_ne=> ? ef. by apply Hwp.
+  repeat (f_contractive || f_equiv); apply Hwp.
 Qed.
 
 Definition wp_def `{irisG Λ Σ} :
@@ -138,12 +134,12 @@ Global Instance wp_ne E e n :
   Proper (pointwise_relation _ (dist n) ==> dist n) (@wp Λ Σ _ E e).
 Proof.
   revert e. induction (lt_wf n) as [n _ IH]=> e Φ Ψ HΦ.
-  rewrite !wp_unfold /wp_pre. apply or_ne, and_ne; auto; first solve_proper.
-  apply forall_ne=> σ1.
-  apply wand_ne, fupd_ne, sep_ne, later_contractive; auto=> i ?.
-  apply forall_ne=> e2; apply forall_ne=> σ2; apply forall_ne=> ef.
-  apply wand_ne, fupd_ne, sep_ne, sep_ne; auto.
-  apply IH; [done|]=> v. eapply dist_le; eauto with omega.
+  rewrite !wp_unfold /wp_pre.
+  (* FIXME: figure out a way to properly automate this proof *)
+  (* FIXME: reflexivity, as being called many times by f_equiv and f_contractive
+  is very slow here *)
+  do 18 (f_contractive || f_equiv). apply IH; first lia.
+  intros v. eapply dist_le; eauto with omega.
 Qed.
 Global Instance wp_proper E e :
   Proper (pointwise_relation _ (≡) ==> (≡)) (@wp Λ Σ _ E e).