phanerozoic/Coq-Iris huggingface dataset:
(* iris/bi/big_op.v *)
(* No need to declare instances for non-expansiveness and properness, we
  get both from the generic [big_opMS] instances. *)
Instance big_sepMS_mono' :
     Proper (pointwise_relation _ (⊢) ==> (=) ==> (⊢)) (big_opMS (@bi_sep PROP) (A:=A)).
Proof. intros f g Hf m ? <-. by apply big_sepMS_mono. Qed.
(* iris/bi/big_op.v *)
Instance big_sepMS_flip_mono' :
     Proper (pointwise_relation _ (flip (⊢)) ==> (=) ==> flip (⊢))
            (big_opMS (@bi_sep PROP) (A:=A)).
Proof. solve_proper. Qed.
(* iris/bi/big_op.v *)
Instance big_sepMS_empty_persistent Φ :
    Persistent ([∗ mset] x ∈ ∅, Φ x).
Proof. rewrite big_opMS_empty. apply _. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepMS_persistent Φ X :
    (∀ x, x ∈ X → Persistent (Φ x)) → Persistent ([∗ mset] x ∈ X, Φ x).
Proof. apply big_opMS_closed; apply _. Qed.
(* iris/bi/big_op.v *)
Instance big_sepMS_persistent' Φ X :
    (∀ x, Persistent (Φ x)) → Persistent ([∗ mset] x ∈ X, Φ x).
Proof. intros; apply big_sepMS_persistent, _. Qed.
(* iris/bi/big_op.v *)
Instance big_sepMS_empty_affine Φ : Affine ([∗ mset] x ∈ ∅, Φ x).
Proof. rewrite big_opMS_empty. apply _. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepMS_affine Φ X :
    (∀ x, x ∈ X → Affine (Φ x)) → Affine ([∗ mset] x ∈ X, Φ x).
Proof. apply big_opMS_closed; apply _. Qed.
(* iris/bi/big_op.v *)
Instance big_sepMS_affine' Φ X :
    (∀ x, Affine (Φ x)) → Affine ([∗ mset] x ∈ X, Φ x).
Proof. intros; apply big_sepMS_affine, _. Qed.
(* iris/bi/big_op.v *)
Instance big_sepMS_empty_timeless `{!Timeless (emp%I : PROP)} Φ :
    Timeless ([∗ mset] x ∈ ∅, Φ x).
Proof. rewrite big_opMS_empty. apply _. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepMS_timeless `{!Timeless (emp%I : PROP)} Φ X :
    (∀ x, x ∈ X → Timeless (Φ x)) → Timeless ([∗ mset] x ∈ X, Φ x).
Proof. apply big_opMS_closed; apply _. Qed.
(* iris/bi/big_op.v *)
Instance big_sepMS_timeless' `{!Timeless (emp%I : PROP)} Φ X :
    (∀ x, Timeless (Φ x)) → Timeless ([∗ mset] x ∈ X, Φ x).
Proof. intros; apply big_sepMS_timeless, _. Qed.
(* iris/bi/big_op.v *)
(* See comment above [big_sepM_subseteq] as for why the [Affine]
     instance is placed late. *)
Lemma big_sepMS_subseteq Φ X Y `{!∀ x, Affine (Φ x)} :
    Y ⊆ X → ([∗ mset] x ∈ X, Φ x) ⊢ [∗ mset] x ∈ Y, Φ x.
Proof.
    intros ->%gmultiset_disj_union_difference.
    by rewrite big_opMS_disj_union sep_elim_l.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepMS_empty Φ : ([∗ mset] x ∈ ∅, Φ x) ⊣⊢ emp.
Proof. by rewrite big_opMS_empty. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepMS_empty' P `{!Affine P} Φ : P ⊢ [∗ mset] x ∈ ∅, Φ x.
Proof. rewrite big_sepMS_empty. apply: affine. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepMS_disj_union Φ X Y :
    ([∗ mset] y ∈ X ⊎ Y, Φ y) ⊣⊢ ([∗ mset] y ∈ X, Φ y) ∗ [∗ mset] y ∈ Y, Φ y.
Proof. apply big_opMS_disj_union. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepMS_delete Φ X x :
    x ∈ X → ([∗ mset] y ∈ X, Φ y) ⊣⊢ Φ x ∗ [∗ mset] y ∈ X ∖ {[+ x +]}, Φ y.
