phanerozoic/Coq-Iris huggingface dataset:
(* iris/bi/monpred.v *)
Definition monPred_fupd_unseal `{BiFUpd PROP} :
    @fupd _ monPred_fupd = monPred_fupd_def.
Proof. by rewrite -monPred_fupd_aux.(seal_eq). Qed.
(* iris/bi/monpred.v *)
Definition monPred_si_pure_def `{Sbi PROP} (Pi : siProp) : monPred
:=
    MonPred (λ _, <si_pure> Pi)%I _.
(* iris/bi/monpred.v *)
Definition monPred_si_pure_aux : seal (@monPred_si_pure_def).
Proof. by eexists. Qed.
(* iris/bi/monpred.v *)
Definition monPred_si_pure
:= monPred_si_pure_aux.(unseal).
(* iris/bi/monpred.v *)
Definition monPred_si_pure_unseal `{Sbi PROP} :
    @si_pure _ monPred_si_pure = monPred_si_pure_def.
Proof. by rewrite -monPred_si_pure_aux.(seal_eq). Qed.
(* iris/bi/monpred.v *)
Definition monPred_si_emp_valid_def `{!Sbi PROP} P : siProp
:=
    <si_emp_valid> ∀ i, P i.
(* iris/bi/monpred.v *)
Definition monPred_si_emp_valid_aux : seal (@monPred_si_emp_valid_def).
Proof. by eexists. Qed.
(* iris/bi/monpred.v *)
Definition monPred_si_emp_valid
:= monPred_si_emp_valid_aux.(unseal).
(* iris/bi/monpred.v *)
Definition monPred_si_emp_valid_unseal `{!Sbi PROP} :
    @si_emp_valid _ monPred_si_emp_valid = monPred_si_emp_valid_def.
Proof. by rewrite -monPred_si_emp_valid_aux.(seal_eq). Qed.
(* iris/bi/monpred.v *)
(* This is not the final collection of unsealing lemmas, below we redefine
[monPred_unseal] to also unfold the BI layer (i.e., the projections of the BI
structures/classes). *)
Definition monPred_unseal
:=
  (@monPred_embed_unseal, @monPred_emp_unseal, @monPred_pure_unseal,
   @monPred_objectively_unseal, @monPred_subjectively_unseal,
   @monPred_and_unseal, @monPred_or_unseal, @monPred_impl_unseal,
   @monPred_forall_unseal, @monPred_exist_unseal, @monPred_sep_unseal,
   @monPred_wand_unseal, @monPred_persistently_unseal,
   @monPred_in_unseal, @monPred_later_unseal).
(* iris/bi/monpred.v *)
Notation "'<obj>' P"
:= (monPred_objectively P) : bi_scope.
(* iris/bi/monpred.v *)
Notation "'<subj>' P"
:= (monPred_subjectively P) : bi_scope.
(* iris/bi/monpred.v *)
Lemma monPred_bi_mixin : BiMixin (PROP:=monPred I PROP)
    monPred_entails monPred_emp monPred_pure monPred_and monPred_or
    monPred_impl monPred_forall monPred_exist monPred_sep monPred_wand.
Proof.
    split; rewrite ?monPred_defs.monPred_unseal;
      try by (split=> ? /=; repeat f_equiv).
    - split.
      + intros P. by split.
      + intros P Q R [H1] [H2]. split => ?. by rewrite H1 H2.
    - split.
      + intros [HPQ]. split; split => i; move: (HPQ i); by apply bi.equiv_entails.
      + intros [[] []]. split=>i. by apply bi.equiv_entails.
    - intros P φ ?. split=> i. by apply bi.pure_intro.
    - intros φ P HP. split=> i. apply bi.pure_elim'=> ?. by apply HP.
    - intros P Q. split=> i. by apply bi.and_elim_l.
    - intros P Q. split=> i. by apply bi.and_elim_r.
    - intros P Q R [?] [?]. split=> i. by apply bi.and_intro.
    - intros P Q. split=> i. by apply bi.or_intro_l.
    - intros P Q. split=> i. by apply bi.or_intro_r.
    - intros P Q R [?] [?]. split=> i. by apply bi.or_elim.
    - intros P Q R [HR]. split=> i /=. setoid_rewrite bi.pure_impl_forall.
      apply bi.forall_intro=> j. apply bi.forall_intro=> Hij.
      apply bi.impl_intro_r. by rewrite -HR /= !Hij.
    - intros P Q R [HR]. split=> i /=.
      rewrite HR /= bi.forall_elim bi.pure_impl_forall bi.forall_elim //.
      apply bi.impl_elim_l.
    - intros A P Ψ HΨ. split=> i. apply bi.forall_intro => ?. by apply HΨ.
    - intros A Ψ. split=> i. by apply: bi.forall_elim.
    - intros A Ψ a. split=> i. by rewrite /= -bi.exist_intro.
    - intros A Ψ Q HΨ. split=> i. apply bi.exist_elim => a. by apply HΨ.
    - intros P P' Q Q' [?] [?]. split=> i. by apply bi.sep_mono.
    - intros P. split=> i. by apply bi.emp_sep_1.
    - intros P. split=> i. by apply bi.emp_sep_2.
    - intros P Q. split=> i. by apply bi.sep_comm'.
    - intros P Q R. split=> i. by apply bi.sep_assoc'.
    - intros P Q R [HR]. split=> i /=. setoid_rewrite bi.pure_impl_forall.
      apply bi.forall_intro=> j. apply bi.forall_intro=> Hij.
      apply bi.wand_intro_r. by rewrite -HR /= !Hij.
    - intros P Q R [HP]. split=> i. apply bi.wand_elim_l'.
      rewrite HP /= bi.forall_elim bi.pure_impl_forall bi.forall_elim //.
  Qed.
(* iris/bi/monpred.v *)
Lemma monPred_bi_persistently_mixin :
    BiPersistentlyMixin (PROP:=monPred I PROP)
      monPred_entails monPred_emp monPred_and
      monPred_exist monPred_sep monPred_persistently.
Proof.
    split; rewrite ?monPred_defs.monPred_unseal;
      try by (split=> ? /=; repeat f_equiv).
    - intros P Q [?]. split=> i /=. by f_equiv.
    - intros P. split=> i. by apply bi.persistently_idemp_2.
    - split=> i. by apply bi.persistently_emp_intro.
    - intros A Ψ. split=> i. by apply bi.persistently_and_2.
    - intros A Ψ. split=> i. by apply bi.persistently_exist_1.
    - intros P Q. split=> i. apply bi.sep_elim_l, _.
    - intros P Q. split=> i. by apply bi.persistently_and_sep_elim.
  Qed.
(* iris/bi/monpred.v *)
Lemma monPred_bi_later_mixin :
    BiLaterMixin (PROP:=monPred I PROP)
      monPred_entails monPred_pure
      monPred_or monPred_impl monPred_forall monPred_exist
      monPred_sep monPred_persistently monPred_later.
Proof.
    split; rewrite ?monPred_defs.monPred_unseal.
    - by split=> ? /=; repeat f_equiv.
    - intros P Q [?]. split=> i. by apply bi.later_mono.
    - intros P. split=> i /=. by apply bi.later_intro.
    - intros A Ψ. split=> i. by apply bi.later_forall_2.
    - intros A Ψ. split=> i. by apply bi.later_exist_false.
    - intros P Q. split=> i. by apply bi.later_sep_1.
    - intros P Q. split=> i. by apply bi.later_sep_2.
    - intros P. split=> i. by apply bi.later_persistently_1.
    - intros P. split=> i. by apply bi.later_persistently_2.
    - intros P. split=> i /=. rewrite -bi.forall_intro.
      + apply bi.later_false_em.
      + intros j. rewrite bi.pure_impl_forall. apply bi.forall_intro=> Hij.
        by rewrite Hij.
  Qed.
(* iris/bi/monpred.v *)
Canonical monPredI : bi
:=
    {| bi_ofe_mixin := monPred_ofe_mixin;
       bi_bi_mixin := monPred_bi_mixin;
       bi_bi_persistently_mixin := monPred_bi_persistently_mixin;
       bi_bi_later_mixin := monPred_bi_later_mixin |}.
(* iris/bi/monpred.v *)
(* We restate the unsealing lemmas so that they also unfold the BI layer. The
  sealing lemmas are partially applied so that they also work under binders. *)
Lemma monPred_emp_unseal :
    bi_emp = @monPred_defs.monPred_emp_def I PROP.
Proof. by rewrite -monPred_defs.monPred_emp_unseal. Qed.
(* iris/bi/monpred.v *)
Lemma monPred_pure_unseal :
    bi_pure = @monPred_defs.monPred_pure_def I PROP.
Proof. by rewrite -monPred_defs.monPred_pure_unseal. Qed.
(* iris/bi/monpred.v *)
Lemma monPred_and_unseal :
    bi_and = @monPred_defs.monPred_and_def I PROP.
Proof. by rewrite -monPred_defs.monPred_and_unseal. Qed.
(* iris/bi/monpred.v *)
Lemma monPred_or_unseal :
    bi_or = @monPred_defs.monPred_or_def I PROP.
Proof. by rewrite -monPred_defs.monPred_or_unseal. Qed.
(* iris/bi/monpred.v *)
Lemma monPred_impl_unseal :
    bi_impl = @monPred_defs.monPred_impl_def I PROP.
Proof. by rewrite -monPred_defs.monPred_impl_unseal. Qed.
(* iris/bi/monpred.v *)
Lemma monPred_forall_unseal :
    @bi_forall _ = @monPred_defs.monPred_forall_def I PROP.
Proof. by rewrite -monPred_defs.monPred_forall_unseal. Qed.
(* iris/bi/monpred.v *)
Lemma monPred_exist_unseal :
    @bi_exist _ = @monPred_defs.monPred_exist_def I PROP.
Proof. by rewrite -monPred_defs.monPred_exist_unseal. Qed.
(* iris/bi/monpred.v *)
Lemma monPred_sep_unseal :
    bi_sep = @monPred_defs.monPred_sep_def I PROP.
Proof. by rewrite -monPred_defs.monPred_sep_unseal. Qed.
(* iris/bi/monpred.v *)
Lemma monPred_wand_unseal :
    bi_wand = @monPred_defs.monPred_wand_def I PROP.
Proof. by rewrite -monPred_defs.monPred_wand_unseal. Qed.
(* iris/bi/monpred.v *)
Lemma monPred_persistently_unseal :
    bi_persistently = @monPred_defs.monPred_persistently_def I PROP.
Proof. by rewrite -monPred_defs.monPred_persistently_unseal. Qed.
(* iris/bi/monpred.v *)
Lemma monPred_later_unseal :
    bi_later = @monPred_defs.monPred_later_def I PROP.
Proof. by rewrite -monPred_defs.monPred_later_unseal. Qed.
(* iris/bi/monpred.v *)
(* This definition only includes the unseal lemmas for the [bi] connectives.
  After we have defined the right class instances, we define [monPred_unseal],
  which also includes [embed], [internal_eq], [bupd], [fupd], [plainly],
  [monPred_objectively], [monPred_subjectively] and [monPred_in]. *)
Definition monPred_unseal_bi
:=
    (monPred_emp_unseal, monPred_pure_unseal, monPred_and_unseal,
    monPred_or_unseal, monPred_impl_unseal, monPred_forall_unseal,
    monPred_exist_unseal, monPred_sep_unseal, monPred_wand_unseal,
    monPred_persistently_unseal, monPred_later_unseal).
(* iris/bi/monpred.v *)
Definition monPred_embedding_mixin : BiEmbedMixin PROP monPredI monPred_embed.
Proof.
    split; try apply _; rewrite /bi_emp_valid
      !(monPred_defs.monPred_embed_unseal, monPred_unseal_bi); try done.
    - move=> P /= [/(_ inhabitant) ?] //.
    - intros P Q. split=> i /=.
      by rewrite bi.forall_elim bi.pure_impl_forall bi.forall_elim.
    - intros P Q. split=> i /=.
      by rewrite bi.forall_elim bi.pure_impl_forall bi.forall_elim.
  Qed.
(* iris/bi/monpred.v *)
Instance monPred_bi_embed : BiEmbed PROP monPredI
:=
    {| bi_embed_mixin := monPred_embedding_mixin |}.
(* iris/bi/monpred.v *)
Lemma monPred_sbi_mixin `{!Sbi PROP} :
    SbiMixin monPredI monPred_si_pure monPred_si_emp_valid.
