diff --git a/_CoqProject b/_CoqProject
index 5098d4b6a402e3b6d57c33c703837c494671d7f1..e0d8ab8b51d57fd4b1b0be8831c10ec46a98d119 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -40,3 +40,4 @@ theories/typing/function.v
 theories/typing/programs.v
 theories/typing/borrow.v
 theories/typing/cont.v
+theories/typing/fixpoint.v
diff --git a/opam.pins b/opam.pins
index cf8bb509d842804cfde671f6522730f9c60e5196..5c7302b34a1e97280d08790970e644cefb751a4f 100644
--- a/opam.pins
+++ b/opam.pins
@@ -1 +1 @@
-coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 9c55bc2cb196512e08ad8756722ac127e539a1da
+coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 34eefd91027b10f99c930cbc15999fb7175a4168
diff --git a/theories/lifetime/definitions.v b/theories/lifetime/definitions.v
index f93130b6886e66342ca4e022c129a4de784c16a2..d98f4dd120fc4f9cfb45fc821bd135a61df8047a 100644
--- a/theories/lifetime/definitions.v
+++ b/theories/lifetime/definitions.v
@@ -281,16 +281,22 @@ Proof. apply (ne_proper_2 _). Qed.
 
 Global Instance idx_bor_ne κ i n : Proper (dist n ==> dist n) (idx_bor κ i).
 Proof. solve_proper. Qed.
+Global Instance idx_bor_contractive κ i : Contractive (idx_bor κ i).
+Proof. solve_contractive. Qed.
 Global Instance idx_bor_proper κ i : Proper ((≡) ==> (≡)) (idx_bor κ i).
 Proof. apply (ne_proper _). Qed.
 
 Global Instance raw_bor_ne i n : Proper (dist n ==> dist n) (raw_bor i).
 Proof. solve_proper. Qed.
+Global Instance raw_bor_contractive i : Contractive (raw_bor i).
+Proof. solve_contractive. Qed.
 Global Instance raw_bor_proper i : Proper ((≡) ==> (≡)) (raw_bor i).
 Proof. apply (ne_proper _). Qed.
 
 Global Instance bor_ne κ n : Proper (dist n ==> dist n) (bor κ).
 Proof. solve_proper. Qed.
+Global Instance bor_contractive κ : Contractive (bor κ).
+Proof. solve_contractive. Qed.
 Global Instance bor_proper κ : Proper ((≡) ==> (≡)) (bor κ).
 Proof. apply (ne_proper _). Qed.
 
diff --git a/theories/typing/bool.v b/theories/typing/bool.v
index 65de7b92faae3a77fc36ab5e13bf422cb9597ae5..ea832478422d397d89291f9ca198bfe338cca331 100644
--- a/theories/typing/bool.v
+++ b/theories/typing/bool.v
@@ -27,8 +27,7 @@ Section typing.
     typed_body E L C T e1 → typed_body E L C T e2 →
     typed_body E L C (TCtx_hasty p bool :: T) (if: p then e1 else e2).
   Proof.
