phanerozoic/Coq-Iris huggingface dataset:
(* iris/algebra/cmra.v *)
Instance discrete_fun_validN_instance : ValidN (discrete_fun B)
:= λ n f,
    ∀ x, ✓{n} f x.
(* iris/algebra/cmra.v *)
Definition discrete_fun_lookup_op f g x : (f ⋅ g) x = f x ⋅ g x
:= eq_refl.
(* iris/algebra/cmra.v *)
Definition discrete_fun_lookup_core f x : (core f) x = core (f x)
:= eq_refl.
(* iris/algebra/cmra.v *)
Lemma discrete_fun_included_spec_1 (f g : discrete_fun B) x : f ≼ g → f x ≼ g x.
Proof.
    by intros [h Hh]; exists (h x); rewrite /op /discrete_fun_op_instance (Hh x).
  Qed.
(* iris/algebra/cmra.v *)
Lemma discrete_fun_included_spec `{Finite A} (f g : discrete_fun B) :
    f ≼ g ↔ ∀ x, f x ≼ g x.
Proof.
    split; [by intros; apply discrete_fun_included_spec_1|].
    intros [h ?]%finite_choice; by exists h.
  Qed.
(* iris/algebra/cmra.v *)
Lemma discrete_fun_cmra_mixin : CmraMixin (discrete_fun B).
Proof.
    apply cmra_total_mixin.
    - eauto.
    - intros n f1 f2 f3 Hf x. by rewrite discrete_fun_lookup_op (Hf x).
    - intros n f1 f2 Hf x. by rewrite discrete_fun_lookup_core (Hf x).
    - intros n f1 f2 Hf ? x. by rewrite -(Hf x).
    - intros g; split.
      + intros Hg n i; apply cmra_valid_validN, Hg.
      + intros Hg i; apply cmra_valid_validN=> n; apply Hg.
    - intros n n' f Hf ? x. eauto using cmra_validN_le.
    - intros f1 f2 f3 x. by rewrite discrete_fun_lookup_op assoc.
    - intros f1 f2 x. by rewrite discrete_fun_lookup_op comm.
    - intros f x.
      by rewrite discrete_fun_lookup_op discrete_fun_lookup_core cmra_core_l.
    - intros f x. by rewrite discrete_fun_lookup_core cmra_core_idemp.
    - intros f1 f2 Hf12. exists (core f2)=>x. rewrite discrete_fun_lookup_op.
      apply (discrete_fun_included_spec_1 _ _ x), (cmra_core_mono (f1 x)) in Hf12.
      rewrite !discrete_fun_lookup_core. destruct Hf12 as [? ->].
      rewrite assoc -cmra_core_dup //.
    - intros n f1 f2 Hf x. apply cmra_validN_op_l with (f2 x), Hf.
    - intros n f f1 f2 Hf Hf12.
      assert (FUN := λ x, cmra_extend n (f x) (f1 x) (f2 x) (Hf x) (Hf12 x)).
      exists (λ x, projT1 (FUN x)), (λ x, proj1_sig (projT2 (FUN x))).
      split; [|split]=>x; [rewrite discrete_fun_lookup_op| |];
        by destruct (FUN x) as (?&?&?&?&?).
  Qed.
(* iris/algebra/cmra.v *)
Canonical discrete_funR
:=
    Cmra (discrete_fun B) discrete_fun_cmra_mixin.
(* iris/algebra/cmra.v *)
Instance discrete_fun_unit_instance : Unit (discrete_fun B)
:= λ x, ε.
(* iris/algebra/cmra.v *)
Definition discrete_fun_lookup_empty x : ε x = ε
:= eq_refl.
(* iris/algebra/cmra.v *)
Lemma discrete_fun_ucmra_mixin : UcmraMixin (discrete_fun B).
Proof.
    split.
    - intros x. apply ucmra_unit_valid.
    - intros f x. by rewrite discrete_fun_lookup_op left_id.
    - constructor=> x. apply core_id_core, _.
  Qed.
(* iris/algebra/cmra.v *)
Canonical discrete_funUR
:=
    Ucmra (discrete_fun B) discrete_fun_ucmra_mixin.
(* iris/algebra/cmra.v *)
Instance discrete_fun_unit_discrete :
    (∀ i, Discrete (ε : B i)) → Discrete (ε : discrete_fun B).
Proof. intros ? f Hf x. by apply: discrete. Qed.
(* iris/algebra/cmra.v *)
Instance discrete_fun_map_cmra_morphism
    {SI : sidx} {A} {B1 B2 : A → ucmra} (f : ∀ x, B1 x → B2 x) :
  (∀ x, CmraMorphism (f x)) → CmraMorphism (discrete_fun_map f).
Proof.
  split; first apply _.
  - intros n g Hg x. rewrite /discrete_fun_map.
    apply (cmra_morphism_validN (f _)), Hg.
  - intros. apply Some_proper=>i. apply (cmra_morphism_core (f i)).
  - intros g1 g2 i.
    by rewrite /discrete_fun_map discrete_fun_lookup_op cmra_morphism_op.
Qed.
(* iris/algebra/cmra.v *)
Definition discrete_funURF
    {SI : sidx} {C} (F : C → urFunctor) : urFunctor := {|
  urFunctor_car A _ B _ := discrete_funUR (λ c, urFunctor_car (F c) A B);
  urFunctor_map A1 _ A2 _ B1 _ B2 _ fg :=
    discrete_funO_map (λ c, urFunctor_map (F c) fg)
|}.
Next Obligation.
  intros ? C F A1 ? A2 ? B1 ? B2 ? n ?? g.
  by apply discrete_funO_map_ne=>?; apply urFunctor_map_ne.
Qed.
(* iris/algebra/cmra.v *)
Instance discrete_funURF_contractive {SI : sidx} {C} (F : C → urFunctor) :
  (∀ c, urFunctorContractive (F c)) → urFunctorContractive (discrete_funURF F).
Proof.
  intros ? A1 ? A2 ? B1 ? B2 ? n ?? g.
  by apply discrete_funO_map_ne=> c; apply urFunctor_map_contractive.
Qed.
(* iris/algebra/cmra.v *)
(* Constructing a CMRA through an isomorphism that may restrict validity. *)
Lemma iso_cmra_mixin_restrict_validity {SI : sidx} {A : cmra} {B : ofe}
  `{!PCore B, !Op B, !Valid B, !ValidN B}
  (f : A → B) (g : B → A)
  (* [g] is proper/non-expansive and injective w.r.t. setoid and OFE equality *)
  (g_dist : ∀ n y1 y2, y1 ≡{n}≡ y2 ↔ g y1 ≡{n}≡ g y2)
  (* [g] is surjective (and [f] its inverse) *)
  (gf : ∀ x : A, g (f x) ≡ x)
  (* [g] commutes with [pcore] and [op] *)
  (g_pcore : ∀ y : B, pcore (g y) ≡ g <$> pcore y)
  (g_op : ∀ y1 y2, g (y1 ⋅ y2) ≡ g y1 ⋅ g y2)
  (* The validity predicate on [B] restricts the one on [A] *)
  (g_validN : ∀ n y, ✓{n} y → ✓{n} (g y))
  (* The validity predicate on [B] satisfies the laws of validity *)
  (valid_validN_ne : ∀ n, Proper (dist n ==> impl) (validN (A:=B) n))
  (valid_rvalidN : ∀ y : B, ✓ y ↔ ∀ n, ✓{n} y)
  (validN_le: ∀ n m (y : B), ✓{n} y → m ≤ n → ✓{m} y)
  (validN_op_l : ∀ n (y1 y2 : B), ✓{n} (y1 ⋅ y2) → ✓{n} y1) :
  CmraMixin B.
