diff --git a/_CoqProject b/_CoqProject
index 46417a25346bf0ed913857e8c0c4fff86c301306..0554a721b36a7cd81f48b48b133fb39b55698315 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -36,7 +36,6 @@ prelude/list.v
 prelude/error.v
 prelude/functions.v
 prelude/hlist.v
-algebra/option.v
 algebra/cmra.v
 algebra/cmra_big_op.v
 algebra/cmra_tactics.v
diff --git a/algebra/cmra.v b/algebra/cmra.v
index e9cc36887737969989d254fcbc31ca71444fa04a..27afdb0be10b5cf255d659319157698a520d76aa 100644
--- a/algebra/cmra.v
+++ b/algebra/cmra.v
@@ -441,6 +441,36 @@ Section cmra_monotone.
   Proof. rewrite !cmra_valid_validN; eauto using validN_preserving. Qed.
 End cmra_monotone.
 
+(** Functors *)
+Structure rFunctor := RFunctor {
+  rFunctor_car : cofeT → cofeT -> cmraT;
+  rFunctor_map {A1 A2 B1 B2} :
+    ((A2 -n> A1) * (B1 -n> B2)) → rFunctor_car A1 B1 -n> rFunctor_car A2 B2;
+  rFunctor_ne A1 A2 B1 B2 n :
+    Proper (dist n ==> dist n) (@rFunctor_map A1 A2 B1 B2);
+  rFunctor_id {A B} (x : rFunctor_car A B) : rFunctor_map (cid,cid) x ≡ x;
+  rFunctor_compose {A1 A2 A3 B1 B2 B3}
+      (f : A2 -n> A1) (g : A3 -n> A2) (f' : B1 -n> B2) (g' : B2 -n> B3) x :
+    rFunctor_map (f◎g, g'◎f') x ≡ rFunctor_map (g,g') (rFunctor_map (f,f') x);
+  rFunctor_mono {A1 A2 B1 B2} (fg : (A2 -n> A1) * (B1 -n> B2)) :
+    CMRAMonotone (rFunctor_map fg) 
+}.
+Existing Instances rFunctor_ne rFunctor_mono.
+Instance: Params (@rFunctor_map) 5.
+
+Class rFunctorContractive (F : rFunctor) :=
+  rFunctor_contractive A1 A2 B1 B2 :> Contractive (@rFunctor_map F A1 A2 B1 B2).
+
+Definition rFunctor_diag (F: rFunctor) (A: cofeT) : cmraT := rFunctor_car F A A.
+Coercion rFunctor_diag : rFunctor >-> Funclass.
+
+Program Definition constRF (B : cmraT) : rFunctor :=
+  {| rFunctor_car A1 A2 := B; rFunctor_map A1 A2 B1 B2 f := cid |}.
+Solve Obligations with done.
+
+Instance constRF_contractive B : rFunctorContractive (constRF B).
+Proof. rewrite /rFunctorContractive; apply _. Qed.
+
 (** * Transporting a CMRA equality *)
 Definition cmra_transport {A B : cmraT} (H : A = B) (x : A) : B :=
   eq_rect A id x _ H.
@@ -624,37 +654,6 @@ Proof.
   - intros x y; rewrite !prod_included=> -[??] /=.
     by split; apply included_preserving.
 Qed.