Proof.
    split; rewrite /Absorbing /bi_affinely /bi_absorbingly
      !(monPred_defs.monPred_si_pure_unseal,
        monPred_defs.monPred_si_emp_valid_unseal, monPred_unseal_bi)
      /monPred_defs.monPred_si_emp_valid_def /=.
    - split=> i /=. solve_proper.
    - solve_proper.
    - intros Pi Qi HPQ. split=> i /=. by rewrite HPQ.
    - intros P Q [HPQ]. by setoid_rewrite HPQ.
    - intros Pi. apply (anti_symm _).
      + by rewrite (bi.forall_elim inhabitant) si_emp_valid_si_pure.
      + rewrite si_emp_valid_forall. apply bi.forall_intro=> _.
        by rewrite si_emp_valid_si_pure.
    - intros P. split=> i /=. by rewrite si_pure_si_emp_valid (bi.forall_elim i).
    - intros Pi Qi. split=> i /=. rewrite si_pure_impl.
      by rewrite (bi.forall_elim i) bi.pure_True // left_id.
    - intros A Φi. split=> i /=. apply si_pure_forall_2.
    - intros P Q. split=> i /=. rewrite (bi.forall_elim i).
      rewrite -si_pure_pure !persistently_impl_si_pure si_pure_pure.
      f_equiv. apply bi.forall_intro=> j.
      apply bi.impl_intro_l, bi.pure_elim_l=> ?. rewrite bi.pure_True // left_id.
      f_equiv. by apply monPred_mono.
    - intros Pi. split=> i /=. apply si_pure_later.
    - intros Pi. split=> i /=. by rewrite bi.sep_elim_r.
    - intros P. by rewrite -si_emp_valid_later_1 bi.later_forall.
    - intros P. rewrite !si_emp_valid_forall. f_equiv=> i.
      apply si_emp_valid_affinely_2.
  Qed.