Proof.
  assert (g_ne : NonExpansive g).
  { intros n ???. apply g_dist. done. }
  assert (g_equiv : ∀ y1 y2, y1 ≡ y2 ↔ g y1 ≡ g y2).
  { intros ??.
    split; intros ?; apply equiv_dist; intros; apply g_dist, equiv_dist; done. }
  apply (inj_cmra_mixin_restrict_validity (λ x, Some (f x)) g); try done.
  - intros. split.
    + intros Hy%(inj Some). rewrite -Hy gf //.
    + intros ?. f_equiv. apply g_dist. rewrite gf. done.
  - intros. rewrite g_pcore. split.
    + intros ->. done.
    + intros (? & -> & ->%g_dist)%fmap_Some_dist. done.
  - intros ??. simpl. rewrite g_op gf //.
Qed.
(* iris/algebra/cmra.v *)
(* * Constructing a camera through an isomorphism *)
Lemma iso_cmra_mixin {SI : sidx} {A : cmra} {B : ofe}
  `{!PCore B, !Op B, !Valid B, !ValidN B}
  (f : A → B) (g : B → A)
  (* [g] is proper/non-expansive and injective w.r.t. OFE equality *)
  (g_dist : ∀ n y1 y2, y1 ≡{n}≡ y2 ↔ g y1 ≡{n}≡ g y2)
  (* [g] is surjective (and [f] its inverse) *)
  (gf : ∀ x : A, g (f x) ≡ x)
  (* [g] commutes with [pcore], [op], [valid], and [validN] *)
  (g_pcore : ∀ y : B, pcore (g y) ≡ g <$> pcore y)
  (g_op : ∀ y1 y2, g (y1 ⋅ y2) ≡ g y1 ⋅ g y2)
  (g_valid : ∀ y, ✓ (g y) ↔ ✓ y)
  (g_validN : ∀ n y, ✓{n} (g y) ↔ ✓{n} y) :
  CmraMixin B.
Proof.
  apply (iso_cmra_mixin_restrict_validity f g); auto.
  - by intros n y ?%g_validN.
  - intros n y1 y2 Hy%g_dist Hy1. by rewrite -g_validN -Hy g_validN.
  - intros y. rewrite -g_valid cmra_valid_validN. naive_solver.
  - intros n m y. rewrite -!g_validN. apply cmra_validN_le.
  - intros n y1 y2. rewrite -!g_validN g_op. apply cmra_validN_op_l.
Qed.
(* iris/algebra/cmra_big_op.v *)
(* Option *)
Lemma big_opL_None {SI : sidx} {M : cmra} {A} (f : nat → A → option M) l :
  ([^op list] k↦x ∈ l, f k x) = None ↔ ∀ k x, l !! k = Some x → f k x = None.
Proof.
  revert f. induction l as [|x l IH]=> f //=. rewrite op_None IH. split.
  - intros [??] [|k] y ?; naive_solver.
  - intros Hl. split; [by apply (Hl 0)|]. intros k. apply (Hl (S k)).
Qed.
(* iris/algebra/cmra_big_op.v *)
Lemma big_opM_None {SI : sidx}
    {M : cmra} `{Countable K} {A} (f : K → A → option M) m :
  ([^op map] k↦x ∈ m, f k x) = None ↔ ∀ k x, m !! k = Some x → f k x = None.