Proof. apply big_opMS_delete. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepMS_elem_of Φ X x
    `{!TCOr (∀ y, Affine (Φ y)) (Absorbing (Φ x))} :
    x ∈ X → ([∗ mset] y ∈ X, Φ y) ⊢ Φ x.
Proof.
    intros ?. rewrite big_sepMS_delete //.
    destruct select (TCOr _ _); by rewrite sep_elim_l.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepMS_elem_of_acc Φ X x :
    x ∈ X →
    ([∗ mset] y ∈ X, Φ y) ⊢ Φ x ∗ (Φ x -∗ ([∗ mset] y ∈ X, Φ y)).
Proof.
    intros. rewrite big_sepMS_delete //. by apply sep_mono_r, wand_intro_l.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepMS_singleton Φ x : ([∗ mset] y ∈ {[+ x +]}, Φ y) ⊣⊢ Φ x.
Proof. apply big_opMS_singleton. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepMS_insert Φ X x :
    ([∗ mset] y ∈ {[+ x +]} ⊎ X, Φ y) ⊣⊢ (Φ x ∗ [∗ mset] y ∈ X, Φ y).
Proof. apply big_opMS_insert. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepMS_sep Φ Ψ X :
    ([∗ mset] y ∈ X, Φ y ∗ Ψ y) ⊣⊢ ([∗ mset] y ∈ X, Φ y) ∗ ([∗ mset] y ∈ X, Ψ y).
Proof. apply big_opMS_op. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepMS_sep_2 Φ Ψ X :
    ([∗ mset] y ∈ X, Φ y) -∗
    ([∗ mset] y ∈ X, Ψ y) -∗
    ([∗ mset] y ∈ X, Φ y ∗ Ψ y).
Proof. apply entails_wand, wand_intro_r. rewrite big_sepMS_sep //. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepMS_and Φ Ψ X :
    ([∗ mset] y ∈ X, Φ y ∧ Ψ y) ⊢ ([∗ mset] y ∈ X, Φ y) ∧ ([∗ mset] y ∈ X, Ψ y).
Proof. auto using and_intro, big_sepMS_mono, and_elim_l, and_elim_r. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepMS_later `{!BiAffine PROP} Φ X :
    ▷ ([∗ mset] y ∈ X, Φ y) ⊣⊢ ([∗ mset] y ∈ X, ▷ Φ y).
Proof. apply (big_opMS_commute _). Qed.
(* iris/bi/big_op.v *)
Lemma big_sepMS_later_2 Φ X :
    ([∗ mset] y ∈ X, ▷ Φ y) ⊢ ▷ [∗ mset] y ∈ X, Φ y.
Proof. by rewrite big_opMS_commute. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepMS_laterN `{!BiAffine PROP} Φ n X :
    ▷^n ([∗ mset] y ∈ X, Φ y) ⊣⊢ ([∗ mset] y ∈ X, ▷^n Φ y).
Proof. apply (big_opMS_commute _). Qed.
(* iris/bi/big_op.v *)
Lemma big_sepMS_laterN_2 Φ n X :
    ([∗ mset] y ∈ X, ▷^n Φ y) ⊢ ▷^n [∗ mset] y ∈ X, Φ y.
Proof. by rewrite big_opMS_commute. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepMS_pure_1 (φ : A → Prop) X :
    ([∗ mset] y ∈ X, ⌜φ y⌝) ⊢@{PROP} ⌜∀ y : A, y ∈ X → φ y⌝.
Proof.
    induction X as [|x X IH] using gmultiset_ind.
    { apply pure_intro=>??. exfalso. multiset_solver. }
    rewrite big_sepMS_insert // IH sep_and -pure_and.
    f_equiv=>-[Hx HX] y /gmultiset_elem_of_disj_union [|].
    - move=>/gmultiset_elem_of_singleton =>->. done.
    - eauto.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepMS_affinely_pure_2 (φ : A → Prop) X :
    <affine> ⌜∀ y : A, y ∈ X → φ y⌝ ⊢@{PROP} ([∗ mset] y ∈ X, <affine> ⌜φ y⌝).
Proof.
    induction X as [|x X IH] using gmultiset_ind.
    { rewrite big_sepMS_empty. apply affinely_elim_emp. }
    rewrite big_sepMS_insert // -IH.
    rewrite -persistent_and_sep_1 -affinely_and -pure_and.
    f_equiv. f_equiv=>HX. split.
    - apply HX. set_solver+.
    - intros y Hy. apply HX. multiset_solver.
  Qed.
(* iris/bi/big_op.v *)
(* The general backwards direction requires [BiAffine] to cover the empty case. *)
Lemma big_sepMS_pure `{!BiAffine PROP} (φ : A → Prop) X :
    ([∗ mset] y ∈ X, ⌜φ y⌝) ⊣⊢@{PROP} ⌜∀ y : A, y ∈ X → φ y⌝.