(* iris/bi/monpred.v *)
Lemma monPred_sbi_prop_ext_mixin `{!Sbi PROP} :
    SbiPropExtMixin monPredI monPred_si_emp_valid.
Proof.
    apply sbi_prop_ext_mixin=> P Q.
    rewrite /bi_wand_iff
      !(monPred_defs.monPred_si_emp_valid_unseal, monPred_unseal_bi)
      /monPred_defs.monPred_si_emp_valid_def /=.
    rewrite -{3}(sig_monPred_sig P) -{3}(sig_monPred_sig Q)
      -f_equivI -sig_equivI !discrete_fun_equivI /=.
    apply bi.forall_intro=> j. rewrite prop_ext_si_emp_valid.
    by rewrite !(bi.forall_elim j) !bi.pure_True // !bi.True_impl.
  Qed.
(* iris/bi/monpred.v *)
Instance monPred_sbi `{!Sbi PROP} : Sbi monPredI
:=
    {| sbi_sbi_mixin := monPred_sbi_mixin;
       sbi_sbi_prop_ext_mixin := monPred_sbi_prop_ext_mixin |}.
(* iris/bi/monpred.v *)
Lemma monPred_bupd_mixin `{BiBUpd PROP} : BiBUpdMixin monPredI monPred_bupd.
Proof.
    split; rewrite !(monPred_defs.monPred_bupd_unseal, monPred_unseal_bi).
    - split=>/= i. solve_proper.
    - intros P. split=>/= i. apply bupd_intro.
    - intros P Q [HPQ]. split=>/= i. by rewrite HPQ.
    - intros P. split=>/= i. apply bupd_trans.
    - intros P Q. split=>/= i. apply bupd_frame_r.
  Qed.
(* iris/bi/monpred.v *)
Instance monPred_bi_bupd `{BiBUpd PROP} : BiBUpd monPredI
:=
    {| bi_bupd_mixin := monPred_bupd_mixin |}.