Proof.
  induction m as [|i x m ? IH] using map_ind=> /=.
  { by rewrite big_opM_empty. }
  rewrite -None_equiv_eq big_opM_insert // None_equiv_eq op_None IH. split.
  { intros [??] k y. rewrite lookup_insert_Some; naive_solver. }
  intros Hm; split.
  - apply (Hm i). by simplify_map_eq.
  - intros k y ?. apply (Hm k). by simplify_map_eq.
Qed.
(* iris/algebra/cmra_big_op.v *)
Lemma big_opS_None {SI : sidx} {M : cmra} `{Countable A} (f : A → option M) X :
  ([^op set] x ∈ X, f x) = None ↔ ∀ x, x ∈ X → f x = None.
Proof.
  induction X as [|x X ? IH] using set_ind_L.
  { by rewrite big_opS_empty. }
  rewrite -None_equiv_eq big_opS_insert // None_equiv_eq op_None IH. set_solver.
Qed.
(* iris/algebra/cmra_big_op.v *)
Lemma big_opMS_None {SI : sidx} {M : cmra} `{Countable A} (f : A → option M) X :
  ([^op mset] x ∈ X, f x) = None ↔ ∀ x, x ∈ X → f x = None.
Proof.
  induction X as [|x X IH] using gmultiset_ind.
  { rewrite big_opMS_empty. multiset_solver. }
  rewrite -None_equiv_eq big_opMS_disj_union big_opMS_singleton None_equiv_eq op_None IH.
  multiset_solver.
Qed.
(* iris/algebra/cofe_solver.v *)
(* Note that [Inhabited] is not derivable. Take [F X := ▶ X], then a possible
solution is [Empty_set]. *)
Record solution (F : oFunctor)
:= Solution {
  solution_car :> ofe;
  solution_inhabited : Inhabited solution_car;
  solution_cofe : Cofe solution_car;
  solution_iso :> ofe_iso (oFunctor_apply F solution_car) solution_car;
}.
(* iris/algebra/cofe_solver.v *)
Notation map
:= (oFunctor_map F).
(* iris/algebra/cofe_solver.v *)
Fixpoint A' (k : nat) : { C : ofe & Cofe C }
:=
  match k with
  | 0 => existT (P:=Cofe) unitO _
  | S k => existT (P:=Cofe) (@oFunctor_apply _ F (projT1 (A' k)) (projT2 (A' k))) _
  end.
