phanerozoic/Coq-Iris huggingface dataset:
(* iris/algebra/ofe.v *)
Instance later_cofe `{!Cofe A} : Cofe laterO := {
    compl c := Next (compl (later_chain c));
    lbcompl n Hn c := Next (lbcompl Hn (later_limit_bchain c Hn))
  }.
Next Obligation.
    intros ? n c; split; intros m Hm%SIdx.le_succ_l; simpl. rewrite conv_compl /=.
    symmetry; apply (chain_cauchy c (Sᵢ m) n); eauto using SIdx.lt_succ_diag_r.
  Qed.
(* iris/algebra/ofe.v *)
(* [f] is contractive iff it can factor into [Next] and a non-expansive
  function. *)
Lemma contractive_alt {B : ofe} (f : A → B) :
    Contractive f ↔ ∃ g : later A → B, NonExpansive g ∧ ∀ x, f x ≡ g (Next x).
Proof.
    split.
    - intros Hf. exists (f ∘ later_car); split=> // n x y ?. by f_equiv.
    - intros (g&Hg&Hf) n x y Hxy. rewrite !Hf. by apply Hg.
  Qed.
(* iris/algebra/ofe.v *)
Definition later_map {A B} (f : A → B) (x : later A) : later B
:=
  Next (f (later_car x)).
(* iris/algebra/ofe.v *)
Instance later_map_ne {SI : sidx} {A B : ofe} (f : A → B) n :
  Proper (dist_later n ==> dist_later n) f →
  Proper (dist n ==> dist n) (later_map f) | 0.
Proof.
  intros P [x] [y] H; rewrite /later_map //=.
  split; intros m Hm; apply P, Hm. apply H.
Qed.
(* iris/algebra/ofe.v *)
Instance later_map_ne' {SI : sidx} {A B : ofe} (f : A → B) :
  NonExpansive f → NonExpansive (later_map f).
Proof.
  intros ?? [x] [y] H. unfold later_map; simpl.
  split; intros ??; simpl. f_equiv. by apply H.
Qed.
(* iris/algebra/ofe.v *)
Instance later_map_proper {SI : sidx} {A B : ofe} (f : A → B) :
  Proper ((≡) ==> (≡)) f →
  Proper ((≡) ==> (≡)) (later_map f).
Proof. solve_proper. Qed.
(* iris/algebra/ofe.v *)
Lemma later_map_Next {SI : sidx} {A B : ofe} (f : A → B) x :
  later_map f (Next x) = Next (f x).
Proof. done. Qed.
(* iris/algebra/ofe.v *)
Lemma later_map_id {SI : sidx} {A} (x : later A) : later_map id x = x.
Proof. by destruct x. Qed.
(* iris/algebra/ofe.v *)
Lemma later_map_compose {SI : sidx}
    {A B C} (f : A → B) (g : B → C) (x : later A) :
  later_map (g ∘ f) x = later_map g (later_map f x).
Proof. by destruct x. Qed.
(* iris/algebra/ofe.v *)
Lemma later_map_ext {SI : sidx} {A B : ofe} (f g : A → B) x :
  (∀ x, f x ≡ g x) → later_map f x ≡ later_map g x.
Proof. destruct x; intros Hf; apply Hf. Qed.
(* iris/algebra/ofe.v *)
Definition laterO_map {SI : sidx}
    {A B: ofe} (f : A -n> B) : laterO A -n> laterO B
:=
  OfeMor (later_map f).
(* iris/algebra/ofe.v *)
Instance laterO_map_contractive {SI : sidx} (A B : ofe) :
  Contractive (@laterO_map SI A B).
Proof. intros n f g Hlater [x]; split; intros ??; simpl. by apply Hlater. Qed.
(* iris/algebra/ofe.v *)
Definition laterOF {SI : sidx} (F : oFunctor) : oFunctor := {|
  oFunctor_car A _ B _ := laterO (oFunctor_car F A B);
  oFunctor_map A1 _ A2 _ B1 _ B2 _ fg := laterO_map (oFunctor_map F fg)
|}.
Next Obligation.
  intros ? F A1 ? A2 ? B1 ? B2 ? n fg fg' ?.
  by apply (contractive_ne laterO_map), oFunctor_map_ne.
Qed.
(* iris/algebra/ofe.v *)
Notation "▶ F"
:= (laterOF F%OF) (at level 20, right associativity) : oFunctor_scope.
(* iris/algebra/ofe.v *)
Instance laterOF_contractive {SI : sidx} F : oFunctorContractive (laterOF F).
Proof.
  intros A1 ? A2 ? B1 ? B2 ? n fg fg' Hfg. apply laterO_map_contractive.
  split; intros ???; simpl. by eapply oFunctor_map_ne, Hfg.
Qed.
(* iris/algebra/ofe.v *)
(* 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.

Note that non-dependent functions over a discrete domain, [A -d> B] (following
the notation we introduce below) are non-expansive if they are
[Proper ((≡) ==> (≡))]. In other words, since the domain is discrete,
non-expansiveness and respecting [(≡)] are the same. If the domain is moreover
Leibniz ([LeibnizEquiv A]), we get both for free.

We make [discrete_fun] a definition so that we can register it as a canonical
structure.  We do not bundle the [Proper] proof to keep [discrete_fun] easier to
use. It turns out all the desired OFE and functorial properties do not rely on
this [Proper] instance. *)
Definition discrete_fun {SI : sidx} {A} (B : A → ofe)
:= ∀ x : A, B x.
(* iris/algebra/ofe.v *)
Instance discrete_fun_equiv : Equiv (discrete_fun B)
:= λ f g, ∀ x, f x ≡ g x.
(* iris/algebra/ofe.v *)
Instance discrete_fun_dist : Dist (discrete_fun B)
:= λ n f g, ∀ x, f x ≡{n}≡ g x.
(* iris/algebra/ofe.v *)
Definition discrete_fun_ofe_mixin : OfeMixin (discrete_fun B).
Proof.
    split.
    - intros f g; split; [intros Hfg n k; apply equiv_dist, Hfg|].
      intros Hfg k; apply equiv_dist=> n; apply Hfg.
    - intros n; split.
      + by intros f x.
      + by intros f g ? x.
      + by intros f g h ?? x; trans (g x).
    - intros n m f g ? H x. by eapply dist_le.
  Qed.
(* iris/algebra/ofe.v *)
Canonical discrete_funO
:= Ofe (discrete_fun B) discrete_fun_ofe_mixin.
(* iris/algebra/ofe.v *)
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.
(* iris/algebra/ofe.v *)
Definition discrete_fun_bchain {n} (c : bchain discrete_funO n)
    (x : A) : bchain (B x) n := {| bchain_car n Hn := c n Hn x |}.
Next Obligation. intros n c x m p Hm Hp Hmp. by apply (bchain_cauchy n c). Qed.
(* iris/algebra/ofe.v *)
Instance discrete_fun_cofe `{!∀ x, Cofe (B x)} :
      Cofe discrete_funO := {
    compl c x := compl (discrete_fun_chain c x);
    lbcompl n Hn c x := lbcompl Hn (discrete_fun_bchain c x)
  }.
