diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index 1454393e0fecb3d6c9c4ac938159bb6c69071ca9..e13e460f18e7d277c17e6cb4bb2c9feb4c206915 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -107,42 +107,34 @@ Instance: Params (@Discrete) 1 := {}.
 Class OfeDiscrete (A : ofeT) := ofe_discrete_discrete (x : A) :> Discrete x.
 
 (** OFEs with a completion *)
-Record chain (A : ofeT) := {
-  chain_car :> nat → A;
-  chain_cauchy n i : n ≤ i → chain_car i ≡{n}≡ chain_car n
-}.
-Arguments chain_car {_} _ _.
-Arguments chain_cauchy {_} _ _ _ _.
+Definition chain A := nat → A.
+Class Cauchy {A : ofeT} (c : chain A) :=
+  cauchy n i : n ≤ i → c i ≡{n}≡ c n.
+Arguments cauchy {_} _ {_} _ _ _.
+
+Instance chain_fmap : FMap chain := λ A B f c n, f (c n).
+Instance chain_fmap_cauchy {A B : ofeT} (f : A → B) c :
+  NonExpansive f → Cauchy c → Cauchy (f <$> c).
+Proof. intros Hf Hc n i ?. by apply Hf, Hc. Qed.
 
-Program Definition chain_map {A B : ofeT} (f : A → B)
-    `{!NonExpansive 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.
+Instance const_cauchy {A : ofeT} (x : A) : Cauchy (const x).
+Proof. by intros n i _. Qed.
 
-Notation Compl A := (chain A%type → A).
+Notation Compl A := (chain A → A).
 Class Cofe (A : ofeT) := {
   compl : Compl A;
-  conv_compl n c : compl c ≡{n}≡ c n;
+  compl_ne n : Proper (pointwise_relation _ (dist n) ==> dist n) compl;
+  conv_compl n c : Cauchy c → compl c ≡{n}≡ c n;
 }.
+Existing Instance compl_ne.
 Arguments compl : simpl never.
 Hint Mode Cofe ! : typeclass_instances.
 
-Lemma compl_chain_map `{Cofe A, Cofe B} (f : A → B) c `(NonExpansive f) :
-  compl (chain_map f c) ≡ f (compl c).
-Proof. apply equiv_dist=>n. by rewrite !conv_compl. Qed.
-
-Program Definition chain_const {A : ofeT} (a : A) : chain A :=
-  {| chain_car n := a |}.
-Next Obligation. by intros A a n i _. Qed.
-
-Lemma compl_chain_const {A : ofeT} `{!Cofe A} (a : A) :
-  compl (chain_const a) ≡ a.
-Proof. apply equiv_dist=>n. by rewrite conv_compl. Qed.
-
 (** General properties *)
 Section ofe.
   Context {A : ofeT}.
   Implicit Types x y : A.
+
   Global Instance ofe_equivalence : Equivalence ((≡) : relation A).
   Proof.
     split.
@@ -179,10 +171,17 @@ Section ofe.
      by intros x1 x2 Hx y1 y2 Hy n; rewrite (Hx n) (Hy n).
   Qed.
 
