phanerozoic/Coq-Iris huggingface dataset:
(* iris/bi/internal_eq.v *)
Lemma internal_eq_rewrite {A : ofe} a b (Ψ : A → PROP) :
    NonExpansive Ψ →
    internal_eq a b ⊢ Ψ a → Ψ b.
Proof.
    intros. (* [True -∗] makes [True -∗ Ψ a → Ψ a'] persistent, needed for
    [si_pure_si_emp_valid_elim] *)
    pose (Φ a' := (<si_emp_valid> (True -∗ Ψ a → Ψ a'))%I).
    assert (⊢ Φ a) as HΦa.
    { apply si_emp_valid_emp_valid, bi.wand_intro_l.
      by rewrite right_id -bi.entails_impl_True. }
    trans (<si_pure> (Φ a → Φ b) : PROP)%I.
    - apply si_pure_mono. apply siProp_primitive.internal_eq_rewrite.
      solve_proper.
    - unfold bi_emp_valid in HΦa. rewrite -HΦa left_id.
      rewrite /Φ si_pure_si_emp_valid_elim.
      by rewrite -(bi.True_intro emp)%I left_id.
  Qed.
(* iris/bi/internal_eq.v *)
Lemma internal_eq_rewrite' {A : ofe} a b (Ψ : A → PROP) P :
    NonExpansive Ψ →
    (P ⊢ a ≡ b) → (P ⊢ Ψ a) → P ⊢ Ψ b.
Proof.
    intros HΨ Heq HΨa. rewrite -(idemp bi_and P) {1}Heq HΨa.
    apply bi.impl_elim_l'. by apply internal_eq_rewrite.
  Qed.