(* iris/algebra/cofe_solver.v *)
Notation A k
:= (projT1 (A' k)).
(* iris/algebra/cofe_solver.v *)
Instance A_cofe k : Cofe (A k)
:= projT2 (A' k).
(* iris/algebra/cofe_solver.v *)
Fixpoint f (k : nat) : A k -n> A (S k)
:=
  match k with 0 => OfeMor (λ _, inhabitant) | S k => map (g k,f k) end
with g (k : nat) : A (S k) -n> A k :=
  match k with 0 => OfeMor (λ _, ()) | S k => map (f k,g k) end.
(* iris/algebra/cofe_solver.v *)
Definition f_S k (x : A (S k)) : f (S k) x = map (g k,f k) x
:= eq_refl.
(* iris/algebra/cofe_solver.v *)
Definition g_S k (x : A (S (S k))) : g (S k) x = map (f k,g k) x
:= eq_refl.
(* iris/algebra/cofe_solver.v *)
Lemma gf {k} (x : A k) : g k (f k x) ≡ x.
Proof using Fcontr.
  induction k as [|k IH]; simpl in *; [by destruct x|].
  rewrite -oFunctor_map_compose -{2}[x]oFunctor_map_id.
  by apply (contractive_proper map).
Qed.
(* iris/algebra/cofe_solver.v *)
Lemma fg {k} (x : A (S (S k))) : f (S k) (g (S k) x) ≡{k}≡ x.
Proof using Fcontr.
  induction k as [|k IH]; simpl.
  - rewrite f_S g_S -{2}[x]oFunctor_map_id -oFunctor_map_compose.
    apply (contractive_0 map).
  - rewrite f_S g_S -{2}[x]oFunctor_map_id -oFunctor_map_compose.
    by apply (contractive_S map).
Qed.
(* iris/algebra/cofe_solver.v *)
Record tower
:= {
  tower_car k :> A k;
  g_tower k : g k (tower_car (S k)) ≡ tower_car k
}.
(* iris/algebra/cofe_solver.v *)
Instance tower_equiv : Equiv tower
:= λ X Y, ∀ k, X k ≡ Y k.
(* iris/algebra/cofe_solver.v *)
Instance tower_dist : Dist tower
:= λ n X Y, ∀ k, X k ≡{n}≡ Y k.
(* iris/algebra/cofe_solver.v *)
Definition tower_ofe_mixin : OfeMixin tower.
Proof.
  apply ofe_mixin_finite.
  - intros X Y; split; [by intros HXY n k; apply equiv_dist|].
    intros HXY k; apply equiv_dist; intros n; apply HXY.
  - intros k; split.
    + by intros X n.
    + by intros X Y ? n.
    + by intros X Y Z ?? n; trans (Y n).
  - intros k X Y HXY n. specialize (HXY (S n)).
    apply (dist_le _ k) in HXY; [|apply SIdx.le_succ_diag_r].
    by rewrite -(g_tower X) HXY g_tower.
Qed.
(* iris/algebra/cofe_solver.v *)
Definition T : ofe
:= Ofe tower tower_ofe_mixin.
(* iris/algebra/cofe_solver.v *)
Definition tower_chain (c : chain T) (k : nat) : chain (A k) :=
  {| chain_car i := c i k |}.
Next Obligation. intros c k n i ?; by apply (chain_cauchy c n). Qed.
(* iris/algebra/cofe_solver.v *)
Definition tower_compl : Compl T := λ c,
  {| tower_car n := compl (tower_chain c n) |}.
Next Obligation.
  intros c k; apply equiv_dist=> n.
  by rewrite (conv_compl n (tower_chain c k))
    (conv_compl n (tower_chain c (S k))) /= (g_tower (c _) k).
Qed.
(* iris/algebra/cofe_solver.v *)
Instance tower_cofe : Cofe T := cofe_finite tower_compl _.
Next Obligation.
  intros n c k; rewrite /= (conv_compl n (tower_chain c k)). done.
Qed.
(* iris/algebra/cofe_solver.v *)
Fixpoint ff {k} (i : nat) : A k -n> A (i + k)
:=
  match i with 0 => cid | S i => f (i + k) ◎ ff i end.
(* iris/algebra/cofe_solver.v *)
Fixpoint gg {k} (i : nat) : A (i + k) -n> A k
:=
  match i with 0 => cid | S i => gg i ◎ g (i + k) end.
(* iris/algebra/cofe_solver.v *)
Lemma ggff {k i} (x : A k) : gg i (ff i x) ≡ x.
Proof using Fcontr. induction i as [|i IH]; simpl; [done|by rewrite (gf (ff i x)) IH]. Qed.
(* iris/algebra/cofe_solver.v *)
Lemma f_tower k (X : tower) : f (S k) (X (S k)) ≡{k}≡ X (S (S k)).
Proof using Fcontr. intros. by rewrite -(fg (X (S (S k)))) -(g_tower X). Qed.
(* iris/algebra/cofe_solver.v *)
Lemma ff_tower k i (X : tower) : ff i (X (S k)) ≡{k}≡ X (i + S k).
Proof using Fcontr.
  intros; induction i as [|i IH]; simpl; [done|].
  by rewrite IH Nat.add_succ_r (dist_le _ _ _ _ (f_tower _ X)); last lia.
Qed.
(* iris/algebra/cofe_solver.v *)
Lemma gg_tower k i (X : tower) : gg i (X (i + k)) ≡ X k.
Proof. by induction i as [|i IH]; simpl; [done|rewrite g_tower IH]. Qed.
(* iris/algebra/cofe_solver.v *)
Instance tower_car_ne k : NonExpansive (λ X, tower_car X k).
Proof. by intros X Y HX. Qed.
(* iris/algebra/cofe_solver.v *)
Definition project (k : nat) : T -n> A k
:= OfeMor (λ X : T, tower_car X k).
(* iris/algebra/cofe_solver.v *)
Definition coerce {i j} (H : i = j) : A i -n> A j
:=
  eq_rect _ (λ i', A i -n> A i') cid _ H.
(* iris/algebra/cofe_solver.v *)
Lemma coerce_id {i} (H : i = i) (x : A i) : coerce H x = x.
Proof. unfold coerce. by rewrite (proof_irrel H (eq_refl i)). Qed.
(* iris/algebra/cofe_solver.v *)
Lemma coerce_proper {i j} (x y : A i) (H1 H2 : i = j) :
  x = y → coerce H1 x = coerce H2 y.
Proof. by destruct H1; rewrite !coerce_id. Qed.
(* iris/algebra/cofe_solver.v *)
Lemma g_coerce {k j} (H : S k = S j) (x : A (S k)) :
  g j (coerce H x) = coerce (Nat.succ_inj _ _ H) (g k x).
Proof. by assert (k = j) by lia; subst; rewrite !coerce_id. Qed.
(* iris/algebra/cofe_solver.v *)
Lemma coerce_f {k j} (H : S k = S j) (x : A k) :
  coerce H (f k x) = f j (coerce (Nat.succ_inj _ _ H) x).
Proof. by assert (k = j) by lia; subst; rewrite !coerce_id. Qed.
(* iris/algebra/cofe_solver.v *)
Lemma gg_gg {k i i1 i2 j} : ∀ (H1: k = i + j) (H2: k = i2 + (i1 + j)) (x: A k),
  gg i (coerce H1 x) = gg i1 (gg i2 (coerce H2 x)).
Proof.
  intros Hij -> x. assert (i = i2 + i1) as -> by lia. revert j x Hij.
  induction i2 as [|i2 IH]; intros j X Hij; simplify_eq/=;
    [by rewrite coerce_id|by rewrite g_coerce IH].
Qed.
(* iris/algebra/cofe_solver.v *)
Lemma ff_ff {k i i1 i2 j} : ∀ (H1: i + k = j) (H2: i1 + (i2 + k) = j) (x: A k),
  coerce H1 (ff i x) = coerce H2 (ff i1 (ff i2 x)).
Proof.
  intros ? <- x. assert (i = i1 + i2) as -> by lia.
  induction i1 as [|i1 IH]; simplify_eq/=;
    [by rewrite coerce_id|by rewrite coerce_f IH].
Qed.
(* iris/algebra/cofe_solver.v *)
Definition embed_coerce {k} (i : nat) : A k -n> A i
:=
  match le_lt_dec i k with
  | left H => gg (k-i) ◎ coerce (eq_sym (Nat.sub_add _ _ H))
  | right H => coerce (Nat.sub_add k i (Nat.lt_le_incl _ _ H)) ◎ ff (i-k)
  end.
(* iris/algebra/cofe_solver.v *)
Lemma g_embed_coerce {k i} (x : A k) :
  g i (embed_coerce (S i) x) ≡ embed_coerce i x.
Proof using Fcontr.
  unfold embed_coerce; destruct (le_lt_dec (S i) k), (le_lt_dec i k); simpl.
  - symmetry; by erewrite (@gg_gg _ _ 1 (k - S i)); simpl.
  - exfalso; lia.
  - assert (i = k) by lia; subst.
    rewrite (ff_ff _ (eq_refl (1 + (0 + k)))) /= gf.
    by rewrite (gg_gg _ (eq_refl (0 + (0 + k)))).
  - assert (H : 1 + ((i - k) + k) = S i) by lia.
    rewrite (ff_ff _ H) /= -{2}(gf (ff (i - k) x)) g_coerce.
    by erewrite coerce_proper by done.
Qed.
(* iris/algebra/cofe_solver.v *)
Definition embed (k : nat) (x : A k) : T :=
  {| tower_car n := embed_coerce n x |}.
Next Obligation. intros k x i. apply g_embed_coerce. Qed.
(* iris/algebra/cofe_solver.v *)
Instance : Params (@embed) 1
:= {}.
(* iris/algebra/cofe_solver.v *)
Instance embed_ne k : NonExpansive (embed k).
Proof. by intros n x y Hxy i; rewrite /= Hxy. Qed.
(* iris/algebra/cofe_solver.v *)
Definition embed' (k : nat) : A k -n> T
:= OfeMor (embed k).
(* iris/algebra/cofe_solver.v *)
Lemma embed_f k (x : A k) : embed (S k) (f k x) ≡ embed k x.
Proof.
  rewrite equiv_dist=> n i; rewrite /embed /= /embed_coerce.
  destruct (le_lt_dec i (S k)), (le_lt_dec i k); simpl.
  - assert (H : S k = S (k - i) + (0 + i)) by lia; rewrite (gg_gg _ H) /=.
    by erewrite g_coerce, gf, coerce_proper by done.
  - assert (S k = 0 + (0 + i)) as H by lia.
    rewrite (gg_gg _ H); simplify_eq/=.
    by rewrite (ff_ff _ (eq_refl (1 + (0 + k)))).
  - exfalso; lia.
  - assert (H : (i - S k) + (1 + k) = i) by lia; rewrite (ff_ff _ H) /=.
    by erewrite coerce_proper by done.
Qed.
(* iris/algebra/cofe_solver.v *)
Lemma embed_tower k (X : T) : embed (S k) (X (S k)) ≡{k}≡ X.
Proof.
  intros i; rewrite /= /embed_coerce.
  destruct (le_lt_dec i (S k)) as [H|H]; simpl.
  - rewrite -(gg_tower i (S k - i) X).
    apply (_ : Proper (_ ==> _) (gg _)); by destruct (eq_sym _).
  - rewrite (ff_tower k (i - S k) X). by destruct (Nat.sub_add _ _ _).
Qed.
(* iris/algebra/cofe_solver.v *)
Instance tower_inhabited : Inhabited tower
:= populate (embed 0 ()).
(* iris/algebra/cofe_solver.v *)
Definition unfold_chain (X : T) : chain (oFunctor_apply F T) :=
  {| chain_car n := map (project n,embed' n) (X (S n)) |}.
Next Obligation.
  simpl; intros X n i Hi.
  assert (∃ k, i = k + n) as [k ?] by (exists (i - n); lia); subst; clear Hi.
  induction k as [|k IH]; simpl; first done.
  rewrite -IH -(dist_le _ _ _ _ (f_tower (k + n) _)); last lia.
  rewrite f_S -oFunctor_map_compose.
  by apply (contractive_ne map); split=> Y /=; rewrite ?g_tower ?embed_f.
Qed.
(* iris/algebra/cofe_solver.v *)
Definition unfold (X : T) : oFunctor_apply F T
:= compl (unfold_chain X).
(* iris/algebra/cofe_solver.v *)
Instance unfold_ne : NonExpansive unfold.
Proof.
  intros n X Y HXY. by rewrite /unfold (conv_compl n (unfold_chain X))
    (conv_compl n (unfold_chain Y)) /= (HXY (S n)).
Qed.
(* iris/algebra/cofe_solver.v *)
Definition fold (X : oFunctor_apply F T) : T :=
  {| tower_car n := g n (map (embed' n,project n) X) |}.
Next Obligation.
  intros X k. apply (_ : Proper ((≡) ==> (≡)) (g k)).
  rewrite g_S -oFunctor_map_compose.
  apply (contractive_proper map); split=> Y; [apply embed_f|apply g_tower].
Qed.
(* iris/algebra/cofe_solver.v *)
Instance fold_ne : NonExpansive fold.
Proof. by intros n X Y HXY k; rewrite /fold /= HXY. Qed.
(* iris/algebra/cofe_solver.v *)
Theorem result : solution F.
Proof using Type*.
  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)))).
    { rewrite /unfold (conv_compl n (unfold_chain X)).
      rewrite -(chain_cauchy (unfold_chain X) n (S (n + k))) /=; last lia.
      rewrite -(dist_le _ _ _ _ (f_tower (n + k) _)); last lia.
      rewrite f_S -!oFunctor_map_compose; apply (contractive_ne map); split=> Y.
      + rewrite /embed' /= /embed_coerce.
        destruct (le_lt_dec _ _); simpl; [exfalso; lia|].
        by rewrite (ff_ff _ (eq_refl (S n + (0 + k)))) /= gf.
      + rewrite /embed' /= /embed_coerce.
        destruct (le_lt_dec _ _); simpl; [|exfalso; lia].
        by rewrite (gg_gg _ (eq_refl (0 + (S n + k)))) /= gf. }
    assert (∀ i k (x : A (S i + k)) (H : S i + k = i + S k),
      map (ff i, gg i) x ≡ gg i (coerce H x)) as map_ff_gg.
    { intros i; induction i as [|i IH]; intros k' x H; simpl.
      { by rewrite coerce_id oFunctor_map_id. }
      rewrite oFunctor_map_compose g_coerce; apply IH. }
    assert (H: S n + k = n + S k) by lia.
    rewrite (map_ff_gg _ _ _ H).
    apply (_ : Proper (_ ==> _) (gg _)); by destruct H.
  - intros X; rewrite equiv_dist=> n /=.
    rewrite /unfold /= (conv_compl_S n (unfold_chain (fold X))) /=.
    rewrite g_S -!oFunctor_map_compose -{2}[X]oFunctor_map_id.
    apply (contractive_ne map); split => Y /=.
    + rewrite f_tower. apply dist_S. by rewrite embed_tower.
    + etrans; [apply embed_ne, equiv_dist, g_tower|apply embed_tower].
Qed.
(* iris/algebra/coPset.v *)
Canonical coPsetO
:= discreteO coPset.
(* iris/algebra/coPset.v *)
Instance coPset_valid_instance : Valid coPset
:= λ _, True.
(* iris/algebra/coPset.v *)
Instance coPset_unit_instance : Unit coPset
:= (∅ : coPset).
(* iris/algebra/coPset.v *)
Instance coPset_op_instance : Op coPset
:= union.
(* iris/algebra/coPset.v *)
Instance coPset_pcore_instance : PCore coPset
:= Some.
(* iris/algebra/coPset.v *)
Lemma coPset_op X Y : X ⋅ Y = X ∪ Y.
Proof. done. Qed.
(* iris/algebra/coPset.v *)
Lemma coPset_core X : core X = X.
Proof. done. Qed.
(* iris/algebra/coPset.v *)
Lemma coPset_included X Y : X ≼ Y ↔ X ⊆ Y.
Proof.
    split.
    - intros [Z ->]. rewrite coPset_op. set_solver.
    - intros (Z&->&?)%subseteq_disjoint_union_L. by exists Z.
  Qed.
(* iris/algebra/coPset.v *)
Lemma coPset_ra_mixin : RAMixin coPset.
Proof.
    apply ra_total_mixin; eauto.
    - solve_proper.
    - solve_proper.
    - solve_proper.
    - intros X1 X2 X3. by rewrite !coPset_op assoc_L.
    - intros X1 X2. by rewrite !coPset_op comm_L.
    - intros X. by rewrite coPset_core idemp_L.
  Qed.
(* iris/algebra/coPset.v *)
Canonical coPsetR
:= discreteR coPset coPset_ra_mixin.
(* iris/algebra/coPset.v *)
Instance coPset_cmra_discrete : CmraDiscrete coPsetR.
Proof. apply discrete_cmra_discrete. Qed.
(* iris/algebra/coPset.v *)
Lemma coPset_ucmra_mixin : UcmraMixin coPset.
Proof. split; [done | | done]. intros X. by rewrite coPset_op left_id_L. Qed.
(* iris/algebra/coPset.v *)
Canonical coPsetUR
:= Ucmra coPset coPset_ucmra_mixin.
(* iris/algebra/coPset.v *)
Lemma coPset_opM X mY : X ⋅? mY = X ∪ default ∅ mY.
Proof using SI. destruct mY; by rewrite /= ?right_id_L. Qed.
(* iris/algebra/coPset.v *)
Lemma coPset_update X Y : X ~~> Y.
Proof. done. Qed.
(* iris/algebra/coPset.v *)
Lemma coPset_local_update X Y X' : X ⊆ X' → (X,Y) ~l~> (X',X').
Proof.
    intros (Z&->&?)%subseteq_disjoint_union_L.
    rewrite local_update_unital_discrete=> Z' _ /leibniz_equiv_iff->.
    split; first done. rewrite coPset_op. set_solver.
  Qed.
(* iris/algebra/coPset.v *)
(* The disjoint union CMRA *)
Inductive coPset_disj
:=
  | CoPset : coPset → coPset_disj
  | CoPsetInvalid : coPset_disj.
(* iris/algebra/coPset.v *)
Canonical coPset_disjO
:= leibnizO coPset_disj.
(* iris/algebra/coPset.v *)
Instance coPset_disj_valid_instance : Valid coPset_disj
:= λ X,
    match X with CoPset _ => True | CoPsetInvalid => False end.
(* iris/algebra/coPset.v *)
Instance coPset_disj_unit_instance : Unit coPset_disj
:= CoPset ∅.
(* iris/algebra/coPset.v *)
Instance coPset_disj_op_instance : Op coPset_disj
:= λ X Y,
    match X, Y with
    | CoPset X, CoPset Y => if decide (X ## Y) then CoPset (X ∪ Y) else CoPsetInvalid
    | _, _ => CoPsetInvalid
    end.
(* iris/algebra/coPset.v *)
Instance coPset_disj_pcore_instance : PCore coPset_disj
:= λ _, Some ε.
(* iris/algebra/coPset.v *)
Ltac coPset_disj_solve
:=
    repeat (simpl || case_decide);
    first [apply (f_equal CoPset)|done|exfalso]; set_solver by eauto.
(* iris/algebra/coPset.v *)
Lemma coPset_disj_included X Y : CoPset X ≼ CoPset Y ↔ X ⊆ Y.
Proof.
    split.
    - move=> [[Z|]]; simpl; try case_decide; set_solver.
    - intros (Z&->&?)%subseteq_disjoint_union_L.
      exists (CoPset Z). coPset_disj_solve.
  Qed.
(* iris/algebra/coPset.v *)
Lemma coPset_disj_valid_inv_l X Y :
    ✓ (CoPset X ⋅ Y) → ∃ Y', Y = CoPset Y' ∧ X ## Y'.
Proof. destruct Y; repeat (simpl || case_decide); by eauto. Qed.
(* iris/algebra/coPset.v *)
Lemma coPset_disj_union X Y : X ## Y → CoPset X ⋅ CoPset Y = CoPset (X ∪ Y).
Proof. intros. by rewrite /= decide_True. Qed.
(* iris/algebra/coPset.v *)
Lemma coPset_disj_valid_op X Y : ✓ (CoPset X ⋅ CoPset Y) ↔ X ## Y.
Proof. simpl. case_decide; by split. Qed.
(* iris/algebra/coPset.v *)
Lemma coPset_disj_ra_mixin : RAMixin coPset_disj.
Proof.
    apply ra_total_mixin; eauto.
    - intros [?|]; destruct 1; coPset_disj_solve.
    - by constructor.
    - by destruct 1.
    - intros [X1|] [X2|] [X3|]; coPset_disj_solve.
    - intros [X1|] [X2|]; coPset_disj_solve.
    - intros [X|]; coPset_disj_solve.
    - exists (CoPset ∅); coPset_disj_solve.
    - intros [X1|] [X2|]; coPset_disj_solve.
  Qed.
(* iris/algebra/coPset.v *)
Canonical coPset_disjR
:= discreteR coPset_disj coPset_disj_ra_mixin.