Proof.
    apply (anti_symm (⊢)); first by apply big_sepMS_pure_1.
    rewrite -(affine_affinely ⌜_⌝%I).
    rewrite big_sepMS_affinely_pure_2. by setoid_rewrite affinely_elim.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepMS_persistently `{!BiAffine PROP} Φ X :
    <pers> ([∗ mset] y ∈ X, Φ y) ⊣⊢ [∗ mset] y ∈ X, <pers> (Φ y).
Proof. apply (big_opMS_commute _). Qed.
(* iris/bi/big_op.v *)
Lemma big_sepMS_intro Φ X :
    □ (∀ x, ⌜x ∈ X⌝ → Φ x) ⊢ [∗ mset] x ∈ X, Φ x.
Proof.
    revert Φ. induction X as [|x X IH] using gmultiset_ind=> Φ.
    { by rewrite (affine (□ _)) big_sepMS_empty. }
    rewrite intuitionistically_sep_dup big_sepMS_disj_union.
    rewrite big_sepMS_singleton. f_equiv.
    - rewrite (forall_elim x) pure_True ?True_impl; last multiset_solver.
      by rewrite intuitionistically_elim.
    - rewrite -IH. f_equiv. apply forall_mono=> y.
      apply impl_intro_l, pure_elim_l=> ?.
      by rewrite pure_True ?True_impl; last multiset_solver.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepMS_forall `{!BiAffine PROP} Φ X :
    (∀ x, Persistent (Φ x)) →
    ([∗ mset] x ∈ X, Φ x) ⊣⊢ (∀ x, ⌜x ∈ X⌝ → Φ x).
Proof.
    intros HΦ. apply (anti_symm _).
    { apply forall_intro=> x.
      apply impl_intro_l, pure_elim_l=> ?; by apply: big_sepMS_elem_of. }
    revert Φ HΦ. induction X as [|x X IH] using gmultiset_ind=> Φ HΦ.
    { rewrite big_sepMS_empty. apply: affine. }
    rewrite big_sepMS_disj_union.
    rewrite big_sepMS_singleton -persistent_and_sep_1. apply and_intro.
    - rewrite (forall_elim x) pure_True ?True_impl; last multiset_solver. done.
    - rewrite -IH. apply forall_mono=> y.
      apply impl_intro_l, pure_elim_l=> ?.
      by rewrite pure_True ?True_impl; last multiset_solver.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepMS_impl Φ Ψ X :
    ([∗ mset] x ∈ X, Φ x) -∗
    □ (∀ x, ⌜x ∈ X⌝ → Φ x -∗ Ψ x) -∗
    [∗ mset] x ∈ X, Ψ x.
Proof.
    apply entails_wand, wand_intro_l. rewrite big_sepMS_intro -big_sepMS_sep.
    by setoid_rewrite wand_elim_l.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepMS_wand Φ Ψ X :
    ([∗ mset] x ∈ X, Φ x) -∗
    ([∗ mset] x ∈ X, Φ x -∗ Ψ x) -∗
    [∗ mset] x ∈ X, Ψ x.