(* iris/bi/internal_eq.v *)
Lemma internal_eq_sym {A : ofe} (a b : A) : a ≡ b ⊢@{PROP} b ≡ a.
Proof. apply (internal_eq_rewrite' a b (λ b, b ≡ a)%I); auto. Qed.
(* iris/bi/internal_eq.v *)
Lemma internal_eq_trans {A : ofe} (a b c : A) : a ≡ b ∧ b ≡ c ⊢ a ≡ c.
Proof.
    apply (internal_eq_rewrite' b a (λ b, b ≡ c)%I); auto.
    rewrite bi.and_elim_l. apply internal_eq_sym.
  Qed.
(* iris/bi/internal_eq.v *)
Lemma f_equivI {A B : ofe} (f : A → B) `{!NonExpansive f} x y :
    x ≡ y ⊢ f x ≡ f y.
Proof. apply (internal_eq_rewrite' x y (λ y, f x ≡ f y)%I); auto. Qed.
(* iris/bi/internal_eq.v *)
(* Equality of data types *)
Lemma discrete_eq_1 {A : ofe} (a b : A) :
    TCOr (Discrete a) (Discrete b) →
    a ≡ b ⊢@{PROP} ⌜a ≡ b⌝.
Proof.
    intros. rewrite -si_pure_pure.
    by apply si_pure_mono, siProp_primitive.discrete_eq_1.
  Qed.
(* iris/bi/internal_eq.v *)
Lemma discrete_eq {A : ofe} (a b : A) :
    TCOr (Discrete a) (Discrete b) →
    a ≡ b ⊣⊢ ⌜a ≡ b⌝.
Proof.
    intros. apply (anti_symm _); auto using discrete_eq_1, pure_internal_eq.
  Qed.
(* iris/bi/internal_eq.v *)
Lemma fun_extI {A} {B : A → ofe} (f g : discrete_fun B) :
    (∀ x, f x ≡ g x) ⊢@{PROP} f ≡ g.
Proof.
    rewrite /internal_eq -si_pure_forall.
    by apply si_pure_mono, siProp_primitive.fun_extI.
  Qed.
(* iris/bi/internal_eq.v *)
Lemma sig_equivI_1 {A : ofe} (P : A → Prop) (x y : sig P) :
    `x ≡ `y ⊢@{PROP} x ≡ y.
Proof. by apply si_pure_mono, siProp_primitive.sig_equivI_1. Qed.
(* iris/bi/internal_eq.v *)
Lemma prod_equivI {A B : ofe} (x y : A * B) : x ≡ y ⊣⊢ x.1 ≡ y.1 ∧ x.2 ≡ y.2.
Proof.
    apply (anti_symm _).
    - apply bi.and_intro; apply f_equivI; apply _.
    - rewrite {3}(surjective_pairing x) {3}(surjective_pairing y).
      apply (internal_eq_rewrite' (x.1) (y.1) (λ a, (x.1,x.2) ≡ (a,y.2))%I); auto.
      apply (internal_eq_rewrite' (x.2) (y.2) (λ b, (x.1,x.2) ≡ (x.1,b))%I); auto.
  Qed.
(* iris/bi/internal_eq.v *)
Lemma sum_equivI {A B : ofe} (x y : A + B) :
    x ≡ y ⊣⊢
      match x, y with
      | inl a, inl a' => a ≡ a' | inr b, inr b' => b ≡ b' | _, _ => False
      end.
Proof.
    apply (anti_symm _).
    - apply (internal_eq_rewrite' x y (λ y,
               match x, y with
               | inl a, inl a' => a ≡ a' | inr b, inr b' => b ≡ b' | _, _ => False
               end)%I); auto.
      destruct x; auto.
    - destruct x as [a|b], y as [a'|b']; auto; apply f_equivI, _.
  Qed.
(* iris/bi/internal_eq.v *)
Lemma option_equivI {A : ofe} (x y : option A) :
    x ≡ y ⊣⊢ match x, y with
             | Some a, Some a' => a ≡ a' | None, None => True | _, _ => False
             end.
Proof.
    apply (anti_symm _).
    - apply (internal_eq_rewrite' x y (λ y,
               match x, y with
               | Some a, Some a' => a ≡ a' | None, None => True | _, _ => False
               end)%I); auto.
      destruct x; auto.
    - destruct x as [a|], y as [a'|]; auto. apply f_equivI, _.
  Qed.
(* iris/bi/internal_eq.v *)
Lemma csum_equivI {A B : ofe} (sx sy : csum A B) :
    sx ≡ sy ⊣⊢ match sx, sy with
               | Cinl x, Cinl y => x ≡ y
               | Cinr x, Cinr y => x ≡ y
               | CsumInvalid, CsumInvalid => True
               | _, _ => False
               end.
Proof.
    apply (anti_symm _).
    - apply (internal_eq_rewrite' sx sy (λ sy',
               match sx, sy' with
               | Cinl x, Cinl y => x ≡ y
               | Cinr x, Cinr y => x ≡ y
               | CsumInvalid, CsumInvalid => True
               | _, _ => False
               end)%I); [solve_proper|auto|].
      destruct sx; eauto.
    - destruct sx; destruct sy; eauto;
      apply f_equivI, _.
  Qed.
(* iris/bi/internal_eq.v *)
Lemma excl_equivI {O : ofe} (x y : excl O) :
    x ≡ y ⊣⊢ match x, y with
             | Excl a, Excl b => a ≡ b
             | ExclInvalid, ExclInvalid => True
             | _, _ => False
             end.
Proof.
    apply (anti_symm _).
    - apply (internal_eq_rewrite' x y (λ y',
               match x, y' with
               | Excl a, Excl b => a ≡ b
               | ExclInvalid, ExclInvalid => True
               | _, _ => False
               end)%I); [solve_proper|auto|].
      destruct x; eauto.
    - destruct x as [e1|]; destruct y as [e2|]; [|by eauto..].
      apply f_equivI, _.
  Qed.
(* iris/bi/internal_eq.v *)
Lemma sig_equivI {A : ofe} (P : A → Prop) (x y : sig P) : `x ≡ `y ⊣⊢ x ≡ y.
Proof.
    apply (anti_symm _).
    - apply sig_equivI_1.
    - apply f_equivI, _.
  Qed.
(* iris/bi/internal_eq.v *)
Lemma sigT_equivI {A : Type} {P : A → ofe} (x y : sigT P) :
      x ≡ y ⊣⊢
      ∃ eq : projT1 x = projT1 y, rew eq in projT2 x ≡ projT2 y.
Proof.
      apply (anti_symm _).
      - apply (internal_eq_rewrite' x y (λ y,
                 ∃ eq : projT1 x = projT1 y, rew eq in projT2 x ≡ projT2 y))%I.
        + move => n [a pa] [b pb] [/=]; intros -> => /= Hab.
          apply bi.exist_ne => ?. by rewrite Hab.
        + done.
        + rewrite -(bi.exist_intro eq_refl) /=. auto.
      - apply bi.exist_elim. move: x y => [a pa] [b pb] /=. intros ->; simpl.
        apply (f_equivI _).
    Qed.
(* iris/bi/internal_eq.v *)
Lemma discrete_fun_equivI {A} {B : A → ofe} (f g : discrete_fun B) :
    f ≡ g ⊣⊢ ∀ x, f x ≡ g x.
Proof.
    apply (anti_symm _); auto using fun_extI.
    apply (internal_eq_rewrite' f g (λ g, ∀ x : A, f x ≡ g x)%I); auto.
  Qed.
(* iris/bi/internal_eq.v *)
Lemma ofe_morO_equivI {A B : ofe} (f g : A -n> B) : f ≡ g ⊣⊢ ∀ x, f x ≡ g x.
Proof.
    apply (anti_symm _).
    - apply (internal_eq_rewrite' f g (λ g, ∀ x : A, f x ≡ g x)%I); auto.
    - rewrite -(discrete_fun_equivI (ofe_mor_car _ _ f) (ofe_mor_car _ _ g)).
      set (h1 (f : A -n> B) :=
        exist (λ f : A -d> B, NonExpansive (f : A → B)) f (ofe_mor_ne A B f)).
      set (h2 (f : sigO (λ f : A -d> B, NonExpansive (f : A → B))) :=
        @OfeMor _ A B (`f) (proj2_sig f)).
      assert (∀ f, h2 (h1 f) = f) as Hh by (by intros []).
      assert (NonExpansive h2) by (intros ??? EQ; apply EQ).
      by rewrite -{2}[f]Hh -{2}[g]Hh -f_equivI -sig_equivI.
  Qed.
