phanerozoic/Coq-Iris huggingface dataset:
(* iris/proofmode/class_instances.v *)
Instance from_forall_pure `{!BiPureForall PROP} {A} (φ : A → Prop) name :
  AsIdentName φ name → @FromForall PROP A ⌜∀ a : A, φ a⌝ (λ a, ⌜ φ a ⌝)%I name.
Proof. by rewrite /FromForall pure_forall_2. Qed.
(* iris/proofmode/class_instances.v *)
Instance from_tforall_pure `{!BiPureForall PROP}
    {TT : tele} (φ : TT → Prop) name :
  AsIdentName φ name → @FromForall PROP TT ⌜tforall φ⌝ (λ x, ⌜ φ x ⌝)%I name.
Proof. by rewrite /FromForall tforall_forall pure_forall. Qed.
(* iris/proofmode/class_instances.v *)
(* [H] is the default name for the [φ] hypothesis, in the following three instances *)
Instance from_forall_pure_not `{!BiPureForall PROP} (φ : Prop) :
  @FromForall PROP φ ⌜¬ φ⌝ (λ _ : φ, False)%I (to_ident_name H).
Proof. by rewrite /FromForall pure_forall. Qed.
(* iris/proofmode/class_instances.v *)
Instance from_forall_impl_pure P Q φ :
  IntoPureT P φ → FromForall (P → Q) (λ _ : φ, Q) (to_ident_name H).
Proof.
  intros (φ'&->&?). by rewrite /FromForall -pure_impl_forall (into_pure P).
Qed.
(* iris/proofmode/class_instances.v *)
Instance from_forall_wand_pure P Q φ :
  IntoPureT P φ → TCOr (Affine P) (Absorbing Q) →
  FromForall (P -∗ Q) (λ _ : φ, Q)%I (to_ident_name H).
Proof.
  intros (φ'&->&?) [|]; rewrite /FromForall; apply wand_intro_r.
  - rewrite -(affine_affinely P) (into_pure P) -persistent_and_affinely_sep_r.
    apply pure_elim_r=>?. by rewrite forall_elim.
  - by rewrite (into_pure P) -pure_wand_forall wand_elim_l.
Qed.
(* iris/proofmode/class_instances.v *)
Instance from_forall_intuitionistically `{!BiAffine PROP, !BiPersistentlyForall PROP}
    {A} P (Φ : A → PROP) name :
  FromForall P Φ name → FromForall (□ P) (λ a, □ (Φ a))%I name.
Proof.
  rewrite /FromForall=> <-. setoid_rewrite intuitionistically_into_persistently.
  by rewrite persistently_forall.
