diff --git a/CHANGELOG.md b/CHANGELOG.md
index d10badce458550810d01b51979a7dbf457b491da..420d3949fb4354fc3b6c5a0b55d6b7f8969c9090 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -79,6 +79,8 @@ Coq development, but not every API-breaking change is listed.  Changes marked
   - Use the non-`_inv` names (that freed up) for the forwards directions:
    `reducible_fill`, `reducible_no_obs_fill`, `irreducible_fill_inv`.
 * The tactic `iAssumption` also recognizes assumptions `⊢ P` in the Coq context.
+* Add notion `ofe_iso A B` that states that OFEs `A` and `B` are isomorphic.
+* Make use of `ofe_iso` in the COFE solver.
 
 **Changes in heap_lang:**
 
diff --git a/theories/algebra/cofe_solver.v b/theories/algebra/cofe_solver.v
index eb85e390096886927603315ade17aee080ecea41..2cb91a39acb0122f2c9e5ee9d3953e6144dd9b17 100644
--- a/theories/algebra/cofe_solver.v
+++ b/theories/algebra/cofe_solver.v
@@ -4,13 +4,8 @@ Set Default Proof Using "Type".
 Record solution (F : oFunctor) := Solution {
   solution_car :> ofeT;
   solution_cofe : Cofe solution_car;
-  solution_unfold : solution_car -n> F solution_car _;
-  solution_fold : F solution_car _ -n> solution_car;
-  solution_fold_unfold X : solution_fold (solution_unfold X) ≡ X;
-  solution_unfold_fold X : solution_unfold (solution_fold X) ≡ X
+  solution_iso :> ofe_iso (F solution_car _) solution_car;
 }.
-Arguments solution_unfold {_} _.
-Arguments solution_fold {_} _.
 Existing Instance solution_cofe.
 
 Module solver. Section solver.
@@ -210,7 +205,7 @@ Proof. by intros n X Y HXY k; rewrite /fold /= HXY. Qed.
 
 Theorem result : solution F.
 Proof using Type*.
-  apply (Solution F T _ (OfeMor unfold) (OfeMor fold)).
+  refine (Solution F T _ (OfeIso (OfeMor fold) (OfeMor unfold) _ _)).
   - move=> X /=. rewrite equiv_dist=> n k; rewrite /unfold /fold /=.
     rewrite -g_tower -(gg_tower _ n); apply (_ : Proper (_ ==> _) (g _)).
     trans (map (ff n, gg n) (X (S (n + k)))).
diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index 4eae60614245cb06c1c17ddc3318b74949a2c988..f8563361ea3e7f509f2665c8ceff7ccab8d60647 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -609,7 +609,7 @@ Proof.
   by repeat apply ccompose_ne.
 Qed.
 
-(** unit *)
+(** * Unit type *)
 Section unit.
   Instance unit_dist : Dist unit := λ _ _ _, True.
   Definition unit_ofe_mixin : OfeMixin unit.
@@ -623,7 +623,7 @@ Section unit.
   Proof. done. Qed.
 End unit.
 
-(** empty *)
+(** * Empty type *)
 Section empty.
   Instance Empty_set_dist : Dist Empty_set := λ _ _ _, True.
   Definition Empty_set_ofe_mixin : OfeMixin Empty_set.
@@ -637,7 +637,7 @@ Section empty.
   Proof. done. Qed.
 End empty.
 
-(** Product *)
+(** * Product type *)
 Section product.
   Context {A B : ofeT}.
 
@@ -684,7 +684,7 @@ Instance prodO_map_ne {A A' B B'} :
   NonExpansive2 (@prodO_map A A' B B').
 Proof. intros n f f' Hf g g' Hg [??]; split; [apply Hf|apply Hg]. Qed.
 