(* iris/bi/monpred.v *)
Lemma monPred_fupd_mixin `{BiFUpd PROP} : BiFUpdMixin monPredI monPred_fupd.
Proof.
    split; rewrite /bi_emp_valid /bi_except_0
      !(monPred_defs.monPred_fupd_unseal, monPred_unseal_bi).
    - split=>/= i. solve_proper.
    - intros E1 E2 HE12. split=>/= i. by apply fupd_mask_intro_subseteq.
    - intros E1 E2 P. split=>/= i. apply except_0_fupd.
    - intros E1 E2 P Q [HPQ]. split=>/= i. by rewrite HPQ.
    - intros E1 E2 E3 P. split=>/= i. apply fupd_trans.
    - intros E1 E2 Ef P HE1f. split=>/= i.
      by rewrite (bi.forall_elim i) bi.pure_True // left_id fupd_mask_frame_r'.
    - intros E1 E2 P Q. split=>/= i. apply fupd_frame_r.
  Qed.
(* iris/bi/monpred.v *)
Instance monPred_bi_fupd `{BiFUpd PROP} : BiFUpd monPredI
:=
    {| bi_fupd_mixin := monPred_fupd_mixin |}.
(* iris/bi/monpred.v *)
Lemma monPred_embed_unseal :
    embed = @monPred_defs.monPred_embed_def I PROP.