Proof.
    apply entails_wand, wand_intro_r. rewrite -big_sepMS_sep.
    setoid_rewrite wand_elim_r. done.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepMS_dup P `{!Affine P} X :
    □ (P -∗ P ∗ P) -∗ P -∗ [∗ mset] x ∈ X, P.
Proof.
    apply entails_wand, wand_intro_l. induction X as [|x X IH] using gmultiset_ind.
    { apply: big_sepMS_empty'. }
    rewrite !big_sepMS_disj_union big_sepMS_singleton.
    rewrite intuitionistically_sep_dup {1}intuitionistically_elim.
    rewrite assoc wand_elim_r -assoc. apply sep_mono; done.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepMS_elem_of_acc_impl {Φ X} x :
    x ∈ X →
    ([∗ mset] y ∈ X, Φ y) -∗
    (* we get [Φ] for [x] *)
    Φ x ∗
    (* we reobtain the bigop for a predicate [Ψ] selected by the user *)
    ∀ Ψ,
      □ (∀ y, ⌜ y ∈ X ∖ {[+ x +]} ⌝ → Φ y -∗ Ψ y) -∗
      Ψ x -∗
      [∗ mset] y ∈ X, Ψ y.
Proof.
    intros. rewrite big_sepMS_delete //. apply entails_wand, sep_mono_r, forall_intro=> Ψ.
    apply wand_intro_r, wand_intro_l.
    rewrite (big_sepMS_delete Ψ X x) //. apply sep_mono_r.
    apply wand_elim_l', wand_entails, big_sepMS_impl.
  Qed.
(* iris/bi/big_op.v *)
(* Commuting lemmas *)
Lemma big_sepL_sepL {A B} (Φ : nat → A → nat → B → PROP) (l1 : list A) (l2 : list B) :
  ([∗ list] k1↦x1 ∈ l1, [∗ list] k2↦x2 ∈ l2, Φ k1 x1 k2 x2) ⊣⊢
  ([∗ list] k2↦x2 ∈ l2, [∗ list] k1↦x1 ∈ l1, Φ k1 x1 k2 x2).
Proof. apply big_opL_opL. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepL_sepM {A} `{Countable K} {B}
    (Φ : nat → A → K → B → PROP) (l1 : list A) (m2 : gmap K B) :
  ([∗ list] k1↦x1 ∈ l1, [∗ map] k2↦x2 ∈ m2, Φ k1 x1 k2 x2) ⊣⊢
  ([∗ map] k2↦x2 ∈ m2, [∗ list] k1↦x1 ∈ l1, Φ k1 x1 k2 x2).
Proof. apply big_opL_opM. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepL_sepS {A} `{Countable B}
    (Φ : nat → A → B → PROP) (l1 : list A) (X2 : gset B) :
  ([∗ list] k1↦x1 ∈ l1, [∗ set] x2 ∈ X2, Φ k1 x1 x2) ⊣⊢
  ([∗ set] x2 ∈ X2, [∗ list] k1↦x1 ∈ l1, Φ k1 x1 x2).
Proof. apply big_opL_opS. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepL_sepMS {A} `{Countable B}
    (Φ : nat → A → B → PROP) (l1 : list A) (X2 : gmultiset B) :
  ([∗ list] k1↦x1 ∈ l1, [∗ mset] x2 ∈ X2, Φ k1 x1 x2) ⊣⊢
  ([∗ mset] x2 ∈ X2, [∗ list] k1↦x1 ∈ l1, Φ k1 x1 x2).
Proof. apply big_opL_opMS. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepM_sepL `{Countable K} {A} {B}
    (Φ : K → A → nat → B → PROP) (m1 : gmap K A) (l2 : list B) :
  ([∗ map] k1↦x1 ∈ m1, [∗ list] k2↦x2 ∈ l2, Φ k1 x1 k2 x2) ⊣⊢
  ([∗ list] k2↦x2 ∈ l2, [∗ map] k1↦x1 ∈ m1, Φ k1 x1 k2 x2).
Proof. apply big_opM_opL. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepM_sepM `{Countable K1} {A} `{Countable K2} {B}
    (Φ : K1 → A → K2 → B → PROP) (m1 : gmap K1 A) (m2 : gmap K2 B) :
  ([∗ map] k1↦x1 ∈ m1, [∗ map] k2↦x2 ∈ m2, Φ k1 x1 k2 x2) ⊣⊢
  ([∗ map] k2↦x2 ∈ m2, [∗ map] k1↦x1 ∈ m1, Φ k1 x1 k2 x2).
Proof. apply big_opM_opM. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepM_sepS `{Countable K} {A} `{Countable B}
    (Φ : K → A → B → PROP) (m1 : gmap K A) (X2 : gset B) :
  ([∗ map] k1↦x1 ∈ m1, [∗ set] x2 ∈ X2, Φ k1 x1 x2) ⊣⊢
  ([∗ set] x2 ∈ X2, [∗ map] k1↦x1 ∈ m1, Φ k1 x1 x2).
Proof. apply big_opM_opS. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepM_sepMS `{Countable K} {A} `{Countable B} (Φ : K → A → B → PROP)
    (m1 : gmap K A) (X2 : gmultiset B) :
  ([∗ map] k1↦x1 ∈ m1, [∗ mset] x2 ∈ X2, Φ k1 x1 x2) ⊣⊢
  ([∗ mset] x2 ∈ X2, [∗ map] k1↦x1 ∈ m1, Φ k1 x1 x2).
Proof. apply big_opM_opMS. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepS_sepL `{Countable A} {B}
    (f : A → nat → B → PROP) (X1 : gset A) (l2 : list B) :
  ([∗ set] x1 ∈ X1, [∗ list] k2↦x2 ∈ l2, f x1 k2 x2) ⊣⊢
  ([∗ list] k2↦x2 ∈ l2, [∗ set] x1 ∈ X1, f x1 k2 x2).