Next Obligation. intros ? n c x. by apply conv_compl. Qed.
(* iris/algebra/ofe.v *)
Instance discrete_fun_lookup_discrete `{EqDecision A} f x :
    Discrete f → Discrete (f x).
Proof.
    intros Hf y ?.
    set (g x' := if decide (x = x') is left H then eq_rect _ B y _ H else f x').
    trans (g x).
    { apply Hf=> x'. unfold g. by destruct (decide _) as [[]|]. }
    unfold g. destruct (decide _) as [Hx|]; last done.
    by rewrite (proof_irrel Hx eq_refl).
  Qed.
(* iris/algebra/ofe.v *)
Notation "A -d> B"
:=
  (@discrete_funO _ A (λ _, B)) (at level 99, B at level 200, right associativity).
(* iris/algebra/ofe.v *)
Definition discrete_fun_map {SI : sidx} {A} {B1 B2 : A → ofe} (f : ∀ x, B1 x → B2 x)
  (g : discrete_fun B1) : discrete_fun B2
:= λ x, f _ (g x).
(* iris/algebra/ofe.v *)
Lemma discrete_fun_map_ext {SI : sidx} {A} {B1 B2 : A → ofe} (f1 f2 : ∀ x, B1 x → B2 x)
  (g : discrete_fun B1) :
  (∀ x, f1 x (g x) ≡ f2 x (g x)) → discrete_fun_map f1 g ≡ discrete_fun_map f2 g.
Proof. done. Qed.
(* iris/algebra/ofe.v *)
Lemma discrete_fun_map_id {SI : sidx} {A} {B : A → ofe} (g : discrete_fun B) :
  discrete_fun_map (λ _, id) g = g.
Proof. done. Qed.
(* iris/algebra/ofe.v *)
Lemma discrete_fun_map_compose {SI : sidx} {A} {B1 B2 B3 : A → ofe}
    (f1 : ∀ x, B1 x → B2 x) (f2 : ∀ x, B2 x → B3 x) (g : discrete_fun B1) :
  discrete_fun_map (λ x, f2 x ∘ f1 x) g = discrete_fun_map f2 (discrete_fun_map f1 g).
Proof. done. Qed.
(* iris/algebra/ofe.v *)
Instance discrete_fun_map_ne {SI : sidx} {A} {B1 B2 : A → ofe}
    (f : ∀ x, B1 x → B2 x) n :
  (∀ x, Proper (dist n ==> dist n) (f x)) →
  Proper (dist n ==> dist n) (discrete_fun_map f).
Proof. by intros ? y1 y2 Hy x; rewrite /discrete_fun_map (Hy x). Qed.
(* iris/algebra/ofe.v *)
Definition discrete_funO_map {SI : sidx} {A} {B1 B2 : A → ofe}
    (f : discrete_fun (λ x, B1 x -n> B2 x)) :
  discrete_funO B1 -n> discrete_funO B2
:= OfeMor (discrete_fun_map f).
(* iris/algebra/ofe.v *)
Instance discrete_funO_map_ne {SI : sidx} {A} {B1 B2 : A → ofe} :
  NonExpansive (@discrete_funO_map SI A B1 B2).
Proof. intros n f1 f2 Hf g x; apply Hf. Qed.
(* iris/algebra/ofe.v *)
Definition discrete_funOF {SI : sidx} {C} (F : C → oFunctor) : oFunctor := {|
  oFunctor_car A _ B _ := discrete_funO (λ c, oFunctor_car (F c) A B);
  oFunctor_map A1 _ A2 _ B1 _ B2 _ fg := discrete_funO_map (λ c, oFunctor_map (F c) fg)
|}.
Next Obligation.
  intros ? C F A1 ? A2 ? B1 ? B2 ? n ?? g.
  by apply discrete_funO_map_ne=>?; apply oFunctor_map_ne.
Qed.
(* iris/algebra/ofe.v *)
Notation "T -d> F"
:= (@discrete_funOF _ T%type (λ _, F%OF)) : oFunctor_scope.
(* iris/algebra/ofe.v *)
Instance discrete_funOF_contractive {SI : sidx} {C} (F : C → oFunctor) :
  (∀ c, oFunctorContractive (F c)) → oFunctorContractive (discrete_funOF F).
Proof.
  intros ? A1 ? A2 ? B1 ? B2 ? n ?? g.
  by apply discrete_funO_map_ne=>c; apply oFunctor_map_contractive.
Qed.
(* iris/algebra/ofe.v *)
(* * Constructing isomorphic OFEs *)
Lemma iso_ofe_mixin {SI : sidx}
  {A : ofe} {B : Type} `{!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.
Proof.
  split.
  - intros y1 y2. rewrite g_equiv. setoid_rewrite g_dist. apply equiv_dist.
  - split.
    + intros y. by apply g_dist.
    + intros y1 y2. by rewrite !g_dist.
    + intros y1 y2 y3. rewrite !g_dist. intros ??; etrans; eauto.
  - intros n m y1 y2. rewrite !g_dist. by eapply dist_le.
Qed.
(* iris/algebra/ofe.v *)
Let Hgne : NonExpansive g.
Proof. intros n y1 y2. apply g_dist. Defined.
(* iris/algebra/ofe.v *)
Definition iso_cofe_subtype : Cofe B := {|
    compl c := f (compl (chain_map g c)) _;
    lbcompl n Hn c := f (lbcompl Hn (bchain_map g c)) _
  |}.
Next Obligation. apply Hlimit. Qed.
(* iris/algebra/ofe.v *)
Lemma iso_cofe_subtype' {SI : sidx} {A B : ofe} `{!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. destruct Hlimit. apply: (iso_cofe_subtype P f g); eauto. Qed.
(* iris/algebra/ofe.v *)
Definition iso_cofe {SI : sidx} {A B : ofe} `{!Cofe A} (f : A → B) (g : B → A)
  (g_dist : ∀ n y1 y2, y1 ≡{n}≡ y2 ↔ g y1 ≡{n}≡ g y2)
  (gf : ∀ x, g (f x) ≡ x) : Cofe B.
Proof. by apply (iso_cofe_subtype (λ _, True) (λ x _, f x) g). Qed.
(* iris/algebra/ofe.v *)
(* TODO: Find a better place for this Equiv instance. It also
     should not depend on A being an OFE. *)
Instance sig_equiv : Equiv (sig P)
:= λ x1 x2, `x1 ≡ `x2.
(* iris/algebra/ofe.v *)
Instance sig_dist : Dist (sig P)
:= λ n x1 x2, `x1 ≡{n}≡ `x2.
(* iris/algebra/ofe.v *)
Definition sig_equiv_def x y : (x ≡ y) = (`x ≡ `y)
:= reflexivity _.
(* iris/algebra/ofe.v *)
Definition sig_dist_def n x y : (x ≡{n}≡ y) = (`x ≡{n}≡ `y)
:= reflexivity _.
(* iris/algebra/ofe.v *)
Lemma exist_ne n a1 a2 (H1 : P a1) (H2 : P a2) :
    a1 ≡{n}≡ a2 → a1 ↾ H1 ≡{n}≡ a2 ↾ H2.
Proof. done. Qed.
(* iris/algebra/ofe.v *)
Instance proj1_sig_ne : NonExpansive (@proj1_sig _ P).
Proof. by intros n [a Ha] [b Hb] ?. Qed.
(* iris/algebra/ofe.v *)
Definition sig_ofe_mixin : OfeMixin (sig P).
Proof. by apply (iso_ofe_mixin proj1_sig). Qed.
(* iris/algebra/ofe.v *)
Canonical sigO : ofe
:= Ofe (sig P) sig_ofe_mixin.
(* iris/algebra/ofe.v *)
Instance sig_cofe `{!Cofe A, !LimitPreserving P} : Cofe sigO.
Proof. apply (iso_cofe_subtype' P (exist P) proj1_sig)=> //. by intros []. Qed.
(* iris/algebra/ofe.v *)
Instance sig_discrete (x : sig P) :  Discrete (`x) → Discrete x.
Proof. intros ? y. rewrite sig_dist_def sig_equiv_def. apply (discrete_0 _). Qed.
(* iris/algebra/ofe.v *)
Instance sig_ofe_discrete : OfeDiscrete A → OfeDiscrete sigO.
Proof. intros ??. apply _. Qed.
(* iris/algebra/ofe.v *)
(* The distance for [{ a : A & P }] uses Leibniz equality on [A] to
    transport the second components to the same type,
    and then step-indexed distance on the second component.
    Unlike in the topos of trees, with (C)OFEs we cannot use step-indexed equality
    on the first component. *)
Instance sigT_dist : Dist (sigT P)
:= λ n x1 x2,
    ∃ Heq : projT1 x1 = projT1 x2, rew Heq in projT2 x1 ≡{n}≡ projT2 x2.
(* iris/algebra/ofe.v *)
(* Usually we'd give a direct definition, and show it equivalent to
    [∀ n, x1 ≡{n}≡ x2] when proving the [equiv_dist] OFE axiom.
    But here the equivalence requires UIP — see [sigT_equiv_eq_alt].
    By defining [equiv] in terms of [dist], we can define an OFE
    without assuming UIP, at the cost of complex reasoning on [equiv]. *)
Instance sigT_equiv : Equiv (sigT P)
:= λ x1 x2,
    ∀ n, x1 ≡{n}≡ x2.
(* iris/algebra/ofe.v *)
(* Unfolding lemmas.
      Written with [↔] not [=] to avoid https://github.com/coq/coq/issues/3814. *)
Definition sigT_equiv_eq x1 x2 : (x1 ≡ x2) ↔ ∀ n, x1 ≡{n}≡ x2
:=
      reflexivity _.
(* iris/algebra/ofe.v *)
Definition sigT_dist_eq x1 x2 n : (x1 ≡{n}≡ x2) ↔
    ∃ Heq : projT1 x1 = projT1 x2, (rew Heq in projT2 x1) ≡{n}≡ projT2 x2
:=
      reflexivity _.
(* iris/algebra/ofe.v *)
Definition sigT_dist_proj1 n {x y} :
    x ≡{n}≡ y → projT1 x = projT1 y
:= proj1_ex.
(* iris/algebra/ofe.v *)
Definition sigT_equiv_proj1 {x y} :
    x ≡ y → projT1 x = projT1 y
:= λ H, proj1_ex (H 0ᵢ).
(* iris/algebra/ofe.v *)
Definition sigT_ofe_mixin : OfeMixin (sigT P).
Proof.
    split => // n.
    - split; hnf; setoid_rewrite sigT_dist_eq.
      + intros. by exists eq_refl.
      + move => [xa x] [ya y] /=. destruct 1 as [-> Heq].
        by exists eq_refl.
      + move => [xa x] [ya y] [za z] /=.
        destruct 1 as [-> Heq1].
        destruct 1 as [-> Heq2]. exists eq_refl => /=. by trans y.
    - setoid_rewrite sigT_dist_eq.
      move => m [xa x] [ya y] /=. destruct 1 as [-> Heq].
      exists eq_refl. eauto using dist_le.
  Qed.
(* iris/algebra/ofe.v *)
Canonical sigTO : ofe
:= Ofe (sigT P) sigT_ofe_mixin.
(* iris/algebra/ofe.v *)
Lemma sigT_equiv_eq_alt `{!∀ a b : A, ProofIrrel (a = b)} x1 x2 :
    x1 ≡ x2 ↔
    ∃ Heq : projT1 x1 = projT1 x2, rew Heq in projT2 x1 ≡ projT2 x2.
Proof.
    setoid_rewrite equiv_dist. setoid_rewrite sigT_dist_eq. split => Heq.
    - move: (Heq 0ᵢ) => [H0eq1 _].
      exists H0eq1 => n. move: (Heq n) => [] Hneq1.
      by rewrite (proof_irrel H0eq1 Hneq1).
    - move: Heq => [Heq1 Heqn2] n. by exists Heq1.
  Qed.
(* iris/algebra/ofe.v *)
(* [projT1] is non-expansive and proper. *)
Instance projT1_ne : NonExpansive (projT1 : sigTO → leibnizO A).
Proof. solve_proper. Qed.
(* iris/algebra/ofe.v *)
Instance projT1_proper : Proper ((≡) ==> (≡)) (projT1 : sigTO → leibnizO A).
Proof. apply ne_proper, projT1_ne. Qed.
(* iris/algebra/ofe.v *)
(* [projT2] is "non-expansive"; the properness lemma [projT2_ne] requires UIP. *)
Lemma projT2_ne n (x1 x2 : sigTO) (Heq : x1 ≡{n}≡ x2) :
    rew (sigT_dist_proj1 n Heq) in projT2 x1 ≡{n}≡ projT2 x2.
Proof. by destruct Heq. Qed.
(* iris/algebra/ofe.v *)
Lemma projT2_proper `{!∀ a b : A, ProofIrrel (a = b)} (x1 x2 : sigTO) (Heqs : x1 ≡ x2):
    rew (sigT_equiv_proj1 Heqs) in projT2 x1 ≡ projT2 x2.
Proof.
    move: x1 x2 Heqs => [a1 x1] [a2 x2] Heqs.
    case: (proj1 (sigT_equiv_eq_alt _ _) Heqs) => /=. intros ->.
    rewrite (proof_irrel (sigT_equiv_proj1 Heqs) eq_refl) /=. done.
  Qed.
(* iris/algebra/ofe.v *)
(* [existT] is "non-expansive" — general, dependently-typed statement. *)
Lemma existT_ne n {i1 i2} {v1 : P i1} {v2 : P i2} :
    ∀ (Heq : i1 = i2), (rew f_equal P Heq in v1 ≡{n}≡ v2) →
      existT i1 v1 ≡{n}≡ existT i2 v2.
Proof. intros ->; simpl. exists eq_refl => /=. done. Qed.
(* iris/algebra/ofe.v *)
Lemma existT_proper {i1 i2} {v1 : P i1} {v2 : P i2} :
    ∀ (Heq : i1 = i2), (rew f_equal P Heq in v1 ≡ v2) →
      existT i1 v1 ≡ existT i2 v2.
Proof. intros Heq Heqv n. apply (existT_ne n Heq), equiv_dist, Heqv. Qed.
(* iris/algebra/ofe.v *)
(* [existT] is "non-expansive" — non-dependently-typed version. *)
Instance existT_ne_2 a : NonExpansive (@existT A P a).
Proof. move => ??? Heq. apply (existT_ne _ eq_refl Heq). Qed.
(* iris/algebra/ofe.v *)
Instance existT_proper_2 a : Proper ((≡) ==> (≡)) (@existT A P a).
Proof. apply ne_proper, _. Qed.
(* iris/algebra/ofe.v *)
Instance sigT_discrete x : Discrete (projT2 x) → Discrete x.
Proof.
    move: x => [xa x] ? [ya y] [] /=; intros -> => /= Hxy n.
    exists eq_refl => /=. apply equiv_dist, (discrete_0 _), Hxy.
  Qed.
(* iris/algebra/ofe.v *)
Instance sigT_ofe_discrete : (∀ a, OfeDiscrete (P a)) → OfeDiscrete sigTO.
Proof. intros ??. apply _. Qed.
(* iris/algebra/ofe.v *)
Lemma sigT_chain_const_proj1 c n : projT1 (c n) = projT1 (c 0ᵢ).
Proof.
    refine (sigT_dist_proj1 _ (chain_cauchy c 0ᵢ n _)). apply SIdx.le_0_l.
  Qed.
(* iris/algebra/ofe.v *)
Lemma sigT_bchain_const_proj1 n Hn (c: bchain sigTO n) m Hm :
    projT1 (c m Hm) = projT1 (c 0ᵢ Hn).
Proof.
    refine (sigT_dist_proj1 _ (bchain_cauchy n c 0ᵢ m _ _ _)). apply SIdx.le_0_l.
  Qed.
(* iris/algebra/ofe.v *)
(* The definitions [sigT_compl] and [sigT_lbcompl] are similar to
    [sum_compl] and [sum_bcompl]. We are given a [chain (sigT P)], i.e., a
    sequence of dependent pairs [existT x_i y_i], but know that all [x_i]s are
    the same. So, given a [chain (sigT P)], we are able to construct a
    [chain (P (projT1 (c 0ᵢ)))] (which involves some programming with dependent
    types), which we can then give to the [compl] operation on [P]. *)
Definition chain_map_snd c : chain (P (projT1 (c 0ᵢ))) :=
      {| chain_car n := rew (sigT_chain_const_proj1 c n) in projT2 (c n) |}.
Next Obligation.
      move => c n i Hle /=.
      (* [Hgoal] is our thesis, up to casts: *)
      case: (chain_cauchy c n i Hle) => [Heqin Hgoal] /=.
      (* Pretty delicate. We have two casts to [projT1 (c 0ᵢ)].
        We replace those by one cast. *)
      move: (sigT_chain_const_proj1 c i) (sigT_chain_const_proj1 c n)
        => Heqi0 Heqn0.
      (* Rewrite [projT1 (c 0ᵢ)] to [projT1 (c n)] in goal and [Heqi0]: *)
      destruct Heqn0.
      by rewrite /= (proof_irrel Heqi0 Heqin).
    Qed.
(* iris/algebra/ofe.v *)
Definition sigT_compl : Compl sigTO
:= λ c,
      existT (projT1 (c 0ᵢ)) (compl (chain_map_snd c)).
(* iris/algebra/ofe.v *)
Definition bchain_map_snd n Hn (c : bchain sigTO n) :
        bchain (P (projT1 (c 0ᵢ Hn))) n :=
      {| bchain_car m Hm :=
        rew (sigT_bchain_const_proj1 n Hn c m Hm) in projT2 (c m Hm) |}.
Next Obligation.
      move => n Hn c m p Hm Hp Hle /=.
      (* [Hgoal] is our thesis, up to casts: *)
      case: (bchain_cauchy n c m p Hm Hp Hle) => [Heqin Hgoal] /=.
      (* Pretty delicate. We have two casts to [projT1 (c 0ᵢ)].
        We replace those by one cast. *)
      move: (sigT_bchain_const_proj1 n Hn c m Hm)
        (sigT_bchain_const_proj1 n Hn c p Hp)=> Heqm0 Heqp0.
      (* Rewrite [projT1 (c 0ᵢ)] to [projT1 (c n)] in goal and [Heqi0]: *)
      destruct Heqm0.
      by rewrite /= (proof_irrel Heqp0 Heqin).
    Qed.
(* iris/algebra/ofe.v *)
Definition sigT_lbcompl : LBCompl sigTO
:= λ n Hn (c : bchain sigTO n),
      existT (projT1 (c _ (SIdx.limit_lt_0 _ Hn)))
             (lbcompl Hn (bchain_map_snd n (SIdx.limit_lt_0 _ Hn) c)).
(* iris/algebra/ofe.v *)
Instance sigT_cofe : Cofe sigTO :=
      { compl := sigT_compl; lbcompl := sigT_lbcompl }.
Next Obligation.
      intros n c. rewrite /sigT_compl sigT_dist_eq /=.
      exists (symmetry (sigT_chain_const_proj1 c n)).
      (* Our thesis, up to casts: *)
      pose proof (conv_compl n (chain_map_snd c)) as Hgoal.
      move: (compl (chain_map_snd c)) Hgoal => pc0 /=.
      by destruct (sigT_chain_const_proj1 c n).
    Qed.
(* iris/algebra/ofe.v *)
Definition sigT_map {P1 P2 : A → ofe} :
    discrete_funO (λ a, P1 a -n> P2 a) -n>
    sigTO P1 -n> sigTO P2 :=
    λne f xpx, existT _ (f _ (projT2 xpx)).
Next Obligation.
    move => ?? f n [x px] [y py] [/= Heq]. destruct Heq; simpl.
    exists eq_refl => /=. by f_equiv.
  Qed.
(* iris/algebra/ofe.v *)
Definition sigTOF (F : A → oFunctor) : oFunctor := {|
    oFunctor_car A CA B CB := sigTO (λ a, oFunctor_car (F a) A B);
    oFunctor_map A1 _ A2 _ B1 _ B2 _ fg := sigT_map (λ a, oFunctor_map (F a) fg)
  |}.
Next Obligation.
    repeat intro. exists eq_refl => /=. solve_proper.
  Qed.
(* iris/algebra/ofe.v *)
Instance sigTOF_contractive {F} :
    (∀ a, oFunctorContractive (F a)) → oFunctorContractive (sigTOF F).
Proof.
    repeat intro. apply sigT_map => a. exact: oFunctor_map_contractive.
  Qed.
(* iris/algebra/ofe.v *)
Notation "{ x  &  P }"
:= (sigTOF (λ x, P%OF)) : oFunctor_scope.
(* iris/algebra/ofe.v *)
Notation "{ x : A &  P }"
:= (@sigTOF _ A%type (λ x, P%OF)) : oFunctor_scope.
(* iris/algebra/ofe.v *)
(* * Isomorphisms between OFEs *)
Record ofe_iso {SI : sidx} (A B : ofe)
:= 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;
}.
(* iris/algebra/ofe.v *)
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.
(* iris/algebra/ofe.v *)
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.
(* iris/algebra/ofe.v *)
Instance ofe_iso_1_ne : NonExpansive (ofe_iso_1 (A:=A) (B:=B)).
Proof. by destruct 1. Qed.
(* iris/algebra/ofe.v *)
Instance ofe_iso_2_ne : NonExpansive (ofe_iso_2 (A:=A) (B:=B)).
Proof. by destruct 1. Qed.
(* iris/algebra/ofe.v *)
Lemma ofe_iso_ofe_mixin : OfeMixin (ofe_iso A B).
Proof. by apply (iso_ofe_mixin (λ I, (ofe_iso_1 I, ofe_iso_2 I))). Qed.
(* iris/algebra/ofe.v *)
Canonical ofe_isoO : ofe
:= Ofe (ofe_iso A B) ofe_iso_ofe_mixin.
(* iris/algebra/ofe.v *)
Instance ofe_iso_cofe `{!SIdxFinite SI}
    `{!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..|].
    apply limit_preserving_and; apply limit_preserving_forall=> ?;
      apply limit_preserving_equiv; solve_proper.
  Qed.
(* iris/algebra/ofe.v *)
Definition iso_ofe_refl {SI : sidx} {A: ofe} : ofe_iso A A
:=
  OfeIso cid cid _ _.
(* iris/algebra/ofe.v *)
Definition iso_ofe_sym {SI : sidx} {A B : ofe} (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).
(* iris/algebra/ofe.v *)
Instance iso_ofe_sym_ne {SI : sidx} {A B : ofe} :
  NonExpansive (iso_ofe_sym (A:=A) (B:=B)).
Proof. intros n I1 I2 []; split; simpl; by f_equiv. Qed.
(* iris/algebra/ofe.v *)
Definition iso_ofe_trans {SI : sidx} {A B C: ofe}
    (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.
(* iris/algebra/ofe.v *)
Instance iso_ofe_trans_ne {SI : sidx} {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.
(* iris/algebra/ofe.v *)
Definition iso_ofe_cong {SI : sidx} (F : oFunctor) `{!Cofe A, !Cofe B}
    (I : ofe_iso A B) : ofe_iso (oFunctor_apply F A) (oFunctor_apply 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_map_compose -{2}(oFunctor_map_id F x).
  apply equiv_dist=> n.
  apply oFunctor_map_ne; split=> ? /=; by rewrite ?ofe_iso_12 ?ofe_iso_21.
Qed.
(* iris/algebra/ofe.v *)
Instance iso_ofe_cong_ne {SI : sidx} (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.
(* iris/algebra/ofe.v *)
Instance iso_ofe_cong_contractive {SI : sidx}
    (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.