-  Lemma conv_compl' `{Cofe A} n (c : chain A) : compl c ≡{n}≡ c (S n).
+  Global Instance conv_proper `{Cofe A} :
+    Proper (pointwise_relation _ (≡) ==> (≡)) (compl (A:=A)).
   Proof.
-    transitivity (c n); first by apply conv_compl. symmetry.
-    apply chain_cauchy. lia.
+    intros c1 c2 Hc. apply equiv_dist=> n. apply compl_ne=> x. by apply equiv_dist.
+  Qed.
+
+  Lemma conv_compl' `{Cofe A} n (c : chain A) :
+    Cauchy c → compl c ≡{n}≡ c (S n).
+  Proof.
+    intros Hc. transitivity (c n); first by apply conv_compl.
+    symmetry. apply Hc. lia.
   Qed.
 
   Lemma discrete_iff n (x : A) `{!Discrete x} y : x ≡ y ↔ x ≡{n}≡ y.
@@ -263,57 +262,82 @@ Section limit_preserving.
 
   Lemma limit_preserving_ext (P Q : A → Prop) :
     (∀ x, P x ↔ Q x) → LimitPreserving P → LimitPreserving Q.
-  Proof. intros HP Hlimit c ?. apply HP, Hlimit=> n; by apply HP. Qed.
+  Proof. intros HP Hlimit c ?. apply HP, Hlimit=> // n. by apply HP. Qed.
 
   Global Instance limit_preserving_const (P : Prop) : LimitPreserving (λ _ : A, P).
   Proof. intros c HP. apply (HP 0). Qed.
 
   Lemma limit_preserving_discrete (P : A → Prop) :
     Proper (dist 0 ==> impl) P → LimitPreserving P.
-  Proof. intros PH c Hc. by rewrite (conv_compl 0). Qed.
+  Proof. intros PH c Hc. rewrite (conv_compl 0). Qed.
+*)
 
   Lemma limit_preserving_and (P1 P2 : A → Prop) :
     LimitPreserving P1 → LimitPreserving P2 →
     LimitPreserving (λ x, P1 x ∧ P2 x).
-  Proof. intros Hlim1 Hlim2 c Hc. split. apply Hlim1, Hc. apply Hlim2, Hc. Qed.
+  Proof. intros Hlim1 Hlim2 c HP. split. by apply Hlim1, HP. by apply Hlim2, HP. Qed.
 
+(*
   Lemma limit_preserving_impl (P1 P2 : A → Prop) :
     Proper (dist 0 ==> impl) P1 → LimitPreserving P2 →
     LimitPreserving (λ x, P1 x → P2 x).
   Proof.
-    intros Hlim1 Hlim2 c Hc HP1. apply Hlim2=> n; apply Hc.
-    eapply Hlim1, HP1. apply dist_le with n; last lia. apply (conv_compl n).
+    intros Hlim1 Hlim2 c HP HPc. apply Hlim2=> // n. apply HP.
+    eapply Hlim1, HPc. apply dist_le with n; last lia. apply (conv_compl n).
   Qed.
+*)
 
   Lemma limit_preserving_forall {B} (P : B → A → Prop) :
     (∀ y, LimitPreserving (P y)) →
     LimitPreserving (λ x, ∀ y, P y x).
-  Proof. intros Hlim c Hc y. by apply Hlim. Qed.
+  Proof. intros Hlim c HPc y. by apply Hlim. Qed.
 End limit_preserving.
 
 (** 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]=> -[|i] //= ?; try lia.
+Definition fixpoint_chain `{Inhabited A} (f : A → A) : chain A :=
+  λ i, Nat.iter (S i) f inhabitant.
+
+Instance fixpoint_chain_cauchy `{Cofe A, Inhabited A} (f : A → A) :
+  Contractive f → Cauchy (fixpoint_chain f).
+Proof.
+  intros ? n. induction n as [|n IH]=> -[|i] //= ?; try lia.
   - apply (contractive_0 f).
   - apply (contractive_S f), IH; auto with lia.
 Qed.
 
-Program Definition fixpoint_def `{Cofe A, Inhabited A} (f : A → A)
-  `{!Contractive f} : A := compl (fixpoint_chain f).
+Program Definition fixpoint_def `{Cofe A, Inhabited A} (f : A → A) : A :=
+  compl (fixpoint_chain f).
 Definition fixpoint_aux : seal (@fixpoint_def). by eexists. Qed.
-Definition fixpoint {A AC AiH} f {Hf} := fixpoint_aux.(unseal) A AC AiH f Hf.
+Definition fixpoint := fixpoint_aux.(unseal).
+Arguments fixpoint {_ _ _} f : assert.
 Definition fixpoint_eq : @fixpoint = @fixpoint_def := fixpoint_aux.(seal_eq).
 
+Instance fixpoint_ne `{Cofe A, Inhabited A} :
+  Proper ((dist n ==> dist n) ==> dist n) (fixpoint (A:=A)).
+Proof.
+  intros n f1 f2 Hf. rewrite fixpoint_eq. apply compl_ne=> i.
+  rewrite /fixpoint_chain. induction (S i) as [|j IH]=> //=. by apply Hf.
+Qed.
+
+Instance fixpoint_proper `{Cofe A, Inhabited A} :
+  Proper (((≡) ==> (≡)) ==> (≡)) (fixpoint (A:=A)).
+Proof.
+  intros f1 f2 Hf. rewrite fixpoint_eq.
+  apply equiv_dist=> n. apply compl_ne=> i. apply equiv_dist.
+  rewrite /fixpoint_chain. induction (S i) as [|j IH]=> //=. by apply Hf.
+Qed.
+
 Section fixpoint.