Proof. by rewrite -monPred_defs.monPred_embed_unseal. Qed.
(* iris/bi/monpred.v *)
Lemma monPred_bupd_unseal `{!BiBUpd PROP} :
    bupd = @monPred_defs.monPred_bupd_def I PROP _.
Proof. by rewrite -monPred_defs.monPred_bupd_unseal. Qed.
(* iris/bi/monpred.v *)
Lemma monPred_fupd_unseal `{!BiFUpd PROP} :
    fupd = @monPred_defs.monPred_fupd_def I PROP _.
Proof. by rewrite -monPred_defs.monPred_fupd_unseal. Qed.
(* iris/bi/monpred.v *)
Lemma monPred_si_pure_unseal `{!Sbi PROP} :
    si_pure = @monPred_defs.monPred_si_pure_def I PROP _.
Proof. by rewrite -monPred_defs.monPred_si_pure_unseal. Qed.
(* iris/bi/monpred.v *)
Lemma monPred_si_emp_valid_unseal `{!Sbi PROP} :
    si_emp_valid = @monPred_defs.monPred_si_emp_valid_def I PROP _.
Proof. by rewrite -monPred_defs.monPred_si_emp_valid_unseal. Qed.
(* iris/bi/monpred.v *)
(* And finally the proper [unseal] tactic (which we also redefine outside
  of the section since Ltac definitions do not outlive a section). *)
Definition monPred_unseal
:=
    (monPred_unseal_bi,
    @monPred_defs.monPred_objectively_unseal,
    @monPred_defs.monPred_subjectively_unseal,
    @monPred_embed_unseal, @monPred_bupd_unseal, @monPred_fupd_unseal,
    @monPred_si_pure_unseal, @monPred_si_emp_valid_unseal,
    @monPred_defs.monPred_in_unseal).
(* iris/bi/monpred.v *)
Ltac unseal
:= rewrite !monPred_unseal /=.
(* iris/bi/monpred.v *)
Instance monPred_bi_löb : BiLöb PROP → BiLöb monPredI.
Proof. rewrite {2}/BiLöb; unseal=> ? P HP; split=> i /=. apply löb_weak, HP. Qed.
(* iris/bi/monpred.v *)
Instance monPred_bi_positive : BiPositive PROP → BiPositive monPredI.
Proof. split => ?. rewrite /bi_affinely. unseal. apply bi_positive. Qed.
(* iris/bi/monpred.v *)
Instance monPred_bi_affine : BiAffine PROP → BiAffine monPredI.
Proof. split => ?. unseal. by apply affine. Qed.
(* iris/bi/monpred.v *)
Instance monPred_bi_persistently_forall :
    BiPersistentlyForall PROP → BiPersistentlyForall monPredI.
Proof. intros ? A φ. split=> /= i. unseal. by apply persistently_forall_2. Qed.
(* iris/bi/monpred.v *)
Instance monPred_bi_pure_forall :
    BiPureForall PROP → BiPureForall monPredI.
Proof. intros ? A φ. split=> /= i. unseal. by apply pure_forall_2. Qed.
(* iris/bi/monpred.v *)
Instance monPred_bi_later_contractive :
    BiLaterContractive PROP → BiLaterContractive monPredI.
Proof. intros ? n. unseal=> P Q HPQ. split=> i /=. f_contractive. apply HPQ. Qed.
(* iris/bi/monpred.v *)
Instance monPred_bi_embed_emp : BiEmbedEmp PROP monPredI.
Proof. split. by unseal. Qed.
(* iris/bi/monpred.v *)
Instance monPred_bi_embed_later : BiEmbedLater PROP monPredI.
Proof. split; by unseal. Qed.
(* iris/bi/monpred.v *)
Instance monPred_bi_bupd_fupd `{BiBUpdFUpd PROP} : BiBUpdFUpd monPredI.
Proof. intros E P. split=> i. unseal. apply bupd_fupd. Qed.
(* iris/bi/monpred.v *)
Instance monPred_bi_embed_bupd `{!BiBUpd PROP} :
    BiEmbedBUpd PROP monPredI.