Qed.
(* iris/proofmode/class_instances.v *)
Instance from_forall_persistently `{!BiPersistentlyForall PROP}
    {A} P (Φ : A → PROP) name :
  FromForall P Φ name → FromForall (<pers> P) (λ a, <pers> (Φ a))%I name.
Proof. rewrite /FromForall=> <-. by rewrite persistently_forall. Qed.
(* iris/proofmode/class_instances.v *)
(* ElimModal *)
Instance elim_modal_wand φ p p' P P' Q Q' R :
  ElimModal φ p p' P P' Q Q' → ElimModal φ p p' P P' (R -∗ Q) (R -∗ Q').
Proof.
  rewrite /ElimModal=> H Hφ. apply wand_intro_r.
  rewrite wand_curry -assoc (comm _ (□?p' _)%I) -wand_curry wand_elim_l; auto.
Qed.
(* iris/proofmode/class_instances.v *)
Instance elim_modal_wandM φ p p' P P' Q Q' mR :
  ElimModal φ p p' P P' Q Q' →
  ElimModal φ p p' P P' (mR -∗? Q) (mR -∗? Q').
Proof. rewrite /ElimModal !wandM_sound. exact: elim_modal_wand. Qed.
(* iris/proofmode/class_instances.v *)
Instance elim_modal_forall {A} φ p p' P P' (Φ Ψ : A → PROP) :
  (∀ x, ElimModal φ p p' P P' (Φ x) (Ψ x)) →
  ElimModal φ p p' P P' (∀ x, Φ x) (∀ x, Ψ x).
Proof.
  rewrite /ElimModal=> H ?. apply forall_intro=> a. rewrite (forall_elim a); auto.
Qed.
(* iris/proofmode/class_instances.v *)
Instance elim_modal_tforall {TT : tele} φ p p' P P' (Φ Ψ : TT → PROP) :
  (∀ x, ElimModal φ p p' P P' (Φ x) (Ψ x)) →
  ElimModal φ p p' P P' (∀.. x, Φ x) (∀.. x, Ψ x).
Proof. rewrite /ElimModal !bi_tforall_forall. apply elim_modal_forall. Qed.
(* iris/proofmode/class_instances.v *)
Instance elim_modal_absorbingly_here p P Q :
  Absorbing Q → ElimModal True p false (<absorb> P) P Q Q.
Proof.
  rewrite /ElimModal=> ? _. by rewrite intuitionistically_if_elim
    absorbingly_sep_l wand_elim_r absorbing_absorbingly.
Qed.
(* iris/proofmode/class_instances.v *)
(* AddModal *)
Instance add_modal_wand P P' Q R :
  AddModal P P' Q → AddModal P P' (R -∗ Q).
Proof.
  rewrite /AddModal=> H. apply wand_intro_r.
  by rewrite wand_curry -assoc (comm _ P') -wand_curry wand_elim_l.
Qed.
(* iris/proofmode/class_instances.v *)
Instance add_modal_wandM P P' Q mR :
  AddModal P P' Q → AddModal P P' (mR -∗? Q).
Proof. rewrite /AddModal wandM_sound. exact: add_modal_wand. Qed.
(* iris/proofmode/class_instances.v *)
Instance add_modal_forall {A} P P' (Φ : A → PROP) :
  (∀ x, AddModal P P' (Φ x)) → AddModal P P' (∀ x, Φ x).
Proof.
  rewrite /AddModal=> H. apply forall_intro=> a. by rewrite (forall_elim a).
Qed.
(* iris/proofmode/class_instances.v *)
Instance add_modal_tforall {TT : tele} P P' (Φ : TT → PROP) :
  (∀ x, AddModal P P' (Φ x)) → AddModal P P' (∀.. x, Φ x).
Proof. rewrite /AddModal bi_tforall_forall. apply add_modal_forall. Qed.
(* iris/proofmode/class_instances.v *)
(* ElimInv *)
Instance elim_inv_acc_without_close {X : Type}
     φ1 φ2 Pinv Pin (M1 M2 : PROP → PROP) α β mγ Q (Q' : X → PROP) :
  IntoAcc (X:=X) Pinv φ1 Pin M1 M2 α β mγ →
  ElimAcc (X:=X) φ2 M1 M2 α β mγ Q Q' →
  ElimInv (φ1 ∧ φ2) Pinv Pin α None Q Q'.
Proof.
  rewrite /ElimAcc /IntoAcc /ElimInv.
  iIntros (Hacc Helim [??]) "(Hinv & Hin & Hcont)".
  iApply (Helim with "[Hcont]"); first done.
  - iIntros (x) "Hα". iApply "Hcont". iSplitL; simpl; done.
  - iApply (Hacc with "Hinv Hin"). done.
Qed.
(* iris/proofmode/class_instances.v *)
(* This uses [pm_default] because, after inference, all accessors will have
[None] or [Some _] there, so we want to reduce the combinator before showing the
goal to the user. *)
Instance elim_inv_acc_with_close {X : Type}
    φ1 φ2 Pinv Pin (M1 M2 : PROP → PROP) α β mγ Q Q' :
  IntoAcc Pinv φ1 Pin M1 M2 α β mγ →
  (∀ R, ElimModal φ2 false false (M1 R) R Q Q') →
  ElimInv (X:=X) (φ1 ∧ φ2) Pinv Pin
          α
          (Some (λ x, β x -∗ M2 (pm_default emp (mγ x))))%I
          Q (λ _, Q').
Proof.
  rewrite /ElimAcc /IntoAcc /ElimInv.
  iIntros (Hacc Helim [??]) "(Hinv & Hin & Hcont)".
  iMod (Hacc with "Hinv Hin") as (x) "[Hα Hclose]"; first done.
  iApply "Hcont". simpl. iSplitL "Hα"; done.
Qed.
(* iris/proofmode/class_instances_cmra.v *)
Instance into_pure_internal_cmra_valid `{!CmraDiscrete A} (a : A) :
    @IntoPure PROP (✓ a) (✓ a).
Proof. by rewrite /IntoPure internal_cmra_valid_discrete. Qed.
(* iris/proofmode/class_instances_cmra.v *)
Instance from_pure_internal_cmra_valid {A : cmra} (a : A) :
    @FromPure PROP false (✓ a) (✓ a).
Proof.
    rewrite /FromPure /=. apply bi.pure_elim'=> ?.
    rewrite -internal_cmra_valid_intro //.
  Qed.