-  Context `{Cofe A, Inhabited A} (f : A → A) `{!Contractive f}.
+  Context `{Cofe A, Inhabited A} (f : A → A) `{Hf : !Contractive f}.
+  Local Unset Default Proof Using.
+
+  Local Hint Extern 0 (cauchy _) => by apply fixpoint_chain_cauchy : core.
 
   Lemma fixpoint_unfold : fixpoint f ≡ f (fixpoint f).
   Proof.
     apply equiv_dist=>n.
     rewrite fixpoint_eq /fixpoint_def (conv_compl n (fixpoint_chain f)) //.
+    rewrite /fixpoint_chain.
     induction n as [|n IH]; simpl; eauto using contractive_0, contractive_S.
   Qed.
 
@@ -324,34 +348,21 @@ Section fixpoint.
     - rewrite Hx fixpoint_unfold. apply (contractive_S _), IH.
   Qed.
 
-  Lemma fixpoint_ne (g : A → A) `{!Contractive g} n :
-    (∀ z, f z ≡{n}≡ g z) → fixpoint f ≡{n}≡ fixpoint g.
-  Proof.
-    intros Hfg. rewrite fixpoint_eq /fixpoint_def
-      (conv_compl n (fixpoint_chain f)) (conv_compl n (fixpoint_chain g)) /=.
-    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.
-  Proof. setoid_rewrite equiv_dist; naive_solver eauto using fixpoint_ne. Qed.
-
   Lemma fixpoint_ind (P : A → Prop) :
     Proper ((≡) ==> impl) P →
     (∃ x, P x) → (∀ x, P x → P (f x)) →
     LimitPreserving P →
     P (fixpoint f).
   Proof.
-    intros ? [x Hx] Hincr Hlim. set (chcar i := Nat.iter (S i) f x).
-    assert (Hcauch : ∀ n i : nat, n ≤ i → chcar i ≡{n}≡ chcar n).
-    { intros n. rewrite /chcar. induction n as [|n IH]=> -[|i] //=;
+    intros ? [x Hx] Hincr Hlim. set (ch i := Nat.iter (S i) f x).
+    assert (Cauchy ch) as Hcauch.
+    { intros n. rewrite /ch. induction n as [|n IH]=> -[|i] //=;
         eauto using contractive_0, contractive_S with lia. }
-    set (fp2 := compl {| chain_cauchy := Hcauch |}).
+    set (fp2 := compl ch).
     assert (f fp2 ≡ fp2).
-    { apply equiv_dist=>n. rewrite /fp2 (conv_compl n) /= /chcar.
+    { apply equiv_dist=>n. rewrite /fp2 (conv_compl n) //= /ch.
       induction n as [|n IH]; simpl; eauto using contractive_0, contractive_S. }
-    rewrite -(fixpoint_unique fp2) //.
-    apply Hlim=> n /=. by apply Nat_iter_ind.
+    rewrite -(fixpoint_unique fp2) //. apply Hlim=> // n. by apply Nat_iter_ind.
   Qed.
 End fixpoint.
 
@@ -361,9 +372,9 @@ Definition fixpointK `{Cofe A, Inhabited A} k (f : A → A)
   `{!Contractive (Nat.iter k f)} := fixpoint (Nat.iter k f).
 
 Section fixpointK.
-  Local Set Default Proof Using "Type*".
   Context `{Cofe A, Inhabited A} (f : A → A) (k : nat).
   Context {f_contractive : Contractive (Nat.iter k f)} {f_ne : NonExpansive f}.