Proof. split. by unseal. Qed.
(* iris/bi/monpred.v *)
Instance monPred_bi_embed_fupd `{BiFUpd PROP} : BiEmbedFUpd PROP monPredI.
Proof. split. by unseal. Qed.
(* iris/bi/monpred.v *)
Instance monPred_sbi_emp_valid_exist `{!Sbi PROP, @BiIndexBottom I bot} :
    SbiEmpValidExist PROP → SbiEmpValidExist monPredI.
Proof.
    intros ? A Φ. unseal. rewrite /monPred_defs.monPred_si_emp_valid_def
      /monPred_defs.monPred_exist_def /=.
    rewrite (bi.forall_elim bot) si_emp_valid_exist_1.
    do 3 f_equiv. apply bi.forall_intro=> ?. by f_equiv.
  Qed.
(* iris/bi/monpred.v *)
Instance monPred_bi_embed_sbi `{!Sbi PROP} : BiEmbedSbi PROP monPredI.
Proof.
    split; unseal; rewrite /monPred_defs.monPred_si_emp_valid_def /=; [|done].
    intros P. apply (anti_symm _).
    + by rewrite (bi.forall_elim inhabitant).
    + rewrite si_emp_valid_forall. by apply bi.forall_intro.
  Qed.
(* iris/bi/monpred.v *)
Instance monPred_bi_bupd_sbi `{BiBUpdSbi PROP} :
    BiBUpdSbi monPredI.