Proof. apply big_opS_opL. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepS_sepM `{Countable A} `{Countable K} {B}
    (f : A → K → B → PROP) (X1 : gset A) (m2 : gmap K B) :
  ([∗ set] x1 ∈ X1, [∗ map] k2↦x2 ∈ m2, f x1 k2 x2) ⊣⊢
  ([∗ map] k2↦x2 ∈ m2, [∗ set] x1 ∈ X1, f x1 k2 x2).
Proof. apply big_opS_opM. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepS_sepS `{Countable A, Countable B}
    (X : gset A) (Y : gset B) (Φ : A → B → PROP) :
  ([∗ set] x ∈ X, [∗ set] y ∈ Y, Φ x y) ⊣⊢ ([∗ set] y ∈ Y, [∗ set] x ∈ X, Φ x y).
Proof. apply big_opS_opS. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepS_sepMS `{Countable A, Countable B}
    (X : gset A) (Y : gmultiset B) (Φ : A → B → PROP) :
  ([∗ set] x ∈ X, [∗ mset] y ∈ Y, Φ x y) ⊣⊢ ([∗ mset] y ∈ Y, [∗ set] x ∈ X, Φ x y).
Proof. apply big_opS_opMS. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepMS_sepL `{Countable A} {B}
    (f : A → nat → B → PROP) (X1 : gmultiset A) (l2 : list B) :
  ([∗ mset] x1 ∈ X1, [∗ list] k2↦x2 ∈ l2, f x1 k2 x2) ⊣⊢
  ([∗ list] k2↦x2 ∈ l2, [∗ mset] x1 ∈ X1, f x1 k2 x2).
Proof. apply big_opMS_opL. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepMS_sepM `{Countable A} `{Countable K} {B} (f : A → K → B → PROP)
    (X1 : gmultiset A) (m2 : gmap K B) :
  ([∗ mset] x1 ∈ X1, [∗ map] k2↦x2 ∈ m2, f x1 k2 x2) ⊣⊢
  ([∗ map] k2↦x2 ∈ m2, [∗ mset] x1 ∈ X1, f x1 k2 x2).
Proof. apply big_opMS_opM. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepMS_sepS `{Countable A, Countable B}
    (X : gmultiset A) (Y : gset B) (f : A → B → PROP) :
  ([∗ mset] x ∈ X, [∗ set] y ∈ Y, f x y) ⊣⊢ ([∗ set] y ∈ Y, [∗ mset] x ∈ X, f x y).
Proof. apply big_opMS_opS. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepMS_sepMS `{Countable A, Countable B}
    (X : gmultiset A) (Y : gmultiset B) (Φ : A → B → PROP) :
  ([∗ mset] x ∈ X, [∗ mset] y ∈ Y, Φ x y) ⊣⊢ ([∗ mset] y ∈ Y, [∗ mset] x ∈ X, Φ x y).
Proof. apply big_opMS_opMS. Qed.
(* iris/bi/cmra.v *)
Definition internal_cmra_valid `{!Sbi PROP} {A : cmra} (a : A) : PROP
:=
  <si_pure> siProp_cmra_valid a.