-
-(** Functors *)
-Structure rFunctor := RFunctor {
-  rFunctor_car : cofeT → cofeT -> cmraT;
-  rFunctor_map {A1 A2 B1 B2} :
-    ((A2 -n> A1) * (B1 -n> B2)) → rFunctor_car A1 B1 -n> rFunctor_car A2 B2;
-  rFunctor_ne A1 A2 B1 B2 n :
-    Proper (dist n ==> dist n) (@rFunctor_map A1 A2 B1 B2);
-  rFunctor_id {A B} (x : rFunctor_car A B) : rFunctor_map (cid,cid) x ≡ x;
-  rFunctor_compose {A1 A2 A3 B1 B2 B3}
-      (f : A2 -n> A1) (g : A3 -n> A2) (f' : B1 -n> B2) (g' : B2 -n> B3) x :
-    rFunctor_map (f◎g, g'◎f') x ≡ rFunctor_map (g,g') (rFunctor_map (f,f') x);
-  rFunctor_mono {A1 A2 B1 B2} (fg : (A2 -n> A1) * (B1 -n> B2)) :
-    CMRAMonotone (rFunctor_map fg) 
-}.
-Existing Instances rFunctor_ne rFunctor_mono.
-Instance: Params (@rFunctor_map) 5.
-
-Class rFunctorContractive (F : rFunctor) :=
-  rFunctor_contractive A1 A2 B1 B2 :> Contractive (@rFunctor_map F A1 A2 B1 B2).
-
-Definition rFunctor_diag (F: rFunctor) (A: cofeT) : cmraT := rFunctor_car F A A.
-Coercion rFunctor_diag : rFunctor >-> Funclass.
-
-Program Definition constRF (B : cmraT) : rFunctor :=
-  {| rFunctor_car A1 A2 := B; rFunctor_map A1 A2 B1 B2 f := cid |}.
-Solve Obligations with done.
-
-Instance constRF_contractive B : rFunctorContractive (constRF B).
-Proof. rewrite /rFunctorContractive; apply _. Qed.
-
 Program Definition prodRF (F1 F2 : rFunctor) : rFunctor := {|
   rFunctor_car A B := prodR (rFunctor_car F1 A B) (rFunctor_car F2 A B);
   rFunctor_map A1 A2 B1 B2 fg :=
@@ -676,3 +675,137 @@ Proof.
   intros ?? A1 A2 B1 B2 n ???;
     by apply prodC_map_ne; apply rFunctor_contractive.
 Qed.
+
+(** ** CMRA for the option type *)
+Section option.
+  Context {A : cmraT}.
+
+  Instance option_valid : Valid (option A) := λ mx,
+    match mx with Some x => ✓ x | None => True end.
+  Instance option_validN : ValidN (option A) := λ n mx,
+    match mx with Some x => ✓{n} x | None => True end.
+  Global Instance option_empty : Empty (option A) := None.
+  Instance option_core : Core (option A) := fmap core.
+  Instance option_op : Op (option A) := union_with (λ x y, Some (x ⋅ y)).
+
+  Definition Some_valid a : ✓ Some a ↔ ✓ a := reflexivity _.
+  Definition Some_op a b : Some (a â‹… b) = Some a â‹… Some b := eq_refl.
+
+  Lemma option_included (mx my : option A) :
+    mx ≼ my ↔ mx = None ∨ ∃ x y, mx = Some x ∧ my = Some y ∧ x ≼ y.
+  Proof.
+    split.
+    - 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_and?; auto;
+        setoid_subst; eauto using cmra_included_l.
+    - intros [->|(x&y&->&->&z&Hz)]; try (by exists my; destruct my; constructor).
+      by exists (Some z); constructor.
+  Qed.
+
+  Definition option_cmra_mixin  : CMRAMixin (option A).
+  Proof.
+    split.
+    - by intros n [x|]; destruct 1; constructor; cofe_subst.
+    - by destruct 1; constructor; cofe_subst.
+    - by destruct 1; rewrite /validN /option_validN //=; cofe_subst.
+    - intros [x|]; [apply cmra_valid_validN|done].
+    - intros n [x|]; unfold validN, option_validN; eauto using cmra_validN_S.
+    - intros [x|] [y|] [z|]; constructor; rewrite ?assoc; auto.
+    - intros [x|] [y|]; constructor; rewrite 1?comm; auto.
+    - by intros [x|]; constructor; rewrite cmra_core_l.
+    - by intros [x|]; constructor; rewrite cmra_core_idemp.
+    - intros mx my; rewrite !option_included ;intros [->|(x&y&->&->&?)]; auto.
+      right; exists (core x), (core y); eauto using cmra_core_preserving.
+    - intros n [x|] [y|]; rewrite /validN /option_validN /=;
+        eauto using cmra_validN_op_l.
+    - 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 n x y1 y2) as ([z1 z2]&?&?&?); auto.
+        { by inversion_clear Hx'. }
+        by exists (Some z1, Some z2); repeat constructor.
+      + by exists (Some x,None); inversion Hx'; repeat constructor.
+      + by exists (None,Some x); inversion Hx'; repeat constructor.
+      + exists (None,None); repeat constructor.
+  Qed.
+  Canonical Structure optionR :=
+    CMRAT (option A) option_cofe_mixin option_cmra_mixin.
+  Global Instance option_cmra_unit : CMRAUnit optionR.
+  Proof. split. done. by intros []. by inversion_clear 1. Qed.
+  Global Instance option_cmra_discrete : CMRADiscrete A → CMRADiscrete optionR.
+  Proof. split; [apply _|]. by intros [x|]; [apply (cmra_discrete_valid x)|]. Qed.
+
+  (** Misc *)
+  Global Instance Some_cmra_monotone : CMRAMonotone Some.
+  Proof. split; [apply _|done|intros x y [z ->]; by exists (Some z)]. Qed.
+  Lemma op_is_Some mx my : is_Some (mx ⋅ my) ↔ is_Some mx ∨ is_Some my.
+  Proof.
+    destruct mx, my; rewrite /op /option_op /= -!not_eq_None_Some; naive_solver.
+  Qed.
+  Lemma option_op_positive_dist_l n mx my : mx ⋅ my ≡{n}≡ None → mx ≡{n}≡ None.
+  Proof. by destruct mx, my; inversion_clear 1. Qed.
+  Lemma option_op_positive_dist_r n mx my : mx ⋅ my ≡{n}≡ None → my ≡{n}≡ None.
+  Proof. by destruct mx, my; inversion_clear 1. Qed.
+
+  Global Instance Some_persistent (x : A) : Persistent x → Persistent (Some x).
+  Proof. by constructor. Qed.
+  Global Instance option_persistent (mx : option A) :
+    (∀ x : A, Persistent x) → Persistent mx.
+  Proof. intros. destruct mx. apply _. apply cmra_unit_persistent. Qed.
+
+  (** Updates *)
+  Lemma option_updateP (P : A → Prop) (Q : option A → Prop) x :
+    x ~~>: P → (∀ y, P y → Q (Some y)) → Some x ~~>: Q.
+  Proof.
+    intros Hx Hy n [y|] ?.
+    { destruct (Hx n y) as (y'&?&?); auto. exists (Some y'); auto. }
+    destruct (Hx n (core x)) as (y'&?&?); rewrite ?cmra_core_r; auto.
+    by exists (Some y'); split; [auto|apply cmra_validN_op_l with (core x)].
+  Qed.
+  Lemma option_updateP' (P : A → Prop) x :
+    x ~~>: P → Some x ~~>: λ my, default False my P.
+  Proof. eauto using option_updateP. Qed.
+  Lemma option_update x y : x ~~> y → Some x ~~> Some y.
+  Proof.
+    rewrite !cmra_update_updateP; eauto using option_updateP with congruence.
+  Qed.
+  Lemma option_update_None `{Empty A, !CMRAUnit A} : ∅ ~~> Some ∅.
+  Proof.
+    intros n [x|] ?; rewrite /op /cmra_op /validN /cmra_validN /= ?left_id;
+      auto using cmra_unit_validN.
+  Qed.
+End option.
+
+Arguments optionR : clear implicits.
+
+Instance option_fmap_cmra_monotone {A B : cmraT} (f: A → B) `{!CMRAMonotone f} :
+  CMRAMonotone (fmap f : option A → option B).
+Proof.
+  split; first apply _.
+  - intros n [x|] ?; rewrite /cmra_validN //=. by apply (validN_preserving f).
+  - intros mx my; rewrite !option_included.
+    intros [->|(x&y&->&->&?)]; simpl; eauto 10 using @included_preserving.
+Qed.
+Program Definition optionRF (F : rFunctor) : rFunctor := {|
+  rFunctor_car A B := optionR (rFunctor_car F A B);
+  rFunctor_map A1 A2 B1 B2 fg := optionC_map (rFunctor_map F fg)
+|}.
+Next Obligation.
+  by intros F A1 A2 B1 B2 n f g Hfg; apply optionC_map_ne, rFunctor_ne.
+Qed.
+Next Obligation.
+  intros F A B x. rewrite /= -{2}(option_fmap_id x).
+  apply option_fmap_setoid_ext=>y; apply rFunctor_id.
+Qed.
+Next Obligation.
+  intros F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -option_fmap_compose.
+  apply option_fmap_setoid_ext=>y; apply rFunctor_compose.
+Qed.
+
+Instance optionRF_contractive F :
+  rFunctorContractive F → rFunctorContractive (optionRF F).
+Proof.
+  by intros ? A1 A2 B1 B2 n f g Hfg; apply optionC_map_ne, rFunctor_contractive.
+Qed.
diff --git a/algebra/cofe.v b/algebra/cofe.v
index c3cefe2fda4212b930c772f78146a9dbd1b8a814..8a157856080bf7dc78e9f4aa77a6672ea8dc6f7a 100644
--- a/algebra/cofe.v
+++ b/algebra/cofe.v
@@ -450,6 +450,91 @@ Proof. by intros x y. Qed.
 Canonical Structure natC := leibnizC nat.
 Canonical Structure boolC := leibnizC bool.
 
+(* Option *)
+Section option.
+  Context {A : cofeT}.
+
+  Inductive option_dist' (n : nat) : relation (option A) :=
+    | Some_dist x y : x ≡{n}≡ y → option_dist' n (Some x) (Some y)
+    | None_dist : option_dist' n None None.
+  Instance option_dist : Dist (option A) := option_dist'.
+
+  Lemma dist_option_Forall2 n mx my : mx ≡{n}≡ my ↔ option_Forall2 (dist n) mx my.
+  Proof. split; destruct 1; constructor; auto. Qed.
+
+  Program Definition option_chain (c : chain (option A)) (x : A) : chain A :=
+    {| chain_car n := from_option x (c n) |}.
+  Next Obligation. intros c x n i ?; simpl. by destruct (chain_cauchy c n i). Qed.
+  Instance option_compl : Compl (option A) := λ c,
+    match c 0 with Some x => Some (compl (option_chain c x)) | None => None end.
+
+  Definition option_cofe_mixin : CofeMixin (option A).
+  Proof.
+    split.
+    - intros mx my; split; [by destruct 1; constructor; apply equiv_dist|].
+      intros Hxy; destruct (Hxy 0); constructor; apply equiv_dist.
+      by intros n; feed inversion (Hxy n).
+    - intros n; split.
+      + by intros [x|]; constructor.
+      + by destruct 1; constructor.
+      + destruct 1; inversion_clear 1; constructor; etrans; eauto.
+    - destruct 1; constructor; by apply dist_S.
+    - intros n c; rewrite /compl /option_compl.
+      feed inversion (chain_cauchy c 0 n); first auto with lia; constructor.
+      rewrite (conv_compl n (option_chain c _)) /=. destruct (c n); naive_solver.
+  Qed.
+  Canonical Structure optionC := CofeT (option A) option_cofe_mixin.
+  Global Instance option_discrete : Discrete A → Discrete optionC.
+  Proof. destruct 2; constructor; by apply (timeless _). Qed.
+
+  Global Instance Some_ne : Proper (dist n ==> dist n) (@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).
+  Proof. by inversion_clear 1. Qed.
+  Global Instance from_option_ne n :
+    Proper (dist n ==> dist n ==> dist n) (@from_option A).
+  Proof. by destruct 2. Qed.
+
+  Global Instance None_timeless : Timeless (@None A).
+  Proof. inversion_clear 1; constructor. Qed.
+  Global Instance Some_timeless x : Timeless x → Timeless (Some x).
+  Proof. by intros ?; inversion_clear 1; constructor; apply timeless. Qed.
+End option.
+
+Arguments optionC : clear implicits.
+
+Instance option_fmap_ne {A B : cofeT} (f : A → B) n:
+  Proper (dist n ==> dist n) f → Proper (dist n==>dist n) (fmap (M:=option) f).
+Proof. by intros Hf; destruct 1; constructor; apply Hf. Qed.
+Definition optionC_map {A B} (f : A -n> B) : optionC A -n> optionC B :=
+  CofeMor (fmap f : optionC A → optionC B).
+Instance optionC_map_ne A B n : Proper (dist n ==> dist n) (@optionC_map A B).
+Proof. by intros f f' Hf []; constructor; apply Hf. Qed.
+
+Program Definition optionCF (F : cFunctor) : cFunctor := {|
+  cFunctor_car A B := optionC (cFunctor_car F A B);
+  cFunctor_map A1 A2 B1 B2 fg := optionC_map (cFunctor_map F fg)
+|}.
+Next Obligation.
+  by intros F A1 A2 B1 B2 n f g Hfg; apply optionC_map_ne, cFunctor_ne.
+Qed.
+Next Obligation.
+  intros F A B x. rewrite /= -{2}(option_fmap_id x).
+  apply option_fmap_setoid_ext=>y; apply cFunctor_id.
+Qed.
+Next Obligation.
+  intros F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -option_fmap_compose.
+  apply option_fmap_setoid_ext=>y; apply cFunctor_compose.
+Qed.
+
+Instance optionCF_contractive F :
+  cFunctorContractive F → cFunctorContractive (optionCF F).
+Proof.
+  by intros ? A1 A2 B1 B2 n f g Hfg; apply optionC_map_ne, cFunctor_contractive.
+Qed.
+
 (** Later *)
 Inductive later (A : Type) : Type := Next { later_car : A }.
 Add Printing Constructor later.
diff --git a/algebra/gmap.v b/algebra/gmap.v
index 30d2f51aa3959b88526ebc3f03f0743fe6ba158a..80a8399f067f04df5d0599ec44645ffe581e94fa 100644
--- a/algebra/gmap.v
+++ b/algebra/gmap.v
@@ -1,4 +1,4 @@
-From iris.algebra Require Export cmra option.
+From iris.algebra Require Export cmra.
 From iris.prelude Require Export gmap.
 From iris.algebra Require Import upred.
 
diff --git a/algebra/list.v b/algebra/list.v
index 581ba0665dead2dc3b7213f6db4e1d5ca32f0f23..47a509cefb7b824870dacc3862d4949741765d07 100644
--- a/algebra/list.v
+++ b/algebra/list.v
@@ -1,5 +1,5 @@
-From iris.algebra Require Import cmra option.
-From iris.prelude Require Import list.
+From iris.algebra Require Export cmra.
+From iris.prelude Require Export list.
 From iris.algebra Require Import upred.
 
 Section cofe.
diff --git a/algebra/option.v b/algebra/option.v
deleted file mode 100644
index c7e4b1bd8793b7811f887ebd1dbb75b1582e52b0..0000000000000000000000000000000000000000
--- a/algebra/option.v
+++ /dev/null
@@ -1,233 +0,0 @@
-From iris.algebra Require Export cmra.
-From iris.algebra Require Import upred.
-
-(* COFE *)
-Section cofe.
-Context {A : cofeT}.
-
-Inductive option_dist' (n : nat) : relation (option A) :=
-  | Some_dist x y : x ≡{n}≡ y → option_dist' n (Some x) (Some y)
-  | None_dist : option_dist' n None None.
-Instance option_dist : Dist (option A) := option_dist'.
-
-Lemma dist_option_Forall2 n mx my : mx ≡{n}≡ my ↔ option_Forall2 (dist n) mx my.
-Proof. split; destruct 1; constructor; auto. Qed.
-
-Program Definition option_chain (c : chain (option A)) (x : A) : chain A :=
-  {| chain_car n := from_option x (c n) |}.
-Next Obligation. intros c x n i ?; simpl. by destruct (chain_cauchy c n i). Qed.
-Instance option_compl : Compl (option A) := λ c,
-  match c 0 with Some x => Some (compl (option_chain c x)) | None => None end.
-
-Definition option_cofe_mixin : CofeMixin (option A).
-Proof.
-  split.
-  - intros mx my; split; [by destruct 1; constructor; apply equiv_dist|].
-    intros Hxy; destruct (Hxy 0); constructor; apply equiv_dist.
-    by intros n; feed inversion (Hxy n).
-  - intros n; split.
-    + by intros [x|]; constructor.
-    + by destruct 1; constructor.
-    + destruct 1; inversion_clear 1; constructor; etrans; eauto.
-  - destruct 1; constructor; by apply dist_S.
-  - intros n c; rewrite /compl /option_compl.
-    feed inversion (chain_cauchy c 0 n); first auto with lia; constructor.
-    rewrite (conv_compl n (option_chain c _)) /=. destruct (c n); naive_solver.
-Qed.
-Canonical Structure optionC := CofeT (option A) option_cofe_mixin.
-Global Instance option_discrete : Discrete A → Discrete optionC.
-Proof. destruct 2; constructor; by apply (timeless _). Qed.
-
-Global Instance Some_ne : Proper (dist n ==> dist n) (@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).
-Proof. by inversion_clear 1. Qed.
-Global Instance from_option_ne n :
-  Proper (dist n ==> dist n ==> dist n) (@from_option A).
-Proof. by destruct 2. Qed.
-
-Global Instance None_timeless : Timeless (@None A).
-Proof. inversion_clear 1; constructor. Qed.
-Global Instance Some_timeless x : Timeless x → Timeless (Some x).
-Proof. by intros ?; inversion_clear 1; constructor; apply timeless. Qed.
-End cofe.
-
-Arguments optionC : clear implicits.
-
-(* CMRA *)
-Section cmra.
-Context {A : cmraT}.
-
-Instance option_valid : Valid (option A) := λ mx,
-  match mx with Some x => ✓ x | None => True end.
-Instance option_validN : ValidN (option A) := λ n mx,
-  match mx with Some x => ✓{n} x | None => True end.
-Global Instance option_empty : Empty (option A) := None.
-Instance option_core : Core (option A) := fmap core.
-Instance option_op : Op (option A) := union_with (λ x y, Some (x ⋅ y)).
-
-Definition Some_valid a : ✓ Some a ↔ ✓ a := reflexivity _.
-Definition Some_op a b : Some (a â‹… b) = Some a â‹… Some b := eq_refl.
-
-Lemma option_included (mx my : option A) :
-  mx ≼ my ↔ mx = None ∨ ∃ x y, mx = Some x ∧ my = Some y ∧ x ≼ y.
-Proof.
-  split.
-  - 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_and?; auto;
-      setoid_subst; eauto using cmra_included_l.
-  - intros [->|(x&y&->&->&z&Hz)]; try (by exists my; destruct my; constructor).
-    by exists (Some z); constructor.
-Qed.
-
-Definition option_cmra_mixin  : CMRAMixin (option A).
-Proof.
-  split.
-  - by intros n [x|]; destruct 1; constructor; cofe_subst.
-  - by destruct 1; constructor; cofe_subst.
-  - by destruct 1; rewrite /validN /option_validN //=; cofe_subst.
-  - intros [x|]; [apply cmra_valid_validN|done].
-  - intros n [x|]; unfold validN, option_validN; eauto using cmra_validN_S.
-  - intros [x|] [y|] [z|]; constructor; rewrite ?assoc; auto.
-  - intros [x|] [y|]; constructor; rewrite 1?comm; auto.
-  - by intros [x|]; constructor; rewrite cmra_core_l.
-  - by intros [x|]; constructor; rewrite cmra_core_idemp.
-  - intros mx my; rewrite !option_included ;intros [->|(x&y&->&->&?)]; auto.
-    right; exists (core x), (core y); eauto using cmra_core_preserving.
-  - intros n [x|] [y|]; rewrite /validN /option_validN /=;
-      eauto using cmra_validN_op_l.
-  - 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 n x y1 y2) as ([z1 z2]&?&?&?); auto.
-      { by inversion_clear Hx'. }
-      by exists (Some z1, Some z2); repeat constructor.
-    + by exists (Some x,None); inversion Hx'; repeat constructor.
-    + by exists (None,Some x); inversion Hx'; repeat constructor.
-    + exists (None,None); repeat constructor.
-Qed.
-Canonical Structure optionR :=
-  CMRAT (option A) option_cofe_mixin option_cmra_mixin.
-Global Instance option_cmra_unit : CMRAUnit optionR.
-Proof. split. done. by intros []. by inversion_clear 1. Qed.
-Global Instance option_cmra_discrete : CMRADiscrete A → CMRADiscrete optionR.
-Proof. split; [apply _|]. by intros [x|]; [apply (cmra_discrete_valid x)|]. Qed.
-
-(** Misc *)
-Global Instance Some_cmra_monotone : CMRAMonotone Some.
-Proof. split; [apply _|done|intros x y [z ->]; by exists (Some z)]. Qed.
-Lemma op_is_Some mx my : is_Some (mx ⋅ my) ↔ is_Some mx ∨ is_Some my.
-Proof.
-  destruct mx, my; rewrite /op /option_op /= -!not_eq_None_Some; naive_solver.
-Qed.
-Lemma option_op_positive_dist_l n mx my : mx ⋅ my ≡{n}≡ None → mx ≡{n}≡ None.
-Proof. by destruct mx, my; inversion_clear 1. Qed.
-Lemma option_op_positive_dist_r n mx my : mx ⋅ my ≡{n}≡ None → my ≡{n}≡ None.
-Proof. by destruct mx, my; inversion_clear 1. Qed.
-
-Global Instance Some_persistent (x : A) : Persistent x → Persistent (Some x).
-Proof. by constructor. Qed.
-Global Instance option_persistent (mx : option A) :
-  (∀ x : A, Persistent x) → Persistent mx.
-Proof. intros. destruct mx. apply _. apply cmra_unit_persistent. Qed.
-
-(** Internalized properties *)
-Lemma option_equivI {M} (mx my : option A) :
-  (mx ≡ my) ⊣⊢ (match mx, my with
-                | Some x, Some y => x ≡ y | None, None => True | _, _ => False
-                end : uPred M).
-Proof.
-  uPred.unseal. do 2 split. by destruct 1. by destruct mx, my; try constructor.
-Qed.
-Lemma option_validI {M} (mx : option A) :
-  (✓ mx) ⊣⊢ (match mx with Some x => ✓ x | None => True end : uPred M).
-Proof. uPred.unseal. by destruct mx. Qed.
-
-(** Updates *)
-Lemma option_updateP (P : A → Prop) (Q : option A → Prop) x :
-  x ~~>: P → (∀ y, P y → Q (Some y)) → Some x ~~>: Q.
-Proof.
-  intros Hx Hy n [y|] ?.
-  { destruct (Hx n y) as (y'&?&?); auto. exists (Some y'); auto. }
-  destruct (Hx n (core x)) as (y'&?&?); rewrite ?cmra_core_r; auto.
-  by exists (Some y'); split; [auto|apply cmra_validN_op_l with (core x)].
-Qed.
-Lemma option_updateP' (P : A → Prop) x :
-  x ~~>: P → Some x ~~>: λ my, default False my P.
-Proof. eauto using option_updateP. Qed.
-Lemma option_update x y : x ~~> y → Some x ~~> Some y.
-Proof.
-  rewrite !cmra_update_updateP; eauto using option_updateP with congruence.
-Qed.
-Lemma option_update_None `{Empty A, !CMRAUnit A} : ∅ ~~> Some ∅.
-Proof.
-  intros n [x|] ?; rewrite /op /cmra_op /validN /cmra_validN /= ?left_id;
-    auto using cmra_unit_validN.
-Qed.
-End cmra.
-Arguments optionR : clear implicits.
-
-(** Functor *)
-Instance option_fmap_ne {A B : cofeT} (f : A → B) n:
-  Proper (dist n ==> dist n) f → Proper (dist n==>dist n) (fmap (M:=option) f).
-Proof. by intros Hf; destruct 1; constructor; apply Hf. Qed.
-Instance option_fmap_cmra_monotone {A B : cmraT} (f: A → B) `{!CMRAMonotone f} :
-  CMRAMonotone (fmap f : option A → option B).
-Proof.
-  split; first apply _.
-  - intros n [x|] ?; rewrite /cmra_validN //=. by apply (validN_preserving f).
-  - intros mx my; rewrite !option_included.
-    intros [->|(x&y&->&->&?)]; simpl; eauto 10 using @included_preserving.
-Qed.
-Definition optionC_map {A B} (f : A -n> B) : optionC A -n> optionC B :=
-  CofeMor (fmap f : optionC A → optionC B).
-Instance optionC_map_ne A B n : Proper (dist n ==> dist n) (@optionC_map A B).
-Proof. by intros f f' Hf []; constructor; apply Hf. Qed.
-
-Program Definition optionCF (F : cFunctor) : cFunctor := {|
-  cFunctor_car A B := optionC (cFunctor_car F A B);
-  cFunctor_map A1 A2 B1 B2 fg := optionC_map (cFunctor_map F fg)
-|}.
-Next Obligation.
-  by intros F A1 A2 B1 B2 n f g Hfg; apply optionC_map_ne, cFunctor_ne.
-Qed.
-Next Obligation.
-  intros F A B x. rewrite /= -{2}(option_fmap_id x).
-  apply option_fmap_setoid_ext=>y; apply cFunctor_id.
-Qed.
-Next Obligation.
-  intros F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -option_fmap_compose.
-  apply option_fmap_setoid_ext=>y; apply cFunctor_compose.
-Qed.
-
-Instance optionCF_contractive F :
-  cFunctorContractive F → cFunctorContractive (optionCF F).
-Proof.
-  by intros ? A1 A2 B1 B2 n f g Hfg; apply optionC_map_ne, cFunctor_contractive.
-Qed.
-
-Program Definition optionRF (F : rFunctor) : rFunctor := {|
-  rFunctor_car A B := optionR (rFunctor_car F A B);
-  rFunctor_map A1 A2 B1 B2 fg := optionC_map (rFunctor_map F fg)
-|}.
-Next Obligation.
-  by intros F A1 A2 B1 B2 n f g Hfg; apply optionC_map_ne, rFunctor_ne.
-Qed.
-Next Obligation.
-  intros F A B x. rewrite /= -{2}(option_fmap_id x).
-  apply option_fmap_setoid_ext=>y; apply rFunctor_id.
-Qed.
-Next Obligation.
-  intros F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -option_fmap_compose.
-  apply option_fmap_setoid_ext=>y; apply rFunctor_compose.
-Qed.
-
-Instance optionRF_contractive F :
-  rFunctorContractive F → rFunctorContractive (optionRF F).
-Proof.
-  by intros ? A1 A2 B1 B2 n f g Hfg; apply optionC_map_ne, rFunctor_contractive.
-Qed.
diff --git a/algebra/upred.v b/algebra/upred.v
index 0e31b28cfb31a275b85ee0c26303e96e6f5e370e..9c327233af9b737048351b502a98105913d9b43c 100644
--- a/algebra/upred.v
+++ b/algebra/upred.v
@@ -1091,6 +1091,18 @@ Proof.
   unseal=> ?. apply (anti_symm (⊢)); split=> n x ?; by apply (timeless_iff n).
 Qed.
 
+(* Option *)
+Lemma option_equivI {A : cofeT} (mx my : option A) :
+  (mx ≡ my) ⊣⊢ (match mx, my with
+                | Some x, Some y => x ≡ y | None, None => True | _, _ => False
+                end : uPred M).
+Proof.
+  uPred.unseal. do 2 split. by destruct 1. by destruct mx, my; try constructor.
+Qed.
+Lemma option_validI {A : cmraT} (mx : option A) :
+  (✓ mx) ⊣⊢ (match mx with Some x => ✓ x | None => True end : uPred M).
+Proof. uPred.unseal. by destruct mx. Qed.
+
 (* Timeless *)
 Lemma timelessP_spec P : TimelessP P ↔ ∀ n x, ✓{n} x → P 0 x → P n x.
 Proof.