(* iris/bi/internal_eq.v *)
(* Modalities *)
Lemma absorbingly_internal_eq {A : ofe} (x y : A) : <absorb> (x ≡ y) ⊣⊢ x ≡ y.
Proof. apply absorbingly_si_pure. Qed.
(* iris/bi/internal_eq.v *)
Lemma persistently_internal_eq {A : ofe} (a b : A) : <pers> (a ≡ b) ⊣⊢ a ≡ b.
Proof. apply persistently_si_pure. Qed.
(* iris/bi/internal_eq.v *)
Instance internal_eq_absorbing {A : ofe} (x y : A) :
    Absorbing (PROP:=PROP) (x ≡ y).
Proof. by rewrite /Absorbing absorbingly_internal_eq. Qed.
(* iris/bi/internal_eq.v *)
Instance internal_eq_persistent {A : ofe} (a b : A) :
    Persistent (PROP:=PROP) (a ≡ b).
Proof. by intros; rewrite /Persistent persistently_internal_eq. Qed.
(* iris/bi/internal_eq.v *)
(* Equality under a later. *)
Lemma later_equivI_1 {A : ofe} (x y : A) : Next x ≡ Next y ⊢@{PROP} ▷ (x ≡ y).
Proof.
    rewrite /internal_eq -si_pure_later.
    by apply si_pure_mono, siProp_primitive.later_equivI_1.
  Qed.
(* iris/bi/internal_eq.v *)
Lemma later_equivI_2 {A : ofe} (x y : A) : ▷ (x ≡ y) ⊢@{PROP} Next x ≡ Next y.
Proof.
    rewrite /internal_eq -si_pure_later.
    by apply si_pure_mono, siProp_primitive.later_equivI_2.
  Qed.