(* iris/bi/cmra.v *)
Instance : Params (@internal_cmra_valid) 3
:= {}.
(* iris/bi/cmra.v *)
Notation "✓ a"
:= (internal_cmra_valid a) : bi_scope.
(* iris/bi/cmra.v *)
(* Derived [≼] connective on [cmra] elements. This can be defined on any [bi]
that has internal equality [≡]. It corresponds to the step-indexed [≼{n}]
connective in the [siProp] model. *)
Definition internal_included `{!Sbi PROP} {A : cmra} (a b : A) : PROP
:=
  ∃ c, b ≡ a ⋅ c.
(* iris/bi/cmra.v *)
Instance : Params (@internal_included) 3
:= {}.
(* iris/bi/cmra.v *)
(* Force implicit argument PROP *)
Notation "P ⊢ Q"
:= (P ⊢@{PROP} Q).
(* iris/bi/cmra.v *)
Notation "P ⊣⊢ Q"
:= (P ⊣⊢@{PROP} Q).
(* iris/bi/cmra.v *)
Instance internal_cmra_valid_ne {A : cmra} :
    NonExpansive (@internal_cmra_valid PROP _ A).
Proof.
    intros n x x' ?. by apply si_pure_ne, siProp_primitive.cmra_valid_ne.
  Qed.
(* iris/bi/cmra.v *)
Instance internal_cmra_valid_proper {A : cmra} :
    Proper ((≡) ==> (⊣⊢)) (@internal_cmra_valid PROP _ A).
Proof. apply ne_proper, _. Qed.
(* iris/bi/cmra.v *)
Lemma internal_cmra_valid_intro {A : cmra} P (a : A) : ✓ a → P ⊢ (✓ a).
Proof.
    intros. rewrite (bi.True_intro P) -si_pure_pure.
    by apply si_pure_mono, siProp_primitive.cmra_valid_intro.
  Qed.
(* iris/bi/cmra.v *)
Lemma internal_cmra_valid_elim {A : cmra} (a : A) : ✓ a ⊢ ⌜ ✓{0} a ⌝.
Proof.
    rewrite -si_pure_pure.
    by apply si_pure_mono, siProp_primitive.cmra_valid_elim.
  Qed.
(* iris/bi/cmra.v *)
(* FIXME: Remove in favor of cmra_validN_op_r *)
Lemma internal_cmra_valid_weaken {A : cmra} (a b : A) : ✓ (a ⋅ b) ⊢ ✓ a.
Proof. by apply si_pure_mono, siProp_primitive.cmra_valid_weaken. Qed.
(* iris/bi/cmra.v *)
Lemma internal_cmra_valid_entails {A B : cmra} (a : A) (b : B) :
    (✓ a ⊢ ✓ b) ↔ ∀ n, ✓{n} a → ✓{n} b.
Proof. rewrite si_pure_entails. apply siProp_primitive.valid_entails. Qed.
(* iris/bi/cmra.v *)
Lemma si_pure_internal_cmra_valid {A : cmra} (a : A) : <si_pure> ✓ a ⊣⊢ ✓ a.
Proof. done. Qed.
(* iris/bi/cmra.v *)
Lemma persistently_internal_cmra_valid {A : cmra} (a : A) : <pers> ✓ a ⊣⊢ ✓ a.
Proof. apply persistently_si_pure. Qed.
(* iris/bi/cmra.v *)
Lemma plainly_internal_cmra_valid {A : cmra} (a : A) : ■ ✓ a ⊣⊢ ✓ a.
Proof. apply plainly_si_pure. Qed.
(* iris/bi/cmra.v *)
Lemma intuitionistically_internal_cmra_valid `{!BiAffine PROP} {A : cmra} (a : A) :
    □ ✓ a ⊣⊢ ✓ a.
Proof.
    by rewrite bi.intuitionistically_into_persistently
      persistently_internal_cmra_valid.
  Qed.
(* iris/bi/cmra.v *)
Lemma internal_cmra_valid_discrete `{!CmraDiscrete A} (a : A) : ✓ a ⊣⊢ ⌜✓ a⌝.
Proof.
    apply (anti_symm _).
    - rewrite internal_cmra_valid_elim. by apply bi.pure_mono, cmra_discrete_valid.
    - apply bi.pure_elim'=> ?. by apply internal_cmra_valid_intro.
  Qed.
(* iris/bi/cmra.v *)
Instance internal_cmra_valid_timeless `{!CmraDiscrete A} (a : A) :
    Timeless (PROP:=PROP) (✓ a).
Proof. rewrite /Timeless !internal_cmra_valid_discrete. apply (timeless _). Qed.
(* iris/bi/cmra.v *)
Instance internal_cmra_valid_absorbing {A : cmra} (a : A) :
    Absorbing (PROP:=PROP) (✓ a).
Proof. rewrite -persistently_internal_cmra_valid. apply _. Qed.
(* iris/bi/cmra.v *)
Instance internal_cmra_valid_plain {A : cmra} (a : A) :
    Plain (PROP:=PROP) (✓ a).
Proof. rewrite -plainly_internal_cmra_valid. apply _. Qed.
(* iris/bi/cmra.v *)
Instance internal_cmra_valid_persistent {A : cmra} (a : A) :
    Persistent (PROP:=PROP) (✓ a).
Proof. rewrite -persistently_internal_cmra_valid. apply _. Qed.
(* iris/bi/cmra.v *)
Instance internal_included_nonexpansive A :
    NonExpansive2 (internal_included (PROP:=PROP) (A:=A)).
Proof. solve_proper. Qed.
(* iris/bi/cmra.v *)
Instance internal_included_proper A :
    Proper ((≡) ==> (≡) ==> (⊣⊢)) (internal_included (PROP:=PROP) (A:=A)).
