diff --git a/algebra/agree.v b/algebra/agree.v
index 236211c7db183be08ff3ac9531350a87b743460a..3e51ad085d6fa3987853548924bbf4463c2bf558 100644
--- a/algebra/agree.v
+++ b/algebra/agree.v
@@ -5,10 +5,9 @@ Local Hint Extern 10 (_ ≤ _) => omega.
 Record agree (A : Type) : Type := Agree {
   agree_car :> nat → A;
   agree_is_valid : nat → Prop;
-  agree_valid_0 : agree_is_valid 0;
   agree_valid_S n : agree_is_valid (S n) → agree_is_valid n
 }.
-Arguments Agree {_} _ _ _ _.
+Arguments Agree {_} _ _ _.
 Arguments agree_car {_} _ _.
 Arguments agree_is_valid {_} _ _.
 
@@ -27,10 +26,9 @@ Instance agree_dist : Dist (agree A) := λ n x y,
   (∀ n', n' ≤ n → agree_is_valid x n' ↔ agree_is_valid y n') ∧
   (∀ n', n' ≤ n → agree_is_valid x n' → x n' ≡{n'}≡ y n').
 Program Instance agree_compl : Compl (agree A) := λ c,
-  {| agree_car n := c n n; agree_is_valid n := agree_is_valid (c n) n |}.
-Next Obligation. intros; apply agree_valid_0. Qed.
+  {| agree_car n := c (S n) n; agree_is_valid n := agree_is_valid (c (S n)) n |}.
 Next Obligation.
-  intros c n ?; apply (chain_cauchy c n (S n)), agree_valid_S; auto.
+  intros c n ?. apply (chain_cauchy c n (S (S n))), agree_valid_S; auto.
 Qed.
 Definition agree_cofe_mixin : CofeMixin (agree A).
 Proof.
@@ -45,9 +43,8 @@ Proof.
       - transitivity (agree_is_valid y n'). by apply Hxy. by apply Hyz.
       - transitivity (y n'). by apply Hxy. by apply Hyz, Hxy.
   * intros n x y Hxy; split; intros; apply Hxy; auto.
-  * intros x y; split; intros n'; rewrite Nat.le_0_r; intros ->; [|done].
-    by split; intros; apply agree_valid_0.
-  * by intros c n; split; intros; apply (chain_cauchy c).
+  * intros c n; apply and_wlog_r; intros;
+      symmetry; apply (chain_cauchy c); naive_solver.
 Qed.
 Canonical Structure agreeC := CofeT agree_cofe_mixin.
 
@@ -59,7 +56,6 @@ Proof. by intros [? Hx]; apply Hx. Qed.
 Program Instance agree_op : Op (agree A) := λ x y,
   {| agree_car := x;
      agree_is_valid n := agree_is_valid x n ∧ agree_is_valid y n ∧ x ≡{n}≡ y |}.
-Next Obligation. by intros; simpl; split_ands; try apply agree_valid_0. Qed.
 Next Obligation. naive_solver eauto using agree_valid_S, dist_S. Qed.
 Instance agree_unit : Unit (agree A) := id.
 Instance agree_minus : Minus (agree A) := λ x y, x.
@@ -100,8 +96,6 @@ Definition agree_cmra_mixin : CMRAMixin (agree A).
 Proof.
   split; try (apply _ || done).
   * by intros n x1 x2 Hx y1 y2 Hy.
-  * intros x; split; [apply agree_valid_0|].
-    by intros n'; rewrite Nat.le_0_r; intros ->.
   * intros n x [? Hx]; split; [by apply agree_valid_S|intros n' ?].
     rewrite (Hx n'); last auto.
     symmetry; apply dist_le with n; try apply Hx; auto.
@@ -142,7 +136,7 @@ Arguments agreeRA : clear implicits.
 
 Program Definition agree_map {A B} (f : A → B) (x : agree A) : agree B :=
   {| agree_car n := f (x n); agree_is_valid := agree_is_valid x |}.
-Solve Obligations with auto using agree_valid_0, agree_valid_S.
+Solve Obligations with auto using agree_valid_S.
 Lemma agree_map_id {A} (x : agree A) : agree_map id x = x.
 Proof. by destruct x. Qed.
 Lemma agree_map_compose {A B C} (f : A → B) (g : B → C) (x : agree A) :
@@ -179,4 +173,3 @@ Qed.
 Program Definition agreeF : iFunctor :=
   {| ifunctor_car := agreeRA; ifunctor_map := @agreeC_map |}.
 Solve Obligations with done.
-
diff --git a/algebra/auth.v b/algebra/auth.v
index 515be218613b1a9b636772a6791482051eb033c7..7860affe800ebeb31f1d0e7ba83d1a359f4875d3 100644
--- a/algebra/auth.v
+++ b/algebra/auth.v
@@ -46,7 +46,6 @@ Proof.
     + by intros ?? [??]; split; symmetry.
     + intros ??? [??] [??]; split; etransitivity; eauto.
   * by intros ? [??] [??] [??]; split; apply dist_S.
-  * by split.
   * intros c n; split. apply (conv_compl (chain_map authoritative c) n).
     apply (conv_compl (chain_map own c) n).
 Qed.
@@ -71,7 +70,7 @@ Instance auth_validN : ValidN (auth A) := λ n x,
   match authoritative x with
   | Excl a => own x ≼{n} a ∧ ✓{n} a
   | ExclUnit => ✓{n} (own x)
-  | ExclBot => n = 0
+  | ExclBot => False
   end.
 Global Arguments auth_validN _ !_ /.
 Instance auth_unit : Unit (auth A) := λ x,
@@ -103,10 +102,9 @@ Proof.
   * by intros n x y1 y2 [Hy Hy']; split; simpl; rewrite ?Hy ?Hy'.
   * by intros n y1 y2 [Hy Hy']; split; simpl; rewrite ?Hy ?Hy'.
   * intros n [x a] [y b] [Hx Ha]; simpl in *;
-      destruct Hx as [[][]| | |]; intros ?; cofe_subst; auto.
+      destruct Hx; intros ?; cofe_subst; auto.
   * by intros n x1 x2 [Hx Hx'] y1 y2 [Hy Hy'];
       split; simpl; rewrite ?Hy ?Hy' ?Hx ?Hx'.
-  * by intros [[] ?]; simpl.
   * intros n [[] ?] ?; naive_solver eauto using cmra_includedN_S, cmra_validN_S.
   * by split; simpl; rewrite associative.
   * by split; simpl; rewrite commutative.
@@ -150,7 +148,7 @@ Lemma auth_both_op a b : Auth (Excl a) b ≡ ● a ⋅ ◯ b.
 Proof. by rewrite /op /auth_op /= left_id. Qed.
 
 Lemma auth_update a a' b b' :
-  (∀ n af, ✓{S n} a → a ≡{S n}≡ a' ⋅ af → b ≡{S n}≡ b' ⋅ af ∧ ✓{S n} b) →
+  (∀ n af, ✓{n} a → a ≡{n}≡ a' ⋅ af → b ≡{n}≡ b' ⋅ af ∧ ✓{n} b) →
   ● a ⋅ ◯ a' ~~> ● b ⋅ ◯ b'.
 Proof.
   move=> Hab [[?| |] bf1] n // =>-[[bf2 Ha] ?]; do 2 red; simpl in *.
@@ -216,4 +214,3 @@ Next Obligation.
   intros Σ A B C f g x. rewrite /= -auth_map_compose.
   apply auth_map_ext=>y; apply ifunctor_map_compose.
 Qed.
-
diff --git a/algebra/cmra.v b/algebra/cmra.v
index 36fb32bc9098b9b66bc77e22f2ca60c3b26895d2..36c3ff1e2bd2927424092ac0bd5ed274607a48a3 100644
--- a/algebra/cmra.v
+++ b/algebra/cmra.v
@@ -40,7 +40,6 @@ Record CMRAMixin A `{Dist A, Equiv A, Unit A, Op A, ValidN A, Minus A} := {
   mixin_cmra_validN_ne n : Proper (dist n ==> impl) (✓{n});
   mixin_cmra_minus_ne n : Proper (dist n ==> dist n ==> dist n) minus;
   (* valid *)
-  mixin_cmra_validN_0 x : ✓{0} x;
   mixin_cmra_validN_S n x : ✓{S n} x → ✓{n} x;
   (* monoid *)
   mixin_cmra_associative : Associative (≡) (⋅);
@@ -99,8 +98,6 @@ Section cmra_mixin.
   Global Instance cmra_minus_ne n :
     Proper (dist n ==> dist n ==> dist n) (@minus A _).
   Proof. apply (mixin_cmra_minus_ne _ (cmra_mixin A)). Qed.
-  Lemma cmra_validN_0 x : ✓{0} x.
-  Proof. apply (mixin_cmra_validN_0 _ (cmra_mixin A)). Qed.
   Lemma cmra_validN_S n x : ✓{S n} x → ✓{n} x.
   Proof. apply (mixin_cmra_validN_S _ (cmra_mixin A)). Qed.
   Global Instance cmra_associative : Associative (≡) (@op A _).
@@ -123,8 +120,6 @@ Section cmra_mixin.
   Proof. apply (cmra_extend_mixin A). Qed.
 End cmra_mixin.
 
-Hint Extern 0 (✓{0} _) => apply cmra_validN_0.
-
 (** * CMRAs with a global identity element *)
 (** We use the notation ∅ because for most instances (maps, sets, etc) the
 `empty' element is the global identity. *)
@@ -142,11 +137,11 @@ Class CMRAMonotone {A B : cmraT} (f : A → B) := {
 
 (** * Frame preserving updates *)
 Definition cmra_updateP {A : cmraT} (x : A) (P : A → Prop) := ∀ z n,
-  ✓{S n} (x ⋅ z) → ∃ y, P y ∧ ✓{S n} (y ⋅ z).
+  ✓{n} (x ⋅ z) → ∃ y, P y ∧ ✓{n} (y ⋅ z).
 Instance: Params (@cmra_updateP) 1.
 Infix "~~>:" := cmra_updateP (at level 70).
 Definition cmra_update {A : cmraT} (x y : A) := ∀ z n,
-  ✓{S n} (x ⋅ z) → ✓{S n} (y ⋅ z).
+  ✓{n} (x ⋅ z) → ✓{n} (y ⋅ z).
 Infix "~~>" := cmra_update (at level 70).
 Instance: Params (@cmra_update) 1.
 
@@ -251,8 +246,6 @@ Proof. intros Hyv [z ?]; cofe_subst y; eauto using cmra_validN_op_l. Qed.
 Lemma cmra_validN_included x y n : ✓{n} y → x ≼ y → ✓{n} x.
 Proof. rewrite cmra_included_includedN; eauto using cmra_validN_includedN. Qed.
 
-Lemma cmra_includedN_0 x y : x ≼{0} y.
-Proof. by exists (unit x). Qed.
 Lemma cmra_includedN_S x y n : x ≼{S n} y → x ≼{n} y.
 Proof. by intros [z Hz]; exists z; apply dist_S. Qed.
 Lemma cmra_includedN_le x y n n' : x ≼{n} y → n' ≤ n → x ≼{n'} y.
@@ -290,19 +283,19 @@ Proof.
 Qed.
 
 (** ** Timeless *)
-Lemma cmra_timeless_included_l x y : Timeless x → ✓{1} y → x ≼{1} y → x ≼ y.
+Lemma cmra_timeless_included_l x y : Timeless x → ✓{0} y → x ≼{0} y → x ≼ y.
 Proof.
   intros ?? [x' ?].
-  destruct (cmra_extend_op 1 y x x') as ([z z']&Hy&Hz&Hz'); auto; simpl in *.
+  destruct (cmra_extend_op 0 y x x') as ([z z']&Hy&Hz&Hz'); auto; simpl in *.
   by exists z'; rewrite Hy (timeless x z).
 Qed.
-Lemma cmra_timeless_included_r n x y : Timeless y → x ≼{1} y → x ≼{n} y.
+Lemma cmra_timeless_included_r n x y : Timeless y → x ≼{0} y → x ≼{n} y.
 Proof. intros ? [x' ?]. exists x'. by apply equiv_dist, (timeless y). Qed.
 Lemma cmra_op_timeless x1 x2 :
   ✓ (x1 ⋅ x2) → Timeless x1 → Timeless x2 → Timeless (x1 ⋅ x2).
 Proof.
   intros ??? z Hz.
-  destruct (cmra_extend_op 1 z x1 x2) as ([y1 y2]&Hz'&?&?); auto; simpl in *.
+  destruct (cmra_extend_op 0 z x1 x2) as ([y1 y2]&Hz'&?&?); auto; simpl in *.
   { by rewrite -?Hz. }
   by rewrite Hz' (timeless x1 y1) // (timeless x2 y2).
 Qed.
@@ -370,8 +363,6 @@ Section identity_updates.
 End identity_updates.
 End cmra.
 
-Hint Extern 0 (_ ≼{0} _) => apply cmra_includedN_0.
-
 (** * Properties about monotone functions *)
 Instance cmra_monotone_id {A : cmraT} : CMRAMonotone (@id A).
 Proof. by split. Qed.
@@ -444,22 +435,16 @@ Section discrete.
   Context {A : cofeT} `{∀ x : A, Timeless x}.
   Context `{Unit A, Op A, Valid A, Minus A} (ra : RA A).
 
-  Instance discrete_validN : ValidN A := λ n x,
-    match n with 0 => True | S n => ✓ x end.
+  Instance discrete_validN : ValidN A := λ n x, ✓ x.
   Definition discrete_cmra_mixin : CMRAMixin A.
   Proof.
-    destruct ra; split; unfold Proper, respectful, includedN;
-      repeat match goal with
-      | |- ∀ n : nat, _ => intros [|?]
-      end; try setoid_rewrite <-(timeless_S _ _ _ _); try done.
-    by intros x y ?; exists x.
+    by destruct ra; split; unfold Proper, respectful, includedN;
+      try setoid_rewrite <-(timeless_iff _ _ _ _).
   Qed.
   Definition discrete_extend_mixin : CMRAExtendMixin A.
   Proof.
-    intros [|n] x y1 y2 ??.
-    * by exists (unit x, x); rewrite /= ra_unit_l.
-    * exists (y1,y2); split_ands; auto.
-      apply (timeless _), dist_le with (S n); auto with lia.
+    intros n x y1 y2 ??; exists (y1,y2); split_ands; auto.
+    apply (timeless _), dist_le with n; auto with lia.
   Qed.
   Definition discreteRA : cmraT :=
     CMRAT (cofe_mixin A) discrete_cmra_mixin discrete_extend_mixin.
@@ -512,7 +497,6 @@ Section prod.
     * by intros n y1 y2 [Hy1 Hy2] [??]; split; rewrite /= -?Hy1 -?Hy2.
     * by intros n x1 x2 [Hx1 Hx2] y1 y2 [Hy1 Hy2];
         split; rewrite /= ?Hx1 ?Hx2 ?Hy1 ?Hy2.
-    * by split.
     * by intros n x [??]; split; apply cmra_validN_S.
     * split; simpl; apply (associative _).
     * split; simpl; apply (commutative _).
diff --git a/algebra/cofe.v b/algebra/cofe.v
index 520cda1e55e4bea5dfb91a2f0fd59f9af295bbc7..646c4d54135cecfc26eb8ebc01893add812601d9 100644
--- a/algebra/cofe.v
+++ b/algebra/cofe.v
@@ -23,7 +23,7 @@ Tactic Notation "cofe_subst" :=
 
 Record chain (A : Type) `{Dist A} := {
   chain_car :> nat → A;
-  chain_cauchy n i : n ≤ i → chain_car n ≡{n}≡ chain_car i
+  chain_cauchy n i : n < i → chain_car i ≡{n}≡ chain_car (S n)
 }.
 Arguments chain_car {_ _} _ _.
 Arguments chain_cauchy {_ _} _ _ _ _.
@@ -33,11 +33,10 @@ Record CofeMixin A `{Equiv A, Compl A} := {
   mixin_equiv_dist x y : x ≡ y ↔ ∀ n, x ≡{n}≡ y;
   mixin_dist_equivalence n : Equivalence (dist n);
   mixin_dist_S n x y : x ≡{S n}≡ y → x ≡{n}≡ y;
-  mixin_dist_0 x y : x ≡{0}≡ y;
-  mixin_conv_compl (c : chain A) n : compl c ≡{n}≡ c n
+  mixin_conv_compl (c : chain A) n : compl c ≡{n}≡ c (S n)
 }.
 Class Contractive `{Dist A, Dist B} (f : A -> B) :=
-  contractive n : Proper (dist n ==> dist (S n)) f.
+  contractive n x y : (∀ i, i < n → x ≡{i}≡ y) → f x ≡{n}≡ f y.
 
 (** Bundeled version *)
 Structure cofeT := CofeT {
@@ -66,14 +65,10 @@ Section cofe_mixin.
   Proof. apply (mixin_dist_equivalence _ (cofe_mixin A)). Qed.
   Lemma dist_S n x y : x ≡{S n}≡ y → x ≡{n}≡ y.
   Proof. apply (mixin_dist_S _ (cofe_mixin A)). Qed.
-  Lemma dist_0 x y : x ≡{0}≡ y.
-  Proof. apply (mixin_dist_0 _ (cofe_mixin A)). Qed.
-  Lemma conv_compl (c : chain A) n : compl c ≡{n}≡ c n.
+  Lemma conv_compl (c : chain A) n : compl c ≡{n}≡ c (S n).
   Proof. apply (mixin_conv_compl _ (cofe_mixin A)). Qed.
 End cofe_mixin.
 
-Hint Extern 0 (_ ≡{0}≡ _) => apply dist_0.
-
 (** General properties *)
 Section cofe.
   Context {A : cofeT}.
@@ -109,13 +104,12 @@ Section cofe.
      unfold Proper, respectful; setoid_rewrite equiv_dist.
      by intros x1 x2 Hx y1 y2 Hy n; rewrite (Hx n) (Hy n).
   Qed.
-  Lemma compl_ne (c1 c2: chain A) n : c1 n ≡{n}≡ c2 n → compl c1 ≡{n}≡ compl c2.
-  Proof. intros. by rewrite (conv_compl c1 n) (conv_compl c2 n). Qed.
-  Lemma compl_ext (c1 c2 : chain A) : (∀ i, c1 i ≡ c2 i) → compl c1 ≡ compl c2.
-  Proof. setoid_rewrite equiv_dist; naive_solver eauto using compl_ne. Qed.
+  Lemma contractive_S {B : cofeT} {f : A → B} `{!Contractive f} n x y :
+    x ≡{n}≡ y → f x ≡{S n}≡ f y.
+  Proof. eauto using contractive, dist_le with omega. Qed.
   Global Instance contractive_ne {B : cofeT} (f : A → B) `{!Contractive f} n :
     Proper (dist n ==> dist n) f | 100.
-  Proof. by intros x1 x2 ?; apply dist_S, contractive. Qed.
+  Proof. by intros x y ?; apply dist_S, contractive_S. Qed.
   Global Instance contractive_proper {B : cofeT} (f : A → B) `{!Contractive f} :
     Proper ((≡) ==> (≡)) f | 100 := _.
 End cofe.
@@ -127,20 +121,21 @@ Program Definition chain_map `{Dist A, Dist B} (f : A → B)
 Next Obligation. by intros ? A ? B f Hf c n i ?; apply Hf, chain_cauchy. Qed.
 
 (** Timeless elements *)
-Class Timeless {A : cofeT} (x : A) := timeless y : x ≡{1}≡ y → x ≡ y.
+Class Timeless {A : cofeT} (x : A) := timeless y : x ≡{0}≡ y → x ≡ y.
 Arguments timeless {_} _ {_} _ _.
-Lemma timeless_S {A : cofeT} (x y : A) n : Timeless x → x ≡ y ↔ x ≡{S n}≡ y.
+Lemma timeless_iff {A : cofeT} (x y : A) n : Timeless x → x ≡ y ↔ x ≡{n}≡ y.
 Proof.
   split; intros; [by apply equiv_dist|].
-  apply (timeless _), dist_le with (S n); auto with lia.
+  apply (timeless _), dist_le with n; auto with lia.
 Qed.
 
 (** Fixpoint *)
 Program Definition fixpoint_chain {A : cofeT} `{Inhabited A} (f : A → A)
-  `{!Contractive f} : chain A := {| chain_car i := Nat.iter i f inhabitant |}.
+  `{!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 ?; first done.
-  destruct i as [|i]; simpl; first lia; apply contractive, IH; auto with lia.
+  intros A ? f ? n. induction n as [|n IH]; intros [|i] ?; simpl; try omega.
+  * apply contractive; auto with omega.
+  * apply contractive_S, IH; auto with omega.
 Qed.
 Program Definition fixpoint {A : cofeT} `{Inhabited A} (f : A → A)
   `{!Contractive f} : A := compl (fixpoint_chain f).
@@ -149,17 +144,16 @@ Section fixpoint.
   Context {A : cofeT} `{Inhabited A} (f : A → A) `{!Contractive f}.
   Lemma fixpoint_unfold : fixpoint f ≡ f (fixpoint f).
   Proof.
-    apply equiv_dist; intros n; unfold fixpoint.
-    rewrite (conv_compl (fixpoint_chain f) n).
-    by rewrite {1}(chain_cauchy (fixpoint_chain f) n (S n)); last lia.
+    apply equiv_dist=>n; rewrite /fixpoint (conv_compl (fixpoint_chain f) n) //.
+    induction n as [|n IH]; simpl; eauto using contractive, dist_le with omega.
   Qed.
   Lemma fixpoint_ne (g : A → A) `{!Contractive g} n :
     (∀ z, f z ≡{n}≡ g z) → fixpoint f ≡{n}≡ fixpoint g.
   Proof.
-    intros Hfg; unfold fixpoint.
-    rewrite (conv_compl (fixpoint_chain f) n) (conv_compl (fixpoint_chain g) n).
-    induction n as [|n IH]; simpl in *; first done.
-    rewrite Hfg; apply contractive, IH; auto using dist_S.
+    intros Hfg. rewrite /fixpoint
+      (conv_compl (fixpoint_chain f) n) (conv_compl (fixpoint_chain g) n) /=.
+    induction n as [|n IH]; simpl in *; [by rewrite !Hfg|].
+    rewrite Hfg; apply contractive_S, IH; auto using dist_S.
   Qed.
   Lemma fixpoint_proper (g : A → A) `{!Contractive g} :
     (∀ x, f x ≡ g x) → fixpoint f ≡ fixpoint g.
@@ -188,9 +182,8 @@ Section cofe_mor.
   Program Instance cofe_mor_compl : Compl (cofeMor A B) := λ c,
     {| cofe_mor_car x := compl (fun_chain c x) |}.
   Next Obligation.
-    intros c n x y Hx.
-    rewrite (conv_compl (fun_chain c x) n) (conv_compl (fun_chain c y) n) /= Hx.
-    apply (chain_cauchy c); lia.
+    intros c n x y Hx. by rewrite (conv_compl (fun_chain c x) n)
+      (conv_compl (fun_chain c y) n) /= Hx.
   Qed.
   Definition cofe_mor_cofe_mixin : CofeMixin (cofeMor A B).
   Proof.
@@ -202,9 +195,8 @@ Section cofe_mor.
       + by intros f g ? x.
       + by intros f g h ?? x; transitivity (g x).
     * by intros n f g ? x; apply dist_S.
-    * by intros f g x.
     * intros c n x; simpl.
-      rewrite (conv_compl (fun_chain c x) n); apply (chain_cauchy c); lia.
+      by rewrite (conv_compl (fun_chain c x) n) /=.
   Qed.
   Canonical Structure cofe_mor : cofeT := CofeT cofe_mor_cofe_mixin.
 
@@ -262,7 +254,6 @@ Section product.
       rewrite !equiv_dist; naive_solver.
     * apply _.
     * by intros n [x1 y1] [x2 y2] [??]; split; apply dist_S.
-    * by split.
     * intros c n; split. apply (conv_compl (chain_map fst c) n).
       apply (conv_compl (chain_map snd c) n).
   Qed.
@@ -288,17 +279,16 @@ Proof. intros f f' Hf g g' Hg [??]; split; [apply Hf|apply Hg]. Qed.
 (** Discrete cofe *)
 Section discrete_cofe.
   Context `{Equiv A, @Equivalence A (≡)}.
-  Instance discrete_dist : Dist A := λ n x y,
-    match n with 0 => True | S n => x ≡ y end.
+  Instance discrete_dist : Dist A := λ n x y, x ≡ y.
   Instance discrete_compl : Compl A := λ c, c 1.
   Definition discrete_cofe_mixin : CofeMixin A.
   Proof.
     split.
-    * intros x y; split; [by intros ? []|intros Hn; apply (Hn 1)].
-    * intros [|n]; [done|apply _].
-    * by intros [|n].
+    * intros x y; split; [done|intros Hn; apply (Hn 0)].
+    * done.
     * done.
-    * intros c [|n]; [done|apply (chain_cauchy c 1 (S n)); lia].
+    * intros c n. rewrite /compl /discrete_compl /=.
+      symmetry; apply (chain_cauchy c 0 (S n)); omega.
   Qed.
   Definition discreteC : cofeT := CofeT discrete_cofe_mixin.
   Global Instance discrete_timeless (x : A) : Timeless (x : discreteC).
@@ -314,11 +304,11 @@ Canonical Structure natC := leibnizC nat.
 Canonical Structure boolC := leibnizC bool.
 
 (** Later *)
-Inductive later (A : Type) : Type := Later { later_car : A }.
+Inductive later (A : Type) : Type := Next { later_car : A }.
 Add Printing Constructor later.
-Arguments Later {_} _.
+Arguments Next {_} _.
 Arguments later_car {_} _.
-Lemma later_eta {A} (x : later A) : Later (later_car x) = x.
+Lemma later_eta {A} (x : later A) : Next (later_car x) = x.
 Proof. by destruct x. Qed.
 
 Section later.
@@ -329,7 +319,7 @@ Section later.
   Program Definition later_chain (c : chain (later A)) : chain A :=
     {| chain_car n := later_car (c (S n)) |}.
   Next Obligation. intros c n i ?; apply (chain_cauchy c (S n)); lia. Qed.
-  Instance later_compl : Compl (later A) := λ c, Later (compl (later_chain c)).
+  Instance later_compl : Compl (later A) := λ c, Next (compl (later_chain c)).
   Definition later_cofe_mixin : CofeMixin (later A).
   Proof.
     split.
@@ -340,20 +330,19 @@ Section later.
       + by intros [x] [y].
       + by intros [x] [y] [z] ??; transitivity y.
     * intros [|n] [x] [y] ?; [done|]; unfold dist, later_dist; by apply dist_S.
-    * done.
     * intros c [|n]; [done|by apply (conv_compl (later_chain c) n)].
   Qed.
   Canonical Structure laterC : cofeT := CofeT later_cofe_mixin.
-  Global Instance Later_contractive : Contractive (@Later A).
-  Proof. by intros n ??. Qed.
-  Global Instance Later_inj n : Injective (dist n) (dist (S n)) (@Later A).
+  Global Instance Next_contractive : Contractive (@Next A).
+  Proof. intros [|n] x y Hxy; [done|]; apply Hxy; lia. Qed.
+  Global Instance Later_inj n : Injective (dist n) (dist (S n)) (@Next A).
   Proof. by intros x y. Qed.
 End later.
 
 Arguments laterC : clear implicits.
 
 Definition later_map {A B} (f : A → B) (x : later A) : later B :=
-  Later (f (later_car x)).
+  Next (f (later_car x)).
 Instance later_map_ne {A B : cofeT} (f : A → B) n :
   Proper (dist (pred n) ==> dist (pred n)) f →
   Proper (dist n ==> dist n) (later_map f) | 0.
@@ -366,4 +355,4 @@ Proof. by destruct x. Qed.
 Definition laterC_map {A B} (f : A -n> B) : laterC A -n> laterC B :=
   CofeMor (later_map f).
 Instance laterC_map_contractive (A B : cofeT) : Contractive (@laterC_map A B).
-Proof. intros n f g Hf n'; apply Hf. Qed.
+Proof. intros [|n] f g Hf n'; [done|]; apply Hf; lia. Qed.
diff --git a/algebra/cofe_solver.v b/algebra/cofe_solver.v
index f03becc088305c661782379f279cc253fcca89f7..1a56cc65e1ef7d2ba43e21fe4d8bab221dc17bbf 100644
--- a/algebra/cofe_solver.v
+++ b/algebra/cofe_solver.v
@@ -28,33 +28,44 @@ Lemma map_ext {A1 A2 B1 B2 : cofeT}
   (∀ x, f x ≡ f' x) → (∀ y, g y ≡ g' y) → x ≡ x' →
   map (f,g) x ≡ map (f',g') x'.
 Proof. by rewrite -!cofe_mor_ext; intros -> -> ->. Qed.
+Lemma map_ne {A1 A2 B1 B2 : cofeT}
+  (f : A2 -n> A1) (f' : A2 -n> A1) (g : B1 -n> B2) (g' : B1 -n> B2) n x :
+  (∀ x, f x ≡{n}≡ f' x) → (∀ y, g y ≡{n}≡ g' y) →
+  map (f,g) x ≡{n}≡ map (f',g') x.
+Proof.
+  intros. by apply map_contractive=> i ?; apply dist_le with n; last lia.
+Qed.
 
 Fixpoint A (k : nat) : cofeT :=
   match k with 0 => unitC | S k => F (A k) (A k) end.
-Fixpoint f {k} : A k -n> A (S k) :=
-  match k with 0 => CofeMor (λ _, inhabitant) | S k => map (g,f) end
-with g {k} : A (S k) -n> A k :=
-  match k with 0 => CofeMor (λ _, ()) | S k => map (f,g) end.
-Definition f_S k (x : A (S k)) : f x = map (g,f) x := eq_refl.
-Definition g_S k (x : A (S (S k))) : g x = map (f,g) x := eq_refl.
-Lemma gf {k} (x : A k) : g (f x) ≡ x.
+Fixpoint f (k : nat) : A k -n> A (S k) :=
+  match k with 0 => CofeMor (λ _, inhabitant) | S k => map (g k,f k) end
+with g (k : nat) : A (S k) -n> A k :=
+  match k with 0 => CofeMor (λ _, ()) | S k => map (f k,g k) end.
+Definition f_S k (x : A (S k)) : f (S k) x = map (g k,f k) x := eq_refl.
+Definition g_S k (x : A (S (S k))) : g (S k) x = map (f k,g k) x := eq_refl.
+Arguments A : simpl never.
+Arguments f : simpl never.
+Arguments g : simpl never.
+
+Lemma gf {k} (x : A k) : g k (f k x) ≡ x.
 Proof.
   induction k as [|k IH]; simpl in *; [by destruct x|].
   rewrite -map_comp -{2}(map_id _ _ x); by apply map_ext.
 Qed.
-Lemma fg {n k} (x : A (S k)) : n ≤ k → f (g x) ≡{n}≡ x.
+Lemma fg {k} (x : A (S (S k))) : f (S k) (g (S k) x) ≡{k}≡ x.
 Proof.
-  intros Hnk; apply dist_le with k; auto; clear Hnk.
-  induction k as [|k IH]; simpl; [apply dist_0|].
-  rewrite -{2}(map_id _ _ x) -map_comp; by apply map_contractive.
+  induction k as [|k IH]; simpl.
+  * rewrite f_S g_S -{2}(map_id _ _ x) -map_comp.
+    apply map_contractive=> i ?; omega.
+  * rewrite f_S g_S -{2}(map_id _ _ x) -map_comp.
+    apply map_contractive=> i ?; apply dist_le with k; [|omega].
+    split=> x' /=; apply IH.
 Qed.
-Arguments A _ : simpl never.
-Arguments f {_} : simpl never.
-Arguments g {_} : simpl never.
 
 Record tower := {
   tower_car k :> A k;
-  g_tower k : g (tower_car (S k)) ≡ tower_car k
+  g_tower k : g k (tower_car (S k)) ≡ tower_car k
 }.
 Instance tower_equiv : Equiv tower := λ X Y, ∀ k, X k ≡ Y k.
 Instance tower_dist : Dist tower := λ n X Y, ∀ k, X k ≡{n}≡ Y k.
@@ -64,9 +75,9 @@ Next Obligation. intros c k n i ?; apply (chain_cauchy c n); lia. Qed.
 Program Instance tower_compl : Compl tower := λ c,
   {| tower_car n := compl (tower_chain c n) |}.
 Next Obligation.
-  intros c k; apply equiv_dist; intros n.
-  rewrite (conv_compl (tower_chain c k) n).
-  by rewrite (conv_compl (tower_chain c (S k)) n) /= (g_tower (c n) k).
+  intros c k; apply equiv_dist=> n.
+  by rewrite (conv_compl (tower_chain c k) n)
+    (conv_compl (tower_chain c (S k)) n) /= (g_tower (c (S n)) k).
 Qed.
 Definition tower_cofe_mixin : CofeMixin tower.
 Proof.
@@ -79,24 +90,23 @@ Proof.
     + by intros X Y Z ?? n; transitivity (Y n).
   * intros k X Y HXY n; apply dist_S.
     by rewrite -(g_tower X) (HXY (S n)) g_tower.
-  * intros X Y k; apply dist_0.
   * intros c n k; rewrite /= (conv_compl (tower_chain c k) n).
     apply (chain_cauchy c); lia.
 Qed.
 Definition T : cofeT := CofeT tower_cofe_mixin.
 
 Fixpoint ff {k} (i : nat) : A k -n> A (i + k) :=
-  match i with 0 => cid | S i => f â—Ž ff i end.
+  match i with 0 => cid | S i => f (i + k) â—Ž ff i end.
 Fixpoint gg {k} (i : nat) : A (i + k) -n> A k :=
-  match i with 0 => cid | S i => gg i â—Ž g end.
+  match i with 0 => cid | S i => gg i â—Ž g (i + k) end.
 Lemma ggff {k i} (x : A k) : gg i (ff i x) ≡ x.
 Proof. induction i as [|i IH]; simpl; [done|by rewrite (gf (ff i x)) IH]. Qed.
-Lemma f_tower {n k} (X : tower) : n ≤ k → f (X k) ≡{n}≡ X (S k).
-Proof. intros. by rewrite -(fg (X (S k))) // -(g_tower X). Qed.
-Lemma ff_tower {n} k i (X : tower) : n ≤ k → ff i (X k) ≡{n}≡ X (i + k).
+Lemma f_tower k (X : tower) : f (S k) (X (S k)) ≡{k}≡ X (S (S k)).
+Proof. intros. by rewrite -(fg (X (S (S k)))) -(g_tower X). Qed.
+Lemma ff_tower k i (X : tower) : ff i (X (S k)) ≡{k}≡ X (i + S k).
 Proof.
   intros; induction i as [|i IH]; simpl; [done|].
-  by rewrite IH (f_tower X); last lia.
+  by rewrite IH Nat.add_succ_r (dist_le _ _ _ _ (f_tower _ X)); last omega.
 Qed.
 Lemma gg_tower k i (X : tower) : gg i (X (i + k)) ≡ X k.
 Proof. by induction i as [|i IH]; simpl; [done|rewrite g_tower IH]. Qed.
@@ -113,10 +123,10 @@ Lemma coerce_proper {i j} (x y : A i) (H1 H2 : i = j) :
   x = y → coerce H1 x = coerce H2 y.
 Proof. by destruct H1; rewrite !coerce_id. Qed.
 Lemma g_coerce {k j} (H : S k = S j) (x : A (S k)) :
-  g (coerce H x) = coerce (Nat.succ_inj _ _ H) (g x).
+  g j (coerce H x) = coerce (Nat.succ_inj _ _ H) (g k x).
 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 x) = f (coerce (Nat.succ_inj _ _ H) x).
+  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) :
   gg i (coerce H1 x) = gg i1 (gg i2 (coerce H2 x)).
@@ -133,14 +143,15 @@ Proof.
     [by rewrite coerce_id|by rewrite coerce_f IH].
 Qed.
 
-Definition embed' {k} (i : nat) : A k -n> A i :=
+Definition embed_coerce {k} (i : nat) : A k -n> A i :=
   match le_lt_dec i k with
   | left H => gg (k-i) â—Ž coerce (eq_sym (Nat.sub_add _ _ H))
   | right H => coerce (Nat.sub_add k i (Nat.lt_le_incl _ _ H)) â—Ž ff (i-k)
   end.
-Lemma g_embed' {k i} (x : A k) : g (embed' (S i) x) ≡ embed' i x.
+Lemma g_embed_coerce {k i} (x : A k) :
+  g i (embed_coerce (S i) x) ≡ embed_coerce i x.
 Proof.
-  unfold embed'; destruct (le_lt_dec (S i) k), (le_lt_dec i k); simpl.
+  unfold embed_coerce; destruct (le_lt_dec (S i) k), (le_lt_dec i k); simpl.
   * symmetry; by erewrite (@gg_gg _ _ 1 (k - S i)); simpl.
   * exfalso; lia.
   * assert (i = k) by lia; subst.
@@ -150,16 +161,16 @@ Proof.
     rewrite (ff_ff _ H) /= -{2}(gf (ff (i - k) x)) g_coerce.
     by erewrite coerce_proper by done.
 Qed.
-Program Definition embed_inf (k : nat) (x : A k) : T :=
-  {| tower_car n := embed' n x |}.
-Next Obligation. intros k x i. apply g_embed'. Qed.
-Instance embed_inf_ne k n : Proper (dist n ==> dist n) (embed_inf k).
+Program Definition embed (k : nat) (x : A k) : T :=
+  {| tower_car n := embed_coerce n x |}.
+Next Obligation. intros k x i. apply g_embed_coerce. Qed.
+Instance: Params (@embed) 1.
+Instance embed_ne k n : Proper (dist n ==> dist n) (embed k).
 Proof. by intros x y Hxy i; rewrite /= Hxy. Qed.
-Definition embed (k : nat) : A k -n> T := CofeMor (embed_inf k).
-Lemma embed_f k (x : A k) : embed (S k) (f x) ≡ embed k x.
+Definition embed' (k : nat) : A k -n> T := CofeMor (embed k).
+Lemma embed_f k (x : A k) : embed (S k) (f k x) ≡ embed k x.
 Proof.
-  rewrite equiv_dist; intros n i.
-  unfold embed_inf, embed; simpl; unfold embed'.
+  rewrite equiv_dist=> n i; rewrite /embed /= /embed_coerce.
   destruct (le_lt_dec i (S k)), (le_lt_dec i k); simpl.
   * assert (H : S k = S (k - i) + (0 + i)) by lia; rewrite (gg_gg _ H) /=.
     by erewrite g_coerce, gf, coerce_proper by done.
@@ -170,33 +181,39 @@ Proof.
   * assert (H : (i - S k) + (1 + k) = i) by lia; rewrite (ff_ff _ H) /=.
     by erewrite coerce_proper by done.
 Qed.
-Lemma embed_tower j n (X : T) : n ≤ j → embed j (X j) ≡{n}≡ X.
+Lemma embed_tower k (X : T) : embed (S k) (X (S k)) ≡{k}≡ X.
 Proof.
-  move=> Hn i; rewrite /= /embed'; destruct (le_lt_dec i j) as [H|H]; simpl.
-  * rewrite -(gg_tower i (j - i) X).
+  intros i; rewrite /= /embed_coerce.
+  destruct (le_lt_dec i (S k)) as [H|H]; simpl.
+  * rewrite -(gg_tower i (S k - i) X).
     apply (_ : Proper (_ ==> _) (gg _)); by destruct (eq_sym _).
-  * rewrite (ff_tower j (i-j) X); last lia. by destruct (Nat.sub_add _ _ _).
+  * rewrite (ff_tower k (i - S k) X). by destruct (Nat.sub_add _ _ _).
 Qed.
 
 Program Definition unfold_chain (X : T) : chain (F T T) :=
-  {| chain_car n := map (project n,embed n) (f (X n)) |}.
+  {| chain_car n := map (project n,embed' n) (X (S n)) |}.
 Next Obligation.
   intros X n i Hi.
   assert (∃ k, i = k + n) as [k ?] by (exists (i - n); lia); subst; clear Hi.
-  induction k as [|k Hk]; simpl; [done|].
-  rewrite Hk (f_tower X); last lia; rewrite f_S -map_comp.
-  apply dist_S, map_contractive.
-  split; intros Y; symmetry; apply equiv_dist; [apply g_tower|apply embed_f].
+  induction k as [|k IH]; simpl.
+  { rewrite -f_tower f_S -map_comp.
+    apply map_ne=> Y /=. by rewrite g_tower. by rewrite embed_f. }
+  rewrite -IH -(dist_le _ _ _ _ (f_tower (k + n) _)); last lia.
+  rewrite f_S -map_comp.
+  apply map_ne=> Y /=. by rewrite g_tower. by rewrite embed_f.
 Qed.
 Definition unfold (X : T) : F T T := compl (unfold_chain X).
 Instance unfold_ne : Proper (dist n ==> dist n) unfold.
-Proof. by intros n X Y HXY; apply compl_ne; rewrite /= (HXY n). Qed.
+Proof.
+  intros n X Y HXY. by rewrite /unfold (conv_compl (unfold_chain X) n)
+    (conv_compl (unfold_chain Y) n) /= (HXY (S (S n))).
+Qed.
 
 Program Definition fold (X : F T T) : T :=
-  {| tower_car n := g (map (embed n,project n) X) |}.
+  {| tower_car n := g n (map (embed' n,project n) X) |}.
 Next Obligation.
-  intros X k; apply (_ : Proper ((≡) ==> (≡)) g).
-  rewrite -(map_comp _ _ _ _ _ _ (embed (S k)) f (project (S k)) g).
+  intros X k. apply (_ : Proper ((≡) ==> (≡)) (g k)).
+  rewrite g_S -map_comp.
   apply map_ext; [apply embed_f|intros Y; apply g_tower|done].
 Qed.
 Instance fold_ne : Proper (dist n ==> dist n) fold.
@@ -205,30 +222,33 @@ Proof. by intros n X Y HXY k; rewrite /fold /= HXY. Qed.
 Theorem result : solution F.
 Proof.
   apply (Solution F T (CofeMor unfold) (CofeMor fold)).
-  * move=> X.
-    assert (map_ff_gg : ∀ i k (x : A (S i + k)) (H : S i + k = i + S k),
-      map (ff i, gg i) x ≡ gg i (coerce H x)).
-    { intros i; induction i as [|i IH]; intros k x H; simpl.
-      { by rewrite coerce_id map_id. }
-      rewrite map_comp g_coerce; apply IH. }
+  * move=> X /=.
     rewrite equiv_dist; intros n k; unfold unfold, fold; simpl.
-    rewrite -g_tower -(gg_tower _ n); apply (_ : Proper (_ ==> _) g).
+    rewrite -g_tower -(gg_tower _ n); apply (_ : Proper (_ ==> _) (g _)).
     transitivity (map (ff n, gg n) (X (S (n + k)))).
     { rewrite /unfold (conv_compl (unfold_chain X) n).
-      rewrite (chain_cauchy (unfold_chain X) n (n + k)) /=; last lia.
-      rewrite (f_tower X); last lia; rewrite -map_comp.
-      apply dist_S. apply map_contractive; split; intros x; simpl; unfold embed'.
-      * destruct (le_lt_dec _ _); simpl.
-        { assert (n = 0) by lia; subst. apply dist_0. }
-        by rewrite (ff_ff _ (eq_refl (n + (0 + k)))).
-      * destruct (le_lt_dec _ _); [|exfalso; lia]; simpl.
-        by rewrite (gg_gg _ (eq_refl (0 + (n + k)))). }
-    assert (H: S n + k = n + S k) by lia; rewrite (map_ff_gg _ _ _ H).
+      rewrite -(chain_cauchy (unfold_chain X) n (S (n + k))) /=; last lia.
+      rewrite -(dist_le _ _ _ _ (f_tower (n + k) _)); last lia.
+      rewrite f_S -!map_comp; apply map_ne; fold A=> Y.
+      + rewrite /embed' /= /embed_coerce.
+        destruct (le_lt_dec _ _); simpl; [exfalso; lia|].
+        by rewrite (ff_ff _ (eq_refl (S n + (0 + k)))) /= gf.
+      + rewrite /embed' /= /embed_coerce.
+        destruct (le_lt_dec _ _); simpl; [|exfalso; lia].
+        by rewrite (gg_gg _ (eq_refl (0 + (S n + k)))) /= gf. }
+    assert (∀ i k (x : A (S i + k)) (H : S i + k = i + S k),
+      map (ff i, gg i) x ≡ gg i (coerce H x)) as map_ff_gg.
+    { intros i; induction i as [|i IH]; intros k' x H; simpl.
+      { by rewrite coerce_id map_id. }
+      rewrite map_comp g_coerce; apply IH. }
+    assert (H: S n + k = n + S k) by lia.
+    rewrite (map_ff_gg _ _ _ H).
     apply (_ : Proper (_ ==> _) (gg _)); by destruct H.
-  * move=>X; rewrite equiv_dist=> n.
-    rewrite /(unfold) /= /(unfold) (conv_compl (unfold_chain (fold X)) n) /=.
-    rewrite (fg (map (embed _,project n) X)); last lia.
-    rewrite -map_comp -{2}(map_id _ _ X).
-    apply dist_S, map_contractive; split; intros Y i; apply embed_tower; lia.
+  * intros X; rewrite equiv_dist=> n /=.
+    rewrite /unfold /= (conv_compl (unfold_chain (fold X)) n) /=.
+    rewrite g_S -!map_comp -{2}(map_id _ _ X); apply map_ne=> Y /=.
+    + apply dist_le with n; last omega.
+      rewrite f_tower. apply dist_S. by rewrite embed_tower.
+    + etransitivity; [apply embed_ne, equiv_dist, g_tower|apply embed_tower].
 Qed.
 End solver. End solver.
diff --git a/algebra/excl.v b/algebra/excl.v
index cc0a05498b7df1dd33ca41942907f2d59a68c9f3..83f4c3039d74cf8298d3181a469af62bec945fee 100644
--- a/algebra/excl.v
+++ b/algebra/excl.v
@@ -23,7 +23,6 @@ Inductive excl_equiv : Equiv (excl A) :=
   | ExclBot_equiv : ExclBot ≡ ExclBot.
 Existing Instance excl_equiv.
 Inductive excl_dist `{Dist A} : Dist (excl A) :=
-  | excl_dist_0 (x y : excl A) : x ≡{0}≡ y
   | Excl_dist (x y : A) n : x ≡{n}≡ y → Excl x ≡{n}≡ Excl y
   | ExclUnit_dist n : ExclUnit ≡{n}≡ ExclUnit
   | ExclBot_dist n : ExclBot ≡{n}≡ ExclBot.
@@ -40,11 +39,9 @@ Program Definition excl_chain
     (c : chain (excl A)) (x : A) (H : maybe Excl (c 1) = Some x) : chain A :=
   {| chain_car n := match c n return _ with Excl y => y | _ => x end |}.
 Next Obligation.
-  intros c x ? n i ?; simpl; destruct (c 1) eqn:?; simplify_equality'.
-  destruct (decide (i = 0)) as [->|].
-  { by replace n with 0 by lia. }
-  feed inversion (chain_cauchy c 1 i); auto with lia congruence.
-  feed inversion (chain_cauchy c n i); simpl; auto with lia congruence.
+  intros c x ? n [|i] ?; [omega|]; simpl.
+  destruct (c 1) eqn:?; simplify_equality'.
+  by feed inversion (chain_cauchy c n (S i)).
 Qed.
 Instance excl_compl : Compl (excl A) := λ c,
   match Some_dec (maybe Excl (c 1)) with
@@ -61,17 +58,15 @@ Proof.
     + by destruct 1; constructor.
     + destruct 1; inversion_clear 1; constructor; etransitivity; eauto.
   * by inversion_clear 1; constructor; apply dist_S.
-  * constructor.
   * intros c n; unfold compl, excl_compl.
-    destruct (decide (n = 0)) as [->|]; [constructor|].
     destruct (Some_dec (maybe Excl (c 1))) as [[x Hx]|].
     { assert (c 1 = Excl x) by (by destruct (c 1); simplify_equality').
-      assert (∃ y, c n = Excl y) as [y Hy].
-      { feed inversion (chain_cauchy c 1 n); try congruence; eauto with lia. }
+      assert (∃ y, c (S n) = Excl y) as [y Hy].
+      { feed inversion (chain_cauchy c 0 (S n)); eauto with lia congruence. }
       rewrite Hy; constructor.
-      by rewrite (conv_compl (excl_chain c x Hx) n); simpl; rewrite Hy. }
-    feed inversion (chain_cauchy c 1 n); auto with lia; constructor.
-    destruct (c 1); simplify_equality'.
+      by rewrite (conv_compl (excl_chain c x Hx) n) /= Hy. }
+    feed inversion (chain_cauchy c 0 (S n)); first lia;
+       constructor; destruct (c 1); simplify_equality'.
 Qed.
 Canonical Structure exclC : cofeT := CofeT excl_cofe_mixin.
 
@@ -89,7 +84,7 @@ Proof. by destruct 2; f_equal; apply leibniz_equiv. Qed.
 
 (* CMRA *)
 Instance excl_validN : ValidN (excl A) := λ n x,
-  match x with Excl _ | ExclUnit => True | ExclBot => n = 0 end.
+  match x with Excl _ | ExclUnit => True | ExclBot => False end.
 Global Instance excl_empty : Empty (excl A) := ExclUnit.
 Instance excl_unit : Unit (excl A) := λ _, ∅.
 Instance excl_op : Op (excl A) := λ x y,
@@ -109,9 +104,8 @@ Proof.
   split.
   * by intros n []; destruct 1; constructor.
   * constructor.
-  * by destruct 1 as [? []| | |]; intros ?.
+  * by destruct 1; intros ?.
   * by destruct 1; inversion_clear 1; constructor.
-  * by intros [].
   * intros n [?| |]; simpl; auto with lia.
   * by intros [?| |] [?| |] [?| |]; constructor.
   * by intros [?| |] [?| |]; constructor.
@@ -123,7 +117,7 @@ Proof.
 Qed.
 Definition excl_cmra_extend_mixin : CMRAExtendMixin (excl A).
 Proof.
-  intros [|n] x y1 y2 ? Hx; [by exists (x,∅); destruct x|].
+  intros n x y1 y2 ? Hx.
   by exists match y1, y2 with
     | Excl a1, Excl a2 => (Excl a1, Excl a2)
     | ExclBot, _ => (ExclBot, y2) | _, ExclBot => (y1, ExclBot)
@@ -134,13 +128,13 @@ Canonical Structure exclRA : cmraT :=
   CMRAT excl_cofe_mixin excl_cmra_mixin excl_cmra_extend_mixin.
 Global Instance excl_cmra_identity : CMRAIdentity exclRA.
 Proof. split. done. by intros []. apply _. Qed.
-Lemma excl_validN_inv_l n x y : ✓{S n} (Excl x ⋅ y) → y = ∅.
+Lemma excl_validN_inv_l n x y : ✓{n} (Excl x ⋅ y) → y = ∅.
 Proof. by destruct y. Qed.
-Lemma excl_validN_inv_r n x y : ✓{S n} (x ⋅ Excl y) → x = ∅.
+Lemma excl_validN_inv_r n x y : ✓{n} (x ⋅ Excl y) → x = ∅.
 Proof. by destruct x. Qed.
 Lemma Excl_includedN n x y : ✓{n} y → Excl x ≼{n} y ↔ y ≡{n}≡ Excl x.
 Proof.
-  intros Hvalid; split; [destruct n as [|n]; [done|]|by intros ->].
+  intros Hvalid; split; [|by intros ->].
   by intros [z ?]; cofe_subst; rewrite (excl_validN_inv_l n x z).
 Qed.
 
@@ -187,4 +181,3 @@ Program Definition exclF : iFunctor :=
   {| ifunctor_car := exclRA; ifunctor_map := @exclC_map |}.
 Next Obligation. by intros A x; rewrite /= excl_map_id. Qed.
 Next Obligation. by intros A B C f g x; rewrite /= excl_map_compose. Qed.
-
diff --git a/algebra/fin_maps.v b/algebra/fin_maps.v
index cf96830870a95eb07d172032ea26b638749f926c..2b6cb4c1cea67438b9475cc524f464de2ab66429 100644
--- a/algebra/fin_maps.v
+++ b/algebra/fin_maps.v
@@ -23,11 +23,9 @@ Proof.
     + by intros m1 m2 ? k.
     + by intros m1 m2 m3 ?? k; transitivity (m2 !! k).
   * by intros n m1 m2 ? k; apply dist_S.
-  * by intros m1 m2 k.
-  * intros c n k; unfold compl, map_compl; rewrite lookup_imap.
-    destruct (decide (n = 0)) as [->|]; [constructor|].
-    feed inversion (λ H, chain_cauchy c 1 n H k); simpl; auto with lia.
-    by rewrite conv_compl; simpl; apply reflexive_eq.
+  * intros c n k; rewrite /compl /map_compl lookup_imap.
+    feed inversion (λ H, chain_cauchy c 0 (S n) H k); simpl; auto with lia.
+    by rewrite conv_compl /=; apply reflexive_eq.
 Qed.
 Canonical Structure mapC : cofeT := CofeT map_cofe_mixin.
 
@@ -60,7 +58,7 @@ Qed.
 Global Instance map_lookup_timeless m i : Timeless m → Timeless (m !! i).
 Proof.
   intros ? [x|] Hx; [|by symmetry; apply (timeless _)].
-  assert (m ≡{1}≡ <[i:=x]> m)
+  assert (m ≡{0}≡ <[i:=x]> m)
     by (by symmetry in Hx; inversion Hx; cofe_subst; rewrite insert_id).
   by rewrite (timeless m (<[i:=x]>m)) // lookup_insert.
 Qed.
@@ -116,7 +114,6 @@ Proof.
   * by intros n m1 m2 Hm i; rewrite !lookup_unit (Hm i).
   * by intros n m1 m2 Hm ? i; rewrite -(Hm i).
   * by intros n m1 m1' Hm1 m2 m2' Hm2 i; rewrite !lookup_minus (Hm1 i) (Hm2 i).
-  * by intros m i.
   * intros n m Hm i; apply cmra_validN_S, Hm.
   * by intros m1 m2 m3 i; rewrite !lookup_op associative.
   * by intros m1 m2 i; rewrite !lookup_op commutative.
diff --git a/algebra/iprod.v b/algebra/iprod.v
index c10b0f7828ba3bdfd93ee60b2923aab12cf354da..5d0da6da5e1e7da28a5b683a547250b6412222ab 100644
--- a/algebra/iprod.v
+++ b/algebra/iprod.v
@@ -37,7 +37,6 @@ Section iprod_cofe.
       + by intros f g ? x.
       + by intros f g h ?? x; transitivity (g x).
     * intros n f g Hfg x; apply dist_S, Hfg.
-    * by intros f g x.
     * intros c n x.
       rewrite /compl /iprod_compl (conv_compl (iprod_chain c x) n).
       apply (chain_cauchy c); lia.
@@ -141,7 +140,6 @@ Section iprod_cmra.
     * by intros n f1 f2 Hf x; rewrite iprod_lookup_unit (Hf x).
     * by intros n f1 f2 Hf ? x; rewrite -(Hf x).
     * by intros n f f' Hf g g' Hg i; rewrite iprod_lookup_minus (Hf i) (Hg i).
-    * by intros f x.
     * intros n f Hf x; apply cmra_validN_S, Hf.
     * by intros f1 f2 f3 x; rewrite iprod_lookup_op associative.
     * by intros f1 f2 x; rewrite iprod_lookup_op commutative.
diff --git a/algebra/option.v b/algebra/option.v
index ec1acec1bb28d4024ad01c1ac5d6d846b426b8e7..2339aa2c7c6892580536c74ddad06f3588642817 100644
--- a/algebra/option.v
+++ b/algebra/option.v
@@ -5,7 +5,6 @@ Require Import algebra.functor.
 Section cofe.
 Context {A : cofeT}.
 Inductive option_dist : Dist (option A) :=
-  | option_0_dist (x y : option A) : x ≡{0}≡ y
   | Some_dist n x y : x ≡{n}≡ y → Some x ≡{n}≡ Some y
   | None_dist n : None ≡{n}≡ None.
 Existing Instance option_dist.
@@ -13,10 +12,9 @@ Program Definition option_chain
     (c : chain (option A)) (x : A) (H : c 1 = Some x) : chain A :=
   {| chain_car n := from_option x (c n) |}.
 Next Obligation.
-  intros c x ? n i ?; simpl; destruct (decide (i = 0)) as [->|].
-  { by replace n with 0 by lia. }
-  feed inversion (chain_cauchy c 1 i); auto with lia congruence.
-  feed inversion (chain_cauchy c n i); simpl; auto with lia congruence.
+  intros c x ? n [|i] ?; [omega|]; simpl.
+  destruct (c 1) eqn:?; simplify_equality'.
+  by feed inversion (chain_cauchy c n (S i)).
 Qed.
 Instance option_compl : Compl (option A) := λ c,
   match Some_dec (c 1) with
@@ -33,20 +31,19 @@ Proof.
     + by destruct 1; constructor.
     + destruct 1; inversion_clear 1; constructor; etransitivity; eauto.
   * by inversion_clear 1; constructor; apply dist_S.
-  * constructor.
   * intros c n; unfold compl, option_compl.
-    destruct (decide (n = 0)) as [->|]; [constructor|].
     destruct (Some_dec (c 1)) as [[x Hx]|].
-    { assert (is_Some (c n)) as [y Hy].
-      { feed inversion (chain_cauchy c 1 n); try congruence; eauto with lia. }
+    { assert (is_Some (c (S n))) as [y Hy].
+      { feed inversion (chain_cauchy c 0 (S n)); eauto with lia congruence. }
       rewrite Hy; constructor.
-      by rewrite (conv_compl (option_chain c x Hx) n); simpl; rewrite Hy. }
-    feed inversion (chain_cauchy c 1 n); auto with lia congruence; constructor.
+      by rewrite (conv_compl (option_chain c x Hx) n) /= Hy. }
+    feed inversion (chain_cauchy c 0 (S n)); eauto with lia congruence.
+    constructor.
 Qed.
 Canonical Structure optionC := CofeT option_cofe_mixin.
 Global Instance Some_ne : Proper (dist n ==> dist n) (@Some A).
 Proof. by constructor. Qed.
-Global Instance is_Some_ne n : Proper (dist (S n) ==> iff) (@is_Some A).
+Global Instance is_Some_ne n : Proper (dist n ==> iff) (@is_Some A).
 Proof. inversion_clear 1; split; eauto. Qed.
 Global Instance Some_dist_inj : Injective (dist n) (dist n) (@Some A).
 Proof. by inversion_clear 1. Qed.
@@ -70,16 +67,15 @@ Instance option_op : Op (option A) := union_with (λ x y, Some (x ⋅ y)).
 Instance option_minus : Minus (option A) :=
   difference_with (λ x y, Some (x ⩪ y)).
 Lemma option_includedN n (mx my : option A) :
-  mx ≼{n} my ↔ n = 0 ∨ mx = None ∨ ∃ x y, mx = Some x ∧ my = Some y ∧ x ≼{n} y.
+  mx ≼{n} my ↔ mx = None ∨ ∃ x y, mx = Some x ∧ my = Some y ∧ x ≼{n} y.
 Proof.
   split.
-  * intros [mz Hmz]; destruct n as [|n]; [by left|right].
+  * intros [mz Hmz].
     destruct mx as [x|]; [right|by left].
     destruct my as [y|]; [exists x, y|destruct mz; inversion_clear Hmz].
     destruct mz as [z|]; inversion_clear Hmz; split_ands; auto;
       cofe_subst; eauto using cmra_includedN_l.
-  * intros [->|[->|(x&y&->&->&z&Hz)]];
-      try (by exists my; destruct my; constructor).
+  * intros [->|(x&y&->&->&z&Hz)]; try (by exists my; destruct my; constructor).
     by exists (Some z); constructor.
 Qed.
 Lemma None_includedN n (mx : option A) : None ≼{n} mx.
@@ -93,29 +89,26 @@ Proof.
   * by intros n [x|]; destruct 1; constructor;
       repeat apply (_ : Proper (dist _ ==> _ ==> _) _).
   * by destruct 1; constructor; apply (_ : Proper (dist n ==> _) _).
-  * destruct 1 as [[?|] [?|]| |]; unfold validN, option_validN; simpl;
-     intros ?; auto using cmra_validN_0;
-     eapply (_ : Proper (dist _ ==> impl) (✓{_})); eauto.
+  * destruct 1; rewrite /validN /option_validN //=.
+    eapply (_ : Proper (dist _ ==> impl) (✓{_})); eauto.
   * by destruct 1; inversion_clear 1; constructor;
       repeat apply (_ : Proper (dist _ ==> _ ==> _) _).
-  * intros [x|]; unfold validN, option_validN; auto using cmra_validN_0.
   * intros n [x|]; unfold validN, option_validN; eauto using cmra_validN_S.
   * intros [x|] [y|] [z|]; constructor; rewrite ?associative; auto.
   * intros [x|] [y|]; constructor; rewrite 1?commutative; auto.
   * by intros [x|]; constructor; rewrite cmra_unit_l.
   * by intros [x|]; constructor; rewrite cmra_unit_idempotent.
-  * intros n mx my; rewrite !option_includedN;intros [|[->|(x&y&->&->&?)]];auto.
-    do 2 right; exists (unit x), (unit y); eauto using cmra_unit_preservingN.
+  * intros n mx my; rewrite !option_includedN;intros [->|(x&y&->&->&?)]; auto.
+    right; exists (unit x), (unit y); eauto using cmra_unit_preservingN.
   * intros n [x|] [y|]; rewrite /validN /option_validN /=;
       eauto using cmra_validN_op_l.
   * intros n mx my; rewrite option_includedN.
-    intros [->|[->|(x&y&->&->&?)]]; [done|by destruct my|].
+    intros [->|(x&y&->&->&?)]; [by destruct my|].
     by constructor; apply cmra_op_minus.
 Qed.
 Definition option_cmra_extend_mixin : CMRAExtendMixin (option A).
 Proof.
-  intros n mx my1 my2; destruct (decide (n = 0)) as [->|].
-  { by exists (mx, None); repeat constructor; destruct mx; constructor. }
+  intros n mx my1 my2.
   destruct mx as [x|], my1 as [y1|], my2 as [y2|]; intros Hx Hx';
     try (by exfalso; inversion Hx'; auto).
   * destruct (cmra_extend_op n x y1 y2) as ([z1 z2]&?&?&?); auto.
@@ -171,7 +164,7 @@ Instance option_fmap_cmra_monotone {A B : cmraT} (f: A → B) `{!CMRAMonotone f}
 Proof.
   split.
   * intros n mx my; rewrite !option_includedN.
-    intros [->|[->|(x&y&->&->&?)]]; simpl; eauto 10 using @includedN_preserving.
+    intros [->|(x&y&->&->&?)]; simpl; eauto 10 using @includedN_preserving.
   * by intros n [x|] ?; rewrite /cmra_validN /=; try apply validN_preserving.
 Qed.
 Definition optionC_map {A B} (f : A -n> B) : optionC A -n> optionC B :=
diff --git a/algebra/upred.v b/algebra/upred.v
index f8898189925b9ca0649d4826335799e04277d625..72b97739d5d55e49e39c3b8e51bf2f5ffc9760b5 100644
--- a/algebra/upred.v
+++ b/algebra/upred.v
@@ -6,14 +6,12 @@ Local Hint Extern 10 (_ ≤ _) => omega.
 Record uPred (M : cmraT) : Type := IProp {
   uPred_holds :> nat → M → Prop;
   uPred_ne x1 x2 n : uPred_holds n x1 → x1 ≡{n}≡ x2 → uPred_holds n x2;
-  uPred_0 x : uPred_holds 0 x;
   uPred_weaken x1 x2 n1 n2 :
     uPred_holds n1 x1 → x1 ≼ x2 → n2 ≤ n1 → ✓{n2} x2 → uPred_holds n2 x2
 }.
 Arguments uPred_holds {_} _ _ _ : simpl never.
 Global Opaque uPred_holds.
 Local Transparent uPred_holds.
-Hint Resolve uPred_0.
 Add Printing Constructor uPred.
 Instance: Params (@uPred_holds) 3.
 
@@ -24,12 +22,11 @@ Section cofe.
   Instance uPred_dist : Dist (uPred M) := λ n P Q, ∀ x n',
     n' ≤ n → ✓{n'} x → P n' x ↔ Q n' x.
   Program Instance uPred_compl : Compl (uPred M) := λ c,
-    {| uPred_holds n x := c n n x |}.
+    {| uPred_holds n x := c (S n) n x |}.
   Next Obligation. by intros c x y n ??; simpl in *; apply uPred_ne with x. Qed.
-  Next Obligation. by intros c x; simpl. Qed.
   Next Obligation.
     intros c x1 x2 n1 n2 ????; simpl in *.
-    apply (chain_cauchy c n2 n1); eauto using uPred_weaken.
+    apply (chain_cauchy c n2 (S n1)); eauto using uPred_weaken.
   Qed.
   Definition uPred_cofe_mixin : CofeMixin (uPred M).
   Proof.
@@ -41,8 +38,7 @@ Section cofe.
       + by intros P Q HPQ x i ??; symmetry; apply HPQ.
       + by intros P Q Q' HP HQ x i ??; transitivity (Q i x);[apply HP|apply HQ].
     * intros n P Q HPQ x i ??; apply HPQ; auto.
-    * intros P Q x i; rewrite Nat.le_0_r=> ->; split; intros; apply uPred_0.
-    * by intros c n x i ??; apply (chain_cauchy c i n).
+    * intros c n x i ??; symmetry; apply (chain_cauchy c i (S n)); auto.
   Qed.
   Canonical Structure uPredC : cofeT := CofeT uPred_cofe_mixin.
 End cofe.
@@ -65,7 +61,6 @@ Program Definition uPred_map {M1 M2 : cmraT} (f : M2 -n> M1)
   `{!CMRAMonotone f} (P : uPred M1) :
   uPred M2 := {| uPred_holds n x := P n (f x) |}.
 Next Obligation. by intros M1 M2 f ? P y1 y2 n ? Hy; rewrite /= -Hy. Qed.
-Next Obligation. intros M1 M2 f _ P x; apply uPred_0. Qed.
 Next Obligation.
   naive_solver eauto using uPred_weaken, included_preserving, validN_preserving.
 Qed.
@@ -103,9 +98,8 @@ Instance uPred_entails_rewrite_relation M : RewriteRelation (@uPred_entails M).
 
 (** logical connectives *)
 Program Definition uPred_const {M} (φ : Prop) : uPred M :=
-  {| uPred_holds n x := match n return _ with 0 => True | _ => φ end |}.
+  {| uPred_holds n x := φ |}.
 Solve Obligations with done.
-Next Obligation. intros M P x1 x2 [|n1] [|n2]; auto with lia. Qed.
 Instance uPred_inhabited M : Inhabited (uPred M) := populate (uPred_const True).
 
 Program Definition uPred_and {M} (P Q : uPred M) : uPred M :=
@@ -125,19 +119,13 @@ Next Obligation.
   eauto using uPred_weaken, uPred_ne.
 Qed.
 Next Obligation. intros M P Q x1 x2 [|n]; auto with lia. Qed.
-Next Obligation. naive_solver eauto 2 with lia. Qed.
 
 Program Definition uPred_forall {M A} (P : A → uPred M) : uPred M :=
   {| uPred_holds n x := ∀ a, P a n x |}.
 Solve Obligations with naive_solver eauto 2 using uPred_ne, uPred_weaken.
 Program Definition uPred_exist {M A} (P : A → uPred M) : uPred M :=
-  {| uPred_holds n x :=
-       match n return _ with 0 => True | _ => ∃ a, P a n x end |}.
-Next Obligation. intros M A P x y [|n]; naive_solver eauto using uPred_ne. Qed.
-Next Obligation. done. Qed.
-Next Obligation.
-  intros M A P x y [|n] [|n']; naive_solver eauto 2 using uPred_weaken with lia.
-Qed.
+  {| uPred_holds n x := ∃ a, P a n x |}.
+Solve Obligations with naive_solver eauto 2 using uPred_ne, uPred_weaken.
 
 Program Definition uPred_eq {M} {A : cofeT} (a1 a2 : A) : uPred M :=
   {| uPred_holds n x := a1 ≡{n}≡ a2 |}.
@@ -148,7 +136,6 @@ Program Definition uPred_sep {M} (P Q : uPred M) : uPred M :=
 Next Obligation.
   by intros M P Q x y n (x1&x2&?&?&?) Hxy; exists x1, x2; rewrite -Hxy.
 Qed.
-Next Obligation. by intros M P Q x; exists x, x. Qed.
 Next Obligation.
   intros M P Q x y n1 n2 (x1&x2&Hx&?&?) Hxy ??.
   assert (∃ x2', y ≡{n2}≡ x1 ⋅ x2' ∧ x2 ≼ x2') as (x2'&Hy&?).
@@ -167,7 +154,6 @@ Next Obligation.
   rewrite -(dist_le _ _ _ _ Hx) //; apply HPQ; auto.
   by rewrite (dist_le _ _ _ n2 Hx).
 Qed.
-Next Obligation. intros M P Q x1 x2 [|n]; auto with lia. Qed.
 Next Obligation.
   intros M P Q x1 x2 n1 n2 HPQ ??? x3 n3 ???; simpl in *.
   apply uPred_weaken with (x1 â‹… x3) n3;
@@ -177,14 +163,12 @@ Qed.
 Program Definition uPred_later {M} (P : uPred M) : uPred M :=
   {| uPred_holds n x := match n return _ with 0 => True | S n' => P n' x end |}.
 Next Obligation. intros M P ?? [|n]; eauto using uPred_ne,(dist_le (A:=M)). Qed.
-Next Obligation. done. Qed.
 Next Obligation.
-  intros M P x1 x2 [|n1] [|n2]; eauto using uPred_weaken, cmra_validN_S.
+  intros M P x1 x2 [|n1] [|n2]; eauto using uPred_weaken,cmra_validN_S; try lia.
 Qed.
 Program Definition uPred_always {M} (P : uPred M) : uPred M :=
   {| uPred_holds n x := P n (unit x) |}.
 Next Obligation. by intros M P x1 x2 n ? Hx; rewrite /= -Hx. Qed.
-Next Obligation. by intros; simpl. Qed.
 Next Obligation.
   intros M P x1 x2 n1 n2 ????; eapply uPred_weaken with (unit x1) n1;
     eauto using cmra_unit_preserving, cmra_unit_validN.
@@ -193,14 +177,13 @@ Qed.
 Program Definition uPred_own {M : cmraT} (a : M) : uPred M :=
   {| uPred_holds n x := a ≼{n} x |}.
 Next Obligation. by intros M a x1 x2 n [a' ?] Hx; exists a'; rewrite -Hx. Qed.
-Next Obligation. by intros M a x; exists x. Qed.
 Next Obligation.
   intros M a x1 x n1 n2 [a' Hx1] [x2 Hx] ??.
   exists (a' â‹… x2). by rewrite (associative op) -(dist_le _ _ _ _ Hx1) // Hx.
 Qed.
 Program Definition uPred_valid {M A : cmraT} (a : A) : uPred M :=
   {| uPred_holds n x := ✓{n} a |}.
-Solve Obligations with naive_solver eauto 2 using cmra_validN_le, cmra_validN_0.
+Solve Obligations with naive_solver eauto 2 using cmra_validN_le.
 
 Delimit Scope uPred_scope with I.
 Bind Scope uPred_scope with uPred.
@@ -329,18 +312,14 @@ Global Instance forall_proper A :
 Proof. by intros P1 P2 HP12 x n'; split; intros HP a; apply HP12. Qed.
 Global Instance exists_ne A :
   Proper (pointwise_relation _ (dist n) ==> dist n) (@uPred_exist M A).
-Proof.
-  by intros n P1 P2 HP x [|n']; [|split; intros [a ?]; exists a; apply HP].
-Qed.
+Proof. by intros n P1 P2 HP x; split; intros [a ?]; exists a; apply HP. Qed.
 Global Instance exist_proper A :
   Proper (pointwise_relation _ (≡) ==> (≡)) (@uPred_exist M A).
-Proof.
-  by intros P1 P2 HP x [|n']; [|split; intros [a ?]; exists a; apply HP].
-Qed.
+Proof. by intros P1 P2 HP x n'; split; intros [a ?]; exists a; apply HP. Qed.
 Global Instance later_contractive : Contractive (@uPred_later M).
 Proof.
   intros n P Q HPQ x [|n'] ??; simpl; [done|].
-  apply HPQ; eauto using cmra_validN_S.
+  apply (HPQ n'); eauto using cmra_validN_S.
 Qed.
 Global Instance later_proper :
   Proper ((≡) ==> (≡)) (@uPred_later M) := ne_proper _.
@@ -364,10 +343,7 @@ Global Instance iff_proper :
 Lemma const_intro φ P : φ → P ⊑ ■ φ.
 Proof. by intros ?? [|?]. Qed.
 Lemma const_elim φ Q R : Q ⊑ ■ φ → (φ → Q ⊑ R) → Q ⊑ R.
-Proof.
-  intros HQP HQR x [|n] ??; first done.
-  apply HQR; first eapply (HQP _ (S n)); eauto.
-Qed.
+Proof. intros HQP HQR x n ??; apply HQR; first eapply (HQP _ n); eauto. Qed.
 Lemma True_intro P : P ⊑ True.
 Proof. by apply const_intro. Qed.
 Lemma False_elim P : False ⊑ P.
@@ -395,9 +371,9 @@ Proof. by intros HPQ x n ?? a; apply HPQ. Qed.
 Lemma forall_elim {A} {P : A → uPred M} a : (∀ a, P a) ⊑ P a.
 Proof. intros x n ? HP; apply HP. Qed.
 Lemma exist_intro {A} {P : A → uPred M} a : P a ⊑ (∃ a, P a).
-Proof. by intros x [|n] ??; [done|exists a]. Qed.
+Proof. by intros x n ??; exists a. Qed.
 Lemma exist_elim {A} (P : A → uPred M) Q : (∀ a, P a ⊑ Q) → (∃ a, P a) ⊑ Q.
-Proof. by intros HPQ x [|n] ?; [|intros [a ?]; apply HPQ with a]. Qed.
+Proof. by intros HPQ x n ? [a ?]; apply HPQ with a. Qed.
 Lemma eq_refl {A : cofeT} (a : A) P : P ⊑ (a ≡ a).
 Proof. by intros x n ??; simpl. Qed.
 Lemma eq_rewrite {A : cofeT} P (Q : A → uPred M)
@@ -408,12 +384,11 @@ Qed.
 Lemma eq_equiv `{Empty M, !CMRAIdentity M} {A : cofeT} (a b : A) :
   True ⊑ (a ≡ b) → a ≡ b.
 Proof.
-  intros Hab; apply equiv_dist; intros n; apply Hab with ∅.
-  * apply cmra_valid_validN, cmra_empty_valid.
-  * by destruct n.
+  intros Hab; apply equiv_dist; intros n; apply Hab with ∅; last done.
+  apply cmra_valid_validN, cmra_empty_valid.
 Qed.
 Lemma iff_equiv P Q : True ⊑ (P ↔ Q) → P ≡ Q.
-Proof. by intros HPQ x [|n] ?; [|split; intros; apply HPQ with x (S n)]. Qed.
+Proof. by intros HPQ x n ?; split; intros; apply HPQ with x n. Qed.
 
 (* Derived logical stuff *)
 Lemma and_elim_l' P Q R : P ⊑ R → (P ∧ Q) ⊑ R.
@@ -577,7 +552,7 @@ Global Instance True_sep : LeftId (≡) True%I (@uPred_sep M).
 Proof.
   intros P x n Hvalid; split.
   * intros (x1&x2&?&_&?); cofe_subst; eauto using uPred_weaken, cmra_included_r.
-  * by destruct n as [|n]; [|intros ?; exists (unit x), x; rewrite cmra_unit_l].
+  * by intros ?; exists (unit x), x; rewrite cmra_unit_l.
 Qed. 
 Global Instance sep_commutative : Commutative (≡) (@uPred_sep M).
 Proof.
@@ -702,8 +677,9 @@ Proof. intros x [|[|n]]; split; done || by exists inhabitant; simpl. Qed.
 Lemma later_sep P Q : (▷ (P ★ Q))%I ≡ (▷ P ★ ▷ Q)%I.
 Proof.
   intros x n ?; split.
-  * destruct n as [|n]; simpl; [by exists x, x|intros (x1&x2&Hx&?&?)].
-    destruct (cmra_extend_op n x x1 x2)
+  * destruct n as [|n]; simpl.
+    { by exists x, (unit x); rewrite cmra_unit_r. } 
+    intros (x1&x2&Hx&?&?); destruct (cmra_extend_op n x x1 x2)
       as ([y1 y2]&Hx'&Hy1&Hy2); eauto using cmra_validN_S; simpl in *.
     exists y1, y2; split; [by rewrite Hx'|by rewrite Hy1 Hy2].
   * destruct n as [|n]; simpl; [done|intros (x1&x2&Hx&?&?)].
@@ -823,15 +799,15 @@ Qed.
 Lemma always_own (a : M) : unit a ≡ a → (□ uPred_own a)%I ≡ uPred_own a.
 Proof. by intros <-; rewrite always_own_unit. Qed.
 Lemma own_something : True ⊑ ∃ a, uPred_own a.
-Proof. intros x [|n] ??; [done|]. by exists x; simpl. Qed.
+Proof. intros x n ??. by exists x; simpl. Qed.
 Lemma own_empty `{Empty M, !CMRAIdentity M} : True ⊑ uPred_own ∅.
-Proof. intros x [|n] ??; [done|]. by  exists x; rewrite (left_id _ _). Qed.
+Proof. intros x n ??; by  exists x; rewrite (left_id _ _). Qed.
 Lemma own_valid (a : M) : uPred_own a ⊑ ✓ a.
 Proof. intros x n Hv [a' ?]; cofe_subst; eauto using cmra_validN_op_l. Qed.
 Lemma valid_intro {A : cmraT} (a : A) : ✓ a → True ⊑ ✓ a.
 Proof. by intros ? x n ? _; simpl; apply cmra_valid_validN. Qed.
-Lemma valid_elim {A : cmraT} (a : A) : ¬ ✓{1} a → ✓ a ⊑ False.
-Proof. intros Ha x [|n] ??; [|apply Ha, cmra_validN_le with (S n)]; auto. Qed.
+Lemma valid_elim {A : cmraT} (a : A) : ¬ ✓{0} a → ✓ a ⊑ False.
+Proof. intros Ha x n ??; apply Ha, cmra_validN_le with n; auto. Qed.
 Lemma valid_mono {A B : cmraT} (a : A) (b : B) :
   (∀ n, ✓{n} a → ✓{n} b) → ✓ a ⊑ ✓ b.
 Proof. by intros ? x n ?; simpl; auto. Qed.
@@ -839,7 +815,7 @@ Lemma always_valid {A : cmraT} (a : A) : (□ (✓ a))%I ≡ (✓ a : uPred M)%I
 Proof. done. Qed.
 
 (* Own and valid derived *)
-Lemma own_invalid (a : M) : ¬ ✓{1} a → uPred_own a ⊑ False.
+Lemma own_invalid (a : M) : ¬ ✓{0} a → uPred_own a ⊑ False.
 Proof. by intros; rewrite own_valid valid_elim. Qed.
 
 (* Big ops *)
@@ -873,13 +849,13 @@ Lemma uPred_big_sep_elem_of Ps P : P ∈ Ps → (Π★ Ps) ⊑ P.
 Proof. induction 1; simpl; auto. Qed.
 
 (* Timeless *)
-Lemma timelessP_spec P : TimelessP P ↔ ∀ x n, ✓{n} x → P 1 x → P n x.
+Lemma timelessP_spec P : TimelessP P ↔ ∀ x n, ✓{n} x → P 0 x → P n x.
 Proof.
   split.
-  * intros HP x n ??; induction n as [|[|n]]; auto.
-    by destruct (HP x (S (S n))); auto using cmra_validN_S.
-  * move=> HP x [|[|n]] /=; auto; left.
-    apply HP, uPred_weaken with x (S n); eauto using cmra_validN_le.
+  * intros HP x n ??; induction n as [|n]; auto.
+    by destruct (HP x (S n)); auto using cmra_validN_S.
+  * move=> HP x [|n] /=; auto; left.
+    apply HP, uPred_weaken with x n; eauto using cmra_validN_le.
 Qed.
 Global Instance const_timeless φ : TimelessP (■ φ : uPred M)%I.
 Proof. by apply timelessP_spec=> x [|n]. Qed.
diff --git a/program_logic/adequacy.v b/program_logic/adequacy.v
index 29df1e9d2db71f040499e43fa6e45a34c94000bb..f6e81accf55dc2fffaa309f1f35f6d41f80170fa 100644
--- a/program_logic/adequacy.v
+++ b/program_logic/adequacy.v
@@ -3,8 +3,9 @@ Require Import program_logic.wsat program_logic.ownership.
 Local Hint Extern 10 (_ ≤ _) => omega.
 Local Hint Extern 100 (@eq coPset _ _) => eassumption || solve_elem_of.
 Local Hint Extern 10 (✓{_} _) =>
-  repeat match goal with H : wsat _ _ _ _ |- _ => apply wsat_valid in H end;
-  solve_validN.
+  repeat match goal with
+  | H : wsat _ _ _ _ |- _ => apply wsat_valid in H; last omega
+  end; solve_validN.
 
 Section adequacy.
 Context {Λ : language} {Σ : iFunctor}.
@@ -67,7 +68,7 @@ Lemma ht_adequacy_own Q e1 t2 σ1 m σ2 :
   ✓m →
   {{ ownP σ1 ★ ownG m }} e1 @ coPset_all {{ Q }} →
   rtc step ([e1],σ1) (t2,σ2) →
-  ∃ rs2 Qs', wptp 3 t2 (Q :: Qs') rs2 ∧ wsat 3 coPset_all σ2 (big_op rs2).
+  ∃ rs2 Qs', wptp 2 t2 (Q :: Qs') rs2 ∧ wsat 2 coPset_all σ2 (big_op rs2).
 Proof.
   intros Hv ? [k ?]%rtc_nsteps.
   eapply ht_adequacy_steps with (r1 := (Res ∅ (Excl σ1) (Some m))); eauto; [|].
@@ -88,7 +89,7 @@ Proof.
              as (rs2&Qs&Hwptp&?); auto.
   { by rewrite -(ht_mask_weaken E coPset_all). }
   inversion Hwptp as [|?? r ?? rs Hwp _]; clear Hwptp; subst.
-  apply wp_value_inv in Hwp; destruct (Hwp (big_op rs) 3 ∅ σ2) as [r' []]; auto.
+  apply wp_value_inv in Hwp; destruct (Hwp (big_op rs) 2 ∅ σ2) as [r' []]; auto.
   by rewrite right_id_L.
 Qed.
 Lemma ht_adequacy_reducible E Q e1 e2 t2 σ1 m σ2 :
@@ -100,9 +101,9 @@ Proof.
   intros Hv ? Hs [i ?]%elem_of_list_lookup He.
   destruct (ht_adequacy_own Q e1 t2 σ1 m σ2) as (rs2&Qs&?&?); auto.
   { by rewrite -(ht_mask_weaken E coPset_all). }
-  destruct (Forall3_lookup_l (λ e Q r, wp coPset_all e Q 3 r) t2
+  destruct (Forall3_lookup_l (λ e Q r, wp coPset_all e Q 2 r) t2
     (Q :: Qs) rs2 i e2) as (Q'&r2&?&?&Hwp); auto.
-  destruct (wp_step_inv coPset_all ∅ Q' e2 2 3 σ2 r2 (big_op (delete i rs2)));
+  destruct (wp_step_inv coPset_all ∅ Q' e2 1 2 σ2 r2 (big_op (delete i rs2)));
     rewrite ?right_id_L ?big_op_delete; auto.
 Qed.
 Theorem ht_adequacy_safe E Q e1 t2 σ1 m σ2 :
diff --git a/program_logic/lifting.v b/program_logic/lifting.v
index 3b474e67a13622e6ddb8433b4600aa1b3694c428..e72e87a056de6b8cf33a945f14e450138919990c 100644
--- a/program_logic/lifting.v
+++ b/program_logic/lifting.v
@@ -3,8 +3,9 @@ Require Import program_logic.wsat program_logic.ownership.
 Local Hint Extern 10 (_ ≤ _) => omega.
 Local Hint Extern 100 (@eq coPset _ _) => solve_elem_of.
 Local Hint Extern 10 (✓{_} _) =>
-  repeat match goal with H : wsat _ _ _ _ |- _ => apply wsat_valid in H end;
-  solve_validN.
+  repeat match goal with
+  | H : wsat _ _ _ _ |- _ => apply wsat_valid in H; last omega
+  end; solve_validN.
 
 Section lifting.
 Context {Λ : language} {Σ : iFunctor}.
@@ -45,10 +46,10 @@ Lemma wp_lift_pure_step E (φ : expr Λ → option (expr Λ) → Prop) Q e1 :
   (∀ σ1 e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef → σ1 = σ2 ∧ φ e2 ef) →
   (▷ ∀ e2 ef, ■ φ e2 ef → wp E e2 Q ★ wp_fork ef) ⊑ wp E e1 Q.
 Proof.
-  intros He Hsafe Hstep r [|n] ?; [done|]; intros Hwp; constructor; auto.
-  intros rf k Ef σ1 ???; split; [done|].
+  intros He Hsafe Hstep r n ? Hwp; constructor; auto.
+  intros rf k Ef σ1 ???; split; [done|]. destruct n as [|n]; first lia.
   intros e2 σ2 ef ?; destruct (Hstep σ1 e2 σ2 ef); auto; subst.
-  destruct (Hwp e2 ef r k) as (r1&r2&Hr&?&?); auto; [by destruct k|].
+  destruct (Hwp e2 ef r k) as (r1&r2&Hr&?&?); auto.
   exists r1,r2; split_ands; [rewrite -Hr| |by intros ? ->]; eauto using wsat_le.
 Qed.
 
@@ -106,4 +107,3 @@ Proof.
 Qed.
 
 End lifting.
-
diff --git a/program_logic/model.v b/program_logic/model.v
index ca0bbec0cac4abb1240ddf7796088f1eb49c5a79..dda84c106aec750600cd2b256482215ef148d638 100644
--- a/program_logic/model.v
+++ b/program_logic/model.v
@@ -23,8 +23,9 @@ Proof.
     rewrite -uPred_map_compose. apply uPred_map_ext=>{P} r /=.
     rewrite -res_map_compose. apply res_map_ext=>{r} r /=.
     by rewrite -later_map_compose.
-  * intros A1 A2 B1 B2 n f f' [??] P.
-    by apply upredC_map_ne, resC_map_ne, laterC_map_contractive.
+  * intros A1 A2 B1 B2 n f f' Hf P [???].
+    apply upredC_map_ne, resC_map_ne, laterC_map_contractive.
+    by intros i ?; apply Hf.
 Qed.
 End iProp.
 
diff --git a/program_logic/ownership.v b/program_logic/ownership.v
index 2899d3b6a0b2da29614cc7734fe052834cd8647c..d1f3a35d914e62922fb8f9be84b4ab57fac87940 100644
--- a/program_logic/ownership.v
+++ b/program_logic/ownership.v
@@ -1,7 +1,7 @@
 Require Export program_logic.model.
 
 Definition ownI {Λ Σ} (i : positive) (P : iProp Λ Σ) : iProp Λ Σ :=
-  uPred_own (Res {[ i ↦ to_agree (Later (iProp_unfold P)) ]} ∅ ∅).
+  uPred_own (Res {[ i ↦ to_agree (Next (iProp_unfold P)) ]} ∅ ∅).
 Arguments ownI {_ _} _ _%I.
 Definition ownP {Λ Σ} (σ: state Λ) : iProp Λ Σ := uPred_own (Res ∅ (Excl σ) ∅).
 Definition ownG {Λ Σ} (m: iGst Λ Σ) : iProp Λ Σ := uPred_own (Res ∅ ∅ (Some m)).
@@ -21,9 +21,9 @@ Implicit Types m : iGst Λ Σ.
 (* Invariants *)
 Global Instance ownI_contractive i : Contractive (@ownI Λ Σ i).
 Proof.
-  intros n P Q HPQ.
-  apply (_: Proper (_ ==> _) iProp_unfold), Later_contractive in HPQ.
-  by unfold ownI; rewrite HPQ.
+  intros n P Q HPQ. rewrite /ownI.
+  apply uPred.own_ne, Res_ne; auto; apply singleton_ne, to_agree_ne.
+  by apply Next_contractive=> j ?; rewrite (HPQ j).
 Qed.
 Lemma always_ownI i P : (□ ownI i P)%I ≡ ownI i P.
 Proof.
@@ -65,7 +65,7 @@ Proof. rewrite /ownG; apply _. Qed.
 (* inversion lemmas *)
 Lemma ownI_spec r n i P :
   ✓{n} r →
-  (ownI i P) n r ↔ wld r !! i ≡{n}≡ Some (to_agree (Later (iProp_unfold P))).
+  (ownI i P) n r ↔ wld r !! i ≡{n}≡ Some (to_agree (Next (iProp_unfold P))).
 Proof.
   intros [??]; rewrite /uPred_holds/=res_includedN/=singleton_includedN; split.
   * intros [(P'&Hi&HP) _]; rewrite Hi.
diff --git a/program_logic/pviewshifts.v b/program_logic/pviewshifts.v
index f76066f5fb585fbf5d1679edc146605aad79e973..6184683cf218223c82f694d6e16d85c638c1911a 100644
--- a/program_logic/pviewshifts.v
+++ b/program_logic/pviewshifts.v
@@ -5,19 +5,19 @@ Local Hint Extern 10 (_ ≤ _) => omega.
 Local Hint Extern 100 (@eq coPset _ _) => solve_elem_of.
 Local Hint Extern 100 (_ ∉ _) => solve_elem_of.
 Local Hint Extern 10 (✓{_} _) =>
-  repeat match goal with H : wsat _ _ _ _ |- _ => apply wsat_valid in H end;
-  solve_validN.
+  repeat match goal with
+  | H : wsat _ _ _ _ |- _ => apply wsat_valid in H; last omega
+  end; solve_validN.
 
 Program Definition pvs {Λ Σ} (E1 E2 : coPset) (P : iProp Λ Σ) : iProp Λ Σ :=
   {| uPred_holds n r1 := ∀ rf k Ef σ,
-       1 < k ≤ n → (E1 ∪ E2) ∩ Ef = ∅ →
+       0 < k ≤ n → (E1 ∪ E2) ∩ Ef = ∅ →
        wsat k (E1 ∪ Ef) σ (r1 ⋅ rf) →
        ∃ r2, P k r2 ∧ wsat k (E2 ∪ Ef) σ (r2 ⋅ rf) |}.
 Next Obligation.
   intros Λ Σ E1 E2 P r1 r2 n HP Hr rf k Ef σ ?? Hwsat; simpl in *.
   apply HP; auto. by rewrite (dist_le _ _ _ _ Hr); last lia.
 Qed.
-Next Obligation. intros Λ Σ E1 E2 P r rf k Ef σ; simpl in *; lia. Qed.
 Next Obligation.
   intros Λ Σ E1 E2 P r1 r2 n1 n2 HP [r3 ?] Hn ? rf k Ef σ ?? Hws; setoid_subst.
   destruct (HP (r3⋅rf) k Ef σ) as (r'&?&Hws'); rewrite ?(associative op); auto.
@@ -121,7 +121,7 @@ Proof.
   intros ? r [|n] ? HP rf [|k] Ef σ ???; try lia.
   destruct (wsat_alloc k E Ef σ rf P r) as (i&?&?&?); auto.
   { apply uPred_weaken with r n; eauto. }
-  exists (Res {[ i ↦ to_agree (Later (iProp_unfold P)) ]} ∅ ∅).
+  exists (Res {[ i ↦ to_agree (Next (iProp_unfold P)) ]} ∅ ∅).
   by split; [by exists i; split; rewrite /uPred_holds /=|].
 Qed.
 
diff --git a/program_logic/resources.v b/program_logic/resources.v
index e6c145f52d40acfb4258df50217ba16afd8e5b78..77d718f57f6aebfaead27bab468d8b36f9ba41bd 100644
--- a/program_logic/resources.v
+++ b/program_logic/resources.v
@@ -38,8 +38,8 @@ Global Instance wld_proper : Proper ((≡) ==> (≡)) (@wld Λ Σ A).
 Proof. by destruct 1. Qed.
 Global Instance pst_ne n : Proper (dist n ==> dist n) (@pst Λ Σ A).
 Proof. by destruct 1. Qed.
-Global Instance pst_ne' n : Proper (dist (S n) ==> (≡)) (@pst Λ Σ A).
-Proof. destruct 1; apply (timeless _), dist_le with (S n); auto with lia. Qed.
+Global Instance pst_ne' n : Proper (dist n ==> (≡)) (@pst Λ Σ A).
+Proof. destruct 1; apply (timeless _), dist_le with n; auto with lia. Qed.
 Global Instance pst_proper : Proper ((≡) ==> (=)) (@pst Λ Σ A).
 Proof. by destruct 1; unfold_leibniz. Qed.
 Global Instance gst_ne n : Proper (dist n ==> dist n) (@gst Λ Σ A).
@@ -60,7 +60,6 @@ Proof.
     + by destruct 1; constructor.
     + do 2 destruct 1; constructor; etransitivity; eauto.
   * by destruct 1; constructor; apply dist_S.
-  * done.
   * intros c n; constructor.
     + apply (conv_compl (chain_map wld c) n).
     + apply (conv_compl (chain_map pst c) n).
@@ -102,7 +101,6 @@ Proof.
   * by intros n [???] ? [???] (?&?&?); split_ands'; simpl in *; cofe_subst.
   * by intros n [???] ? [???] [???] ? [???];
       constructor; simpl in *; cofe_subst.
-  * done.
   * by intros n ? (?&?&?); split_ands'; apply cmra_validN_S.
   * intros ???; constructor; simpl; apply (associative _).
   * intros ??; constructor; simpl; apply (commutative _).
@@ -220,9 +218,5 @@ Program Definition resF {Λ Σ} : iFunctor := {|
   ifunctor_car := resRA Λ Σ;
   ifunctor_map A B := resC_map
 |}.
-Next Obligation.
-  intros Λ Σ A x. by rewrite /= res_map_id.
-Qed.
-Next Obligation.
-  intros Λ Σ A B C f g x. by rewrite /= res_map_compose.
-Qed.
+Next Obligation. intros Λ Σ A x. by rewrite /= res_map_id. Qed.
+Next Obligation. intros Λ Σ A B C f g x. by rewrite /= res_map_compose. Qed.
diff --git a/program_logic/weakestpre.v b/program_logic/weakestpre.v
index 3618e8753f046428e8e0a73ecc3deefefb1771dd..1f03296f35da1c82a894ca553c699f54724911a4 100644
--- a/program_logic/weakestpre.v
+++ b/program_logic/weakestpre.v
@@ -5,8 +5,9 @@ Local Hint Extern 100 (@eq coPset _ _) => eassumption || solve_elem_of.
 Local Hint Extern 100 (_ ∉ _) => solve_elem_of.
 Local Hint Extern 100 (@subseteq coPset _ _ _) => solve_elem_of.
 Local Hint Extern 10 (✓{_} _) =>
-  repeat match goal with H : wsat _ _ _ _ |- _ => apply wsat_valid in H end;
-  solve_validN.
+  repeat match goal with
+  | H : wsat _ _ _ _ |- _ => apply wsat_valid in H; last omega
+  end; solve_validN.
 
 Record wp_go {Λ Σ} (E : coPset) (Q Qfork : expr Λ → nat → iRes Λ Σ → Prop)
     (k : nat) (rf : iRes Λ Σ) (e1 : expr Λ) (σ1 : state Λ) := {
@@ -24,7 +25,7 @@ CoInductive wp_pre {Λ Σ} (E : coPset)
   | wp_pre_step n r1 e1 :
      to_val e1 = None →
      (∀ rf k Ef σ1,
-       1 < k < n → E ∩ Ef = ∅ →
+       0 < k < n → E ∩ Ef = ∅ →
        wsat (S k) (E ∪ Ef) σ1 (r1 ⋅ rf) →
        wp_go (E ∪ Ef) (wp_pre E Q)
                       (wp_pre coPset_all (λ _, True%I)) k rf e1 σ1) →
@@ -36,11 +37,6 @@ Next Obligation.
   destruct Hwp as [|n r1 e2 ? Hgo]; constructor; rewrite -?Hr; auto.
   intros rf k Ef σ1 ?; rewrite -(dist_le _ _ _ _ Hr); naive_solver.
 Qed.
-Next Obligation.
-  intros Λ Σ E e Q r; destruct (to_val e) as [v|] eqn:?.
-  * by rewrite -(of_to_val e v) //; constructor.
-  * constructor; auto with lia.
-Qed.
 Next Obligation.
   intros Λ Σ E e Q r1 r2 n1; revert Q E e r1 r2.
   induction n1 as [n1 IH] using lt_wf_ind; intros Q E e r1 r1' n2.
@@ -104,7 +100,7 @@ Proof.
   by inversion 1 as [|??? He]; [|rewrite ?to_of_val in He]; simplify_equality.
 Qed.
 Lemma wp_step_inv E Ef Q e k n σ r rf :
-  to_val e = None → 1 < k < n → E ∩ Ef = ∅ →
+  to_val e = None → 0 < k < n → E ∩ Ef = ∅ →
   wp E e Q n r → wsat (S k) (E ∪ Ef) σ (r ⋅ rf) →
   wp_go (E ∪ Ef) (λ e, wp E e Q) (λ e, wp coPset_all e (λ _, True%I)) k rf e σ.
 Proof. intros He; destruct 3; [by rewrite ?to_of_val in He|eauto]. Qed.
@@ -113,7 +109,7 @@ Lemma wp_value E Q v : Q v ⊑ wp E (of_val v) Q.
 Proof. by constructor; apply pvs_intro. Qed.
 Lemma pvs_wp E e Q : pvs E E (wp E e Q) ⊑ wp E e Q.
 Proof.
-  intros r [|n] ?; [done|]; intros Hvs.
+  intros r n ? Hvs.
   destruct (to_val e) as [v|] eqn:He; [apply of_to_val in He; subst|].
   { constructor; eapply pvs_trans', pvs_mono, Hvs; eauto.
     intros ???; apply wp_value_inv. }
@@ -171,8 +167,8 @@ Lemma wp_frame_later_r E e Q R :
   to_val e = None → (wp E e Q ★ ▷ R) ⊑ wp E e (λ v, Q v ★ R).
 Proof.
   intros He r' n Hvalid (r&rR&Hr&Hwp&?); revert Hvalid; rewrite Hr; clear Hr.
-  destruct Hwp as [|[|n] r e ? Hgo]; [by rewrite to_of_val in He|done|].
-  constructor; [done|intros rf k Ef σ1 ???].
+  destruct Hwp as [|n r e ? Hgo]; [by rewrite to_of_val in He|].
+  constructor; [done|]=>rf k Ef σ1 ???; destruct n as [|n]; first omega.
   destruct (Hgo (rR⋅rf) k Ef σ1) as [Hsafe Hstep];rewrite ?(associative _);auto.
   split; [done|intros e2 σ2 ef ?].
   destruct (Hstep e2 σ2 ef) as (r2&r2'&?&?&?); auto.
diff --git a/program_logic/wsat.v b/program_logic/wsat.v
index 6ec7b21a41a3249bf202c5ef54ac1510809e5a86..b187cd7448f851a88211ea2d66de4ed1abd20d20 100644
--- a/program_logic/wsat.v
+++ b/program_logic/wsat.v
@@ -12,7 +12,7 @@ Record wsat_pre {Λ Σ} (n : nat) (E : coPset)
   wsat_pre_dom i : is_Some (rs !! i) → i ∈ E ∧ is_Some (wld r !! i);
   wsat_pre_wld i P :
     i ∈ E →
-    wld r !! i ≡{S n}≡ Some (to_agree (Later (iProp_unfold P))) →
+    wld r !! i ≡{S n}≡ Some (to_agree (Next (iProp_unfold P))) →
     ∃ r', rs !! i = Some r' ∧ P n r'
 }.
 Arguments wsat_pre_valid {_ _ _ _ _ _ _} _.
@@ -50,22 +50,22 @@ Proof.
   intros [rs [Hval Hσ HE Hwld]] ?; exists rs; constructor; auto.
   intros i P ? HiP; destruct (wld (r â‹… big_opM rs) !! i) as [P'|] eqn:HP';
     [apply (injective Some) in HiP|inversion_clear HiP].
-  assert (P' ≡{S n}≡ to_agree $ Later $ iProp_unfold $
+  assert (P' ≡{S n}≡ to_agree $ Next $ iProp_unfold $
                        iProp_fold $ later_car $ P' (S n)) as HPiso.
   { rewrite iProp_unfold_fold later_eta to_agree_car //.
     apply (map_lookup_validN _ (wld (r â‹… big_opM rs)) i); rewrite ?HP'; auto. }
   assert (P ≡{n'}≡ iProp_fold (later_car (P' (S n)))) as HPP'.
-  { apply (injective iProp_unfold), (injective Later), (injective to_agree).
+  { apply (injective iProp_unfold), (injective Next), (injective to_agree).
     by rewrite -HiP -(dist_le _ _ _ _ HPiso). }
   destruct (Hwld i (iProp_fold (later_car (P' (S n))))) as (r'&?&?); auto.
   { by rewrite HP' -HPiso. }
   assert (✓{S n} r') by (apply (big_opM_lookup_valid _ rs i); auto).
   exists r'; split; [done|apply HPP', uPred_weaken with r' n; auto].
 Qed.
-Lemma wsat_valid n E σ r : wsat n E σ r → ✓{n} r.
+Lemma wsat_valid n E σ r : n ≠ 0 → wsat n E σ r → ✓{n} r.
 Proof.
-  destruct n; [done|intros [rs ?]].
-  eapply cmra_validN_op_l, wsat_pre_valid; eauto.
+  destruct n; first done.
+  intros _ [rs ?]; eapply cmra_validN_op_l, wsat_pre_valid; eauto.
 Qed.
 Lemma wsat_init k E σ mm : ✓{S k} mm → wsat (S k) E σ (Res ∅ (Excl σ) mm).
 Proof.
@@ -77,7 +77,7 @@ Proof.
   * intros i P ?; rewrite /= left_id lookup_empty; inversion_clear 1.
 Qed.
 Lemma wsat_open n E σ r i P :
-  wld r !! i ≡{S n}≡ Some (to_agree (Later (iProp_unfold P))) → i ∉ E →
+  wld r !! i ≡{S n}≡ Some (to_agree (Next (iProp_unfold P))) → i ∉ E →
   wsat (S n) ({[i]} ∪ E) σ r → ∃ rP, wsat (S n) E σ (rP ⋅ r) ∧ P n rP.
 Proof.
   intros HiP Hi [rs [Hval Hσ HE Hwld]].
@@ -92,7 +92,7 @@ Proof.
     apply Hwld; [solve_elem_of +Hj|done].
 Qed.
 Lemma wsat_close n E σ r i P rP :
-  wld rP !! i ≡{S n}≡ Some (to_agree (Later (iProp_unfold P))) → i ∉ E →
+  wld rP !! i ≡{S n}≡ Some (to_agree (Next (iProp_unfold P))) → i ∉ E →
   wsat (S n) E σ (rP ⋅ r) → P n rP → wsat (S n) ({[i]} ∪ E) σ r.
 Proof.
   intros HiP HiE [rs [Hval Hσ HE Hwld]] ?.
@@ -106,7 +106,7 @@ Proof.
   * intros j P'; rewrite Hr elem_of_union elem_of_singleton=>-[?|?]; subst.
     + rewrite !lookup_wld_op_l ?HiP; auto=> HP.
       apply (injective Some), (injective to_agree),
-        (injective Later), (injective iProp_unfold) in HP.
+        (injective Next), (injective iProp_unfold) in HP.
       exists rP; split; [rewrite lookup_insert|apply HP]; auto.
     + intros. destruct (Hwld j P') as (r'&?&?); auto.
       exists r'; rewrite lookup_insert_ne; naive_solver.
@@ -117,7 +117,7 @@ Lemma wsat_update_pst n E σ1 σ1' r rf :
 Proof.
   intros Hpst_r [rs [(?&?&?) Hpst HE Hwld]]; simpl in *.
   assert (pst rf ⋅ pst (big_opM rs) = ∅) as Hpst'.
-  { by apply: (excl_validN_inv_l n σ1); rewrite -Hpst_r associative. }
+  { by apply: (excl_validN_inv_l (S n) σ1); rewrite -Hpst_r associative. }
   assert (σ1' = σ1) as ->.
   { apply leibniz_equiv, (timeless _), dist_le with (S n); auto.
     apply (injective Excl).
@@ -130,14 +130,14 @@ Lemma wsat_update_gst n E σ r rf mm1 (P : iGst Λ Σ → Prop) :
   wsat (S n) E σ (r ⋅ rf) → ∃ m2, wsat (S n) E σ (update_gst m2 r ⋅ rf) ∧ P m2.
 Proof.
   intros [mf Hr] Hup [rs [(?&?&?) Hσ HE Hwld]].
-  destruct (Hup (mf â‹… gst (rf â‹… big_opM rs)) n) as ([m2|]&?&Hval'); try done.
+  destruct (Hup (mf â‹… gst (rf â‹… big_opM rs)) (S n)) as ([m2|]&?&Hval'); try done.
   { by rewrite /= (associative _ mm1) -Hr associative. }
   exists m2; split; [exists rs; split; split_ands'; auto|done].
 Qed.
 Lemma wsat_alloc n E1 E2 σ r P rP :
   ¬set_finite E1 → P n rP → wsat (S n) (E1 ∪ E2) σ (rP ⋅ r) →
   ∃ i, wsat (S n) (E1 ∪ E2) σ
-         (Res {[i ↦ to_agree (Later (iProp_unfold P))]} ∅ ∅ ⋅ r) ∧
+         (Res {[i ↦ to_agree (Next (iProp_unfold P))]} ∅ ∅ ⋅ r) ∧
        wld r !! i = None ∧ i ∈ E1.
 Proof.
   intros HE1 ? [rs [Hval Hσ HE Hwld]].
@@ -167,7 +167,7 @@ Proof.
   * intros j P'; rewrite -associative Hr; destruct (decide (j=i)) as [->|].
     + rewrite /= !lookup_op Hri HrPi Hrsi right_id lookup_singleton=>? HP.
       apply (injective Some), (injective to_agree),
-        (injective Later), (injective iProp_unfold) in HP.
+        (injective Next), (injective iProp_unfold) in HP.
       exists rP; rewrite lookup_insert; split; [|apply HP]; auto.
     + rewrite /= lookup_op lookup_singleton_ne // left_id=> ??.
       destruct (Hwld j P') as [r' ?]; auto.