(* iris/bi/internal_eq.v *)
Lemma later_equivI {A : ofe} (x y : A) : Next x ≡ Next y ⊣⊢ ▷ (x ≡ y).
Proof. apply (anti_symm _); auto using later_equivI_1, later_equivI_2. Qed.
(* iris/bi/internal_eq.v *)
Lemma f_equivI_contractive {A B : ofe} (f : A → B) `{Hf : !Contractive f} x y :
    ▷ (x ≡ y) ⊢ f x ≡ f y.
Proof.
    rewrite later_equivI_2. move: Hf=>/contractive_alt [g [? Hfg]].
    rewrite !Hfg. by apply f_equivI.
  Qed.
(* iris/bi/internal_eq.v *)
Lemma internal_eq_rewrite_contractive {A : ofe} a b (Ψ : A → PROP) :
    Contractive Ψ →
    ▷ (a ≡ b) ⊢ Ψ a → Ψ b.
Proof.
    intros. rewrite f_equivI_contractive.
    apply (internal_eq_rewrite (Ψ a) (Ψ b) id _).
  Qed.
(* iris/bi/internal_eq.v *)
Lemma internal_eq_rewrite_contractive' {A : ofe} a b (Ψ : A → PROP) P :
    Contractive Ψ →
    (P ⊢ ▷ (a ≡ b)) → (P ⊢ Ψ a) → P ⊢ Ψ b.
Proof.
    intros HΨ Heq HΨa. rewrite -(idemp bi_and P) {1}Heq HΨa.
    apply bi.impl_elim_l'. by apply internal_eq_rewrite_contractive.
  Qed.
(* iris/bi/internal_eq.v *)
Instance eq_timeless {A : ofe} (a b : A) :
    TCOr (Discrete a) (Discrete b) →
    Timeless (PROP:=PROP) (a ≡ b).
Proof. intros. rewrite /Discrete !discrete_eq. apply (timeless _). Qed.
(* iris/bi/internal_eq.v *)
(* Equality of propositions *)
Lemma internal_eq_iff P Q : P ≡ Q ⊢ P ↔ Q.
Proof.
    apply (internal_eq_rewrite' P Q (λ Q, P ↔ Q))%I; auto using bi.iff_refl.
  Qed.
(* iris/bi/internal_eq.v *)
Lemma affinely_internal_eq_wand_iff P Q : <affine> (P ≡ Q) ⊢ P ∗-∗ Q.
Proof.
    apply (internal_eq_rewrite' P Q (λ Q, P ∗-∗ Q))%I; auto.
    - by rewrite bi.affinely_elim.
    - rewrite bi.affinely_elim_emp. apply bi.wand_iff_refl.
  Qed.
(* iris/bi/internal_eq.v *)
Lemma internal_eq_wand_iff P Q : P ≡ Q ⊢ <absorb> (P ∗-∗ Q).
Proof.
    rewrite -(bi.persistent_absorbingly_affinely (P ≡ Q)).
    by rewrite affinely_internal_eq_wand_iff.
  Qed.
(* iris/bi/internal_eq.v *)
Lemma si_pure_internal_eq {A : ofe} (x y : A) : <si_pure> (x ≡ y) ⊣⊢ x ≡ y.
Proof. done. Qed.
(* iris/bi/internal_eq.v *)
Lemma prop_ext_si_emp_valid P Q : P ≡ Q ⊣⊢@{siPropI} <si_emp_valid> (P ∗-∗ Q).
Proof.
    apply (anti_symm _); [|apply prop_ext_si_emp_valid_2].
    rewrite -(@si_pure_entails PROP) si_pure_internal_eq.
    apply (internal_eq_rewrite' P Q
      (λ Q, <si_pure> <si_emp_valid> (P ∗-∗ Q)))%I; auto.
    rewrite -bi.wand_iff_refl si_emp_valid_emp si_pure_pure. auto.
  Qed.
(* iris/bi/internal_eq.v *)
Lemma later_equivI_prop_2 P Q : ▷ (P ≡ Q) ⊢ (▷ P) ≡ (▷ Q).
Proof.
    rewrite -!si_pure_internal_eq -si_pure_later !prop_ext_si_emp_valid.
    by rewrite -si_emp_valid_later bi.later_wand_iff.
  Qed.
(* iris/bi/internal_eq.v *)
Lemma internal_eq_soundness {A : ofe} (x y : A) : (⊢@{PROP} x ≡ y) → x ≡ y.
Proof.
    intros ?%si_pure_emp_valid. by apply siProp_primitive.internal_eq_soundness.
  Qed.
(* iris/bi/internal_eq.v *)
(* Derive [NonExpansive]/[Contractive] from an internal statement *)
Lemma internal_eq_entails {A B : ofe} (a1 a2 : A) (b1 b2 : B) :
    (a1 ≡ a2 ⊢ b1 ≡ b2) ↔ (∀ n, a1 ≡{n}≡ a2 → b1 ≡{n}≡ b2).
Proof. rewrite si_pure_entails. apply siProp_primitive.internal_eq_entails. Qed.
(* iris/bi/internal_eq.v *)
Lemma ne_internal_eq {A B : ofe} (f : A → B) :
    NonExpansive f ↔ ∀ x1 x2, x1 ≡ x2 ⊢ f x1 ≡ f x2.
Proof.
    split; [apply f_equivI|]. intros Hf n x1 x2. by apply internal_eq_entails.
  Qed.
(* iris/bi/internal_eq.v *)
Lemma ne_2_internal_eq {A B C : ofe} (f : A → B → C) :
    NonExpansive2 f ↔ ∀ x1 x2 y1 y2, x1 ≡ x2 ∧ y1 ≡ y2 ⊢ f x1 y1 ≡ f x2 y2.
Proof.
    split.
    - intros Hf x1 x2 y1 y2.
      change ((x1,y1).1 ≡ (x2,y2).1 ∧ (x1,y1).2 ≡ (x2,y2).2
        ⊢ uncurry f (x1,y1) ≡ uncurry f (x2,y2)).
      rewrite -prod_equivI. apply ne_internal_eq. solve_proper.
    - intros Hf n x1 x2 Hx y1 y2 Hy.
      change (uncurry f (x1,y1) ≡{n}≡ uncurry f (x2,y2)).
      apply ne_internal_eq; [|done].
      intros [??] [??]. rewrite prod_equivI. apply Hf.
  Qed.
(* iris/bi/internal_eq.v *)
Lemma contractive_internal_eq {A B : ofe} (f : A → B) :
    Contractive f ↔ ∀ x1 x2, ▷ (x1 ≡ x2) ⊢ f x1 ≡ f x2.
Proof.
    split; [apply f_equivI_contractive|].
    intros Hf n x1 x2 Hx. specialize (Hf x1 x2).
    rewrite -later_equivI internal_eq_entails in Hf. apply Hf. by f_contractive.
  Qed.
(* iris/bi/internal_eq.v *)
Instance sbi_later_contractive : BiLaterContractive PROP.
Proof using Type*.
    rewrite /BiLaterContractive.
    apply contractive_internal_eq, later_equivI_prop_2.
  Qed.
(* iris/bi/monpred.v *)
(* Definitions. *)
Structure biIndex
:=
  BiIndex
    { bi_index_type :> Type;
      bi_index_inhabited : Inhabited bi_index_type;
      bi_index_rel : SqSubsetEq bi_index_type;
      bi_index_rel_preorder : PreOrder (⊑@{bi_index_type}) }.
(* iris/bi/monpred.v *)
(* We may want to instantiate monPred with the reflexivity relation in
   the case where there is no relevant order. In that case, there is
   no bottom element, so that we do not want to force any BI index to
   have one. *)
Class BiIndexBottom {I : biIndex} (bot : I)
:=
  bi_index_bot i : bot ⊑ i.
(* iris/bi/monpred.v *)
Record monPred
:=
    MonPred { monPred_at :> I → PROP;
              monPred_mono : Proper ((⊑) ==> (⊢)) monPred_at }.
(* iris/bi/monpred.v *)
Inductive monPred_equiv' P Q : Prop
:=
      { monPred_in_equiv i : P i ≡ Q i } .
(* iris/bi/monpred.v *)
Instance monPred_equiv : Equiv monPred
:= monPred_equiv'.
(* iris/bi/monpred.v *)
Inductive monPred_dist' (n : nat) (P Q : monPred) : Prop
:=
      { monPred_in_dist i : P i ≡{n}≡ Q i }.
(* iris/bi/monpred.v *)
Instance monPred_dist : Dist monPred
:= monPred_dist'.
(* iris/bi/monpred.v *)
Definition monPred_sig P : { f : I -d> PROP | Proper ((⊑) ==> (⊢)) f }
:=
      exist _ (monPred_at P) (monPred_mono P).
(* iris/bi/monpred.v *)
Definition sig_monPred (P' : { f : I -d> PROP | Proper ((⊑) ==> (⊢)) f })
      : monPred
:=
      MonPred (proj1_sig P') (proj2_sig P').
(* iris/bi/monpred.v *)
(* These two lemma use the wrong Equiv and Dist instance for
      monPred. so we make sure they are not accessible outside of the
      section by using Let. *)
Let monPred_sig_equiv:
      ∀ P Q, P ≡ Q ↔ monPred_sig P ≡ monPred_sig Q.
Proof. by split; [intros []|]. Defined.
(* iris/bi/monpred.v *)
Let monPred_sig_dist:
      ∀ n, ∀ P Q : monPred, P ≡{n}≡ Q ↔ monPred_sig P ≡{n}≡ monPred_sig Q.
Proof. by split; [intros []|]. Defined.
(* iris/bi/monpred.v *)
Definition monPred_ofe_mixin : OfeMixin monPred.
Proof.
      by apply (iso_ofe_mixin monPred_sig monPred_sig_equiv monPred_sig_dist).
    Qed.
(* iris/bi/monpred.v *)
Canonical monPredO
:= Ofe monPred monPred_ofe_mixin.
(* iris/bi/monpred.v *)
Instance monPred_cofe `{!Cofe PROP} : Cofe monPredO.
Proof.
      refine ((iso_cofe_subtype' (A:=I-d>PROP) _ MonPred monPred_at _ _ _) _);
        [done..|].
      apply limit_preserving_forall=> y. apply limit_preserving_forall=> x.
      apply limit_preserving_impl; [solve_proper|].
      apply bi.limit_preserving_entails; solve_proper.
    Qed.
(* iris/bi/monpred.v *)
Lemma monPred_sig_monPred (P' : { f : I -d> PROP | Proper ((⊑) ==> (⊢)) f }) :
    monPred_sig (sig_monPred P') ≡ P'.
Proof. by change (P' ≡ P'). Qed.
(* iris/bi/monpred.v *)
Lemma sig_monPred_sig P : sig_monPred (monPred_sig P) ≡ P.
Proof. done. Qed.
(* iris/bi/monpred.v *)
Instance monPred_sig_ne : NonExpansive monPred_sig.
Proof. move=> ??? [?] ? //=. Qed.
(* iris/bi/monpred.v *)
Instance monPred_sig_proper : Proper ((≡) ==> (≡)) monPred_sig.
Proof. eapply (ne_proper _). Qed.
(* iris/bi/monpred.v *)
Instance sig_monPred_ne : NonExpansive (@sig_monPred).
Proof. split=>? //=. Qed.
(* iris/bi/monpred.v *)
Instance sig_monPred_proper : Proper ((≡) ==> (≡)) sig_monPred.
Proof. eapply (ne_proper _). Qed.
(* iris/bi/monpred.v *)
(* We generalize over the relation R which is morally the equivalence
     relation over B. That way, the BI index can use equality as an
     equivalence relation (and Coq is able to infer the Proper and
     Reflexive instances properly), or any other equivalence relation,
     provided it is compatible with (⊑). *)
Instance monPred_at_ne (R : relation I) :
    Proper (R ==> R ==> iff) (⊑) → Reflexive R →
    ∀ n, Proper (dist n ==> R ==> dist n) monPred_at.
Proof.
    intros ????? [Hd] ?? HR. rewrite Hd.
    apply equiv_dist, bi.equiv_entails; split; f_equiv; rewrite ->HR; done.
  Qed.
(* iris/bi/monpred.v *)
Instance monPred_at_proper (R : relation I) :
    Proper (R ==> R ==> iff) (⊑) → Reflexive R →
    Proper ((≡) ==> R ==> (≡)) monPred_at.
Proof. repeat intro. apply equiv_dist=>?. f_equiv=>//. by apply equiv_dist. Qed.
(* iris/bi/monpred.v *)
Notation monPred
:= (monPred I PROP).
(* iris/bi/monpred.v *)
Inductive monPred_entails (P1 P2 : monPred) : Prop
:=
    { monPred_in_entails i : P1 i ⊢ P2 i }.
(* iris/bi/monpred.v *)
Definition monPred_upclosed (Φ : I → PROP) : monPred :=
    MonPred (λ i, (∀ j, ⌜i ⊑ j⌝ → Φ j)%I) _.
Next Obligation. solve_proper. Qed.
(* iris/bi/monpred.v *)
Definition monPred_embed_def : Embed PROP monPred
:= λ (P : PROP),
    MonPred (λ _, P) _.
(* iris/bi/monpred.v *)
Definition monPred_embed_aux : seal (@monPred_embed_def).
Proof. by eexists. Qed.
(* iris/bi/monpred.v *)
Definition monPred_embed
:= monPred_embed_aux.(unseal).
(* iris/bi/monpred.v *)
Definition monPred_embed_unseal :
    @embed _ _ monPred_embed = _
:= monPred_embed_aux.(seal_eq).
(* iris/bi/monpred.v *)
Definition monPred_emp_def : monPred
:= MonPred (λ _, emp)%I _.
(* iris/bi/monpred.v *)
Definition monPred_emp_aux : seal (@monPred_emp_def).
Proof. by eexists. Qed.
(* iris/bi/monpred.v *)
Definition monPred_emp
:= monPred_emp_aux.(unseal).
(* iris/bi/monpred.v *)
Definition monPred_emp_unseal :
    @monPred_emp = _
:= monPred_emp_aux.(seal_eq).
(* iris/bi/monpred.v *)
Definition monPred_pure_def (φ : Prop) : monPred
:= MonPred (λ _, ⌜φ⌝)%I _.
(* iris/bi/monpred.v *)
Definition monPred_pure_aux : seal (@monPred_pure_def).
Proof. by eexists. Qed.
(* iris/bi/monpred.v *)
Definition monPred_pure
:= monPred_pure_aux.(unseal).
(* iris/bi/monpred.v *)
Definition monPred_pure_unseal :
    @monPred_pure = _
:= monPred_pure_aux.(seal_eq).
(* iris/bi/monpred.v *)
Definition monPred_objectively_def P : monPred
:=
    MonPred (λ _, ∀ i, P i)%I _.
(* iris/bi/monpred.v *)
Definition monPred_objectively_aux : seal (@monPred_objectively_def).
Proof. by eexists. Qed.
(* iris/bi/monpred.v *)
Definition monPred_objectively
:= monPred_objectively_aux.(unseal).
(* iris/bi/monpred.v *)
Definition monPred_objectively_unseal :
    @monPred_objectively = _
:= monPred_objectively_aux.(seal_eq).
(* iris/bi/monpred.v *)
Definition monPred_subjectively_def P : monPred
:= MonPred (λ _, ∃ i, P i)%I _.
(* iris/bi/monpred.v *)
Definition monPred_subjectively_aux : seal (@monPred_subjectively_def).
Proof. by eexists. Qed.
(* iris/bi/monpred.v *)
Definition monPred_subjectively
:= monPred_subjectively_aux.(unseal).
(* iris/bi/monpred.v *)
Definition monPred_subjectively_unseal :
    @monPred_subjectively = _
:= monPred_subjectively_aux.(seal_eq).
(* iris/bi/monpred.v *)
Definition monPred_and_def P Q : monPred :=
    MonPred (λ i, P i ∧ Q i)%I _.
Next Obligation. solve_proper. Qed.
(* iris/bi/monpred.v *)
Definition monPred_and_aux : seal (@monPred_and_def).
Proof. by eexists. Qed.
(* iris/bi/monpred.v *)
Definition monPred_and
:= monPred_and_aux.(unseal).
(* iris/bi/monpred.v *)
Definition monPred_and_unseal :
    @monPred_and = _
:= monPred_and_aux.(seal_eq).
(* iris/bi/monpred.v *)
Definition monPred_or_def P Q : monPred :=
    MonPred (λ i, P i ∨ Q i)%I _.
Next Obligation. solve_proper. Qed.
(* iris/bi/monpred.v *)
Definition monPred_or_aux : seal (@monPred_or_def).
Proof. by eexists. Qed.
(* iris/bi/monpred.v *)
Definition monPred_or
:= monPred_or_aux.(unseal).
(* iris/bi/monpred.v *)
Definition monPred_or_unseal :
    @monPred_or = _
:= monPred_or_aux.(seal_eq).
(* iris/bi/monpred.v *)
Definition monPred_impl_def P Q : monPred
:=
    monPred_upclosed (λ i, P i → Q i)%I.
(* iris/bi/monpred.v *)
Definition monPred_impl_aux : seal (@monPred_impl_def).
Proof. by eexists. Qed.
(* iris/bi/monpred.v *)
Definition monPred_impl
:= monPred_impl_aux.(unseal).
(* iris/bi/monpred.v *)
Definition monPred_impl_unseal :
    @monPred_impl = _
:= monPred_impl_aux.(seal_eq).
(* iris/bi/monpred.v *)
Definition monPred_forall_def A (Φ : A → monPred) : monPred :=
    MonPred (λ i, ∀ x : A, Φ x i)%I _.
Next Obligation. solve_proper. Qed.
(* iris/bi/monpred.v *)
Definition monPred_forall_aux : seal (@monPred_forall_def).
Proof. by eexists. Qed.
(* iris/bi/monpred.v *)
Definition monPred_forall
:= monPred_forall_aux.(unseal).
(* iris/bi/monpred.v *)
Definition monPred_forall_unseal :
    @monPred_forall = _
:= monPred_forall_aux.(seal_eq).
(* iris/bi/monpred.v *)
Definition monPred_exist_def A (Φ : A → monPred) : monPred :=
    MonPred (λ i, ∃ x : A, Φ x i)%I _.
Next Obligation. solve_proper. Qed.
(* iris/bi/monpred.v *)
Definition monPred_exist_aux : seal (@monPred_exist_def).
Proof. by eexists. Qed.
(* iris/bi/monpred.v *)
Definition monPred_exist
:= monPred_exist_aux.(unseal).
(* iris/bi/monpred.v *)
Definition monPred_exist_unseal :
    @monPred_exist = _
:= monPred_exist_aux.(seal_eq).
(* iris/bi/monpred.v *)
Definition monPred_sep_def P Q : monPred :=
    MonPred (λ i, P i ∗ Q i)%I _.
Next Obligation. solve_proper. Qed.
(* iris/bi/monpred.v *)
Definition monPred_sep_aux : seal (@monPred_sep_def).
Proof. by eexists. Qed.
(* iris/bi/monpred.v *)
Definition monPred_sep
:= monPred_sep_aux.(unseal).
(* iris/bi/monpred.v *)
Definition monPred_sep_unseal :
    @monPred_sep = _
:= monPred_sep_aux.(seal_eq).
(* iris/bi/monpred.v *)
Definition monPred_wand_def P Q : monPred
:=
    monPred_upclosed (λ i, P i -∗ Q i)%I.
(* iris/bi/monpred.v *)
Definition monPred_wand_aux : seal (@monPred_wand_def).
Proof. by eexists. Qed.
(* iris/bi/monpred.v *)
Definition monPred_wand
:= monPred_wand_aux.(unseal).
(* iris/bi/monpred.v *)
Definition monPred_wand_unseal :
    @monPred_wand = _
:= monPred_wand_aux.(seal_eq).
(* iris/bi/monpred.v *)
Definition monPred_persistently_def P : monPred :=
    MonPred (λ i, <pers> (P i))%I _.
Next Obligation. solve_proper. Qed.
(* iris/bi/monpred.v *)
Definition monPred_persistently_aux : seal (@monPred_persistently_def).
Proof. by eexists. Qed.
(* iris/bi/monpred.v *)
Definition monPred_persistently
:= monPred_persistently_aux.(unseal).
(* iris/bi/monpred.v *)
Definition monPred_persistently_unseal :
    @monPred_persistently = _
:= monPred_persistently_aux.(seal_eq).
(* iris/bi/monpred.v *)
Definition monPred_in_def (i0 : I) : monPred :=
    MonPred (λ i : I, ⌜i0 ⊑ i⌝%I) _.
Next Obligation. solve_proper. Qed.
(* iris/bi/monpred.v *)
Definition monPred_in_aux : seal (@monPred_in_def).
Proof. by eexists. Qed.
(* iris/bi/monpred.v *)
Definition monPred_in
:= monPred_in_aux.(unseal).
(* iris/bi/monpred.v *)
Definition monPred_in_unseal :
    @monPred_in = _
:= monPred_in_aux.(seal_eq).
(* iris/bi/monpred.v *)
Definition monPred_later_def P : monPred := MonPred (λ i, ▷ (P i))%I _.
Next Obligation. solve_proper. Qed.
(* iris/bi/monpred.v *)
Definition monPred_later_aux : seal monPred_later_def.
Proof. by eexists. Qed.
(* iris/bi/monpred.v *)
Definition monPred_later
:= monPred_later_aux.(unseal).
(* iris/bi/monpred.v *)
Definition monPred_later_unseal :
    monPred_later = _
:= monPred_later_aux.(seal_eq).
(* iris/bi/monpred.v *)
Definition monPred_bupd_def `{BiBUpd PROP}
    (P : monPred) : monPred := MonPred (λ i, |==> P i)%I _.
Next Obligation. solve_proper. Qed.
(* iris/bi/monpred.v *)
Definition monPred_bupd_aux : seal (@monPred_bupd_def).
Proof. by eexists. Qed.
(* iris/bi/monpred.v *)
Definition monPred_bupd
:= monPred_bupd_aux.(unseal).
(* iris/bi/monpred.v *)
Definition monPred_bupd_unseal `{BiBUpd PROP} :
    @bupd _ monPred_bupd = monPred_bupd_def.
Proof. by rewrite -monPred_bupd_aux.(seal_eq). Qed.
(* iris/bi/monpred.v *)
Definition monPred_fupd_def `{BiFUpd PROP} (E1 E2 : coPset)
    (P : monPred) : monPred := MonPred (λ i, |={E1,E2}=> P i)%I _.
Next Obligation. solve_proper. Qed.
(* iris/bi/monpred.v *)
Definition monPred_fupd_aux : seal (@monPred_fupd_def).
Proof. by eexists. Qed.
(* iris/bi/monpred.v *)
Definition monPred_fupd
:= monPred_fupd_aux.(unseal).