Proof. solve_proper. Qed.
(* iris/bi/cmra.v *)
Lemma internal_included_intro {A : cmra} P (a b : A) : a ≼ b → P ⊢ a ≼ b.
Proof.
    intros [c ->]. rewrite /internal_included -(bi.exist_intro c).
    apply internal_eq_refl.
  Qed.
(* iris/bi/cmra.v *)
Lemma si_pure_internal_included {A : cmra} (a b : A) :
    <si_pure> (a ≼ b) ⊣⊢ a ≼ b.
Proof. rewrite /internal_included si_pure_exist //. Qed.
(* iris/bi/cmra.v *)
Lemma persistently_internal_included {A : cmra} (a b : A) :
    <pers> (a ≼ b) ⊣⊢ a ≼ b.
Proof. by rewrite -si_pure_internal_included persistently_si_pure. Qed.
(* iris/bi/cmra.v *)
Lemma plainly_internal_included {A : cmra} (a b : A) : ■ (a ≼ b) ⊣⊢ a ≼ b.
Proof. by rewrite -si_pure_internal_included plainly_si_pure. Qed.
(* iris/bi/cmra.v *)
Lemma intuitionistically_internal_included `{!BiAffine PROP} {A : cmra} (a b : A) :
    □ (a ≼ b) ⊣⊢ a ≼ b.
Proof.
    by rewrite bi.intuitionistically_into_persistently
      persistently_internal_included.
  Qed.
(* iris/bi/cmra.v *)
Lemma internal_included_discrete {A : cmra} (a b : A) `{!Discrete b} :
    a ≼ b ⊣⊢ ⌜a ≼ b⌝.