(* iris/proofmode/class_instances_cmra.v *)
Instance into_pure_internal_included {A : cmra} (a b : A) `{!Discrete b} :
    @IntoPure PROP (a ≼ b) (a ≼ b).
Proof. by rewrite /IntoPure internal_included_discrete. Qed.
(* iris/proofmode/class_instances_cmra.v *)
Instance from_pure_internal_included {A : cmra} (a b : A) :
    @FromPure PROP false (a ≼ b) (a ≼ b).
Proof.
    rewrite /FromPure /=. apply bi.pure_elim'=> ?.
    rewrite -internal_included_intro //.
  Qed.
(* iris/proofmode/class_instances_cmra.v *)
Instance into_exist_internal_included {A : cmra} (a b : A) :
    IntoExist (PROP:=PROP) (a ≼ b) (λ c, b ≡ a ⋅ c)%I (λ x, x).
Proof. by rewrite /IntoExist. Qed.
(* iris/proofmode/class_instances_cmra.v *)
Instance from_exist_internal_included {A : cmra} (a b : A) :
    FromExist (PROP:=PROP) (a ≼ b) (λ c, b ≡ a ⋅ c)%I.
Proof. by rewrite /FromExist. Qed.
(* iris/proofmode/class_instances_embedding.v *)
(* We add a useless hypothesis [BiEmbed PROP PROP'] in order to make sure this
instance is not used when there is no embedding between [PROP] and [PROP']. The
first [`{BiEmbed PROP PROP'}] is not considered as a premise by Coq TC search
mechanism because the rest of the hypothesis is dependent on it. *)
Instance as_emp_valid_embed `{!BiEmbed PROP PROP'} d (φ : Prop) (P : PROP) :
  BiEmbed PROP PROP' →
  AsEmpValid0 d φ P → AsEmpValid d φ ⎡P⎤.
Proof. rewrite /AsEmpValid0 /AsEmpValid=> _ [? ?]. rewrite embed_emp_valid //. Qed.
(* iris/proofmode/class_instances_embedding.v *)
Instance into_pure_embed P φ :
  IntoPure P φ → IntoPure ⎡P⎤ φ.
Proof. rewrite /IntoPure=> ->. by rewrite embed_pure. Qed.
(* iris/proofmode/class_instances_embedding.v *)
Instance from_pure_embed a P φ :
  FromPure a P φ → FromPure a ⎡P⎤ φ.
Proof. rewrite /FromPure=> <-. by rewrite -embed_pure embed_affinely_if_2. Qed.
(* iris/proofmode/class_instances_embedding.v *)
Instance into_persistent_embed p P Q :
  IntoPersistent p P Q → IntoPersistent p ⎡P⎤ ⎡Q⎤ | 0.
Proof.
  rewrite /IntoPersistent -embed_persistently -embed_persistently_if=> -> //.
Qed.
(* iris/proofmode/class_instances_embedding.v *)
(* When having a modality nested in an embedding, e.g. [ ⎡|==> P⎤ ], we prefer
the embedding over the modality. *)
Instance from_modal_embed P :
  FromModal True (@modality_embed PROP PROP' _) ⎡P⎤ ⎡P⎤ P.
Proof. by rewrite /FromModal. Qed.
(* iris/proofmode/class_instances_embedding.v *)
Instance from_modal_id_embed φ `(sel : A) P Q :
  FromModal φ modality_id sel P Q →
  FromModal φ modality_id sel ⎡P⎤ ⎡Q⎤ | 100.
Proof. rewrite /FromModal /= =>HPQ ?. by rewrite -HPQ. Qed.
(* iris/proofmode/class_instances_embedding.v *)
Instance from_modal_affinely_embed φ `(sel : A) P Q :
  FromModal φ modality_affinely sel P Q →
  FromModal φ modality_affinely sel ⎡P⎤ ⎡Q⎤ | 100.
Proof. rewrite /FromModal /= =>HPQ ?. by rewrite -HPQ // embed_affinely_2. Qed.
(* iris/proofmode/class_instances_embedding.v *)
Instance from_modal_persistently_embed φ `(sel : A) P Q :
  FromModal φ modality_persistently sel P Q →
  FromModal φ modality_persistently sel ⎡P⎤ ⎡Q⎤ | 100.