+  Local Unset Default Proof Using.
   (* Note than f_ne is crucial here:  there are functions f such that f^2 is contractive,
      but f is not non-expansive.
      Consider for example f: SPred → SPred (where SPred is "downclosed sets of natural numbers").
@@ -392,13 +403,13 @@ Section fixpointK.
 
   Lemma fixpointK_unfold : fixpointK k f ≡ f (fixpointK k f).
   Proof.
-    symmetry. rewrite /fixpointK. apply fixpoint_unique.
+    symmetry. rewrite /fixpointK. apply (fixpoint_unique _).
     by rewrite -Nat_iter_S_r Nat_iter_S -fixpoint_unfold.
   Qed.
 
   Lemma fixpointK_unique (x : A) : x ≡ f x → x ≡ fixpointK k f.
   Proof.
-    intros Hf. apply fixpoint_unique. clear f_contractive.
+    intros Hf. apply (fixpoint_unique _). clear f_contractive.
     induction k as [|k' IH]=> //=. by rewrite -IH.
   Qed.
 
@@ -408,7 +419,7 @@ Section fixpointK.
 
     Lemma fixpointK_ne n : (∀ z, f z ≡{n}≡ g z) → fixpointK k f ≡{n}≡ fixpointK k g.
     Proof.
-      rewrite /fixpointK=> Hfg /=. apply fixpoint_ne=> z.
+      rewrite /fixpointK=> Hfg /=. apply fixpoint_ne=> z1 z2 Hz.
       clear f_contractive g_contractive.
       induction k as [|k' IH]=> //=. by rewrite IH Hfg.
     Qed.
@@ -430,23 +441,22 @@ End fixpointK.
 
 (** Mutual fixpoints *)
 Section fixpointAB.
-  Local Unset Default Proof Using.
-
   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 Unset Default Proof Using.
 
   Local Definition fixpoint_AB (x : A) : B := fixpoint (fB x).
-  Local Instance fixpoint_AB_contractive : Contractive fixpoint_AB.
+  Global Instance fixpoint_AB_contractive : Contractive fixpoint_AB.
   Proof.
-    intros n x x' Hx; rewrite /fixpoint_AB.
-    apply fixpoint_ne=> y. by f_contractive.
+    intros n x1 x2 Hx; rewrite /fixpoint_AB.
+    apply fixpoint_ne=> y1 y2 Hy. f_contractive. done. by apply dist_S.
   Qed.
 
   Local Definition fixpoint_AA (x : A) : A := fA x (fixpoint_AB x).
-  Local Instance fixpoint_AA_contractive : Contractive fixpoint_AA.
+  Global Instance fixpoint_AA_contractive : Contractive fixpoint_AA.
   Proof. solve_contractive. Qed.
 
   Definition fixpoint_A : A := fixpoint fixpoint_AA.
@@ -468,11 +478,11 @@ Section fixpointAB.
 
   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.
+    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.
+  Proof. intros. apply (fixpoint_unique _). by rewrite -fixpoint_A_unique. Qed.
 End fixpointAB.
 
 Section fixpointAB_ne.
@@ -483,20 +493,22 @@ Section fixpointAB_ne.
   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'}.
+  Local Unset Default Proof Using.
 
   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.
+    intros HfA HfB. apply fixpoint_ne=> z1 z2 Hz.
+    rewrite /fixpoint_AA /fixpoint_AB HfA. f_equiv; [by apply dist_dist_later|].
+    apply fixpoint_ne=> y1 y2 Hy. rewrite HfB. f_equiv; by apply dist_dist_later.
   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.
+    intros HfA HfB. apply fixpoint_ne=> y1 y2 Hy. rewrite HfB.
+    f_equiv; auto using dist_dist_later, fixpoint_A_ne.
   Qed.
 
   Lemma fixpoint_A_proper :
@@ -541,24 +553,25 @@ Section ofe_mor.
   Qed.
   Canonical Structure ofe_morO := OfeT (ofe_mor A B) ofe_mor_ofe_mixin.
 
-  Program Definition ofe_mor_chain (c : chain ofe_morO)
-    (x : A) : chain B := {| chain_car n := c n x |}.
-  Next Obligation. intros c x n i ?. by apply (chain_cauchy c). Qed.
   Program Definition ofe_mor_compl `{Cofe B} : Compl ofe_morO := λ c,
-    {| ofe_mor_car x := compl (ofe_mor_chain c x) |}.
+    λne x, compl (flip c x).
   Next Obligation.
-    intros ? c n x y Hx. by rewrite (conv_compl n (ofe_mor_chain c x))
-      (conv_compl n (ofe_mor_chain c y)) /= Hx.
+    intros ? c n x1 x2 Hx. apply compl_ne=> i /=. by rewrite Hx.
   Qed.
+
   Global Program Instance ofe_mor_cofe `{Cofe B} : Cofe ofe_morO :=
     {| compl := ofe_mor_compl |}.
   Next Obligation.
-    intros ? n c x; simpl.
-    by rewrite (conv_compl n (ofe_mor_chain c x)) /=.
+    intros ? n c1 c2 Hc x. rewrite /ofe_mor_compl /=.
+    apply compl_ne=> i. apply Hc.
+  Qed.
+  Next Obligation.
+    intros ? n c Hc x. assert (Cauchy (flip c x)).
+    { intros n' i ?. by apply Hc. }
+    by rewrite /ofe_mor_compl /= conv_compl.
   Qed.
 
-  Global Instance ofe_mor_car_ne :
-    NonExpansive2 (@ofe_mor_car A B).
+  Global Instance ofe_mor_car_ne : NonExpansive2 (@ofe_mor_car A B).
   Proof. intros n f g Hfg x y Hx; rewrite Hx; apply Hfg. Qed.
   Global Instance ofe_mor_car_proper :
     Proper ((≡) ==> (≡) ==> (≡)) (@ofe_mor_car A B) := ne_proper_2 _.
@@ -582,8 +595,7 @@ Definition ccompose {A B C}
   (f : B -n> C) (g : A -n> B) : A -n> C := OfeMor (f ∘ g).
 Instance: Params (@ccompose) 3 := {}.
 Infix "â—Ž" := ccompose (at level 40, left associativity).
-Global Instance ccompose_ne {A B C} :
-  NonExpansive2 (@ccompose A B C).
+Global Instance ccompose_ne {A B C} : NonExpansive2 (@ccompose A B C).
 Proof. intros n ?? Hf g1 g2 Hg x. rewrite /= (Hg x) (Hf (g2 x)) //. Qed.
 
 (* Function space maps *)
@@ -595,8 +607,7 @@ Proof. intros ??? ??? ???. by repeat apply ccompose_ne. Qed.
 
 Definition ofe_morO_map {A A' B B'} (f : A' -n> A) (g : B -n> B') :
   (A -n> B) -n> (A' -n>  B') := OfeMor (ofe_mor_map f g).
-Instance ofe_morO_map_ne {A A' B B'} :
-  NonExpansive2 (@ofe_morO_map A A' B B').
+Instance ofe_morO_map_ne {A A' B B'} : NonExpansive2 (@ofe_morO_map A A' B B').
 Proof.
   intros n f f' Hf g g' Hg ?. rewrite /= /ofe_mor_map.
   by repeat apply ccompose_ne.
@@ -625,6 +636,7 @@ Section empty.
 
   Global Program Instance Empty_set_cofe : Cofe Empty_setO := { compl x := x 0 }.
   Next Obligation. by repeat split; try exists 0. Qed.
+  Next Obligation. done. Qed.
 
   Global Instance Empty_set_ofe_discrete : OfeDiscrete Empty_setO.
   Proof. done. Qed.
@@ -635,8 +647,7 @@ Section product.
   Context {A B : ofeT}.
 
   Instance prod_dist : Dist (A * B) := λ n, prod_relation (dist n) (dist n).
-  Global Instance pair_ne :
-    NonExpansive2 (@pair A B) := _.
+  Global Instance pair_ne : NonExpansive2 (@pair A B) := _.
   Global Instance fst_ne : NonExpansive (@fst A B) := _.
   Global Instance snd_ne : NonExpansive (@snd A B) := _.
   Definition prod_ofe_mixin : OfeMixin (A * B).
@@ -650,11 +661,9 @@ Section product.
   Canonical Structure prodO : ofeT := OfeT (A * B) prod_ofe_mixin.
 
   Global Program Instance prod_cofe `{Cofe A, Cofe B} : Cofe prodO :=
-    { compl c := (compl (chain_map fst c), compl (chain_map snd c)) }.
-  Next Obligation.
-    intros ?? n c; split. apply (conv_compl n (chain_map fst c)).
-    apply (conv_compl n (chain_map snd c)).
-  Qed.
+    { compl c := (compl (fst <$> c), compl (snd <$> c)) }.
+  Next Obligation. intros ?? n c1 c2 Hc. split; apply compl_ne=> i; apply Hc. Qed.
+  Next Obligation. intros ?? n c ?. by rewrite /= !conv_compl. Qed.
 
   Global Instance prod_discrete (x : A * B) :
     Discrete (x.1) → Discrete (x.2) → Discrete x.
@@ -792,12 +801,14 @@ Section sum.
   Qed.
   Canonical Structure sumO : ofeT := OfeT (A + B) sum_ofe_mixin.
 
-  Program Definition inl_chain (c : chain sumO) (a : A) : chain A :=
-    {| chain_car n := match c n return _ with inl a' => a' | _ => a end |}.
-  Next Obligation. intros c a n i ?; simpl. by destruct (chain_cauchy c n i). Qed.
-  Program Definition inr_chain (c : chain sumO) (b : B) : chain B :=
-    {| chain_car n := match c n return _ with inr b' => b' | _ => b end |}.
-  Next Obligation. intros c b n i ?; simpl. by destruct (chain_cauchy c n i). Qed.
+  Definition inl_chain (c : chain sumO) (a : A) : chain A :=
+    λ n, match c n with inl a' => a' | _ => a end.
+  Instance inl_chain_cauchy c a : Cauchy c → Cauchy (inl_chain c a).
+  Proof. intros ? n i ?. rewrite /inl_chain. by destruct (cauchy c n i). Qed.
+  Definition inr_chain (c : chain sumO) (b : B) : chain B :=
+    λ n, match c n with inr b' => b' | _ => b end.
+  Instance inr_chain_cauchy c a : Cauchy c → Cauchy (inr_chain c a).
+  Proof. intros ? n i ?. rewrite /inr_chain. by destruct (cauchy c n i). Qed.
 
   Definition sum_compl `{Cofe A, Cofe B} : Compl sumO := λ c,
     match c 0 with
@@ -807,10 +818,15 @@ Section sum.
   Global Program Instance sum_cofe `{Cofe A, Cofe B} : Cofe sumO :=
     { compl := sum_compl }.
   Next Obligation.
-    intros ?? n c; rewrite /compl /sum_compl.
-    feed inversion (chain_cauchy c 0 n); first by auto with lia; constructor.
-    - rewrite (conv_compl n (inl_chain c _)) /=. destruct (c n); naive_solver.
-    - rewrite (conv_compl n (inr_chain c _)) /=. destruct (c n); naive_solver.
+    intros ?? n c1 c2 Hc. rewrite /sum_compl.
+    destruct (Hc 0); simpl; do 2 f_equiv; intros i;
+      rewrite /inl_chain /inr_chain; by destruct (Hc i).
+  Qed.
+  Next Obligation.
+    intros ?? n c ?; rewrite /compl /sum_compl.
+    feed inversion (cauchy c 0 n); first by auto with lia; constructor.
+    - rewrite (conv_compl n (inl_chain c _)) /inl_chain. destruct (c n); naive_solver.
+    - rewrite (conv_compl n (inr_chain c _)) /inr_chain. destruct (c n); naive_solver.
   Qed.
 
   Global Instance inl_discrete (x : A) : Discrete x → Discrete (inl x).
@@ -878,10 +894,8 @@ Section discrete_ofe.
 
   Global Program Instance discrete_cofe : Cofe (OfeT A discrete_ofe_mixin) :=
     { compl c := c 0 }.
-  Next Obligation.
-    intros n c. rewrite /compl /=;
-    symmetry; apply (chain_cauchy c 0 n). lia.
-  Qed.
+  Next Obligation. solve_proper. Qed.
+  Next Obligation. intros n c ?; simpl. rewrite (cauchy c 0 n); auto with lia. Qed.
 End discrete_ofe.
 
 Notation discreteO A := (OfeT A (discrete_ofe_mixin _)).
@@ -917,6 +931,9 @@ Section option.
   Lemma dist_option_Forall2 n mx my : mx ≡{n}≡ my ↔ option_Forall2 (dist n) mx my.
   Proof. done. Qed.
 
+  Global Instance Some_ne : NonExpansive (@Some A).
+  Proof. by constructor. Qed.
+
   Definition option_ofe_mixin : OfeMixin (option A).
   Proof.
     split.
@@ -928,25 +945,29 @@ Section option.
   Qed.
   Canonical Structure optionO := OfeT (option A) option_ofe_mixin.
 
-  Program Definition option_chain (c : chain optionO) (x : A) : chain A :=
-    {| chain_car n := default x (c n) |}.
-  Next Obligation. intros c x n i ?; simpl. by destruct (chain_cauchy c n i). Qed.
+  Definition option_chain (c : chain optionO) (x : A) : chain A :=
+    λ n, default x (c n).
+  Instance option_chain_cauchy c x : Cauchy c → Cauchy (option_chain c x).
+  Proof. intros ? n i ?. rewrite /option_chain. by destruct (cauchy c n i). Qed.
   Definition option_compl `{Cofe A} : Compl optionO := λ c,
     match c 0 with Some x => Some (compl (option_chain c x)) | None => None end.
   Global Program Instance option_cofe `{Cofe A} : Cofe optionO :=
     { compl := option_compl }.
   Next Obligation.
-    intros ? n c; rewrite /compl /option_compl.
-    feed inversion (chain_cauchy c 0 n); auto with lia; [].
-    constructor. rewrite (conv_compl n (option_chain c _)) /=.
+    intros ? n c1 c2 Hc. rewrite /option_compl.
+    destruct (Hc 0) as [x1 x2 Hx|]; last done.
+    f_equiv; f_equiv=> i. rewrite /option_chain. f_equiv; [done|apply Hc].
+  Qed.
+  Next Obligation.
+    intros ? n c ?; rewrite /compl /option_compl.
+    feed inversion (cauchy c 0 n); auto with lia; [].
+    constructor. rewrite (conv_compl n (option_chain c _)) /option_chain.
     destruct (c n); naive_solver.
   Qed.
 
   Global Instance option_ofe_discrete : OfeDiscrete A → OfeDiscrete optionO.
   Proof. destruct 2; constructor; by apply (discrete _). Qed.
 
-  Global Instance Some_ne : NonExpansive (@Some A).
-  Proof. by constructor. Qed.
   Global Instance is_Some_ne n : Proper (dist n ==> iff) (@is_Some A).
   Proof. destruct 1; split; eauto. Qed.
   Global Instance Some_dist_inj : Inj (dist n) (dist n) (@Some A).
@@ -1030,6 +1051,10 @@ Section later.
   Instance later_equiv : Equiv (later A) := λ x y, later_car x ≡ later_car y.
   Instance later_dist : Dist (later A) := λ n x y,
     dist_later n (later_car x) (later_car y).
+
+  Global Instance Next_contractive : Contractive (@Next A).
+  Proof. by intros [|n] x y. Qed.
+
   Definition later_ofe_mixin : OfeMixin (later A).
   Proof.
     split.
@@ -1043,17 +1068,17 @@ Section later.
   Qed.
   Canonical Structure laterO : ofeT := OfeT (later A) later_ofe_mixin.
 
-  Program Definition later_chain (c : chain laterO) : chain A :=
-    {| chain_car n := later_car (c (S n)) |}.
-  Next Obligation. intros c n i ?; apply (chain_cauchy c (S n)); lia. Qed.
+  Definition later_chain (c : chain laterO) : chain A :=
+    λ n, later_car (c (S n)).
+  Instance later_chain_cauchy c : Cauchy c → Cauchy (later_chain c).
+  Proof. intros ? n i ?; apply (cauchy c (S n)); lia. Qed.
   Global Program Instance later_cofe `{Cofe A} : Cofe laterO :=
     { compl c := Next (compl (later_chain c)) }.
+  Next Obligation. intros ? n c1 c2 Hc. f_contractive; f_equiv=> i. apply Hc. Qed.
   Next Obligation.
-    intros ? [|n] c; [done|by apply (conv_compl n (later_chain c))].
+    intros ? [|n] c ?; [done|]. apply (conv_compl n (later_chain c) _).
   Qed.
 
-  Global Instance Next_contractive : Contractive (@Next A).
-  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.
 
@@ -1157,12 +1182,14 @@ Section discrete_fun.
   Qed.
   Canonical Structure discrete_funO := OfeT (discrete_fun B) discrete_fun_ofe_mixin.
 
-  Program Definition discrete_fun_chain `(c : chain discrete_funO)
-    (x : A) : chain (B x) := {| chain_car n := c n x |}.
-  Next Obligation. intros c x n i ?. by apply (chain_cauchy c). Qed.
+  Definition discrete_fun_chain (c : chain discrete_funO) (x : A) : chain (B x) :=
+    λ n, c n x.
+  Instance discrete_fun_chain_cauchy c x : Cauchy c → Cauchy (discrete_fun_chain c x).
+  Proof. intros ? n i ?. by apply (cauchy c). Qed.
   Global Program Instance discrete_fun_cofe `{∀ x, Cofe (B x)} : Cofe discrete_funO :=
     { compl c x := compl (discrete_fun_chain c x) }.
-  Next Obligation. intros ? n c x. apply (conv_compl n (discrete_fun_chain c x)). Qed.
+  Next Obligation. intros ? n c1 c2 Hc x. f_equiv=> i. apply Hc. Qed.
+  Next Obligation. intros ? n c ? x. apply (conv_compl n (discrete_fun_chain c x) _). Qed.
 
   Global Instance discrete_fun_inhabited `{∀ x, Inhabited (B x)} : Inhabited discrete_funO :=
     populate (λ _, inhabitant).
@@ -1255,22 +1282,29 @@ Section iso_cofe_subtype.
   Proof. intros n y1 y2. apply g_dist. Qed.
   Existing Instance Hgne.
   Context (gf : ∀ x Hx, g (f x Hx) ≡ x).
-  Context (Hlimit : ∀ c : chain B, P (compl (chain_map g c))).
+  Context (Hlimit : ∀ c : chain B, P (compl (g <$> c))).
   Program Definition iso_cofe_subtype : Cofe B :=
-    {| compl c := f (compl (chain_map g c)) _ |}.
-  Next Obligation. apply Hlimit. Qed.
+    {| compl c := f (compl (g <$> c)) (Hlimit c) |}.
+  Next Obligation.
+    intros n c1 c2 Hc. apply g_dist. rewrite !gf. f_equiv=> i. apply g_dist, Hc.
+  Qed.
   Next Obligation.
-    intros n c; simpl. apply g_dist. by rewrite gf conv_compl.
+    intros n c ?; simpl. apply g_dist. by rewrite gf conv_compl.
   Qed.
 End iso_cofe_subtype.
 
+(*
 Lemma iso_cofe_subtype' {A B : ofeT} `{Cofe A}
   (P : A → Prop) (f : ∀ x, P x → B) (g : B → A)
   (Pg : ∀ y, P (g y))
   (g_dist : ∀ n y1 y2, y1 ≡{n}≡ y2 ↔ g y1 ≡{n}≡ g y2)
   (gf : ∀ x Hx, g (f x Hx) ≡ x)
   (Hlimit : LimitPreserving P) : Cofe B.
-Proof. apply: (iso_cofe_subtype P f g)=> // c. apply Hlimit=> ?; apply Pg. Qed.
+Proof. apply: (iso_cofe_subtype P f g)=> // c.
+
+
+ apply Hlimit. => ?. apply Pg. Qed.
+*)
 
 Definition iso_cofe {A B : ofeT} `{Cofe A} (f : A → B) (g : B → A)
   (g_dist : ∀ n y1 y2, y1 ≡{n}≡ y2 ↔ g y1 ≡{n}≡ g y2)
@@ -1301,7 +1335,7 @@ Section sigma.
   Canonical Structure sigO : ofeT := OfeT (sig P) sig_ofe_mixin.
 
   Global Instance sig_cofe `{Cofe A, !LimitPreserving P} : Cofe sigO.
-  Proof. apply (iso_cofe_subtype' P (exist P) proj1_sig)=> //. by intros []. Qed.
+  Proof. apply (iso_cofe_subtype' P (exist P) proj1_sig). => //. by intros []. Qed.
 
   Global Instance sig_discrete (x : sig P) :  Discrete (`x) → Discrete x.
   Proof. intros ? y. rewrite sig_dist_alt sig_equiv_alt. apply (discrete _). Qed.