(* iris/proofmode/class_instances.v *)
From iris.bi Require Import telescopes
From iris.proofmode Require Import base modality_instances classes classes_make
From iris.proofmode Require Import ltac_tactics
From iris.prelude Require Import options
FromAffinely (□ P) (<pers> P) | 100
FromAssumption true P Q → KnownRFromAssumption true P (<pers> Q)
FromAssumption true P Q → KnownRFromAssumption true P (<affine> Q)
FromAssumption true P Q → KnownRFromAssumption true P (□ Q)
FromAssumption p P Q → KnownRFromAssumption p P (<absorb> Q)
FromAssumption true P Q → KnownLFromAssumption p (□ P) Q
FromAssumption true P Q → KnownLFromAssumption true (<pers> P) Q
FromAssumption true P Q → KnownLFromAssumption false (<pers> P) Q
FromAssumption p P Q → KnownLFromAssumption p (<affine> P) Q
FromAssumption p P Q → KnownLFromAssumption p (□ P) Q
FromAssumption p (Φ x) Q → KnownLFromAssumption p (∀ x, Φ x) Q
FromAssumption p (Φ x) Q → KnownLFromAssumption p (∀.. x, Φ x) Q
FromPure false P1 φ1 → IntoPure P2 φ2 → IntoPure (P1 → P2) (φ1 → φ2)
FromPure a P1 φ1 → IntoPure P2 φ2 → IntoPure (P1 -∗ P2) (φ1 → φ2)
FromPure a1 P1 φ1 → FromPure a2 P2 φ2 →
FromPure (if a1 then true else a2) (P1 ∧ P2) (φ1 ∧ φ2)
FromPure a1 P1 φ1 → FromPure a2 P2 φ2 →
FromPure (if a1 then true else a2) (P1 ∨ P2) (φ1 ∨ φ2)
FromPure a1 P1 φ1 → FromPure a2 P2 φ2 →
FromPure (if a1 then a2 else false) (P1 ∗ P2) (φ1 ∧ φ2)
FromPure a (P1 -∗ P2) (φ1 → φ2)
FromPure true P φ → FromPure a (<pers> P) φ
FromPure a P φ → FromPure true (<affine> P) φ
FromPure a P φ → FromPure true (□ P) φ
FromPure a P φ → FromPure false (<absorb> P) φ
FromPure a ([∗ list] k↦x ∈ l, Φ k x) (∀ k x, l !! k = Some x → φ k x)
FromPure a ([∗ map] k↦x ∈ m, Φ k x) (map_Forall φ m)
FromPure a ([∗ set] x ∈ X, Φ x) (set_Forall φ X)
FromPure a ([∗ mset] x ∈ X, Φ x) (∀ y : A, y ∈ X → φ y)
FromModal True modality_affinely (<affine> P) (<affine> P) P | 2
FromModal True modality_persistently (<pers> P) (<pers> P) P | 2
FromModal True modality_intuitionistically (□ P) (□ P) P | 1
FromModal True modality_id (<absorb> P) (<absorb> P) P
FromAssumption q P P' → IntoWand p q (P' -∗ Q) P Q
FromAssumption false P'' P' →
FromAssumption true P P' →
FromAssumption false P'' P' →
FromAssumption true P P' →
FromAssumption q P (default emp%I mP') → IntoWand p q (mP' -∗? Q) P Q
FromWand (mP1 -∗? P2) (default emp mP1)%I P2
FromAnd P Q1 Q2 →
FromAnd (<pers> P) (<pers> Q1) (<pers> Q2)
FromSep P Q1 Q2 →
FromAnd (<pers> P) (<pers> Q1) (<pers> Q2) | 11
FromAnd ([∗ list] k ↦ y ∈ l, Φ k y) (Φ 0 x) ([∗ list] k ↦ y ∈ l', Φ (S k) y)
FromAnd ([∗ list] k ↦ y ∈ l, Φ k y)
FromAnd ([∗ list] k ↦ y1;y2 ∈ l1;l2, Φ k y1 y2)
FromAnd ([∗ list] k ↦ y1;y2 ∈ l1;l2, Φ k y1 y2)
FromAnd ([∗ mset] y ∈ X1 ⊎ X2, Φ y) ([∗ mset] y ∈ X1, Φ y) ([∗ mset] y ∈ X2, Φ y)
FromSep (P1 ∧ P2) P1 P2 | 101
FromSep P Q1 Q2 → FromSep (<affine> P) (<affine> Q1) (<affine> Q2)
FromSep P Q1 Q2 → FromSep (□ P) (□ Q1) (□ Q2)
FromSep P Q1 Q2 → FromSep (<absorb> P) (<absorb> Q1) (<absorb> Q2)
FromSep P Q1 Q2 →
FromSep (<pers> P) (<pers> Q1) (<pers> Q2)
FromSep ([∗ list] k ↦ y ∈ l, Φ k y) (Φ 0 x) ([∗ list] k ↦ y ∈ l', Φ (S k) y)
FromSep ([∗ list] k ↦ y ∈ l, Φ k y)
FromSep ([∗ list] k ↦ y1;y2 ∈ l1;l2, Φ k y1 y2)
FromSep ([∗ list] k ↦ y1;y2 ∈ l1;l2, Φ k y1 y2)
FromSep ([∗ mset] y ∈ X1 ⊎ X2, Φ y) ([∗ mset] y ∈ X1, Φ y) ([∗ mset] y ∈ X2, Φ y)
FromOr P Q1 Q2 → FromOr (<affine> P) (<affine> Q1) (<affine> Q2)
FromOr P Q1 Q2 → FromOr (□ P) (□ Q1) (□ Q2)
FromOr P Q1 Q2 → FromOr (<absorb> P) (<absorb> Q1) (<absorb> Q2)
FromOr P Q1 Q2 →
FromOr (<pers> P) (<pers> Q1) (<pers> Q2)
FromExist (∃.. a, Φ a) Φ
FromExist P Φ → FromExist (<affine> P) (λ a, <affine> (Φ a))%I
FromExist P Φ → FromExist (□ P) (λ a, □ (Φ a))%I
FromExist P Φ → FromExist (<absorb> P) (λ a, <absorb> (Φ a))%I
FromExist P Φ → FromExist (<pers> P) (λ a, <pers> (Φ a))%I
FromPureT a P φ →
FromPureT a P φ → IntoForall (P -∗ Q) (λ _ : φ, Q)
FromForall (P -∗ Q) (λ _ : φ, Q)%I (to_ident_name H)
FromForall P Φ name → FromForall (□ P) (λ a, □ (Φ a))%I name
FromForall P Φ name → FromForall (<pers> P) (λ a, <pers> (Φ a))%I name

Lemma from_assumption_exact{PROP : bi} p (P : PROP) : FromAssumption p P P.
Proof. by rewrite /FromAssumption /= intuitionistically_if_elim. Qed.

Global HintExtern 0 (FromAssumption _ _ _) =>
  notypeclasses refine (from_assumption_exact _ _); shelve : typeclass_instances.

Lemma from_exist_exist{PROP : bi} {A} (Φ : A → PROP) : FromExist (∃ a, Φ a) Φ.
Proof. by rewrite /FromExist. Qed.

Global HintExtern 0 (FromExist _ _) =>
  notypeclasses refine (from_exist_exist _) : typeclass_instances.

Global Instanceas_emp_valid_emp_valid d P : AsEmpValid0 d (⊢ P) P | 0.
Proof. by rewrite /AsEmpValid. Qed.

Global Instanceas_emp_valid_entails d P Q : AsEmpValid0 d (P ⊢ Q) (P -∗ Q).
Proof. split => _; [ apply bi.entails_wand | apply bi.wand_entails ]. Qed.

Global Instanceas_emp_valid_equiv d P Q : AsEmpValid0 d (P ≡ Q) (P ∗-∗ Q).
Proof. split => _; [ apply bi.equiv_wand_iff | apply bi.wand_iff_equiv ]. Qed.

Global Instanceas_emp_valid_forall d {A : Type} (φ : A → Prop) (P : A → PROP) :
  (∀ x, AsEmpValid d (φ x) (P x)) → AsEmpValid d (∀ x, φ x) (∀ x, P x).
Proof.
  move=>H1. split=>? H2.
  - apply bi.forall_intro=>?. by apply H1, H2.
  - intros x. apply H1 => //. revert H2. by rewrite (bi.forall_elim x).
Qed.

Global Instanceas_emp_valid_tforall d {TT : tele} (φ : TT → Prop) (P : TT → PROP) :
  (∀ x, AsEmpValid d (φ x) (P x)) → AsEmpValid d (∀.. x, φ x) (∀.. x, P x).
Proof.
  rewrite /AsEmpValid !tforall_forall bi_tforall_forall.
  apply as_emp_valid_forall.
Qed.

Global Instancefrom_affinely_affine P : Affine P → FromAffinely P P.
Proof. intros. by rewrite /FromAffinely affinely_elim. Qed.

Global Instancefrom_affinely_default P : FromAffinely (<affine> P) P | 100.
Proof. by rewrite /FromAffinely. Qed.

Global Instancefrom_affinely_intuitionistically P :
  FromAffinely (□ P) (<pers> P) | 100.
Proof. by rewrite /FromAffinely. Qed.

Global Instanceinto_absorbingly_True : @IntoAbsorbingly PROP True emp | 0.
Proof. by rewrite /IntoAbsorbingly -absorbingly_emp_True. Qed.

Global Instanceinto_absorbingly_absorbing P : Absorbing P → IntoAbsorbingly P P | 1.
Proof. intros. by rewrite /IntoAbsorbingly absorbing_absorbingly. Qed.

Global Instanceinto_absorbingly_intuitionistically P :
  IntoAbsorbingly (<pers> P) (□ P) | 2.
Proof.
  by rewrite /IntoAbsorbingly -absorbingly_intuitionistically_into_persistently.
Qed.

Global Instanceinto_absorbingly_default P : IntoAbsorbingly (<absorb> P) P | 100.
Proof. by rewrite /IntoAbsorbingly. Qed.

Global Instancefrom_assumption_persistently_r P Q :
  FromAssumption true P Q → KnownRFromAssumption true P (<pers> Q).
Proof.
  rewrite /KnownRFromAssumption /FromAssumption /= =><-.
  apply intuitionistically_persistent.
Qed.

Global Instancefrom_assumption_affinely_r P Q :
  FromAssumption true P Q → KnownRFromAssumption true P (<affine> Q).
Proof.
  rewrite /KnownRFromAssumption /FromAssumption /= =><-.
  by rewrite affinely_idemp.
Qed.

Global Instancefrom_assumption_intuitionistically_r P Q :
  FromAssumption true P Q → KnownRFromAssumption true P (□ Q).
Proof.
  rewrite /KnownRFromAssumption /FromAssumption /= =><-.
  by rewrite intuitionistically_idemp.
Qed.

Global Instancefrom_assumption_absorbingly_r p P Q :
  FromAssumption p P Q → KnownRFromAssumption p P (<absorb> Q).
Proof.
  rewrite /KnownRFromAssumption /FromAssumption /= =><-.
  apply absorbingly_intro.
Qed.

Global Instancefrom_assumption_intuitionistically_l p P Q :
  FromAssumption true P Q → KnownLFromAssumption p (□ P) Q.
Proof.
  rewrite /KnownLFromAssumption /FromAssumption /= =><-.
  by rewrite intuitionistically_if_elim.
Qed.

Global Instancefrom_assumption_persistently_l_true P Q :
  FromAssumption true P Q → KnownLFromAssumption true (<pers> P) Q.
Proof.
  rewrite /KnownLFromAssumption /FromAssumption /= =><-.
  rewrite intuitionistically_persistently_elim //.
Qed.

Global Instancefrom_assumption_persistently_l_false `{!BiAffine PROP} P Q :
  FromAssumption true P Q → KnownLFromAssumption false (<pers> P) Q.
Proof.
  rewrite /KnownLFromAssumption /FromAssumption /= =><-.
  by rewrite intuitionistically_into_persistently.
Qed.

Global Instancefrom_assumption_affinely_l_true p P Q :
  FromAssumption p P Q → KnownLFromAssumption p (<affine> P) Q.
Proof.
  rewrite /KnownLFromAssumption /FromAssumption /= =><-.
  by rewrite affinely_elim.
Qed.

Global Instancefrom_assumption_intuitionistically_l_true p P Q :
  FromAssumption p P Q → KnownLFromAssumption p (□ P) Q.
Proof.
  rewrite /KnownLFromAssumption /FromAssumption /= =><-.
  by rewrite intuitionistically_elim.
Qed.

Global Instancefrom_assumption_forall {A} p (Φ : A → PROP) Q x :
  FromAssumption p (Φ x) Q → KnownLFromAssumption p (∀ x, Φ x) Q.
Proof.
  rewrite /KnownLFromAssumption /FromAssumption=> <-.
  by rewrite forall_elim.
Qed.

Global Instancefrom_assumption_tforall {TT : tele} p (Φ : TT → PROP) Q x :
  FromAssumption p (Φ x) Q → KnownLFromAssumption p (∀.. x, Φ x) Q.
Proof.
  rewrite /KnownLFromAssumption /FromAssumption=> <-.
  by rewrite bi_tforall_forall forall_elim.
Qed.

Global Instanceinto_pure_pure φ : @IntoPure PROP ⌜φ⌝ φ.
Proof. by rewrite /IntoPure. Qed.

Global Instanceinto_pure_pure_and (φ1 φ2 : Prop) P1 P2 :
  IntoPure P1 φ1 → IntoPure P2 φ2 → IntoPure (P1 ∧ P2) (φ1 ∧ φ2).
Proof. rewrite /IntoPure pure_and. by intros -> ->. Qed.

Global Instanceinto_pure_pure_or (φ1 φ2 : Prop) P1 P2 :
  IntoPure P1 φ1 → IntoPure P2 φ2 → IntoPure (P1 ∨ P2) (φ1 ∨ φ2).
Proof. rewrite /IntoPure pure_or. by intros -> ->. Qed.

Global Instanceinto_pure_pure_impl `{!BiPureForall PROP} (φ1 φ2 : Prop) P1 P2 :
  FromPure false P1 φ1 → IntoPure P2 φ2 → IntoPure (P1 → P2) (φ1 → φ2).
Proof. rewrite /FromPure /IntoPure /= => <- ->. apply pure_impl_2. Qed.

Global Instanceinto_pure_exist {A} (Φ : A → PROP) (φ : A → Prop) :
  (∀ x, IntoPure (Φ x) (φ x)) → IntoPure (∃ x, Φ x) (∃ x, φ x).
Proof. rewrite /IntoPure=>Hx. rewrite pure_exist. by setoid_rewrite Hx. Qed.

Global Instanceinto_pure_texist {TT : tele} (Φ : TT → PROP) (φ : TT → Prop) :
  (∀ x, IntoPure (Φ x) (φ x)) → IntoPure (∃.. x, Φ x) (∃.. x, φ x).
Proof. rewrite /IntoPure texist_exist bi_texist_exist. apply into_pure_exist. Qed.

Global Instanceinto_pure_forall `{!BiPureForall PROP}
    {A} (Φ : A → PROP) (φ : A → Prop) :
  (∀ x, IntoPure (Φ x) (φ x)) → IntoPure (∀ x, Φ x) (∀ x, φ x).
Proof. rewrite /IntoPure=>Hx. rewrite -pure_forall_2. by setoid_rewrite Hx. Qed.

Global Instanceinto_pure_tforall `{!BiPureForall PROP}
    {TT : tele} (Φ : TT → PROP) (φ : TT → Prop) :
  (∀ x, IntoPure (Φ x) (φ x)) → IntoPure (∀.. x, Φ x) (∀.. x, φ x).
Proof.
  rewrite /IntoPure !tforall_forall bi_tforall_forall. apply into_pure_forall.
Qed.

Global Instanceinto_pure_pure_sep (φ1 φ2 : Prop) P1 P2 :
  IntoPure P1 φ1 → IntoPure P2 φ2 → IntoPure (P1 ∗ P2) (φ1 ∧ φ2).
Proof. rewrite /IntoPure=> -> ->. by rewrite sep_and pure_and. Qed.

Global Instanceinto_pure_pure_wand `{!BiPureForall PROP} a (φ1 φ2 : Prop) P1 P2 :
  FromPure a P1 φ1 → IntoPure P2 φ2 → IntoPure (P1 -∗ P2) (φ1 → φ2).
Proof.
  rewrite /FromPure /IntoPure=> <- -> /=. rewrite pure_impl.
  apply impl_intro_l, pure_elim_l=> ?. rewrite (pure_True φ1) //.
  by rewrite -affinely_affinely_if affinely_True_emp left_id.
Qed.

Global Instanceinto_pure_affinely P φ : IntoPure P φ → IntoPure (<affine> P) φ.
Proof. rewrite /IntoPure=> ->. apply affinely_elim. Qed.

Global Instanceinto_pure_intuitionistically P φ :
  IntoPure P φ → IntoPure (□ P) φ.
Proof. rewrite /IntoPure=> ->. apply intuitionistically_elim. Qed.

Global Instanceinto_pure_absorbingly P φ : IntoPure P φ → IntoPure (<absorb> P) φ.
Proof. rewrite /IntoPure=> ->. by rewrite absorbingly_pure. Qed.

Global Instanceinto_pure_persistently P φ :
  IntoPure P φ → IntoPure (<pers> P) φ.
Proof. rewrite /IntoPure=> ->. apply: persistently_elim. Qed.

Global Instanceinto_pure_big_sepL {A}
    (Φ : nat → A → PROP) (φ : nat → A → Prop) (l : list A) :
  (∀ k x, IntoPure (Φ k x) (φ k x)) →
  IntoPure ([∗ list] k↦x ∈ l, Φ k x) (∀ k x, l !! k = Some x → φ k x).
Proof.
  rewrite /IntoPure. intros HΦ.
  setoid_rewrite HΦ. rewrite big_sepL_pure_1. done.
Qed.

Global Instanceinto_pure_big_sepM `{Countable K} {A}
    (Φ : K → A → PROP) (φ : K → A → Prop) (m : gmap K A) :
  (∀ k x, IntoPure (Φ k x) (φ k x)) →
  IntoPure ([∗ map] k↦x ∈ m, Φ k x) (map_Forall φ m).
Proof.
  rewrite /IntoPure. intros HΦ.
  setoid_rewrite HΦ. rewrite big_sepM_pure_1. done.
Qed.

Global Instanceinto_pure_big_sepS `{Countable A}
    (Φ : A → PROP) (φ : A → Prop) (X : gset A) :
  (∀ x, IntoPure (Φ x) (φ x)) →
  IntoPure ([∗ set] x ∈ X, Φ x) (set_Forall φ X).
Proof.
  rewrite /IntoPure. intros HΦ.
  setoid_rewrite HΦ. rewrite big_sepS_pure_1. done.
Qed.

Global Instanceinto_pure_big_sepMS `{Countable A}
    (Φ : A → PROP) (φ : A → Prop) (X : gmultiset A) :
  (∀ x, IntoPure (Φ x) (φ x)) →
  IntoPure ([∗ mset] x ∈ X, Φ x) (∀ y : A, y ∈ X → φ y).
Proof.
  rewrite /IntoPure. intros HΦ.
  setoid_rewrite HΦ. rewrite big_sepMS_pure_1. done.
Qed.

Global Instancefrom_pure_emp : @FromPure PROP true emp True.
Proof. rewrite /FromPure /=. apply (affine _). Qed.

Global Instancefrom_pure_pure φ : @FromPure PROP false ⌜φ⌝ φ.
Proof. by rewrite /FromPure /=. Qed.

Global Instancefrom_pure_pure_and a1 a2 (φ1 φ2 : Prop) P1 P2 :
  FromPure a1 P1 φ1 → FromPure a2 P2 φ2 →
  FromPure (if a1 then true else a2) (P1 ∧ P2) (φ1 ∧ φ2).
Proof.
  rewrite /FromPure pure_and=> <- <- /=. rewrite affinely_if_and.
  f_equiv; apply affinely_if_flag_mono; destruct a1; naive_solver.
Qed.

Global Instancefrom_pure_pure_or a1 a2 (φ1 φ2 : Prop) P1 P2 :
  FromPure a1 P1 φ1 → FromPure a2 P2 φ2 →
  FromPure (if a1 then true else a2) (P1 ∨ P2) (φ1 ∨ φ2).
Proof.
  rewrite /FromPure pure_or=> <- <- /=. rewrite affinely_if_or.
  f_equiv; apply affinely_if_flag_mono; destruct a1; naive_solver.
Qed.

Global Instancefrom_pure_pure_impl a (φ1 φ2 : Prop) P1 P2 :
  IntoPure P1 φ1 → FromPure a P2 φ2 → FromPure a (P1 → P2) (φ1 → φ2).
Proof.
  rewrite /FromPure /IntoPure pure_impl_1=> -> <-. destruct a=>//=.
  apply bi.impl_intro_l. by rewrite affinely_and_r bi.impl_elim_r.
Qed.

Global Instancefrom_pure_exist {A} a (Φ : A → PROP) (φ : A → Prop) :
  (∀ x, FromPure a (Φ x) (φ x)) → FromPure a (∃ x, Φ x) (∃ x, φ x).
Proof.
  rewrite /FromPure=>Hx. rewrite pure_exist affinely_if_exist.
  by setoid_rewrite Hx.
Qed.

Global Instancefrom_pure_texist {TT : tele} a (Φ : TT → PROP) (φ : TT → Prop) :
  (∀ x, FromPure a (Φ x) (φ x)) → FromPure a (∃.. x, Φ x) (∃.. x, φ x).
Proof. rewrite /FromPure texist_exist bi_texist_exist. apply from_pure_exist. Qed.

Global Instancefrom_pure_forall {A} a (Φ : A → PROP) (φ : A → Prop) :
  (∀ x, FromPure a (Φ x) (φ x)) → FromPure a (∀ x, Φ x) (∀ x, φ x).
Proof.
  rewrite /FromPure=>Hx. rewrite pure_forall_1. setoid_rewrite <-Hx.
  destruct a=>//=. apply affinely_forall.
Qed.

Global Instancefrom_pure_tforall {TT : tele} a (Φ : TT → PROP) (φ : TT → Prop) :
  (∀ x, FromPure a (Φ x) (φ x)) → FromPure a (∀.. x, Φ x) (∀.. x, φ x).
Proof.
  rewrite /FromPure !tforall_forall bi_tforall_forall. apply from_pure_forall.
Qed.

Global Instancefrom_pure_pure_sep_true a1 a2 (φ1 φ2 : Prop) P1 P2 :
  FromPure a1 P1 φ1 → FromPure a2 P2 φ2 →
  FromPure (if a1 then a2 else false) (P1 ∗ P2) (φ1 ∧ φ2).
Proof.
  rewrite /FromPure=> <- <-. destruct a1; simpl.
  - by rewrite pure_and -persistent_and_affinely_sep_l affinely_if_and_r.
  - by rewrite pure_and -affinely_affinely_if -persistent_and_affinely_sep_r_1.
Qed.

Global Instancefrom_pure_pure_wand a (φ1 φ2 : Prop) P1 P2 :
  IntoPure P1 φ1 → FromPure a P2 φ2 →
  TCOr (TCEq a false) (Affine P1) →
  FromPure a (P1 -∗ P2) (φ1 → φ2).
Proof.
  rewrite /FromPure /IntoPure=> HP1 <- Ha /=. apply wand_intro_l.
  destruct a; simpl.
  - destruct Ha as [Ha|?]; first inversion Ha.
    rewrite -persistent_and_affinely_sep_r -(affine_affinely P1) HP1.
    by rewrite affinely_and_l pure_impl_1 impl_elim_r.
  - by rewrite HP1 sep_and pure_impl_1 impl_elim_r.
Qed.

Global Instancefrom_pure_persistently P a φ :
  FromPure true P φ → FromPure a (<pers> P) φ.
Proof.
  rewrite /FromPure=> <- /=.
  by rewrite persistently_affinely_elim affinely_if_elim persistently_pure.
Qed.

Global Instancefrom_pure_affinely_true a P φ :
  FromPure a P φ → FromPure true (<affine> P) φ.
Proof. rewrite /FromPure=><- /=. by rewrite -affinely_affinely_if affinely_idemp. Qed.

Global Instancefrom_pure_intuitionistically_true a P φ :
  FromPure a P φ → FromPure true (□ P) φ.
Proof.
  rewrite /FromPure=><- /=.
  rewrite -intuitionistically_affinely_elim -affinely_affinely_if affinely_idemp.
  by rewrite intuitionistic_intuitionistically.
Qed.

Global Instancefrom_pure_absorbingly a P φ :
  FromPure a P φ → FromPure false (<absorb> P) φ.
Proof.
  rewrite /FromPure=> <- /=. rewrite -affinely_affinely_if.
  by rewrite -persistent_absorbingly_affinely_2.
Qed.

Global Instancefrom_pure_big_sepL {A}
    a (Φ : nat → A → PROP) (φ : nat → A → Prop) (l : list A) :
  (∀ k x, FromPure a (Φ k x) (φ k x)) →
  TCOr (TCEq a true) (BiAffine PROP) →
  FromPure a ([∗ list] k↦x ∈ l, Φ k x) (∀ k x, l !! k = Some x → φ k x).
Proof.
  rewrite /FromPure. destruct a; simpl; intros HΦ Haffine.
  - rewrite big_sepL_affinely_pure_2.
    setoid_rewrite HΦ. done.
  - destruct Haffine as [[=]%TCEq_eq|?].
    rewrite -big_sepL_pure. setoid_rewrite HΦ. done.
Qed.

Global Instancefrom_pure_big_sepM `{Countable K} {A}
    a (Φ : K → A → PROP) (φ : K → A → Prop) (m : gmap K A) :
  (∀ k x, FromPure a (Φ k x) (φ k x)) →
  TCOr (TCEq a true) (BiAffine PROP) →
  FromPure a ([∗ map] k↦x ∈ m, Φ k x) (map_Forall φ m).
Proof.
  rewrite /FromPure. destruct a; simpl; intros HΦ Haffine.
  - rewrite big_sepM_affinely_pure_2.
    setoid_rewrite HΦ. done.
  - destruct Haffine as [[=]%TCEq_eq|?].
    rewrite -big_sepM_pure. setoid_rewrite HΦ. done.
Qed.

Global Instancefrom_pure_big_sepS `{Countable A}
    a (Φ : A → PROP) (φ : A → Prop) (X : gset A) :
  (∀ x, FromPure a (Φ x) (φ x)) →
  TCOr (TCEq a true) (BiAffine PROP) →
  FromPure a ([∗ set] x ∈ X, Φ x) (set_Forall φ X).
Proof.
  rewrite /FromPure. destruct a; simpl; intros HΦ Haffine.
  - rewrite big_sepS_affinely_pure_2.
    setoid_rewrite HΦ. done.
  - destruct Haffine as [[=]%TCEq_eq|?].
    rewrite -big_sepS_pure. setoid_rewrite HΦ. done.
Qed.

Global Instancefrom_pure_big_sepMS `{Countable A}
    a (Φ : A → PROP) (φ : A → Prop) (X : gmultiset A) :
  (∀ x, FromPure a (Φ x) (φ x)) →
  TCOr (TCEq a true) (BiAffine PROP) →
  FromPure a ([∗ mset] x ∈ X, Φ x) (∀ y : A, y ∈ X → φ y).
Proof.
  rewrite /FromPure. destruct a; simpl; intros HΦ Haffine.
  - rewrite big_sepMS_affinely_pure_2.
    setoid_rewrite HΦ. done.
  - destruct Haffine as [[=]%TCEq_eq|?].
    rewrite -big_sepMS_pure. setoid_rewrite HΦ. done.
Qed.

Global Instanceinto_persistent_persistently p P Q :
  IntoPersistent true P Q → IntoPersistent p (<pers> P) Q | 0.
Proof.
  rewrite /IntoPersistent /= => ->.
  destruct p; simpl; auto using persistently_idemp_1.
Qed.

Global Instanceinto_persistent_affinely p P Q :
  IntoPersistent p P Q → IntoPersistent p (<affine> P) Q | 0.
Proof. rewrite /IntoPersistent /= => <-. by rewrite affinely_elim. Qed.

Global Instanceinto_persistent_intuitionistically p P Q :
  IntoPersistent true P Q → IntoPersistent p (□ P) Q | 0.
Proof.
  rewrite /IntoPersistent /= =><-.
  destruct p; simpl;
    eauto using persistently_mono, intuitionistically_elim,
    intuitionistically_into_persistently_1.
Qed.

Global Instanceinto_persistent_here P : IntoPersistent true P P | 1.
Proof. by rewrite /IntoPersistent. Qed.

Global Instanceinto_persistent_persistent P :
  Persistent P → IntoPersistent false P P | 100.
Proof. intros. by rewrite /IntoPersistent. Qed.

Global Instancefrom_modal_affinely P :
  FromModal True modality_affinely (<affine> P) (<affine> P) P | 2.
Proof. by rewrite /FromModal. Qed.

Global Instancefrom_modal_persistently P :
  FromModal True modality_persistently (<pers> P) (<pers> P) P | 2.
Proof. by rewrite /FromModal. Qed.

Global Instancefrom_modal_intuitionistically P :
  FromModal True modality_intuitionistically (□ P) (□ P) P | 1.
Proof. by rewrite /FromModal. Qed.

Global Instancefrom_modal_intuitionistically_affine_bi P :
  BiAffine PROP → FromModal True modality_persistently (□ P) (□ P) P | 0.
Proof.
  intros. by rewrite /FromModal /= intuitionistically_into_persistently.
Qed.

Global Instancefrom_modal_absorbingly P :
  FromModal True modality_id (<absorb> P) (<absorb> P) P.
Proof. by rewrite /FromModal /= -absorbingly_intro. Qed.

Global Instanceinto_wand_wand' p q (P Q P' Q' : PROP) :
  IntoWand' p q (P -∗ Q) P' Q' → IntoWand p q (P -∗ Q) P' Q' | 100.
Proof. done. Qed.

Global Instanceinto_wand_impl' p q (P Q P' Q' : PROP) :
  IntoWand' p q (P → Q) P' Q' → IntoWand p q (P → Q) P' Q' | 100.
Proof. done. Qed.

Global Instanceinto_wand_wandM' p q mP (Q P' Q' : PROP) :
  IntoWand' p q (mP -∗? Q) P' Q' → IntoWand p q (mP -∗? Q) P' Q' | 100.
Proof. done. Qed.

Global Instanceinto_wand_wand p q P Q P' :
  FromAssumption q P P' → IntoWand p q (P' -∗ Q) P Q.
Proof.
  rewrite /FromAssumption /IntoWand=> HP. by rewrite HP intuitionistically_if_elim.
Qed.

Global Instanceinto_wand_impl_false_false P Q P' P'' :
  Absorbing P →

Global Instanceinto_wand_impl_false_true P Q P' :
  Absorbing P' →
  FromAssumption true P P' →
  IntoWand false true (P' → Q) P Q.
Proof.
  rewrite /IntoWand /FromAssumption /= => ? HP. apply wand_intro_l.
  rewrite -(persistently_elim P').
  rewrite persistent_impl_wand_affinely.
  rewrite -(intuitionistically_idemp P) HP.
  apply wand_elim_r.
Qed.

Global Instanceinto_wand_impl_true_false P Q P' P'' :
  MakeAffinely P P' →
  FromAssumption false P'' P' →
  IntoWand true false (P → Q) P'' Q.
Proof.
  rewrite /MakeAffinely /IntoWand /FromAssumption /= => <- ->.
  apply wand_intro_r.
  rewrite sep_and intuitionistically_elim affinely_elim impl_elim_l //.
Qed.

Global Instanceinto_wand_impl_true_true P Q P' :
  FromAssumption true P P' →
  IntoWand true true (P' → Q) P Q.
Proof.
  rewrite /FromAssumption /IntoWand /= => <-. apply wand_intro_l.
  rewrite sep_and [(□ (_ → _))%I]intuitionistically_elim impl_elim_r //.
Qed.

Global Instanceinto_wand_wandM p q mP' P Q :
  FromAssumption q P (default emp%I mP') → IntoWand p q (mP' -∗? Q) P Q.
Proof. rewrite /IntoWand wandM_sound. exact: into_wand_wand. Qed.

Global Instanceinto_wand_and_l p q R1 R2 P' Q' :
  IntoWand p q R1 P' Q' → IntoWand p q (R1 ∧ R2) P' Q'.
Proof. rewrite /IntoWand=> ?. by rewrite /bi_wand_iff and_elim_l. Qed.

Global Instanceinto_wand_and_r p q R1 R2 P' Q' :
  IntoWand p q R2 Q' P' → IntoWand p q (R1 ∧ R2) Q' P'.
Proof. rewrite /IntoWand=> ?. by rewrite /bi_wand_iff and_elim_r. Qed.

Global Instanceinto_wand_forall_prop_true p (φ : Prop) P :
  IntoWand p true (∀ _ : φ, P) ⌜ φ ⌝ P.
Proof.
  rewrite /IntoWand (intuitionistically_if_elim p) /=
          -impl_wand_intuitionistically -pure_impl_forall
          bi.persistently_elim //.
Qed.

Global Instanceinto_wand_forall_prop_false p (φ : Prop) Pφ P :
  MakeAffinely ⌜ φ ⌝ Pφ →
  IntoWand p false (∀ _ : φ, P) Pφ P.
Proof.
  rewrite /MakeAffinely /IntoWand=> <-.
  rewrite (intuitionistically_if_elim p) /=.
  by rewrite -pure_impl_forall -persistent_impl_wand_affinely.
Qed.

Global Instanceinto_wand_forall {A} p q (Φ : A → PROP) P Q x :
  IntoWand p q (Φ x) P Q → IntoWand p q (∀ x, Φ x) P Q.
Proof. rewrite /IntoWand=> <-. by rewrite (forall_elim x). Qed.

Global Instanceinto_wand_tforall {TT : tele} p q (Φ : TT → PROP) P Q x :
  IntoWand p q (Φ x) P Q → IntoWand p q (∀.. x, Φ x) P Q.
Proof. rewrite /IntoWand=> <-. by rewrite bi_tforall_forall (forall_elim x). Qed.

Global Instanceinto_wand_affine p q R P Q :
  IntoWand p q R P Q → IntoWand p q (<affine> R) (<affine> P) (<affine> Q).
Proof.
  rewrite /IntoWand /= => HR. apply wand_intro_r. destruct p; simpl in *.
  - rewrite (affinely_elim R) -(affine_affinely (□ R)) HR. destruct q; simpl in *.
    + rewrite (affinely_elim P) -{2}(affine_affinely (□ P)).
      by rewrite affinely_sep_2 wand_elim_l.
    + by rewrite affinely_sep_2 wand_elim_l.
  - rewrite HR. destruct q; simpl in *.
    + rewrite (affinely_elim P) -{2}(affine_affinely (□ P)).
      by rewrite affinely_sep_2 wand_elim_l.
    + by rewrite affinely_sep_2 wand_elim_l.
Qed.

Global Instanceinto_wand_affine_args q R P Q :
  IntoWand true q R P Q → IntoWand' true q R (<affine> P) (<affine> Q).
Proof.
  rewrite /IntoWand' /IntoWand /= => HR. apply wand_intro_r.
  rewrite -(affine_affinely (□ R)) HR. destruct q; simpl.
  - rewrite (affinely_elim P) -{2}(affine_affinely (□ P)).
    by rewrite affinely_sep_2 wand_elim_l.
  - by rewrite affinely_sep_2 wand_elim_l.
Qed.

Global Instanceinto_wand_intuitionistically p q R P Q :
  IntoWand true q R P Q → IntoWand p q (□ R) P Q.
Proof. rewrite /IntoWand /= => ->. by rewrite {1}intuitionistically_if_elim. Qed.

Global Instanceinto_wand_persistently_true q R P Q :
  IntoWand true q R P Q → IntoWand true q (<pers> R) P Q.
Proof. by rewrite /IntoWand /= intuitionistically_persistently_elim. Qed.

Global Instanceinto_wand_persistently_false q R P Q :
  Absorbing R → IntoWand false q R P Q → IntoWand false q (<pers> R) P Q.
Proof. intros ?. by rewrite /IntoWand persistently_elim. Qed.

Global Instancefrom_wand_wand P1 P2 : FromWand (P1 -∗ P2) P1 P2.
Proof. by rewrite /FromWand. Qed.

Global Instancefrom_wand_wandM mP1 P2 :
  FromWand (mP1 -∗? P2) (default emp mP1)%I P2.
Proof. by rewrite /FromWand wandM_sound. Qed.

Global Instancefrom_impl_impl P1 P2 : FromImpl (P1 → P2) P1 P2.
Proof. by rewrite /FromImpl. Qed.

Global Instancefrom_and_and P1 P2 : FromAnd (P1 ∧ P2) P1 P2 | 100.
Proof. by rewrite /FromAnd. Qed.

Global Instancefrom_and_sep_persistent_l P1 P1' P2 :
  Persistent P1 → IntoAbsorbingly P1' P1 → FromAnd (P1 ∗ P2) P1' P2 | 9.
Proof.
  rewrite /IntoAbsorbingly /FromAnd=> ? ->.
  rewrite persistent_and_affinely_sep_l_1 {1}(persistent_persistently_2 P1).
  by rewrite absorbingly_elim_persistently -{2}(intuitionistically_elim P1).
Qed.

Global Instancefrom_and_sep_persistent_r P1 P2 P2' :
  Persistent P2 → IntoAbsorbingly P2' P2 → FromAnd (P1 ∗ P2) P1 P2' | 10.
Proof.
  rewrite /IntoAbsorbingly /FromAnd=> ? ->.
  rewrite persistent_and_affinely_sep_r_1 {1}(persistent_persistently_2 P2).
  by rewrite absorbingly_elim_persistently -{2}(intuitionistically_elim P2).
Qed.

Global Instancefrom_and_pure φ ψ : @FromAnd PROP ⌜φ ∧ ψ⌝ ⌜φ⌝ ⌜ψ⌝.
Proof. by rewrite /FromAnd pure_and. Qed.

Global Instancefrom_and_pure_iff φ ψ : @FromAnd PROP ⌜φ ↔ ψ⌝ ⌜φ → ψ⌝ ⌜ψ → φ⌝.
Proof. rewrite /iff. apply _. Qed.

Global Instancefrom_and_persistently P Q1 Q2 :
  FromAnd P Q1 Q2 →
  FromAnd (<pers> P) (<pers> Q1) (<pers> Q2).
Proof. rewrite /FromAnd=> <-. by rewrite persistently_and. Qed.

Global Instancefrom_and_persistently_sep P Q1 Q2 :
  FromSep P Q1 Q2 →
  FromAnd (<pers> P) (<pers> Q1) (<pers> Q2) | 11.
Proof. rewrite /FromAnd=> <-. by rewrite -persistently_and persistently_and_sep. Qed.

Global Instancefrom_and_big_sepL_cons_persistent {A} (Φ : nat → A → PROP) l x l' :
  IsCons l x l' →
  Persistent (Φ 0 x) →
  FromAnd ([∗ list] k ↦ y ∈ l, Φ k y) (Φ 0 x) ([∗ list] k ↦ y ∈ l', Φ (S k) y).
Proof. rewrite /IsCons=> -> ?. by rewrite /FromAnd big_sepL_cons persistent_and_sep_1. Qed.

Global Instancefrom_and_big_sepL_app_persistent {A} (Φ : nat → A → PROP) l l1 l2 :
  IsApp l l1 l2 →
  (∀ k y, Persistent (Φ k y)) →
  FromAnd ([∗ list] k ↦ y ∈ l, Φ k y)
    ([∗ list] k ↦ y ∈ l1, Φ k y) ([∗ list] k ↦ y ∈ l2, Φ (length l1 + k) y).
Proof. rewrite /IsApp=> -> ?. by rewrite /FromAnd big_sepL_app persistent_and_sep_1. Qed.

Global Instancefrom_and_big_sepL2_cons_persistent {A B}
    (Φ : nat → A → B → PROP) l1 x1 l1' l2 x2 l2' :
  IsCons l1 x1 l1' → IsCons l2 x2 l2' →
  Persistent (Φ 0 x1 x2) →
  FromAnd ([∗ list] k ↦ y1;y2 ∈ l1;l2, Φ k y1 y2)
    (Φ 0 x1 x2) ([∗ list] k ↦ y1;y2 ∈ l1';l2', Φ (S k) y1 y2).
Proof.
  rewrite /IsCons=> -> -> ?.
  by rewrite /FromAnd big_sepL2_cons persistent_and_sep_1.
Qed.

Global Instancefrom_and_big_sepL2_app_persistent {A B}
    (Φ : nat → A → B → PROP) l1 l1' l1'' l2 l2' l2'' :
  IsApp l1 l1' l1'' → IsApp l2 l2' l2'' →
  (∀ k y1 y2, Persistent (Φ k y1 y2)) →
  FromAnd ([∗ list] k ↦ y1;y2 ∈ l1;l2, Φ k y1 y2)
    ([∗ list] k ↦ y1;y2 ∈ l1';l2', Φ k y1 y2)
    ([∗ list] k ↦ y1;y2 ∈ l1'';l2'', Φ (length l1' + k) y1 y2).
Proof.
  rewrite /IsApp=> -> -> ?. rewrite /FromAnd persistent_and_sep_1.
  apply wand_elim_l', big_sepL2_app.
Qed.

Global Instancefrom_and_big_sepMS_disj_union_persistent
    `{Countable A} (Φ : A → PROP) X1 X2 :
  (∀ y, Persistent (Φ y)) →
  FromAnd ([∗ mset] y ∈ X1 ⊎ X2, Φ y) ([∗ mset] y ∈ X1, Φ y) ([∗ mset] y ∈ X2, Φ y).
Proof. intros. by rewrite /FromAnd big_sepMS_disj_union persistent_and_sep_1. Qed.

Global Instancefrom_sep_sep P1 P2 : FromSep (P1 ∗ P2) P1 P2 | 100.
Proof. by rewrite /FromSep. Qed.

Global Instancefrom_sep_and P1 P2 :
  TCOr (Affine P1) (Absorbing P2) → TCOr (Affine P2) (Absorbing P1) →
  FromSep (P1 ∧ P2) P1 P2 | 101.
Proof. intros. by rewrite /FromSep sep_and. Qed.

Global Instancefrom_sep_pure φ ψ : @FromSep PROP ⌜φ ∧ ψ⌝ ⌜φ⌝ ⌜ψ⌝.
Proof. by rewrite /FromSep pure_and sep_and. Qed.

Global Instancefrom_sep_pure_iff φ ψ : @FromSep PROP ⌜φ ↔ ψ⌝ ⌜φ → ψ⌝ ⌜ψ → φ⌝.
Proof. rewrite /iff. apply _. Qed.

Global Instancefrom_sep_affinely P Q1 Q2 :
  FromSep P Q1 Q2 → FromSep (<affine> P) (<affine> Q1) (<affine> Q2).
Proof. rewrite /FromSep=> <-. by rewrite affinely_sep_2. Qed.

Global Instancefrom_sep_intuitionistically P Q1 Q2 :
  FromSep P Q1 Q2 → FromSep (□ P) (□ Q1) (□ Q2).
Proof. rewrite /FromSep=> <-. by rewrite intuitionistically_sep_2. Qed.

Global Instancefrom_sep_absorbingly P Q1 Q2 :
  FromSep P Q1 Q2 → FromSep (<absorb> P) (<absorb> Q1) (<absorb> Q2).
Proof. rewrite /FromSep=> <-. by rewrite absorbingly_sep. Qed.

Global Instancefrom_sep_persistently P Q1 Q2 :
  FromSep P Q1 Q2 →
  FromSep (<pers> P) (<pers> Q1) (<pers> Q2).
Proof. rewrite /FromSep=> <-. by rewrite persistently_sep_2. Qed.

Global Instancefrom_sep_big_sepL_cons {A} (Φ : nat → A → PROP) l x l' :
  IsCons l x l' →
  FromSep ([∗ list] k ↦ y ∈ l, Φ k y) (Φ 0 x) ([∗ list] k ↦ y ∈ l', Φ (S k) y).
Proof. rewrite /IsCons=> ->. by rewrite /FromSep big_sepL_cons. Qed.

Global Instancefrom_sep_big_sepL_app {A} (Φ : nat → A → PROP) l l1 l2 :
  IsApp l l1 l2 →
  FromSep ([∗ list] k ↦ y ∈ l, Φ k y)
    ([∗ list] k ↦ y ∈ l1, Φ k y) ([∗ list] k ↦ y ∈ l2, Φ (length l1 + k) y).
Proof. rewrite /IsApp=> ->. by rewrite /FromSep big_opL_app. Qed.

Global Instancefrom_sep_big_sepL2_cons {A B} (Φ : nat → A → B → PROP)
    l1 x1 l1' l2 x2 l2' :
  IsCons l1 x1 l1' → IsCons l2 x2 l2' →
  FromSep ([∗ list] k ↦ y1;y2 ∈ l1;l2, Φ k y1 y2)
    (Φ 0 x1 x2) ([∗ list] k ↦ y1;y2 ∈ l1';l2', Φ (S k) y1 y2).
Proof. rewrite /IsCons=> -> ->. by rewrite /FromSep big_sepL2_cons. Qed.

Global Instancefrom_sep_big_sepL2_app {A B} (Φ : nat → A → B → PROP)
    l1 l1' l1'' l2 l2' l2'' :
  IsApp l1 l1' l1'' → IsApp l2 l2' l2'' →
  FromSep ([∗ list] k ↦ y1;y2 ∈ l1;l2, Φ k y1 y2)
    ([∗ list] k ↦ y1;y2 ∈ l1';l2', Φ k y1 y2)
    ([∗ list] k ↦ y1;y2 ∈ l1'';l2'', Φ (length l1' + k) y1 y2).
Proof. rewrite /IsApp=>-> ->. apply wand_elim_l', big_sepL2_app. Qed.

Global Instancefrom_sep_big_sepMS_disj_union `{Countable A} (Φ : A → PROP) X1 X2 :
  FromSep ([∗ mset] y ∈ X1 ⊎ X2, Φ y) ([∗ mset] y ∈ X1, Φ y) ([∗ mset] y ∈ X2, Φ y).
Proof. by rewrite /FromSep big_sepMS_disj_union. Qed.

Global Instancemaybe_combine_sep_as_affinely Q1 Q2 P progress :
  MaybeCombineSepAs Q1 Q2 P progress →
  MaybeCombineSepAs (<affine> Q1) (<affine> Q2) (<affine> P) progress | 30.
Proof. rewrite /MaybeCombineSepAs =><-. by rewrite affinely_sep_2. Qed.

Global Instancemaybe_combine_sep_as_intuitionistically Q1 Q2 P progress :
  MaybeCombineSepAs Q1 Q2 P progress →
  MaybeCombineSepAs (□ Q1) (□ Q2) (□ P) progress | 30.
Proof. rewrite /MaybeCombineSepAs =><-. by rewrite intuitionistically_sep_2. Qed.

Global Instancemaybe_combine_sep_as_absorbingly Q1 Q2 P progress :
  MaybeCombineSepAs Q1 Q2 P progress →
  MaybeCombineSepAs (<absorb> Q1) (<absorb> Q2) (<absorb> P) progress | 30.
Proof. rewrite /MaybeCombineSepAs =><-. by rewrite absorbingly_sep. Qed.

Global Instancemaybe_combine_sep_as_persistently Q1 Q2 P progress :
  MaybeCombineSepAs Q1 Q2 P progress →
  MaybeCombineSepAs (<pers> Q1) (<pers> Q2) (<pers> P) progress | 30.
Proof. rewrite /MaybeCombineSepAs =><-. by rewrite persistently_sep_2. Qed.

Global Instancecombine_sep_as_affinely Q1 Q2 P :
  CombineSepGives Q1 Q2 P → CombineSepGives (<affine> Q1) (<affine> Q2) P | 30.
Proof. by rewrite /CombineSepGives affinely_sep_2 affinely_elim => ->. Qed.

Global Instancecombine_sep_as_intuitionistically Q1 Q2 P :
  CombineSepGives Q1 Q2 P → CombineSepGives (□ Q1) (□ Q2) P | 30.
Proof. rewrite /CombineSepGives => <-. by rewrite !intuitionistically_elim. Qed.

Global Instancecombine_sep_as_absorbingly Q1 Q2 P :
  CombineSepGives Q1 Q2 P → CombineSepGives (<absorb> Q1) (<absorb> Q2) P | 30.
Proof.
  rewrite /CombineSepGives -absorbingly_sep =>->.
  by rewrite absorbingly_elim_persistently.
Qed.

Global Instancecombine_sep_as_persistently Q1 Q2 P :
  CombineSepGives Q1 Q2 P → CombineSepGives (<pers> Q1) (<pers> Q2) P | 30.
Proof.
  rewrite /CombineSepGives persistently_sep_2 => ->.
  by rewrite persistently_idemp.
Qed.

Global Instanceinto_and_and p P Q : IntoAnd p (P ∧ Q) P Q | 10.
Proof. by rewrite /IntoAnd intuitionistically_if_and. Qed.

Global Instanceinto_and_and_affine_l P Q Q' :
  Affine P → FromAffinely Q' Q → IntoAnd false (P ∧ Q) P Q'.
Proof.
  intros. rewrite /IntoAnd /=.
  by rewrite -(affine_affinely P) affinely_and_l affinely_and (from_affinely Q').
Qed.

Global Instanceinto_and_and_affine_r P P' Q :
  Affine Q → FromAffinely P' P → IntoAnd false (P ∧ Q) P' Q.
Proof.
  intros. rewrite /IntoAnd /=.
  by rewrite -(affine_affinely Q) affinely_and_r affinely_and (from_affinely P').
Qed.

Global Instanceinto_and_sep `{!BiPositive PROP} P Q : IntoAnd true (P ∗ Q) P Q.
Proof.
  rewrite /IntoAnd /= intuitionistically_sep
    -and_sep_intuitionistically intuitionistically_and //.
Qed.

Global Instanceinto_and_sep_affine p P Q :
  TCOr (Affine P) (Absorbing Q) → TCOr (Affine Q) (Absorbing P) →
  IntoAnd p (P ∗ Q) P Q.
Proof. intros. by rewrite /IntoAnd /= sep_and. Qed.

Global Instanceinto_and_pure p φ ψ : @IntoAnd PROP p ⌜φ ∧ ψ⌝ ⌜φ⌝ ⌜ψ⌝.
Proof. by rewrite /IntoAnd pure_and intuitionistically_if_and. Qed.

Global Instanceinto_and_affinely p P Q1 Q2 :
  IntoAnd p P Q1 Q2 → IntoAnd p (<affine> P) (<affine> Q1) (<affine> Q2).
Proof.
  rewrite /IntoAnd. destruct p; simpl.
  - rewrite -affinely_and !intuitionistically_affinely_elim //.
  - intros ->. by rewrite affinely_and.
Qed.

Global Instanceinto_and_intuitionistically p P Q1 Q2 :
  IntoAnd p P Q1 Q2 → IntoAnd p (□ P) (□ Q1) (□ Q2).
Proof.
  rewrite /IntoAnd. destruct p; simpl.
  - rewrite -intuitionistically_and !intuitionistically_idemp //.
  - intros ->. by rewrite intuitionistically_and.
Qed.

Global Instanceinto_and_persistently p P Q1 Q2 :
  IntoAnd p P Q1 Q2 →
  IntoAnd p (<pers> P) (<pers> Q1) (<pers> Q2).
Proof.
  rewrite /IntoAnd /=. destruct p; simpl.
  - rewrite -persistently_and !intuitionistically_persistently_elim //.
  - intros ->. by rewrite persistently_and.
Qed.

Global Instanceinto_sep_sep P Q : IntoSep (P ∗ Q) P Q.
Proof. by rewrite /IntoSep. Qed.

Inductive AndIntoSep: PROP → PROP → PROP → PROP → Prop :=
  | and_into_sep_affine P Q Q' : Affine P → FromAffinely Q' Q → AndIntoSep P P Q Q'
  | and_into_sep P Q : AndIntoSep P (<affine> P) Q Q.
Existing Class AndIntoSep.

Global ExistingInstance and_into_sep_affine | 0.

Global ExistingInstance and_into_sep | 2.

Global Instanceinto_sep_and_persistent_l P P' Q Q' :
  Persistent P → AndIntoSep P P' Q Q' → IntoSep (P ∧ Q) P' Q'.
Proof.
  destruct 2 as [P Q Q'|P Q]; rewrite /IntoSep.
  - rewrite -(from_affinely Q' Q) -(affine_affinely P) affinely_and_lr.
    by rewrite persistent_and_affinely_sep_l_1.
  - by rewrite persistent_and_affinely_sep_l_1.
Qed.

Global Instanceinto_sep_and_persistent_r P P' Q Q' :
  Persistent Q → AndIntoSep Q Q' P P' → IntoSep (P ∧ Q) P' Q'.
Proof.
  destruct 2 as [Q P P'|Q P]; rewrite /IntoSep.
  - rewrite -(from_affinely P' P) -(affine_affinely Q) -affinely_and_lr.
    by rewrite persistent_and_affinely_sep_r_1.
  - by rewrite persistent_and_affinely_sep_r_1.
Qed.

Global Instanceinto_sep_pure φ ψ : @IntoSep PROP ⌜φ ∧ ψ⌝ ⌜φ⌝ ⌜ψ⌝.
Proof. by rewrite /IntoSep pure_and persistent_and_sep_1. Qed.

Global Instanceinto_sep_affinely `{!BiPositive PROP} P Q1 Q2 :
  IntoSep P Q1 Q2 → IntoSep (<affine> P) (<affine> Q1) (<affine> Q2) | 0.
Proof. rewrite /IntoSep /= => ->. by rewrite affinely_sep. Qed.

Global Instanceinto_sep_intuitionistically `{!BiPositive PROP} P Q1 Q2 :
  IntoSep P Q1 Q2 → IntoSep (□ P) (□ Q1) (□ Q2) | 0.
Proof. rewrite /IntoSep /= => ->. by rewrite intuitionistically_sep. Qed.

Global Instanceinto_sep_affinely_trim P Q1 Q2 :
  IntoSep P Q1 Q2 → IntoSep (<affine> P) Q1 Q2 | 20.
Proof. rewrite /IntoSep /= => ->. by rewrite affinely_elim. Qed.

Global Instanceinto_sep_persistently `{!BiPositive PROP} P Q1 Q2 :
  IntoSep P Q1 Q2 →
  IntoSep (<pers> P) (<pers> Q1) (<pers> Q2).
Proof. rewrite /IntoSep /= => ->. by rewrite persistently_sep. Qed.

Global Instanceinto_sep_persistently_affine P Q1 Q2 :
  IntoSep P Q1 Q2 →
  TCOr (Affine Q1) (Absorbing Q2) → TCOr (Affine Q2) (Absorbing Q1) →
  IntoSep (<pers> P) (<pers> Q1) (<pers> Q2).
Proof.
  rewrite /IntoSep /= => -> ??.
  by rewrite sep_and persistently_and persistently_and_sep_l_1.
Qed.

Global Instanceinto_sep_intuitionistically_affine P Q1 Q2 :
  IntoSep P Q1 Q2 →
  TCOr (Affine Q1) (Absorbing Q2) → TCOr (Affine Q2) (Absorbing Q1) →
  IntoSep (□ P) (□ Q1) (□ Q2).
Proof.
  rewrite /IntoSep /= => -> ??.
  by rewrite sep_and intuitionistically_and and_sep_intuitionistically.
Qed.

Global Instanceinto_sep_big_sepL_cons {A} (Φ : nat → A → PROP) l x l' :
  IsCons l x l' →
  IntoSep ([∗ list] k ↦ y ∈ l, Φ k y)
    (Φ 0 x) ([∗ list] k ↦ y ∈ l', Φ (S k) y).
Proof. rewrite /IsCons=>->. by rewrite /IntoSep big_sepL_cons. Qed.

Global Instanceinto_sep_big_sepL_app {A} (Φ : nat → A → PROP) l l1 l2 :
  IsApp l l1 l2 →
  IntoSep ([∗ list] k ↦ y ∈ l, Φ k y)
    ([∗ list] k ↦ y ∈ l1, Φ k y) ([∗ list] k ↦ y ∈ l2, Φ (length l1 + k) y).
Proof. rewrite /IsApp=>->. by rewrite /IntoSep big_sepL_app. Qed.

Global Instanceinto_sep_big_sepL2_cons {A B}
    (Φ : nat → A → B → PROP) l1 x1 l1' l2 x2 l2' :
  IsCons l1 x1 l1' → IsCons l2 x2 l2' →
  IntoSep ([∗ list] k ↦ y1;y2 ∈ l1;l2, Φ k y1 y2)
    (Φ 0 x1 x2) ([∗ list] k ↦ y1;y2 ∈ l1';l2', Φ (S k) y1 y2).
Proof. rewrite /IsCons=>-> ->. by rewrite /IntoSep big_sepL2_cons. Qed.

Global Instanceinto_sep_big_sepMS_disj_union `{Countable A} (Φ : A → PROP) X1 X2 :
  IntoSep ([∗ mset] y ∈ X1 ⊎ X2, Φ y) ([∗ mset] y ∈ X1, Φ y) ([∗ mset] y ∈ X2, Φ y).
Proof. by rewrite /IntoSep big_sepMS_disj_union. Qed.

Global Instancefrom_or_or P1 P2 : FromOr (P1 ∨ P2) P1 P2.
Proof. by rewrite /FromOr. Qed.

Global Instancefrom_or_pure φ ψ : @FromOr PROP ⌜φ ∨ ψ⌝ ⌜φ⌝ ⌜ψ⌝.
Proof. by rewrite /FromOr pure_or. Qed.

Global Instancefrom_or_affinely P Q1 Q2 :
  FromOr P Q1 Q2 → FromOr (<affine> P) (<affine> Q1) (<affine> Q2).
Proof. rewrite /FromOr=> <-. by rewrite affinely_or. Qed.

Global Instancefrom_or_intuitionistically P Q1 Q2 :
  FromOr P Q1 Q2 → FromOr (□ P) (□ Q1) (□ Q2).
Proof. rewrite /FromOr=> <-. by rewrite intuitionistically_or. Qed.

Global Instancefrom_or_absorbingly P Q1 Q2 :
  FromOr P Q1 Q2 → FromOr (<absorb> P) (<absorb> Q1) (<absorb> Q2).
Proof. rewrite /FromOr=> <-. by rewrite absorbingly_or. Qed.

Global Instancefrom_or_persistently P Q1 Q2 :
  FromOr P Q1 Q2 →
  FromOr (<pers> P) (<pers> Q1) (<pers> Q2).
Proof. rewrite /FromOr=> <-. by rewrite persistently_or. Qed.

Global Instanceinto_or_or P Q : IntoOr (P ∨ Q) P Q.
Proof. by rewrite /IntoOr. Qed.

Global Instanceinto_or_pure φ ψ : @IntoOr PROP ⌜φ ∨ ψ⌝ ⌜φ⌝ ⌜ψ⌝.
Proof. by rewrite /IntoOr pure_or. Qed.

Global Instanceinto_or_affinely P Q1 Q2 :
  IntoOr P Q1 Q2 → IntoOr (<affine> P) (<affine> Q1) (<affine> Q2).
Proof. rewrite /IntoOr=>->. by rewrite affinely_or. Qed.

Global Instanceinto_or_intuitionistically P Q1 Q2 :
  IntoOr P Q1 Q2 → IntoOr (□ P) (□ Q1) (□ Q2).
Proof. rewrite /IntoOr=>->. by rewrite intuitionistically_or. Qed.

Global Instanceinto_or_absorbingly P Q1 Q2 :
  IntoOr P Q1 Q2 → IntoOr (<absorb> P) (<absorb> Q1) (<absorb> Q2).
Proof. rewrite /IntoOr=>->. by rewrite absorbingly_or. Qed.

Global Instanceinto_or_persistently P Q1 Q2 :
  IntoOr P Q1 Q2 →
  IntoOr (<pers> P) (<pers> Q1) (<pers> Q2).
Proof. rewrite /IntoOr=>->. by rewrite persistently_or. Qed.

Global Instancefrom_exist_texist {TT : tele} (Φ : TT → PROP) :
  FromExist (∃.. a, Φ a) Φ.
Proof. by rewrite /FromExist bi_texist_exist. Qed.

Global Instancefrom_exist_pure {A} (φ : A → Prop) :
  @FromExist PROP A ⌜∃ x, φ x⌝ (λ a, ⌜φ a⌝)%I.
Proof. by rewrite /FromExist pure_exist. Qed.

Global Instancefrom_exist_affinely {A} P (Φ : A → PROP) :
  FromExist P Φ → FromExist (<affine> P) (λ a, <affine> (Φ a))%I.
Proof. rewrite /FromExist=> <-. by rewrite affinely_exist. Qed.

Global Instancefrom_exist_intuitionistically {A} P (Φ : A → PROP) :
  FromExist P Φ → FromExist (□ P) (λ a, □ (Φ a))%I.
Proof. rewrite /FromExist=> <-. by rewrite intuitionistically_exist. Qed.

Global Instancefrom_exist_absorbingly {A} P (Φ : A → PROP) :
  FromExist P Φ → FromExist (<absorb> P) (λ a, <absorb> (Φ a))%I.
Proof. rewrite /FromExist=> <-. by rewrite absorbingly_exist. Qed.

Global Instancefrom_exist_persistently {A} P (Φ : A → PROP) :
  FromExist P Φ → FromExist (<pers> P) (λ a, <pers> (Φ a))%I.
Proof. rewrite /FromExist=> <-. by rewrite persistently_exist. Qed.

Global Instanceinto_exist_exist {A} (Φ : A → PROP) name :
  AsIdentName Φ name → IntoExist (bi_exist Φ) Φ name.
Proof. by rewrite /IntoExist. Qed.

Global Instanceinto_exist_pure {A} (φ : A → Prop) name :
  AsIdentName φ name →
  @IntoExist PROP A ⌜ex φ⌝ (λ a, ⌜φ a⌝)%I name.
Proof. by rewrite /IntoExist pure_exist. Qed.

Global Instanceinto_exist_texist {TT : tele} (Φ : TT → PROP) name :
  AsIdentName Φ name → IntoExist (bi_texist Φ) Φ name | 10.
Proof. by rewrite /IntoExist bi_texist_exist. Qed.

Global Instanceinto_exist_affinely {A} P (Φ : A → PROP) name :
  IntoExist P Φ name → IntoExist (<affine> P) (λ a, <affine> (Φ a))%I name.
Proof. rewrite /IntoExist=> HP. by rewrite HP affinely_exist. Qed.

Global Instanceinto_exist_intuitionistically {A} P (Φ : A → PROP) name :
  IntoExist P Φ name → IntoExist (□ P) (λ a, □ (Φ a))%I name.
Proof. rewrite /IntoExist=> HP. by rewrite HP intuitionistically_exist. Qed.

Global Instanceinto_exist_and_pure PQ P Q (φ : Type) :
  IntoAnd false PQ P Q →
  IntoPureT P φ →
  IntoExist PQ (λ _ : φ, Q) (to_ident_name H) | 10.
Proof.
  intros HPQ (φ'&->&?). rewrite /IntoAnd /= in HPQ.
  rewrite /IntoExist HPQ (into_pure P).
  apply pure_elim_l=> Hφ. by rewrite -(exist_intro Hφ).
Qed.

Global Instanceinto_exist_sep_pure P Q (φ : Type) :
  IntoPureT P φ →
  TCOr (Affine P) (Absorbing Q) →
  IntoExist (P ∗ Q) (λ _ : φ, Q) (to_ident_name H).
Proof.
  intros (φ'&->&?) ?. rewrite /IntoExist.
  eapply (pure_elim φ'); [by rewrite (into_pure P); apply sep_elim_l, _|]=>?.
  rewrite -exist_intro //. apply sep_elim_r, _.
Qed.

Global Instanceinto_exist_absorbingly {A} P (Φ : A → PROP) name :
  IntoExist P Φ name → IntoExist (<absorb> P) (λ a, <absorb> (Φ a))%I name.
Proof. rewrite /IntoExist=> HP. by rewrite HP absorbingly_exist. Qed.

Global Instanceinto_exist_persistently {A} P (Φ : A → PROP) name :
  IntoExist P Φ name → IntoExist (<pers> P) (λ a, <pers> (Φ a))%I name.
Proof. rewrite /IntoExist=> HP. by rewrite HP persistently_exist. Qed.

Global Instanceinto_forall_forall {A} (Φ : A → PROP) : IntoForall (∀ a, Φ a) Φ.
Proof. by rewrite /IntoForall. Qed.

Global Instanceinto_forall_tforall {TT : tele} (Φ : TT → PROP) :
  IntoForall (∀.. a, Φ a) Φ | 10.
Proof. by rewrite /IntoForall bi_tforall_forall. Qed.

Global Instanceinto_forall_affinely {A} P (Φ : A → PROP) :
  IntoForall P Φ → IntoForall (<affine> P) (λ a, <affine> (Φ a))%I.
Proof. rewrite /IntoForall=> HP. by rewrite HP affinely_forall. Qed.

Global Instanceinto_forall_intuitionistically {A} P (Φ : A → PROP) :
  IntoForall P Φ → IntoForall (□ P) (λ a, □ (Φ a))%I.
Proof. rewrite /IntoForall=> HP. by rewrite HP intuitionistically_forall. Qed.

Global Instanceinto_forall_persistently `{!BiPersistentlyForall PROP} {A} P (Φ : A → PROP) :
  IntoForall P Φ → IntoForall (<pers> P) (λ a, <pers> (Φ a))%I.
Proof. rewrite /IntoForall=> HP. by rewrite HP persistently_forall. Qed.

Global Instanceinto_forall_impl_pure a φ P Q :
  FromPureT a P φ →
  TCOr (TCEq a false) (BiAffine PROP) →
  IntoForall (P → Q) (λ _ : φ, Q).
Proof.
  rewrite /FromPureT /FromPure /IntoForall=> -[φ' [-> <-]] [->|?] /=.
  - by rewrite pure_impl_forall.
  - by rewrite -affinely_affinely_if affine_affinely pure_impl_forall.
Qed.

Global Instanceinto_forall_wand_pure a φ P Q :
  FromPureT a P φ → IntoForall (P -∗ Q) (λ _ : φ, Q).
Proof.
  rewrite /FromPureT /FromPure /IntoForall=> -[φ' [-> <-]] /=.
  apply forall_intro=>? /=. rewrite -affinely_affinely_if.
  by rewrite -(pure_intro _ True) // /bi_affinely right_id emp_wand.
Qed.

Global Instanceinto_forall_wand P Q :
  IntoForall (P -∗ Q) (λ _ : ⊢ P, Q) | 10.
Proof. rewrite /IntoForall. apply forall_intro=><-. rewrite emp_wand //. Qed.

Global Instanceinto_forall_impl `{!BiAffine PROP} P Q :
  IntoForall (P → Q) (λ _ : ⊢ P, Q) | 10.
Proof.
  rewrite /IntoForall. apply forall_intro=><-. rewrite -True_emp True_impl //.
Qed.

Global Instancefrom_forall_forall {A} (Φ : A → PROP) name :
  AsIdentName Φ name → FromForall (bi_forall Φ) Φ name.
Proof. by rewrite /FromForall. Qed.

Global Instancefrom_forall_tforall {TT : tele} (Φ : TT → PROP) name :
  AsIdentName Φ name → FromForall (bi_tforall Φ) Φ name.
Proof. by rewrite /FromForall bi_tforall_forall. Qed.

Global Instancefrom_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.

Global Instancefrom_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.

Global Instancefrom_forall_pure_not `{!BiPureForall PROP} (φ : Prop) :
  @FromForall PROP φ ⌜¬ φ⌝ (λ _ : φ, False)%I (to_ident_name H).
Proof. by rewrite /FromForall pure_forall. Qed.

Global Instancefrom_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.

Global Instancefrom_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.

Global Instancefrom_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.

Global Instancefrom_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.

Global Instanceelim_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.

Global Instanceelim_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.

Global Instanceelim_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.

Global Instanceelim_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.

Global Instanceelim_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.

Global Instanceadd_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.

Global Instanceadd_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.

Global Instanceadd_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.

Global Instanceadd_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.

Global Instanceelim_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.

Global Instanceelim_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.