Proof.
    apply (anti_symm _).
    - apply bi.exist_elim=> a'. rewrite /internal_included bi.pure_exist.
      rewrite -(bi.exist_intro a'). by rewrite discrete_eq.
    - apply bi.pure_elim'=> ?. by apply internal_included_intro.
  Qed.
(* iris/bi/cmra.v *)
Lemma internal_included_refl `{!CmraTotal A} (a : A) : ⊢@{PROP} a ≼ a.
Proof.
    rewrite /internal_included -(bi.exist_intro (core a)).
    rewrite cmra_core_r. apply internal_eq_refl.
  Qed.
(* iris/bi/cmra.v *)
Lemma internal_included_trans {A : cmra} (a b c : A) :
    ⊢@{PROP} a ≼ b -∗ b ≼ c -∗ a ≼ c.
Proof.
    apply bi.entails_wand, bi.exist_elim=> a'.
    apply bi.wand_intro_l. rewrite /internal_included bi.sep_exist_r.
    apply bi.exist_elim=> b'. rewrite bi.sep_and -(bi.exist_intro (a' ⋅ b')).
    rewrite -(internal_eq_trans c (b ⋅ b') (a ⋅ _)). f_equiv.
    rewrite assoc. apply: (f_equivI (λ z, z ⋅ b')). solve_proper.
  Qed.
(* iris/bi/cmra.v *)
Instance internal_included_timeless {A : cmra} (a b : A) `{!Discrete b} :
    Timeless (PROP:=PROP) (a ≼ b).
Proof. rewrite /internal_included. apply _. Qed.
(* iris/bi/cmra.v *)
Instance internal_included_plain {A : cmra} (a b : A) :
    Plain (PROP:=PROP) (a ≼ b).
Proof. rewrite /internal_included. apply _. Qed.
(* iris/bi/cmra.v *)
Instance internal_included_persistent {A : cmra} (a b : A) :
    Persistent (PROP:=PROP) (a ≼ b).
Proof. rewrite /internal_included. apply _. Qed.
(* iris/bi/cmra.v *)
Instance internal_included_absorbing {A : cmra} (a b : A) :
    Absorbing (PROP:=PROP) (a ≼ b).
Proof. rewrite /internal_included. apply _. Qed.
(* iris/bi/derived_connectives.v *)
Definition bi_iff {PROP : bi} (P Q : PROP) : PROP
:= (P → Q) ∧ (Q → P).
(* iris/bi/derived_connectives.v *)
Instance : Params (@bi_iff) 1
:= {}.
(* iris/bi/derived_connectives.v *)
Definition bi_wand_iff {PROP : bi} (P Q : PROP) : PROP
:=
  (P -∗ Q) ∧ (Q -∗ P).
(* iris/bi/derived_connectives.v *)
Instance : Params (@bi_wand_iff) 1
:= {}.
(* iris/bi/derived_connectives.v *)
Notation "P ∗-∗ Q"
:= (⊢ P ∗-∗ Q) : stdpp_scope.
(* iris/bi/derived_connectives.v *)
Class Persistent {PROP : bi} (P : PROP)
:= persistent : P ⊢ <pers> P.
(* iris/bi/derived_connectives.v *)
Instance : Params (@Persistent) 1
:= {}.
(* iris/bi/derived_connectives.v *)
Definition bi_affinely {PROP : bi} (P : PROP) : PROP
:= emp ∧ P.
(* iris/bi/derived_connectives.v *)
Instance : Params (@bi_affinely) 1
:= {}.
(* iris/bi/derived_connectives.v *)
Notation "'<affine>' P"
:= (bi_affinely P) : bi_scope.
(* iris/bi/derived_connectives.v *)
Class Affine {PROP : bi} (Q : PROP)
:= affine : Q ⊢ emp.
(* iris/bi/derived_connectives.v *)
Definition bi_absorbingly {PROP : bi} (P : PROP) : PROP
:= True ∗ P.
(* iris/bi/derived_connectives.v *)
Instance : Params (@bi_absorbingly) 1
:= {}.
(* iris/bi/derived_connectives.v *)
Notation "'<absorb>' P"
:= (bi_absorbingly P) : bi_scope.
(* iris/bi/derived_connectives.v *)
Class Absorbing {PROP : bi} (P : PROP)
:= absorbing : <absorb> P ⊢ P.
(* iris/bi/derived_connectives.v *)
Definition bi_persistently_if {PROP : bi} (p : bool) (P : PROP) : PROP
:=
  (if p then <pers> P else P)%I.
(* iris/bi/derived_connectives.v *)
Instance : Params (@bi_persistently_if) 2
:= {}.
(* iris/bi/derived_connectives.v *)
Notation "'<pers>?' p P"
:= (bi_persistently_if p P) : bi_scope.
(* iris/bi/derived_connectives.v *)
Definition bi_affinely_if {PROP : bi} (p : bool) (P : PROP) : PROP
:=
  (if p then <affine> P else P)%I.
(* iris/bi/derived_connectives.v *)
Instance : Params (@bi_affinely_if) 2
:= {}.
(* iris/bi/derived_connectives.v *)
Notation "'<affine>?' p P"
:= (bi_affinely_if p P) : bi_scope.
(* iris/bi/derived_connectives.v *)
Definition bi_absorbingly_if {PROP : bi} (p : bool) (P : PROP) : PROP
:=
  (if p then <absorb> P else P)%I.
(* iris/bi/derived_connectives.v *)
Instance : Params (@bi_absorbingly_if) 2
:= {}.
(* iris/bi/derived_connectives.v *)
Notation "'<absorb>?' p P"
:= (bi_absorbingly_if p P) : bi_scope.
(* iris/bi/derived_connectives.v *)
Definition bi_intuitionistically {PROP : bi} (P : PROP) : PROP
:=
  (<affine> <pers> P)%I.
(* iris/bi/derived_connectives.v *)
Instance : Params (@bi_intuitionistically) 1
:= {}.
(* iris/bi/derived_connectives.v *)
Notation "□ P"
:= (bi_intuitionistically P) : bi_scope.
(* iris/bi/derived_connectives.v *)
Definition bi_intuitionistically_if {PROP : bi} (p : bool) (P : PROP) : PROP
:=
  (if p then □ P else P)%I.
(* iris/bi/derived_connectives.v *)
Instance : Params (@bi_intuitionistically_if) 2
:= {}.
(* iris/bi/derived_connectives.v *)
Notation "'□?' p P"
:= (bi_intuitionistically_if p P) : bi_scope.
(* iris/bi/derived_connectives.v *)
Fixpoint bi_laterN {PROP : bi} (n : nat) (P : PROP) : PROP
:=
  match n with
  | O => P
  | S n' => ▷ ▷^n' P
  end
where "▷^ n P" := (bi_laterN n P) : bi_scope.
(* iris/bi/derived_connectives.v *)
Instance : Params (@bi_laterN) 2
:= {}.
(* iris/bi/derived_connectives.v *)
Notation "▷? p P"
:= (bi_laterN (Nat.b2n p) P) : bi_scope.
(* iris/bi/derived_connectives.v *)
Definition bi_except_0 {PROP : bi} (P : PROP) : PROP
:= ▷ False ∨ P.
(* iris/bi/derived_connectives.v *)
Notation "◇ P"
:= (bi_except_0 P) : bi_scope.
(* iris/bi/derived_connectives.v *)
Instance : Params (@bi_except_0) 1
:= {}.