Proof. intros P. split=> /= i. unseal. apply bupd_si_pure. Qed.
(* iris/bi/monpred.v *)
Instance monPred_bi_fupd_sbi `{BiFUpdSbi PROP} :
    BiFUpdSbi monPredI.
Proof.
    split; rewrite /bi_except_0; unseal.
    - intros E E' P R. split=>/= i.
      rewrite (bi.forall_elim i) bi.pure_True // bi.True_impl.
      apply fupd_keep_si_pure'.
    - intros E P. split=>/= i. apply fupd_si_pure_later.
    - intros E A Φ. split=>/= i. apply fupd_si_pure_forall_2.
  Qed.
(* iris/bi/monpred.v *)
Class Objective {I : biIndex} {PROP : bi} (P : monPred I PROP)
:=
  objective_at i j : P i ⊢ P j.
(* iris/bi/monpred.v *)
Instance : Params (@Objective) 2
:= {}.
(* iris/bi/monpred.v *)
Notation monPredI
:= (monPredI I PROP).
(* iris/bi/monpred.v *)
Notation monPred_at
:= (@monPred_at I PROP).
(* iris/bi/monpred.v *)
Notation BiIndexBottom
:= (@BiIndexBottom I).
(* iris/bi/monpred.v *)
(* monPred_at unfolding laws *)
Lemma monPred_at_dist n P Q : (P ≡{n}≡ Q) ↔ (∀ i, P i ≡{n}≡ Q i).
Proof. split; [by intros []|by split]. Qed.
(* iris/bi/monpred.v *)
Lemma monPred_at_equiv P Q : (P ⊣⊢ Q) ↔ (∀ i, P i ⊣⊢ Q i).
Proof. split; [by intros []|by split]. Qed.
(* iris/bi/monpred.v *)
Lemma monPred_at_entails P Q : (P ⊢ Q) ↔ (∀ i, P i ⊢ Q i).
Proof. split; [by intros []|by split]. Qed.
(* iris/bi/monpred.v *)
Lemma monPred_at_emp_valid P : (⊢ P) ↔ (∀ i, ⊢ P i).
Proof. unfold bi_emp_valid. unseal. split; [by intros []|by split]. Qed.
(* iris/bi/monpred.v *)
Lemma monPred_at_pure i (φ : Prop) : monPred_at ⌜φ⌝ i ⊣⊢ ⌜φ⌝.
Proof. by unseal. Qed.
(* iris/bi/monpred.v *)
Lemma monPred_at_emp i : monPred_at emp i ⊣⊢ emp.
Proof. by unseal. Qed.
(* iris/bi/monpred.v *)
Lemma monPred_at_and i P Q : (P ∧ Q) i ⊣⊢ P i ∧ Q i.
Proof. by unseal. Qed.
(* iris/bi/monpred.v *)
Lemma monPred_at_or i P Q : (P ∨ Q) i ⊣⊢ P i ∨ Q i.
Proof. by unseal. Qed.
(* iris/bi/monpred.v *)
Lemma monPred_at_impl i P Q : (P → Q) i ⊣⊢ ∀ j, ⌜i ⊑ j⌝ → P j → Q j.
Proof. by unseal. Qed.
(* iris/bi/monpred.v *)
Lemma monPred_at_forall {A} i (Φ : A → monPred) : (∀ x, Φ x) i ⊣⊢ ∀ x, Φ x i.
Proof. by unseal. Qed.
(* iris/bi/monpred.v *)
Lemma monPred_at_exist {A} i (Φ : A → monPred) : (∃ x, Φ x) i ⊣⊢ ∃ x, Φ x i.
Proof. by unseal. Qed.
(* iris/bi/monpred.v *)
Lemma monPred_at_sep i P Q : (P ∗ Q) i ⊣⊢ P i ∗ Q i.
Proof. by unseal. Qed.
(* iris/bi/monpred.v *)
Lemma monPred_at_wand i P Q : (P -∗ Q) i ⊣⊢ ∀ j, ⌜i ⊑ j⌝ → P j -∗ Q j.
Proof. by unseal. Qed.
(* iris/bi/monpred.v *)
Lemma monPred_at_persistently i P : (<pers> P) i ⊣⊢ <pers> (P i).
Proof. by unseal. Qed.
(* iris/bi/monpred.v *)
Lemma monPred_at_in i j : monPred_at (monPred_in j) i ⊣⊢ ⌜j ⊑ i⌝.
Proof. by unseal. Qed.
(* iris/bi/monpred.v *)
Lemma monPred_at_objectively i P : (<obj> P) i ⊣⊢ ∀ j, P j.
Proof. by unseal. Qed.
(* iris/bi/monpred.v *)
Lemma monPred_at_subjectively i P : (<subj> P) i ⊣⊢ ∃ j, P j.
Proof. by unseal. Qed.
(* iris/bi/monpred.v *)
Lemma monPred_at_persistently_if i p P : (<pers>?p P) i ⊣⊢ <pers>?p (P i).
Proof. destruct p=>//=. apply monPred_at_persistently. Qed.
(* iris/bi/monpred.v *)
Lemma monPred_at_affinely i P : (<affine> P) i ⊣⊢ <affine> (P i).
Proof. by rewrite /bi_affinely monPred_at_and monPred_at_emp. Qed.
(* iris/bi/monpred.v *)
Lemma monPred_at_affinely_if i p P : (<affine>?p P) i ⊣⊢ <affine>?p (P i).
Proof. destruct p=>//=. apply monPred_at_affinely. Qed.
(* iris/bi/monpred.v *)
Lemma monPred_at_intuitionistically i P : (□ P) i ⊣⊢ □ (P i).
Proof.
    by rewrite /bi_intuitionistically monPred_at_affinely monPred_at_persistently.
  Qed.
(* iris/bi/monpred.v *)
Lemma monPred_at_intuitionistically_if i p P : (□?p P) i ⊣⊢ □?p (P i).
Proof. destruct p=>//=. apply monPred_at_intuitionistically. Qed.
(* iris/bi/monpred.v *)
Lemma monPred_at_absorbingly i P : (<absorb> P) i ⊣⊢ <absorb> (P i).
Proof. by rewrite /bi_absorbingly monPred_at_sep monPred_at_pure. Qed.
(* iris/bi/monpred.v *)
Lemma monPred_at_absorbingly_if i p P : (<absorb>?p P) i ⊣⊢ <absorb>?p (P i).
Proof. destruct p=>//=. apply monPred_at_absorbingly. Qed.
(* iris/bi/monpred.v *)
Lemma monPred_wand_force i P Q : (P -∗ Q) i ⊢ (P i -∗ Q i).
Proof. unseal. rewrite bi.forall_elim bi.pure_impl_forall bi.forall_elim //. Qed.
(* iris/bi/monpred.v *)
Lemma monPred_impl_force i P Q : (P → Q) i ⊢ (P i → Q i).
Proof. unseal. rewrite bi.forall_elim bi.pure_impl_forall bi.forall_elim //. Qed.
(* iris/bi/monpred.v *)
(* Instances *)
Instance monPred_at_mono :
    Proper ((⊢) ==> (⊑) ==> (⊢)) monPred_at.
Proof. by move=> ?? [?] ?? ->. Qed.
(* iris/bi/monpred.v *)
Instance monPred_at_flip_mono :
    Proper (flip (⊢) ==> flip (⊑) ==> flip (⊢)) monPred_at.
Proof. solve_proper. Qed.
(* iris/bi/monpred.v *)
Instance monPred_in_proper (R : relation I) :
    Proper (R ==> R ==> iff) (⊑) → Reflexive R →
    Proper (R ==> (≡)) (@monPred_in I PROP).
Proof. unseal. split. solve_proper. Qed.
(* iris/bi/monpred.v *)
Instance monPred_in_mono : Proper (flip (⊑) ==> (⊢)) (@monPred_in I PROP).
Proof. unseal. split. solve_proper. Qed.
(* iris/bi/monpred.v *)
Instance monPred_in_flip_mono : Proper ((⊑) ==> flip (⊢)) (@monPred_in I PROP).
Proof. solve_proper. Qed.
(* iris/bi/monpred.v *)
Lemma monPred_persistent P : (∀ i, Persistent (P i)) → Persistent P.
Proof. intros HP. constructor=> i. unseal. apply HP. Qed.
(* iris/bi/monpred.v *)
Lemma monPred_absorbing P : (∀ i, Absorbing (P i)) → Absorbing P.
Proof. intros HP. constructor=> i. rewrite /bi_absorbingly. unseal. apply HP. Qed.
(* iris/bi/monpred.v *)
Lemma monPred_affine P : (∀ i, Affine (P i)) → Affine P.
Proof. intros HP. constructor=> i. unseal. apply HP. Qed.
(* iris/bi/monpred.v *)
Instance monPred_at_persistent P i : Persistent P → Persistent (P i).
Proof. move => [] /(_ i). by unseal. Qed.
(* iris/bi/monpred.v *)
Instance monPred_at_absorbing P i : Absorbing P → Absorbing (P i).
Proof. move => [] /(_ i). rewrite /Absorbing /bi_absorbingly. by unseal. Qed.
(* iris/bi/monpred.v *)
Instance monPred_at_affine P i : Affine P → Affine (P i).
Proof. move => [] /(_ i). unfold Affine. by unseal. Qed.
(* iris/bi/monpred.v *)
(* Note that [monPred_in] is *not* [Plain], because it depends on the index. *)
Instance monPred_in_persistent i : Persistent (@monPred_in I PROP i).
Proof. apply monPred_persistent=> j. rewrite monPred_at_in. apply _. Qed.
(* iris/bi/monpred.v *)
Instance monPred_in_absorbing i : Absorbing (@monPred_in I PROP i).
Proof. apply monPred_absorbing=> j. rewrite monPred_at_in. apply _. Qed.
(* iris/bi/monpred.v *)
Lemma monPred_at_embed i (P : PROP) : monPred_at ⎡P⎤ i ⊣⊢ P.
Proof. by unseal. Qed.
(* iris/bi/monpred.v *)
Lemma monPred_emp_unfold : emp%I =@{monPred} ⎡emp : PROP⎤%I.
Proof. by unseal. Qed.
(* iris/bi/monpred.v *)
Lemma monPred_pure_unfold : bi_pure =@{_ → monPred} λ φ, ⎡ ⌜ φ ⌝ : PROP⎤%I.
Proof. by unseal. Qed.
(* iris/bi/monpred.v *)
Lemma monPred_objectively_unfold : monPred_objectively = λ P, ⎡∀ i, P i⎤%I.
Proof. by unseal. Qed.
(* iris/bi/monpred.v *)
Lemma monPred_subjectively_unfold : monPred_subjectively = λ P, ⎡∃ i, P i⎤%I.
Proof. by unseal. Qed.
(* iris/bi/monpred.v *)
Instance monPred_objectively_ne : NonExpansive (@monPred_objectively I PROP).
Proof. rewrite monPred_objectively_unfold. solve_proper. Qed.
(* iris/bi/monpred.v *)
Instance monPred_objectively_proper :
    Proper ((≡) ==> (≡)) (@monPred_objectively I PROP).
Proof. apply (ne_proper _). Qed.