Proof. rewrite /FromModal /= =>HPQ ?. by rewrite -HPQ // embed_persistently. Qed.
(* iris/proofmode/class_instances_embedding.v *)
Instance from_modal_intuitionistically_embed φ `(sel : A) P Q :
  FromModal φ modality_intuitionistically sel P Q →
  FromModal φ modality_intuitionistically sel ⎡P⎤ ⎡Q⎤ | 100.
Proof. rewrite /FromModal /= =>HPQ ?. by rewrite -HPQ // embed_intuitionistically_2. Qed.
(* iris/proofmode/class_instances_embedding.v *)
Instance into_wand_embed p q R P Q :
  IntoWand p q R P Q → IntoWand p q ⎡R⎤ ⎡P⎤ ⎡Q⎤.
Proof. by rewrite /IntoWand !embed_intuitionistically_if_2 -embed_wand=> ->. Qed.
(* iris/proofmode/class_instances_embedding.v *)
(* There are two versions for [IntoWand ⎡R⎤ ...] with the argument being
[<affine> ⎡P⎤]. When the wand [⎡R⎤] resides in the intuitionistic context
the result of wand elimination will have the affine modality. Otherwise, it
won't. Note that when the wand [⎡R⎤] is under an affine modality, the instance
[into_wand_affine] would already have been used. *)
Instance into_wand_affine_embed_true q P Q R :
  IntoWand true q R P Q → IntoWand true q ⎡R⎤ (<affine> ⎡P⎤) (<affine> ⎡Q⎤) | 100.
Proof.
  rewrite /IntoWand /=.
  rewrite -(intuitionistically_idemp ⎡ _ ⎤) embed_intuitionistically_2=> ->.
  apply bi.wand_intro_l. destruct q; simpl.
  - rewrite affinely_elim  -(intuitionistically_idemp ⎡ _ ⎤).
    rewrite embed_intuitionistically_2 intuitionistically_sep_2 -embed_sep.
    by rewrite wand_elim_r intuitionistically_affinely.
  - by rewrite intuitionistically_affinely affinely_sep_2 -embed_sep wand_elim_r.
Qed.
(* iris/proofmode/class_instances_embedding.v *)
Instance into_wand_affine_embed_false q P Q R :
  IntoWand false q R (<affine> P) Q →
  IntoWand false q ⎡R⎤ (<affine> ⎡P⎤) ⎡Q⎤ | 100.
Proof.
  rewrite /IntoWand /= => ->.
  by rewrite embed_affinely_2 embed_intuitionistically_if_2 embed_wand.
Qed.
(* iris/proofmode/class_instances_embedding.v *)
Instance from_wand_embed P Q1 Q2 :
  FromWand P Q1 Q2 → FromWand ⎡P⎤ ⎡Q1⎤ ⎡Q2⎤.
Proof. by rewrite /FromWand -embed_wand => <-. Qed.
(* iris/proofmode/class_instances_embedding.v *)
Instance from_impl_embed P Q1 Q2 :
  FromImpl P Q1 Q2 → FromImpl ⎡P⎤ ⎡Q1⎤ ⎡Q2⎤.
Proof. by rewrite /FromImpl -embed_impl => <-. Qed.
(* iris/proofmode/class_instances_embedding.v *)
Instance from_and_embed P Q1 Q2 :
  FromAnd P Q1 Q2 → FromAnd ⎡P⎤ ⎡Q1⎤ ⎡Q2⎤.
Proof. by rewrite /FromAnd -embed_and => <-. Qed.
(* iris/proofmode/class_instances_embedding.v *)
Instance from_sep_embed P Q1 Q2 :
  FromSep P Q1 Q2 → FromSep ⎡P⎤ ⎡Q1⎤ ⎡Q2⎤.
Proof. by rewrite /FromSep -embed_sep => <-. Qed.
(* iris/proofmode/class_instances_embedding.v *)
Instance maybe_combine_sep_as_embed Q1 Q2 P progress :
  MaybeCombineSepAs Q1 Q2 P progress →
  MaybeCombineSepAs ⎡Q1⎤ ⎡Q2⎤ ⎡P⎤ progress.
Proof. by rewrite /MaybeCombineSepAs -embed_sep => <-. Qed.
(* iris/proofmode/class_instances_embedding.v *)
Instance combine_sep_gives_embed Q1 Q2 P :
  CombineSepGives Q1 Q2 P →
  CombineSepGives ⎡Q1⎤ ⎡Q2⎤ ⎡P⎤.
Proof. by rewrite /CombineSepGives -embed_sep -embed_persistently => ->. Qed.
(* iris/proofmode/class_instances_embedding.v *)
Instance into_and_embed p P Q1 Q2 :
  IntoAnd p P Q1 Q2 → IntoAnd p ⎡P⎤ ⎡Q1⎤ ⎡Q2⎤.
Proof.
  rewrite /IntoAnd -embed_and=> HP. apply intuitionistically_if_intro'.
  by rewrite embed_intuitionistically_if_2 HP intuitionistically_if_elim.
Qed.
(* iris/proofmode/class_instances_embedding.v *)
Instance into_sep_embed P Q1 Q2 :
  IntoSep P Q1 Q2 → IntoSep ⎡P⎤ ⎡Q1⎤ ⎡Q2⎤.
Proof. rewrite /IntoSep -embed_sep=> -> //. Qed.
(* iris/proofmode/class_instances_embedding.v *)
Instance from_or_embed P Q1 Q2 :
  FromOr P Q1 Q2 → FromOr ⎡P⎤ ⎡Q1⎤ ⎡Q2⎤.
Proof. by rewrite /FromOr -embed_or => <-. Qed.
(* iris/proofmode/class_instances_embedding.v *)
Instance into_or_embed P Q1 Q2 :
  IntoOr P Q1 Q2 → IntoOr ⎡P⎤ ⎡Q1⎤ ⎡Q2⎤.
Proof. by rewrite /IntoOr -embed_or => <-. Qed.
(* iris/proofmode/class_instances_embedding.v *)
Instance from_exist_embed {A} P (Φ : A → PROP) :
  FromExist P Φ → FromExist ⎡P⎤ (λ a, ⎡Φ a⎤%I).
Proof. by rewrite /FromExist -embed_exist => <-. Qed.
(* iris/proofmode/class_instances_embedding.v *)
Instance into_exist_embed {A} P (Φ : A → PROP) name :
  IntoExist P Φ name → IntoExist ⎡P⎤ (λ a, ⎡Φ a⎤%I) name.
Proof. by rewrite /IntoExist -embed_exist => <-. Qed.
(* iris/proofmode/class_instances_embedding.v *)
Instance into_forall_embed {A} P (Φ : A → PROP) :
  IntoForall P Φ → IntoForall ⎡P⎤ (λ a, ⎡Φ a⎤%I).
Proof. by rewrite /IntoForall -embed_forall => <-. Qed.
(* iris/proofmode/class_instances_embedding.v *)
Instance from_forall_embed {A} P (Φ : A → PROP) name :
  FromForall P Φ name → FromForall ⎡P⎤ (λ a, ⎡Φ a⎤%I) name.
Proof. by rewrite /FromForall -embed_forall => <-. Qed.
(* iris/proofmode/class_instances_embedding.v *)
Instance into_inv_embed P N : IntoInv P N → IntoInv ⎡P⎤ N
:= {}.
(* iris/proofmode/class_instances_embedding.v *)
Instance is_except_0_embed `{!BiEmbedLater PROP PROP'} P :
  IsExcept0 P → IsExcept0 ⎡P⎤.
Proof. by rewrite /IsExcept0 -embed_except_0=>->. Qed.
(* iris/proofmode/class_instances_embedding.v *)
Instance from_modal_later_embed `{!BiEmbedLater PROP PROP'} φ `(sel : A) n P Q :
  FromModal φ (modality_laterN n) sel P Q →
  FromModal φ (modality_laterN n) sel ⎡P⎤ ⎡Q⎤.
Proof. rewrite /FromModal /= =>HPQ ?. by rewrite -HPQ // embed_laterN. Qed.
(* iris/proofmode/class_instances_embedding.v *)
Instance from_modal_plainly_embed
    `{!Sbi PROP, !Sbi PROP', !BiEmbedSbi PROP PROP'} φ `(sel : A) P Q :
  FromModal φ modality_plainly sel P Q →
  FromModal φ (PROP2:=PROP') modality_plainly sel ⎡P⎤ ⎡Q⎤ | 100.
Proof. rewrite /FromModal /= =>HPQ ?. by rewrite -HPQ // embed_plainly. Qed.
(* iris/proofmode/class_instances_embedding.v *)
Instance into_internal_eq_embed
    `{!Sbi PROP, !Sbi PROP', !BiEmbedSbi PROP PROP'}
    {A : ofe} (x y : A) (P : PROP) :
  IntoInternalEq P x y → IntoInternalEq (⎡P⎤ : PROP')%I x y.
Proof. rewrite /IntoInternalEq=> ->. by rewrite embed_internal_eq. Qed.
(* iris/proofmode/class_instances_embedding.v *)
Instance into_except_0_embed `{!BiEmbedLater PROP PROP'} P Q :
  IntoExcept0 P Q → IntoExcept0 ⎡P⎤ ⎡Q⎤.
Proof. rewrite /IntoExcept0=> ->. by rewrite embed_except_0. Qed.
(* iris/proofmode/class_instances_embedding.v *)
Instance elim_modal_embed_bupd_goal
    `{!BiBUpd PROP, !BiBUpd PROP', !BiEmbedBUpd PROP PROP'}
    p p' φ (P P' : PROP') (Q Q' : PROP) :
  ElimModal φ p p' P P' (|==> ⎡Q⎤)%I (|==> ⎡Q'⎤)%I →
  ElimModal φ p p' P P' ⎡|==> Q⎤ ⎡|==> Q'⎤.
Proof. by rewrite /ElimModal !embed_bupd. Qed.
(* iris/proofmode/class_instances_embedding.v *)
Instance elim_modal_embed_bupd_hyp
    `{!BiBUpd PROP, !BiBUpd PROP', !BiEmbedBUpd PROP PROP'}
    p p' φ (P : PROP) (P' Q Q' : PROP') :
  ElimModal φ p p' (|==> ⎡P⎤)%I P' Q Q' →
  ElimModal φ p p' ⎡|==> P⎤ P' Q Q'.
Proof. by rewrite /ElimModal !embed_bupd. Qed.
(* iris/proofmode/class_instances_embedding.v *)
Instance elim_modal_embed_fupd_goal
    `{!BiFUpd PROP, !BiFUpd PROP', !BiEmbedFUpd PROP PROP'}
    p p' φ E1 E2 E3 (P P' : PROP') (Q Q' : PROP) :
  ElimModal φ p p' P P' (|={E1,E3}=> ⎡Q⎤)%I (|={E2,E3}=> ⎡Q'⎤)%I →
  ElimModal φ p p' P P' ⎡|={E1,E3}=> Q⎤ ⎡|={E2,E3}=> Q'⎤.
Proof. by rewrite /ElimModal !embed_fupd. Qed.
(* iris/proofmode/class_instances_embedding.v *)
Instance elim_modal_embed_fupd_hyp
    `{!BiFUpd PROP, !BiFUpd PROP', !BiEmbedFUpd PROP PROP'}
    p p' φ E1 E2 (P : PROP) (P' Q Q' : PROP') :
  ElimModal φ p p' (|={E1,E2}=> ⎡P⎤)%I P' Q Q' →
  ElimModal φ p p' ⎡|={E1,E2}=> P⎤ P' Q Q'.
Proof. by rewrite /ElimModal embed_fupd. Qed.
(* iris/proofmode/class_instances_embedding.v *)
Instance add_modal_embed_bupd_goal
    `{!BiBUpd PROP, !BiBUpd PROP', !BiEmbedBUpd PROP PROP'}
    (P P' : PROP') (Q : PROP) :
  AddModal P P' (|==> ⎡Q⎤)%I → AddModal P P' ⎡|==> Q⎤.
Proof. by rewrite /AddModal !embed_bupd. Qed.
(* iris/proofmode/class_instances_embedding.v *)
Instance add_modal_embed_fupd_goal
    `{!BiFUpd PROP, !BiFUpd PROP', !BiEmbedFUpd PROP PROP'}
    E1 E2 (P P' : PROP') (Q : PROP) :
  AddModal P P' (|={E1,E2}=> ⎡Q⎤)%I → AddModal P P' ⎡|={E1,E2}=> Q⎤.
Proof. by rewrite /AddModal !embed_fupd. Qed.
(* iris/proofmode/class_instances_embedding.v *)
Instance into_embed_embed P : IntoEmbed ⎡P⎤ P.
Proof. by rewrite /IntoEmbed. Qed.
(* iris/proofmode/class_instances_embedding.v *)
Instance into_embed_affinely
    `{!BiBUpd PROP, !BiBUpd PROP', !BiEmbedBUpd PROP PROP'} (P : PROP') (Q : PROP) :
  IntoEmbed P Q → IntoEmbed (<affine> P) (<affine> Q).
Proof. rewrite /IntoEmbed=> ->. by rewrite embed_affinely_2. Qed.
(* iris/proofmode/class_instances_embedding.v *)
Instance into_later_embed `{!BiEmbedLater PROP PROP'} n P Q :
  IntoLaterN false n P Q → IntoLaterN false n ⎡P⎤ ⎡Q⎤.
Proof. rewrite /IntoLaterN /MaybeIntoLaterN=> ->. by rewrite embed_laterN. Qed.
(* iris/proofmode/class_instances_frame.v *)
(* When framing [R] against itself, we leave [True] if possible (via
[frame_here_absorbing] or [frame_affinely_here_absorbing]) since it is a weaker
goal. Otherwise we leave [emp] via [frame_here].
Only if all those options fail, we start decomposing [R], via instances like
[frame_exist]. To ensure that, all other instances must have cost > 1. *)
Lemma frame_here_absorbing {PROP : bi} p (R : PROP) :
  QuickAbsorbing R → Frame p R R True.
Proof.
  rewrite /QuickAbsorbing /Frame. intros.
  by rewrite intuitionistically_if_elim sep_elim_l.
Qed.
(* iris/proofmode/class_instances_frame.v *)
Lemma frame_here {PROP : bi} p (R : PROP) : Frame p R R emp.
Proof. intros. by rewrite /Frame intuitionistically_if_elim sep_elim_l. Qed.
(* iris/proofmode/class_instances_frame.v *)
Lemma frame_affinely_here_absorbing {PROP : bi} p (R : PROP) :
  QuickAbsorbing R → Frame p (<affine> R) R True.
Proof.
  rewrite /QuickAbsorbing /Frame. intros.
  rewrite intuitionistically_if_elim affinely_elim. apply sep_elim_l, _.
Qed.
(* iris/proofmode/class_instances_frame.v *)
Lemma frame_affinely_here {PROP : bi} p (R : PROP) : Frame p (<affine> R) R emp.
Proof.
  intros. rewrite /Frame intuitionistically_if_elim affinely_elim.
  apply sep_elim_l, _.
Qed.
(* iris/proofmode/class_instances_frame.v *)
Instance frame_here_pure_persistent a φ Q :
  FromPure a Q φ → Frame true ⌜φ⌝ Q emp | 2.
Proof.
  rewrite /FromPure /Frame /= => <-. rewrite right_id.
  by rewrite -affinely_affinely_if intuitionistically_affinely.
Qed.
(* iris/proofmode/class_instances_frame.v *)
Instance frame_here_pure a φ Q :
  FromPure a Q φ →
  TCOr (TCEq a false) (BiAffine PROP) →
  Frame false ⌜φ⌝ Q emp | 2.
(* Same cost as default. *)
Proof.
  rewrite /FromPure /Frame => <- [->|?] /=.
  - by rewrite right_id.
  - by rewrite right_id -affinely_affinely_if affine_affinely.
Qed.
(* iris/proofmode/class_instances_frame.v *)
Instance frame_embed `{!BiEmbed PROP PROP'} p P Q (Q' : PROP') R :
  Frame p R P Q → MakeEmbed Q Q' →
  Frame p ⎡R⎤ ⎡P⎤ Q' | 2.
(* Same cost as default. *)
Proof.
  rewrite /Frame /MakeEmbed => <- <-.
  rewrite embed_sep embed_intuitionistically_if_2 => //.
Qed.
(* iris/proofmode/class_instances_frame.v *)
Instance frame_pure_embed `{!BiEmbed PROP PROP'} p P Q (Q' : PROP') φ :
  Frame p ⌜φ⌝ P Q → MakeEmbed Q Q' →
  Frame p ⌜φ⌝ ⎡P⎤ Q' | 2.
(* Same cost as default. *)
Proof. rewrite /Frame /MakeEmbed -embed_pure. apply (frame_embed p P Q). Qed.
(* iris/proofmode/class_instances_frame.v *)
Instance frame_sep_persistent_l progress R P1 P2 Q1 Q2 Q' :
  Frame true R P1 Q1 →
  MaybeFrame true R P2 Q2 progress →
  MakeSep Q1 Q2 Q' →
  Frame true R (P1 ∗ P2) Q' | 9.
Proof.
  rewrite /Frame /MaybeFrame' /MakeSep /= => <- [<-] <-.
  rewrite {1}(intuitionistically_sep_dup R).
  by rewrite !assoc -(assoc _ _ _ Q1) -(comm _ Q1) assoc -(comm _ Q1).
Qed.
(* iris/proofmode/class_instances_frame.v *)
Instance frame_sep_l R P1 P2 Q Q' :
  Frame false R P1 Q → MakeSep Q P2 Q' → Frame false R (P1 ∗ P2) Q' | 9.
Proof. rewrite /Frame /MakeSep => <- <-. by rewrite assoc. Qed.
(* iris/proofmode/class_instances_frame.v *)
Instance frame_sep_r p R P1 P2 Q Q' :
  Frame p R P2 Q → MakeSep P1 Q Q' → Frame p R (P1 ∗ P2) Q' | 10.
Proof.
  rewrite /Frame /MakeSep => <- <-. by rewrite assoc -(comm _ P1) assoc.
Qed.
(* iris/proofmode/class_instances_frame.v *)
Instance frame_big_sepL_cons {A} p (Φ : nat → A → PROP) R Q l x l' :
  IsCons l x l' →
  Frame p R (Φ 0 x ∗ [∗ list] k ↦ y ∈ l', Φ (S k) y) Q →
  Frame p R ([∗ list] k ↦ y ∈ l, Φ k y) Q | 2.
(* Same cost as default. *)
Proof. rewrite /IsCons=>->. by rewrite /Frame big_sepL_cons. Qed.
(* iris/proofmode/class_instances_frame.v *)
Instance frame_big_sepL_app {A} p (Φ : nat → A → PROP) R Q l l1 l2 :
  IsApp l l1 l2 →
  Frame p R (([∗ list] k ↦ y ∈ l1, Φ k y) ∗
           [∗ list] k ↦ y ∈ l2, Φ (length l1 + k) y) Q →
  Frame p R ([∗ list] k ↦ y ∈ l, Φ k y) Q | 2.
(* Same cost as default. *)
Proof. rewrite /IsApp=>->. by rewrite /Frame big_sepL_app. Qed.
(* iris/proofmode/class_instances_frame.v *)
Instance frame_big_sepL2_cons {A B} p (Φ : nat → A → B → PROP)
    R Q l1 x1 l1' l2 x2 l2' :
  IsCons l1 x1 l1' → IsCons l2 x2 l2' →
  Frame p R (Φ 0 x1 x2 ∗ [∗ list] k ↦ y1;y2 ∈ l1';l2', Φ (S k) y1 y2) Q →
  Frame p R ([∗ list] k ↦ y1;y2 ∈ l1;l2, Φ k y1 y2) Q.
(* Default cost > 1. *)
Proof. rewrite /IsCons=>-> ->. by rewrite /Frame big_sepL2_cons. Qed.
(* iris/proofmode/class_instances_frame.v *)
Instance frame_big_sepL2_app {A B} p (Φ : nat → A → B → PROP)
    R Q l1 l1' l1'' l2 l2' l2'' :
  IsApp l1 l1' l1'' → IsApp l2 l2' l2'' →
  Frame p R (([∗ list] k ↦ y1;y2 ∈ l1';l2', Φ k y1 y2) ∗
           [∗ list] k ↦ y1;y2 ∈ l1'';l2'', Φ (length l1' + k) y1 y2) Q →
  Frame p R ([∗ list] k ↦ y1;y2 ∈ l1;l2, Φ k y1 y2) Q.
Proof. rewrite /IsApp /Frame=>-> -> ->. apply wand_elim_l', big_sepL2_app. Qed.
(* iris/proofmode/class_instances_frame.v *)
Instance frame_big_sepMS_disj_union `{Countable A} p (Φ : A → PROP) R Q X X1 X2 :
  IsDisjUnion X X1 X2 ->
  Frame p R (([∗ mset] y ∈ X1, Φ y) ∗ [∗ mset] y ∈ X2, Φ y) Q →
  Frame p R ([∗ mset] y ∈ X, Φ y) Q | 2.
Proof. rewrite /IsDisjUnion=>->. by rewrite /Frame big_sepMS_disj_union. Qed.
(* iris/proofmode/class_instances_frame.v *)
(* For framing below [∧], we can frame [R] away in *both* conjuncts
(unlike with [∗] where we can only frame it in one conjunct).
We require at least one of those to make progress though. *)
Instance frame_and p progress1 progress2 R P1 P2 Q1 Q2 Q' :
  MaybeFrame p R P1 Q1 progress1 →
  MaybeFrame p R P2 Q2 progress2 →
  (** If below [TCEq] fails, the [frame_and] instance is immediately abandoned:
    the [TCNoBackTrack]s above prevent Coq from considering other ways to
    construct [MaybeFrame] instances. *)
  TCEq (progress1 || progress2) true →
  MakeAnd Q1 Q2 Q' →
  Frame p R (P1 ∧ P2) Q' | 9.
Proof.
  rewrite /MaybeFrame' /Frame /MakeAnd => [[<-]] [<-] _ <-.
  apply and_intro; [rewrite and_elim_l|rewrite and_elim_r]; done.
Qed.