-    (* FIXME why can't I merge these two iIntros? *)
-    iIntros (He1 He2). iIntros (tid qE) "#HEAP #LFT Htl HE HL HC".
+    iIntros (He1 He2 tid qE) "#HEAP #LFT Htl HE HL HC".
     rewrite tctx_interp_cons. iIntros "[Hp HT]".
     wp_bind p. iApply (wp_hasty with "Hp"). iIntros (v) "_ Hown".
     iDestruct "Hown" as (b) "Hv". iDestruct "Hv" as %[=->].
diff --git a/theories/typing/borrow.v b/theories/typing/borrow.v
index 5b1c1824b266a92a996adb36be58b9a373d14282..c61c66963ae838c7a83792787934302fefdd3c95 100644
--- a/theories/typing/borrow.v
+++ b/theories/typing/borrow.v
@@ -44,7 +44,7 @@ Section borrow.
       iMod (bor_sep _ _ _ (l' ↦∗: ty_own ty tid) with "LFT Hbor") as "[_ Hbor]". done.
       iMod ("Hclose" with "Htok") as "($ & $)".
       rewrite tctx_interp_singleton tctx_hasty_val' //. iExists _, _.
-      iFrame. iSplitR. done. by rewrite -uPred.iff_refl.
+      iFrame. iSplitR. done. rewrite -uPred.iff_refl. auto.
     - iFrame "H↦ H† Hown".
     - iIntros "!>(?&?&?)!>". iNext. iExists _.
       rewrite -heap_mapsto_vec_singleton. iFrame. iExists _. by iFrame.
@@ -123,5 +123,4 @@ Section borrow.
       rewrite tctx_interp_singleton tctx_hasty_val' //.
       iExists _. iSplitR. done. by iApply (ty_shr_mono with "LFT Hincl' Hshr").
   Qed.
-
 End borrow.
diff --git a/theories/typing/fixpoint.v b/theories/typing/fixpoint.v
new file mode 100644
index 0000000000000000000000000000000000000000..4d527fd0c0cef825e42fb66e6310eb0913b1596e
--- /dev/null
+++ b/theories/typing/fixpoint.v
@@ -0,0 +1,67 @@
+From lrust.lifetime Require Import definitions.
+From lrust.typing Require Export type bool.
+
+Section fixpoint.
+  Context `{typeG Σ}.
+
+  Global Instance type_inhabited : Inhabited type := populate bool.
+
+  Context (T : type → type) `{Contractive T}.
+
+  (* FIXME : Contrarily to the rule on paper, these rules are
+     coinductive: they let one assume [ty] is [Copy]/[Send]/[Sync] to
+     prove that [T ty] is [Copy]/[Send]/[Sync]. *)
+  Global Instance fixpoint_copy :
+    (∀ `(!Copy ty), Copy (T ty)) → Copy (fixpoint T).
+  Proof.
+    intros ?. apply fixpoint_ind.
+    - intros ??[[EQsz%leibniz_equiv EQown]EQshr].
+      specialize (λ tid vl, EQown tid vl). specialize (λ κ tid l, EQshr κ tid l).
+      simpl in *=>-[Hp Hsh]; (split; [intros ??|intros ???]).
+      + revert Hp. by rewrite /PersistentP -EQown.
+      + intros F l q. rewrite -EQsz -EQshr. setoid_rewrite <-EQown. auto.
+    - exists bool. apply _.
+    - done.
+    - intros c Hc. split.
+      + intros tid vl. apply uPred.equiv_entails, equiv_dist=>n.
+        by rewrite conv_compl uPred.always_always.
+      + intros κ tid E F l q ? ?.
+        apply uPred.entails_equiv_and, equiv_dist=>n. etrans.
+        { apply equiv_dist, uPred.entails_equiv_and, (copy_shr_acc κ tid E F)=>//.
+          by rewrite -conv_compl. }
+        do 2 f_equiv; first by rewrite conv_compl. do 8 (f_contractive || f_equiv).
+        * by rewrite -conv_compl.
+        * destruct n. done. by setoid_rewrite conv_compl.
+        * by rewrite -conv_compl.
+        * f_equiv. f_contractive. unfold dist_later. destruct n=>//.
+          by setoid_rewrite conv_compl.
+  Qed.
+
+  Global Instance fixpoint_send :
+    (∀ `(!Send ty), Send (T ty)) → Send (fixpoint T).
+  Proof.
+    intros ?. apply fixpoint_ind.
+    - intros ?? EQ ????. by rewrite -EQ.
+    - exists bool. apply _.
+    - done.
+    - intros c Hc ???. apply uPred.entails_equiv_and, equiv_dist=>n.
+      rewrite conv_compl. apply equiv_dist, uPred.entails_equiv_and; apply Hc.
+  Qed.
+
+  Global Instance fixpoint_sync :
+    (∀ `(!Sync ty), Sync (T ty)) → Sync (fixpoint T).
+  Proof.
+    intros ?. apply fixpoint_ind.
+    - intros ?? EQ ?????. by rewrite -EQ.
+    - exists bool. apply _.
+    - done.
+    - intros c Hc ????. apply uPred.entails_equiv_and, equiv_dist=>n.
+      rewrite conv_compl. apply equiv_dist, uPred.entails_equiv_and; apply Hc.
+  Qed.
+
+  Lemma fixpoint_unfold_eqtype E L : eqtype E L (fixpoint T) (T (fixpoint T)).
+  Proof.
+    unfold eqtype, subtype, type_incl. setoid_rewrite <-fixpoint_unfold.
+    split; iIntros "_ _ _"; (iSplit; first done); iSplit; iIntros "!#*$".
+  Qed.
+End fixpoint.
diff --git a/theories/typing/function.v b/theories/typing/function.v
index eeea31facbc0b892f1cfd555252873304b83d9c5..76c6fe6beb5f82adaf626d1cb5421cbc076924c0 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -4,6 +4,9 @@ From lrust.lifetime Require Import borrow.
 From lrust.typing Require Export type.
 From lrust.typing Require Import programs.
 
+(* TODO : prove contractiveness.
+   Prerequisite : cofe structure on lists and vectors. *)
+
 Section fn.
   Context `{typeG Σ}.
 
diff --git a/theories/typing/own.v b/theories/typing/own.v
index e02642a1b64b9b5f50594577a29b24658997c65f..9bec068d45e5ad765f049ddca8f55c2c2babe4a7 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -116,6 +116,17 @@ Section own.
     Proper (eqtype E L ==> eqtype E L) (own n).
   Proof. intros ?? Heq. split; f_equiv; apply Heq. Qed.
 
+  Global Instance own_contractive n : Contractive (own n).
+  Proof.
+    intros m ?? EQ. split; [split|]; simpl.
+    - done.
+    - destruct m=>// tid vl /=. repeat (apply EQ || f_contractive || f_equiv).
+    - intros κ tid l. repeat (apply EQ || f_contractive || f_equiv).
+  Qed.
+
+  Global Instance own_ne n m : Proper (dist m ==> dist m) (own n).
+  Proof. apply contractive_ne, _. Qed.
+
   Global Instance own_send n ty :
     Send ty → Send (own n ty).
   Proof.
@@ -198,5 +209,4 @@ Section typing.
     iApply (wp_delete with "[-]"); try (by auto); [].
     rewrite freeable_sz_full. by iFrame.
   Qed.
-
 End typing.
diff --git a/theories/typing/product.v b/theories/typing/product.v
index e1d8f2ce3ed62d24afb3cfa28ef7d2ed59443bda..bc59d38f7052aad033e3aa7cc7cc54b7062909c0 100644
--- a/theories/typing/product.v
+++ b/theories/typing/product.v
@@ -2,6 +2,9 @@ From iris.proofmode Require Import tactics.
 From lrust.lifetime Require Import borrow frac_borrow.
 From lrust.typing Require Export type.
 
+(* TODO : prove contractiveness.
+   Prerequisite : cofe structure on lists and vectors. *)
+
 Section product.
   Context `{typeG Σ}.
 
@@ -66,6 +69,16 @@ Section product.
     iSplitL "H1"; by iApply (ty_shr_mono with "LFT H⊑").
   Qed.
 
+  Global Instance product2_ne n:
+    Proper (dist n ==> dist n ==> dist n) product2.
+  Proof.
+    intros ?? EQ1 ?? EQ2. split; [split|]; simpl.
+    - by rewrite EQ1 EQ2.
+    - f_contractive. destruct n=>// tid vl.
+        by setoid_rewrite EQ1; setoid_rewrite EQ2.
+    - intros ???. by rewrite EQ1 EQ2.
+  Qed.
+
   Global Instance product2_mono E L:
     Proper (subtype E L ==> subtype E L ==> subtype E L) product2.
   Proof.
@@ -216,5 +229,4 @@ Section typing.
   Lemma prod_app E L tyl1 tyl2 :
     eqtype E L (Π[Π tyl1; Π tyl2]) (Π(tyl1 ++ tyl2)).
   Proof. by rewrite -prod_flatten_r -prod_flatten_l. Qed.
-
 End typing.
diff --git a/theories/typing/shr_bor.v b/theories/typing/shr_bor.v
index eb7f2f4cc325c5eec0fd276281599cdfc4a2c873..be0262334a488a58db7a6a0c1402028c340bc320 100644
--- a/theories/typing/shr_bor.v
+++ b/theories/typing/shr_bor.v
@@ -8,8 +8,7 @@ Section shr_bor.
   Context `{typeG Σ}.
 
   Program Definition shr_bor (κ : lft) (ty : type) : type :=
-    {| st_own tid vl :=
-         (∃ (l:loc), ⌜vl = [ #l ]⌝ ∗ ty.(ty_shr) κ tid l)%I |}.
+    {| st_own tid vl := (∃ (l:loc), ⌜vl = [ #l ]⌝ ∗ ty.(ty_shr) κ tid l)%I |}.
   Next Obligation.
     iIntros (κ ty tid vl) "H". iDestruct "H" as (l) "[% _]". by subst.
   Qed.
@@ -20,7 +19,7 @@ Section shr_bor.
     intros κ1 κ2 Hκ ty1 ty2 Hty. apply subtype_simple_type.
     iIntros (??) "#LFT #HE #HL H". iDestruct (Hκ with "HE HL") as "#Hκ".
     iDestruct "H" as (l) "(% & H)". subst. iExists _. iSplit. done.
-    iApply (ty2.(ty_shr_mono) with "LFT Hκ"). 
+    iApply (ty2.(ty_shr_mono) with "LFT Hκ").
     iDestruct (Hty with "* [] [] []") as "(_ & _ & #Hs1)"; [done..|clear Hty].
     by iApply "Hs1".
   Qed.
@@ -31,6 +30,15 @@ Section shr_bor.
     Proper (eqtype E L ==> eqtype E L) (shr_bor κ).
   Proof. intros ??[]. by split; apply subtype_shr_bor_mono. Qed.
 
+  Global Instance shr_contractive κ : Contractive (shr_bor κ).
+  Proof.
+    intros n ?? EQ. apply ty_of_st_ne. apply Next_contractive.
+    destruct n=>// tid vl /=. apply uPred.exist_ne.
+    repeat (apply EQ || f_contractive || f_equiv).
+  Qed.
+  Global Instance shr_ne κ n : Proper (dist n ==> dist n) (shr_bor κ).
+  Proof. apply contractive_ne, _. Qed.
+
   Global Instance shr_send κ ty :
     Sync ty → Send (shr_bor κ ty).
   Proof.
diff --git a/theories/typing/sum.v b/theories/typing/sum.v
index a55d5ee10ab60d9325ea51ac4ec88f00b4b6baee..2f33dc402f5010b668a9078bf048d7ce1d43ecd1 100644
--- a/theories/typing/sum.v
+++ b/theories/typing/sum.v
@@ -3,6 +3,9 @@ From iris.base_logic Require Import fractional.
 From lrust.lifetime Require Import borrow frac_borrow.
 From lrust.typing Require Export type.
 
+(* TODO : prove contractiveness.
+   Prerequisite : cofe structure on lists and vectors. *)
+
 Section sum.
   Context `{typeG Σ}.
 
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 51a4d8c963db81eb482d4af12806e6616a4d68b5..3d3ddae374b6ed40436a7f68ffc2365f14e78c7c 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -35,7 +35,7 @@ Section type.
          invariants, which does not need the mask.  Moreover, it is
          more consistent with thread-local tokens, which we do not
          give any.
- 
+
          The lifetime token is needed (a) to make the definition of simple types
          nicer (they would otherwise require a "∨ □|=>[†κ]"), and (b) so that
          we can have emp == sum [].
@@ -62,7 +62,7 @@ Section type.
     - rewrite -Nat.add_1_l Nat2Z.inj_add /= IHn shift_loc_assoc.
       set_solver+.
   Qed.
-  
+
   Lemma shr_locsE_disj l n m :
     shr_locsE l n ⊥ shr_locsE (shift_loc l n) m.
   Proof.
@@ -202,6 +202,146 @@ Coercion ty_of_st : simple_type >-> type.
 Delimit Scope lrust_type_scope with T.
 Bind Scope lrust_type_scope with type.
 
+(* OFE and COFE structures on types and simple types. *)
+Section ofe.
+  Context `{typeG Σ}.
+
+  Section def.
+    Definition tuple_of_type (ty : type) : prodC (prodC _ _) _ :=
+      (ty.(ty_size),
+       Next (ty.(ty_own) : _ -c> _ -c> _),
+       ty.(ty_shr) :  _ -c> _ -c> _ -c> _).
+
+    Instance type_equiv : Equiv type := λ ty1 ty2,
+       tuple_of_type ty1 ≡ tuple_of_type ty2.
+    Instance type_dist : Dist type := λ n ty1 ty2,
+       tuple_of_type ty1 ≡{n}≡ tuple_of_type ty2.
+
+    Definition type_ofe_mixin : OfeMixin type.
+    Proof.
+      split; [|split|]; unfold equiv, dist, type_equiv, type_dist.
+      - intros. apply equiv_dist.
+      - by intros ?.
+      - by intros ???.
+      - by intros ???->.
+      - by intros ????; apply dist_S.
+    Qed.
+
+    Canonical Structure typeC : ofeT := OfeT type type_ofe_mixin.
+
+    Instance st_equiv : Equiv simple_type := λ st1 st2,
+      @Next (_ -c> _ -c> _) st1.(st_own) ≡ Next st2.(st_own).
+    Instance st_dist : Dist simple_type := λ n st1 st2,
+      @Next (_ -c> _ -c> _) st1.(st_own) ≡{n}≡ Next st2.(st_own).
+
+    Definition st_ofe_mixin : OfeMixin simple_type.
+    Proof.
+      split; [|split|]; unfold equiv, dist, st_equiv, st_dist.
+      - intros. apply equiv_dist.
+      - by intros ?.
+      - by intros ???.
+      - by intros ???->.
+      - by intros ????; apply dist_S.
+    Qed.
+
+    Canonical Structure simple_typeC : ofeT := OfeT simple_type st_ofe_mixin.
+  End def.
+
+  Global Instance ty_size_proper_d n:
+    Proper (dist n ==> eq) ty_size.
+  Proof. intros ?? EQ. apply EQ. Qed.
+  Global Instance ty_size_proper_e :
+    Proper ((≡) ==> eq) ty_size.
+  Proof. intros ?? EQ. apply EQ. Qed.
+  Global Instance ty_own_ne n:
+    Proper (dist (S n) ==> eq ==> eq ==> dist n) ty_own.
+  Proof. intros ?? EQ ??-> ??->. apply EQ. Qed.
+  Global Instance ty_own_proper_e:
+    Proper ((≡) ==> eq ==> eq ==> (≡)) ty_own.
+  Proof. intros ?? EQ ??-> ??->. apply EQ. Qed.
+  Global Instance ty_shr_ne n:
+    Proper (dist n ==> eq ==> eq ==> eq ==> dist n) ty_shr.
+  Proof. intros ?? EQ ??-> ??-> ??->. apply EQ. Qed.
+  Global Instance ty_shr_proper_e :
+    Proper ((≡) ==> eq ==> eq ==> eq ==> (≡)) ty_shr.
+  Proof. intros ?? EQ ??-> ??-> ??->. apply EQ. Qed.
+  Global Instance st_own_ne n:
+    Proper (dist (S n) ==> eq ==> eq ==> dist n) st_own.
+  Proof. intros ?? EQ ??-> ??->. apply EQ. Qed.
+  Global Instance st_own_proper_e :
+    Proper ((≡) ==> eq ==> eq ==> (≡)) st_own.
+  Proof. intros ?? EQ ??-> ??->. apply EQ. Qed.
+
+  Global Program Instance type_cofe : Cofe typeC :=
+    {| compl c :=
+         let '(ty_size, Next ty_own, ty_shr) :=
+             compl {| chain_car := tuple_of_type ∘ c |}
+         in
+         {| ty_size := ty_size; ty_own := ty_own; ty_shr := ty_shr |}
+    |}.
+  Next Obligation. intros [c Hc]. apply Hc. Qed.
+  Next Obligation.
+    simpl. intros c _ _ shr [=_ _ ->] κ tid l.
+    apply uPred.equiv_entails, equiv_dist=>n.
+    by rewrite (λ c, conv_compl (A:=_ -c> _ -c> _ -c> _) n c κ tid l) /=
+               uPred.always_always.
+  Qed.
+  Next Obligation.
+    simpl. intros c sz own _ [=-> -> _] tid vl.
+    apply uPred.entails_equiv_and, equiv_dist=>n.
+    rewrite (λ c, conv_compl (A:=_ -c> _ -c> _) n c tid vl) /= conv_compl /=.
+    apply equiv_dist, uPred.entails_equiv_and, ty_size_eq.
+  Qed.
+  Next Obligation.
+    simpl. intros c _ own shr [=_ -> ->] E κ l tid q ?.
+    apply uPred.entails_equiv_and, equiv_dist=>n.
+    rewrite (λ c, conv_compl (A:=_ -c> _ -c> _ -c> _) n c κ tid l) /=.
+    setoid_rewrite (λ c vl, conv_compl (A:=_ -c> _ -c> _) n c tid vl). simpl.
+    etrans. { by apply equiv_dist, uPred.entails_equiv_and, (c n).(ty_share). }
+    simpl. destruct n; repeat (simpl; (f_contractive || f_equiv)).
+    rewrite (c.(chain_cauchy) (S n) (S (S n))) //. lia.
+  Qed.
+  Next Obligation.
+    simpl. intros c _ _ shr [=_ _ ->] κ κ' tid l.
+    apply uPred.entails_equiv_and, equiv_dist=>n.
+    rewrite !(λ c, conv_compl (A:=_ -c> _ -c> _ -c> _) n c _ tid l) /=.
+    apply equiv_dist, uPred.entails_equiv_and. apply ty_shr_mono.
+  Qed.
+  Next Obligation.
+    intros n c. split; [split|]; simpl; try by rewrite conv_compl.
+    f_contractive. destruct n; first done. rewrite /= conv_compl //.
+  Qed.
+
+  Global Program Instance simple_type_cofe : Cofe simple_typeC :=
+    {| compl c :=
+         let 'Next st_own := compl
+                {| chain_car := Next ∘ (st_own : _ -> _ -c> _ -c> _) ∘ c |} in
+         {| st_own := st_own |}
+    |}.
+  Next Obligation. intros [c Hc]. apply Hc. Qed.
+  Next Obligation.
+    simpl. intros c own [=->] tid vl.
+    apply uPred.entails_equiv_and, equiv_dist=>n.
+    rewrite (λ c, conv_compl (A:=_ -c> _ -c> _) n c tid vl) /=.
+    apply equiv_dist, uPred.entails_equiv_and, st_size_eq.
+  Qed.
+  Next Obligation.
+    simpl. intros c own [=->] tid vl.
+    apply uPred.equiv_entails, equiv_dist=>n.
+    by rewrite (λ c, conv_compl (A:=_ -c> _ -c> _) n c tid vl) /=
+               uPred.always_always.
+  Qed.
+  Next Obligation.
+    intros n c. apply Next_contractive. destruct n=>//=. rewrite conv_compl //.
+  Qed.
+
+  Global Instance ty_of_st_ne n : Proper (dist n ==> dist n) ty_of_st.
+  Proof.
+    intros [][]EQ. split;[split|]=>//= κ tid l.
+    repeat (f_contractive || f_equiv). apply EQ.
+  Qed.
+End ofe.
+
 Section subtyping.
   Context `{typeG Σ}.
   Definition type_incl (ty1 ty2 : type) : iProp Σ :=
diff --git a/theories/typing/uninit.v b/theories/typing/uninit.v
index f25c3d1f1415fd98b56b5db032d1e698257a8085..6153466d31c78feb7a2f2101a1d2d5124b5091a8 100644
--- a/theories/typing/uninit.v
+++ b/theories/typing/uninit.v
@@ -11,7 +11,7 @@ Section uninit.
 
   Global Instance uninit_1_send : Send uninit_1.
   Proof. iIntros (tid1 tid2 vl) "H". done. Qed.
-    
+
   Definition uninit (n : nat) : type :=
     Π (replicate n uninit_1).
 
@@ -44,5 +44,5 @@ Section uninit.
       + iIntros (Heq). destruct n; first done. simpl.
         iExists [v], vl. iSplit; first done. iSplit; first done.
         iApply "IH". by inversion Heq.
-  Qed. 
+  Qed.
 End uninit.
diff --git a/theories/typing/uniq_bor.v b/theories/typing/uniq_bor.v
index 1f2ca93a026ada43c707c0b62a8ae7c987f73184..3d21619697f3072b5317c85ff3fce5b703bfc1ac 100644
--- a/theories/typing/uniq_bor.v
+++ b/theories/typing/uniq_bor.v
@@ -20,7 +20,7 @@ Section uniq_bor.
           The trouble with this definition is that bor_unnest as proven is too
           weak. The original unnesting with open borrows was strong enough. *)
        ty_own tid vl :=
-         (∃ (l:loc) P, (⌜vl = [ #l ]⌝ ∗ □ (P ↔ l ↦∗: ty.(ty_own) tid)) ∗ &{κ} P)%I;
+         (∃ (l:loc) P, (⌜vl = [ #l ]⌝ ∗ ▷ □ (P ↔ l ↦∗: ty.(ty_own) tid)) ∗ &{κ} P)%I;
        ty_shr κ' tid l :=
          (∃ l':loc, &frac{κ'}(λ q', l ↦{q'} #l') ∗
             □ ∀ F q, ⌜↑shrN ∪ lftE ⊆ F⌝ -∗ q.[κ∪κ']
@@ -81,7 +81,7 @@ Section uniq_bor.
     iSplit; iAlways.
     - iIntros (??) "H". iDestruct "H" as (l P) "[[% #HPiff] Hown]". subst.
       iExists _, _. iSplitR; last by iApply (bor_shorten with "Hκ"). iSplit. done.
-      iIntros "!#". iSplit; iIntros "H".
+      iNext. iIntros "!#". iSplit; iIntros "H".
       + iDestruct ("HPiff" with "H") as (vl) "[??]". iExists vl. iFrame.
         by iApply "Ho1".
       + iDestruct "H" as (vl) "[??]". iApply "HPiff". iExists vl. iFrame.
@@ -104,11 +104,21 @@ Section uniq_bor.
     Proper (eqtype E L ==> eqtype E L) (uniq_bor κ).
   Proof. split; by apply subtype_uniq_mono. Qed.
 
+  Global Instance uniq_contractive κ : Contractive (uniq_bor κ).
+  Proof.
+    intros n ?? EQ. split; [split|]; simpl.
+    - done.
+    - destruct n=>// tid vl /=. repeat (apply EQ || f_contractive || f_equiv).
+    - intros κ' tid l. repeat (apply EQ || f_contractive || f_equiv).
+  Qed.
+  Global Instance uniq_ne κ n : Proper (dist n ==> dist n) (uniq_bor κ).
+  Proof. apply contractive_ne, _. Qed.
+
   Global Instance uniq_send κ ty :
     Send ty → Send (uniq_bor κ ty).
   Proof.
     iIntros (Hsend tid1 tid2 vl) "H". iDestruct "H" as (l P) "[[% #HPiff] H]".
-    iExists _, _. iFrame "H". iSplit; first done. iAlways. iSplit.
+    iExists _, _. iFrame "H". iSplit; first done. iNext. iAlways. iSplit.
     - iIntros "HP". iApply (heap_mapsto_pred_wand with "[HP]").
       { by iApply "HPiff". }
       clear dependent vl. iIntros (vl) "?". by iApply Hsend.
@@ -138,14 +148,14 @@ Section typing.
     iIntros (Hκ ???) "#LFT HE HL Huniq".
     iMod (Hκ with "HE HL") as (q) "[Htok Hclose]"; [try done..|].
     rewrite /tctx_interp !big_sepL_singleton /=.
-    iDestruct "Huniq" as (v) "[% Huniq]". 
+    iDestruct "Huniq" as (v) "[% Huniq]".
     iDestruct "Huniq" as (l P) "[[% #HPiff] HP]".
     iMod (bor_iff with "LFT [] HP") as "H↦". set_solver. by eauto.
     iMod (ty.(ty_share) with "LFT H↦ Htok") as "[Hown Htok]"; [solve_ndisj|].
     iMod ("Hclose" with "Htok") as "[$ $]". iExists _. iFrame "%".
     iIntros "!>/=". eauto.
   Qed.
-  
+
   Lemma tctx_reborrow_uniq E L p ty κ κ' :
     lctx_lft_incl E L κ' κ →
     tctx_incl E L [TCtx_hasty p (&uniq{κ}ty)]
@@ -185,7 +195,7 @@ Section typing.
   Lemma write_uniq E L κ ty :
     lctx_lft_alive E L κ → typed_write E L (&uniq{κ}ty) ty (&uniq{κ}ty).
   Proof.
-    iIntros (Halive p tid F qE qL ?) "#LFT HE HL Hown". 
+    iIntros (Halive p tid F qE qL ?) "#LFT HE HL Hown".
     iMod (Halive with "HE HL") as (q) "[Htok Hclose]"; first set_solver.
     iDestruct "Hown" as (l P) "[[EQ #HP] H↦]". iDestruct "EQ" as %[=->].
     iMod (bor_iff with "LFT [] H↦") as "H↦". set_solver. by eauto.
@@ -197,5 +207,4 @@ Section typing.
     iMod ("Hclose" with "Htok") as "($ & $ & $)".
     iExists _, _. erewrite <-uPred.iff_refl. auto.
   Qed.
-
 End typing.