-(** COFE → OFE Functors *)
+(** * COFE → OFE Functors *)
 Record oFunctor := OFunctor {
   oFunctor_car : ∀ A `{!Cofe A} B `{!Cofe B}, ofeT;
   oFunctor_map `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :
@@ -778,7 +778,7 @@ Proof.
   apply ofe_morO_map_ne; apply oFunctor_contractive; destruct n, Hfg; by split.
 Qed.
 
-(** Sum *)
+(** * Sum type *)
 Section sum.
   Context {A B : ofeT}.
 
@@ -867,7 +867,7 @@ Proof.
     by apply sumO_map_ne; apply oFunctor_contractive.
 Qed.
 
-(** Discrete OFE *)
+(** * Discrete OFEs *)
 Section discrete_ofe.
   Context `{Equiv A} (Heq : @Equivalence A (≡)).
 
@@ -919,7 +919,7 @@ Canonical Structure positiveO := leibnizO positive.
 Canonical Structure NO := leibnizO N.
 Canonical Structure ZO := leibnizO Z.
 
-(* Option *)
+(** * Option type *)
 Section option.
   Context {A : ofeT}.
 
@@ -1024,7 +1024,7 @@ Proof.
   by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply optionO_map_ne, oFunctor_contractive.
 Qed.
 
-(** Later *)
+(** * Later type *)
 (** Note that the projection [later_car] is not non-expansive (see also the
 lemma [later_car_anti_contractive] below), so it cannot be used in the logic.
 If you need to get a witness out, you should use the lemma [Next_uninj]
@@ -1073,7 +1073,8 @@ Section later.
     Proper (dist n ==> dist_later n) later_car.
   Proof. move=> [x] [y] /= Hxy. done. Qed.
 
-  (* f is contractive iff it can factor into `Next` and a non-expansive function. *)
+  (** [f] is contractive iff it can factor into [Next] and a non-expansive
+  function. *)
   Lemma contractive_alt {B : ofeT} (f : A → B) :
     Contractive f ↔ ∃ g : later A → B, NonExpansive g ∧ ∀ x, f x ≡ g (Next x).
   Proof.
@@ -1132,7 +1133,7 @@ Proof.
   destruct n as [|n]; simpl in *; first done. apply oFunctor_ne, Hfg.
 Qed.
 
-(** Dependently-typed functions over a discrete domain *)
+(** * Dependently-typed functions over a discrete domain *)
 (** This separate notion is useful whenever we need dependent functions, and
 whenever we want to avoid the hassle of the bundled non-expansive function type.
 
@@ -1244,7 +1245,7 @@ Proof.
   by apply discrete_funO_map_ne=>c; apply oFunctor_contractive.
 Qed.
 
-(** Constructing isomorphic OFEs *)
+(** * Constructing isomorphic OFEs *)
 Lemma iso_ofe_mixin {A : ofeT} `{Equiv B, Dist B} (g : B → A)
   (g_equiv : ∀ y1 y2, y1 ≡ y2 ↔ g y1 ≡ g y2)
   (g_dist : ∀ n y1 y2, y1 ≡{n}≡ y2 ↔ g y1 ≡{n}≡ g y2) : OfeMixin B.
@@ -1287,7 +1288,7 @@ Definition iso_cofe {A B : ofeT} `{Cofe A} (f : A → B) (g : B → A)
   (gf : ∀ x, g (f x) ≡ x) : Cofe B.
 Proof. by apply (iso_cofe_subtype (λ _, True) (λ x _, f x) g). Qed.
 
-(** Sigma *)
+(** * Sigma type *)
 Section sigma.
   Context {A : ofeT} {P : A → Prop}.
   Implicit Types x : sig P.
@@ -1321,8 +1322,9 @@ End sigma.
 
 Arguments sigO {_} _.
 
-(** Ofe for [sigT]. The first component must be discrete
-    and use Leibniz equality, while the second component might be any OFE. *)
+(** * SigmaT type *)
+(** Ofe for [sigT]. The first component must be discrete and use Leibniz
+equality, while the second component might be any OFE. *)
 Section sigT.
   Import EqNotations.
 
@@ -1519,3 +1521,85 @@ Arguments sigTOF {_} _%OF.
 
 Notation "{ x  &  P }" := (sigTOF (λ x, P%OF)) : oFunctor_scope.
 Notation "{ x : A &  P }" := (@sigTOF A%type (λ x, P%OF)) : oFunctor_scope.
+
+(** * Isomorphisms between OFEs *)
+Record ofe_iso (A B : ofeT) := OfeIso {
+  ofe_iso_1 : A -n> B;
+  ofe_iso_2 : B -n> A;
+  ofe_iso_12 y : ofe_iso_1 (ofe_iso_2 y) ≡ y;
+  ofe_iso_21 x : ofe_iso_2 (ofe_iso_1 x) ≡ x;
+}.
+Arguments OfeIso {_ _} _ _ _ _.
+Arguments ofe_iso_1 {_ _} _.
+Arguments ofe_iso_2 {_ _} _.
+Arguments ofe_iso_12 {_ _} _ _.
+Arguments ofe_iso_21 {_ _} _ _.
+
+Section ofe_iso.
+  Context {A B : ofeT}.
+
+  Instance ofe_iso_equiv : Equiv (ofe_iso A B) := λ I1 I2,
+    ofe_iso_1 I1 ≡ ofe_iso_1 I2 ∧ ofe_iso_2 I1 ≡ ofe_iso_2 I2.
+
+  Instance ofe_iso_dist : Dist (ofe_iso A B) := λ n I1 I2,
+    ofe_iso_1 I1 ≡{n}≡ ofe_iso_1 I2 ∧ ofe_iso_2 I1 ≡{n}≡ ofe_iso_2 I2.
+
+  Global Instance ofe_iso_1_ne : NonExpansive (ofe_iso_1 (A:=A) (B:=B)).
+  Proof. by destruct 1. Qed.
+  Global Instance ofe_iso_2_ne : NonExpansive (ofe_iso_2 (A:=A) (B:=B)).
+  Proof. by destruct 1. Qed.
+
+  Lemma iso_ofe_ofe_mixin : OfeMixin (ofe_iso A B).
+  Proof. by apply (iso_ofe_mixin (λ I, (ofe_iso_1 I, ofe_iso_2 I))). Qed.
+  Canonical Structure ofe_isoO : ofeT := OfeT (ofe_iso A B) iso_ofe_ofe_mixin.
+
+  Global Instance iso_ofe_cofe `{!Cofe A, !Cofe B} : Cofe ofe_isoO.
+  Proof.
+    apply (iso_cofe_subtype'
+      (λ I : prodO (A -n> B) (B -n> A),
+        (∀ y, I.1 (I.2 y) ≡ y) ∧ (∀ x, I.2 (I.1 x) ≡ x))
+      (λ I HI, OfeIso (I.1) (I.2) (proj1 HI) (proj2 HI))
+      (λ I, (ofe_iso_1 I, ofe_iso_2 I))); [by intros []|done|done|].
+    apply limit_preserving_and; apply limit_preserving_forall=> ?;
+      apply limit_preserving_equiv; first [intros ???; done|solve_proper].
+  Qed.
+End ofe_iso.
+
+Arguments ofe_isoO : clear implicits.
+
+Program Definition iso_ofe_refl {A} : ofe_iso A A := OfeIso cid cid _ _.
+Solve Obligations with done.
+
+Definition iso_ofe_sym {A B : ofeT} (I : ofe_iso A B) : ofe_iso B A :=
+  OfeIso (ofe_iso_2 I) (ofe_iso_1 I) (ofe_iso_21 I) (ofe_iso_12 I).
+Instance iso_ofe_sym_ne {A B} : NonExpansive (iso_ofe_sym (A:=A) (B:=B)).
+Proof. intros n I1 I2 []; split; simpl; by f_equiv. Qed.
+
+Program Definition iso_ofe_trans {A B C}
+    (I : ofe_iso A B) (J : ofe_iso B C) : ofe_iso A C :=
+  OfeIso (ofe_iso_1 J â—Ž ofe_iso_1 I) (ofe_iso_2 I â—Ž ofe_iso_2 J) _ _.
+Next Obligation. intros A B C I J z; simpl. by rewrite !ofe_iso_12. Qed.
+Next Obligation. intros A B C I J z; simpl. by rewrite !ofe_iso_21. Qed.
+Instance iso_ofe_trans_ne {A B C} : NonExpansive2 (iso_ofe_trans (A:=A) (B:=B) (C:=C)).
+Proof. intros n I1 I2 [] J1 J2 []; split; simpl; by f_equiv. Qed.
+
+Program Definition iso_ofe_cong (F : oFunctor) `{!Cofe A, !Cofe B}
+    (I : ofe_iso A B) : ofe_iso (F A _) (F B _) :=
+  OfeIso (oFunctor_map F (ofe_iso_2 I, ofe_iso_1 I))
+    (oFunctor_map F (ofe_iso_1 I, ofe_iso_2 I)) _ _.
+Next Obligation.
+  intros F A ? B ? I x. rewrite -oFunctor_compose -{2}(oFunctor_id F x).
+  apply equiv_dist=> n.
+  apply oFunctor_ne; split=> ? /=; by rewrite ?ofe_iso_12 ?ofe_iso_21.
+Qed.
+Next Obligation.
+  intros F A ? B ? I y. rewrite -oFunctor_compose -{2}(oFunctor_id F y).
+  apply equiv_dist=> n.
+  apply oFunctor_ne; split=> ? /=; by rewrite ?ofe_iso_12 ?ofe_iso_21.
+Qed.
+Instance iso_ofe_cong_ne (F : oFunctor) `{!Cofe A, !Cofe B} :
+  NonExpansive (iso_ofe_cong F (A:=A) (B:=B)).
+Proof. intros n I1 I2 []; split; simpl; by f_equiv. Qed.
+Instance iso_ofe_cong_contractive (F : oFunctor) `{!Cofe A, !Cofe B} :
+  oFunctorContractive F → Contractive (iso_ofe_cong F (A:=A) (B:=B)).
+Proof. intros ? n I1 I2 HI; split; simpl; f_contractive; by destruct HI. Qed.
diff --git a/theories/base_logic/lib/iprop.v b/theories/base_logic/lib/iprop.v
index 5439c7df98c314b3a12baba33a4559d9bf2abc90..50169bddc9318016d0c19a2d71b29b2a95295291 100644
--- a/theories/base_logic/lib/iprop.v
+++ b/theories/base_logic/lib/iprop.v
@@ -147,12 +147,13 @@ Module Export iProp_solution : iProp_solution_sig.
   Notation iPropO Σ := (uPredO (iResUR Σ)).
 
   Definition iProp_unfold {Σ} : iPropO Σ -n> iPrePropO Σ :=
-    solution_fold (iProp_result Σ).
-  Definition iProp_fold {Σ} : iPrePropO Σ -n> iPropO Σ := solution_unfold _.
+    ofe_iso_1 (iProp_result Σ).
+  Definition iProp_fold {Σ} : iPrePropO Σ -n> iPropO Σ :=
+    ofe_iso_2 (iProp_result Σ).
   Lemma iProp_fold_unfold {Σ} (P : iProp Σ) : iProp_fold (iProp_unfold P) ≡ P.
-  Proof. apply solution_unfold_fold. Qed.
+  Proof. apply ofe_iso_21. Qed.
   Lemma iProp_unfold_fold {Σ} (P : iPrePropO Σ) : iProp_unfold (iProp_fold P) ≡ P.
-  Proof. apply solution_fold_unfold. Qed.
+  Proof. apply ofe_iso_12. Qed.
 End iProp_solution.