phanerozoic/Coq-Iris huggingface dataset:
(* iris/bi/big_op.v *)
Lemma big_sepL2_replicate_l l x Φ n :
    length l = n →
    ([∗ list] k↦x1;x2 ∈ replicate n x; l, Φ k x1 x2) ⊣⊢ [∗ list] k↦x2 ∈ l, Φ k x x2.
Proof. intros <-. revert Φ. induction l as [|y l IH]=> //= Φ. by rewrite IH. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepL2_replicate_r l x Φ n :
    length l = n →
    ([∗ list] k↦x1;x2 ∈ l;replicate n x, Φ k x1 x2) ⊣⊢ [∗ list] k↦x1 ∈ l, Φ k x1 x.
Proof. intros <-. revert Φ. induction l as [|y l IH]=> //= Φ. by rewrite IH. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepL2_sep Φ Ψ l1 l2 :
    ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2 ∗ Ψ k y1 y2)
    ⊣⊢ ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2) ∗ ([∗ list] k↦y1;y2 ∈ l1;l2, Ψ k y1 y2).
Proof.
    rewrite !big_sepL2_alt big_sepL_sep !persistent_and_affinely_sep_l.
    rewrite -assoc (assoc _ _ (<affine> _)%I). rewrite -(comm bi_sep (<affine> _)%I).
    rewrite -assoc (assoc _ _ (<affine> _)%I) -!persistent_and_affinely_sep_l.
    by rewrite affinely_and_r persistent_and_affinely_sep_l idemp.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepL2_sep_2 Φ Ψ l1 l2 :
    ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2) -∗
    ([∗ list] k↦y1;y2 ∈ l1;l2, Ψ k y1 y2) -∗
    ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2 ∗ Ψ k y1 y2).
Proof. apply entails_wand, wand_intro_r. rewrite big_sepL2_sep //. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepL2_and Φ Ψ l1 l2 :
    ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2 ∧ Ψ k y1 y2)
    ⊢ ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2) ∧ ([∗ list] k↦y1;y2 ∈ l1;l2, Ψ k y1 y2).
Proof. auto using and_intro, big_sepL2_mono, and_elim_l, and_elim_r. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepL2_pure_1 (φ : nat → A → B → Prop) l1 l2 :
    ([∗ list] k↦y1;y2 ∈ l1;l2, ⌜φ k y1 y2⌝) ⊢@{PROP}
      ⌜∀ k y1 y2, l1 !! k = Some y1 → l2 !! k = Some y2 → φ k y1 y2⌝.
Proof.
    rewrite big_sepL2_alt big_sepL_pure_1.
    rewrite -pure_and. f_equiv=>-[Hlen Hlookup] k y1 y2 Hy1 Hy2.
    eapply (Hlookup k (y1, y2)).
    rewrite lookup_zip_with Hy1 /= Hy2 /= //.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepL2_affinely_pure_2 (φ : nat → A → B → Prop) l1 l2 :
    length l1 = length l2 →
    <affine> ⌜∀ k y1 y2, l1 !! k = Some y1 → l2 !! k = Some y2 → φ k y1 y2⌝ ⊢@{PROP}
    ([∗ list] k↦y1;y2 ∈ l1;l2, <affine> ⌜φ k y1 y2⌝).
Proof.
    intros Hdom. rewrite big_sepL2_alt.
    rewrite -big_sepL_affinely_pure_2.
    rewrite affinely_and_r -pure_and. f_equiv. f_equiv=>-Hforall.
    split; first done.
    intros k [y1 y2] (? & ? & [= <- <-] & Hy1 & Hy2)%lookup_zip_with_Some.
    by eapply Hforall.
  Qed.
(* iris/bi/big_op.v *)
(* The general backwards direction requires [BiAffine] to cover the empty case. *)
Lemma big_sepL2_pure `{!BiAffine PROP} (φ : nat → A → B → Prop) l1 l2 :
    ([∗ list] k↦y1;y2 ∈ l1;l2, ⌜φ k y1 y2⌝) ⊣⊢@{PROP}
      ⌜length l1 = length l2 ∧
       ∀ k y1 y2, l1 !! k = Some y1 → l2 !! k = Some y2 → φ k y1 y2⌝.
Proof.
    apply (anti_symm (⊢)).
    { rewrite pure_and. apply and_intro.
      - apply big_sepL2_length.
      - apply big_sepL2_pure_1. }
    rewrite -(affine_affinely ⌜_⌝%I).
    rewrite pure_and -affinely_and_r.
    apply pure_elim_l=>Hdom.
    rewrite big_sepL2_affinely_pure_2 //. by setoid_rewrite affinely_elim.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepL2_persistently `{!BiAffine PROP} Φ l1 l2 :
    <pers> ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2)
    ⊣⊢ [∗ list] k↦y1;y2 ∈ l1;l2, <pers> (Φ k y1 y2).
Proof.
    by rewrite !big_sepL2_alt persistently_and persistently_pure big_sepL_persistently.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepL2_intro Φ l1 l2 :
    length l1 = length l2 →
    □ (∀ k x1 x2, ⌜l1 !! k = Some x1⌝ → ⌜l2 !! k = Some x2⌝ → Φ k x1 x2) ⊢
    [∗ list] k↦x1;x2 ∈ l1;l2, Φ k x1 x2.
Proof.
    revert l2 Φ. induction l1 as [|x1 l1 IH]=> -[|x2 l2] Φ ?; simplify_eq/=.
    { by apply (affine _). }
    rewrite intuitionistically_sep_dup. f_equiv.
    - rewrite (forall_elim 0) (forall_elim x1) (forall_elim x2).
      by rewrite !pure_True // !True_impl intuitionistically_elim.
    - rewrite -IH //. f_equiv.
      by apply forall_intro=> k; by rewrite (forall_elim (S k)).
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepL2_forall `{!BiAffine PROP} Φ l1 l2 :
    (∀ k x1 x2, Persistent (Φ k x1 x2)) →
    ([∗ list] k↦x1;x2 ∈ l1;l2, Φ k x1 x2) ⊣⊢
      ⌜length l1 = length l2⌝
      ∧ (∀ k x1 x2, ⌜l1 !! k = Some x1⌝ → ⌜l2 !! k = Some x2⌝ → Φ k x1 x2).
Proof.
    intros HΦ. apply (anti_symm _).
    { apply and_intro; [apply big_sepL2_length|].
      apply forall_intro=> k. apply forall_intro=> x1. apply forall_intro=> x2.
      do 2 (apply impl_intro_l; apply pure_elim_l=> ?). by apply: big_sepL2_lookup. }
    apply pure_elim_l=> Hlen.
    revert l2 Φ HΦ Hlen. induction l1 as [|x1 l1 IH]=> -[|x2 l2] Φ HΦ Hlen; simplify_eq/=.
    { by apply (affine _). }
    rewrite -persistent_and_sep_1. apply and_intro.
    - rewrite (forall_elim 0) (forall_elim x1) (forall_elim x2).
      by rewrite !pure_True // !True_impl.
    - rewrite -IH //.
      by apply forall_intro=> k; by rewrite (forall_elim (S k)).
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepL2_impl Φ Ψ l1 l2 :
    ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2) -∗
    □ (∀ k x1 x2,
      ⌜l1 !! k = Some x1⌝ → ⌜l2 !! k = Some x2⌝ → Φ k x1 x2 -∗ Ψ k x1 x2) -∗
    [∗ list] k↦y1;y2 ∈ l1;l2, Ψ k y1 y2.
Proof.
    apply entails_wand. rewrite -(idemp bi_and (big_sepL2 _ _ _)) {1}big_sepL2_length.
    apply pure_elim_l=> ?. rewrite big_sepL2_intro //.
    apply bi.wand_intro_l. rewrite -big_sepL2_sep. by setoid_rewrite wand_elim_l.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepL2_wand Φ Ψ l1 l2 :
    ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2) -∗
    ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2 -∗ Ψ k y1 y2) -∗
    [∗ list] k↦y1;y2 ∈ l1;l2, Ψ k y1 y2.
Proof.
    apply entails_wand, wand_intro_r. rewrite -big_sepL2_sep.
    setoid_rewrite wand_elim_r. done.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepL2_delete Φ l1 l2 i x1 x2 :
    l1 !! i = Some x1 → l2 !! i = Some x2 →
    ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2) ⊣⊢
    Φ i x1 x2 ∗ [∗ list] k↦y1;y2 ∈ l1;l2, if decide (k = i) then emp else Φ k y1 y2.
Proof.
    intros. rewrite -(take_drop_middle l1 i x1) // -(take_drop_middle l2 i x2) //.
    assert (i < length l1 ∧ i < length l2) as [??] by eauto using lookup_lt_Some.
    rewrite !big_sepL2_app_same_length /=; [|rewrite ?length_take; lia..].
    rewrite Nat.add_0_r length_take_le; [|lia].
    rewrite decide_True // left_id.
    rewrite assoc -!(comm _ (Φ _ _ _)) -assoc. do 2 f_equiv.
    - apply big_sepL2_proper=> k y1 y2 Hk. apply lookup_lt_Some in Hk.
      rewrite length_take in Hk. by rewrite decide_False; last lia.
    - apply big_sepL2_proper=> k y1 y2 _. by rewrite decide_False; last lia.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepL2_delete' `{!BiAffine PROP} Φ l1 l2 i x1 x2 :
    l1 !! i = Some x1 → l2 !! i = Some x2 →
    ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2) ⊣⊢
    Φ i x1 x2 ∗ [∗ list] k↦y1;y2 ∈ l1;l2, ⌜ k ≠ i ⌝ → Φ k y1 y2.
Proof.
    intros. rewrite big_sepL2_delete //. (do 2 f_equiv)=> k y1 y2.
    rewrite -decide_emp. by repeat case_decide.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepL2_lookup_acc_impl {Φ l1 l2} i x1 x2 :
    l1 !! i = Some x1 →
    l2 !! i = Some x2 →
    ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2) -∗
    (* We obtain [Φ] for the [x1] and [x2] *)
    Φ i x1 x2 ∗
    (* We reobtain the bigop for a predicate [Ψ] selected by the user *)
    ∀ Ψ,
      □ (∀ k y1 y2,
        ⌜ l1 !! k = Some y1 ⌝ → ⌜ l2 !! k = Some y2 ⌝ → ⌜ k ≠ i ⌝ →
        Φ k y1 y2 -∗ Ψ k y1 y2) -∗
      Ψ i x1 x2 -∗
      [∗ list] k↦y1;y2 ∈ l1;l2, Ψ k y1 y2.
Proof.
    intros. rewrite big_sepL2_delete //. apply entails_wand, sep_mono_r, forall_intro=> Ψ.
    apply wand_intro_r, wand_intro_l.
    rewrite (big_sepL2_delete Ψ l1 l2 i) //. apply sep_mono_r.
    eapply wand_apply; [apply wand_entails, big_sepL2_impl|apply sep_mono_r].
    apply intuitionistically_intro', forall_intro=> k;
      apply forall_intro=> y1; apply forall_intro=> y2.
    do 2 (apply impl_intro_l, pure_elim_l=> ?); apply wand_intro_r.
    rewrite (forall_elim k) (forall_elim y1) (forall_elim y2).
    rewrite !(pure_True (_ = Some _)) // !left_id.
    destruct (decide _) as [->|]; [by apply: affine|].
    by rewrite pure_True //left_id intuitionistically_elim wand_elim_l.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepL2_later_1 `{!BiAffine PROP} Φ l1 l2 :
    (▷ [∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2) ⊢ ◇ [∗ list] k↦y1;y2 ∈ l1;l2, ▷ Φ k y1 y2.
Proof.
    rewrite !big_sepL2_alt later_and big_sepL_later (timeless ⌜ _ ⌝).
    rewrite except_0_and. auto using and_mono, except_0_intro.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepL2_later_2 Φ l1 l2 :
    ([∗ list] k↦y1;y2 ∈ l1;l2, ▷ Φ k y1 y2) ⊢ ▷ [∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2.
Proof.
    rewrite !big_sepL2_alt later_and big_sepL_later_2.
    auto using and_mono, later_intro.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepL2_laterN_2 Φ n l1 l2 :
    ([∗ list] k↦y1;y2 ∈ l1;l2, ▷^n Φ k y1 y2) ⊢ ▷^n [∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2.
Proof.
    rewrite !big_sepL2_alt laterN_and big_sepL_laterN_2.
    auto using and_mono, laterN_intro.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepL2_flip Φ l1 l2 :
    ([∗ list] k↦y1;y2 ∈ l2; l1, Φ k y2 y1) ⊣⊢ ([∗ list] k↦y1;y2 ∈ l1; l2, Φ k y1 y2).
Proof.
    revert Φ l2. induction l1 as [|x1 l1 IH]=> Φ -[|x2 l2]//=; simplify_eq.
    by rewrite IH.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepL2_sepL (Φ1 : nat → A → PROP) (Φ2 : nat → B → PROP) l1 l2 :
    length l1 = length l2 →
    ([∗ list] k↦y1;y2 ∈ l1;l2, Φ1 k y1 ∗ Φ2 k y2) ⊣⊢
    ([∗ list] k↦y1 ∈ l1, Φ1 k y1) ∗ ([∗ list] k↦y2 ∈ l2, Φ2 k y2).
Proof.
    intros. rewrite -big_sepL_sep_zip // big_sepL2_alt pure_True // left_id //.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_sepL2_sepL_2 (Φ1 : nat → A → PROP) (Φ2 : nat → B → PROP) l1 l2 :
    length l1 = length l2 →
    ([∗ list] k↦y1 ∈ l1, Φ1 k y1) -∗
    ([∗ list] k↦y2 ∈ l2, Φ2 k y2) -∗
    [∗ list] k↦y1;y2 ∈ l1;l2, Φ1 k y1 ∗ Φ2 k y2.
Proof. intros. apply entails_wand, wand_intro_r. by rewrite big_sepL2_sepL. Qed.
(* iris/bi/big_op.v *)
Lemma big_sepL2_const_sepL_l {A B} (Φ : nat → A → PROP) (l1 : list A) (l2 : list B) :
  ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1)
  ⊣⊢ ⌜length l1 = length l2⌝ ∧ ([∗ list] k↦y1 ∈ l1, Φ k y1).
Proof.
  rewrite big_sepL2_alt.
  trans (⌜length l1 = length l2⌝ ∧ [∗ list] k↦y1 ∈ (zip l1 l2).*1, Φ k y1)%I.
  { rewrite big_sepL_fmap //. }
  apply (anti_symm (⊢)); apply pure_elim_l=> Hl; rewrite fst_zip;
    rewrite ?Hl //;
    (apply and_intro; [by apply pure_intro|done]).
Qed.
(* iris/bi/big_op.v *)
Lemma big_sepL2_const_sepL_r {A B}  (Φ : nat → B → PROP) (l1 : list A) (l2 : list B) :
  ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k y2)
  ⊣⊢ ⌜length l1 = length l2⌝ ∧ ([∗ list] k↦y2 ∈ l2, Φ k y2).
Proof. by rewrite big_sepL2_flip big_sepL2_const_sepL_l (symmetry_iff (=)). Qed.
(* iris/bi/big_op.v *)
Lemma big_sepL2_sep_sepL_l {A B} (Φ : nat → A → PROP)
    (Ψ : nat → A → B → PROP) l1 l2 :
  ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 ∗ Ψ k y1 y2)
  ⊣⊢ ([∗ list] k↦y1 ∈ l1, Φ k y1) ∗ ([∗ list] k↦y1;y2 ∈ l1;l2, Ψ k y1 y2).
Proof.
  rewrite big_sepL2_sep big_sepL2_const_sepL_l. apply (anti_symm _).
  { rewrite and_elim_r. done. }
  rewrite !big_sepL2_alt [(_ ∗ _)%I]comm -!persistent_and_sep_assoc.
  apply pure_elim_l=>Hl. apply and_intro.
  { apply pure_intro. done. }
  rewrite [(_ ∗ _)%I]comm. apply sep_mono; first done.
  apply and_intro; last done.
  apply pure_intro. done.
Qed.
(* iris/bi/big_op.v *)
Lemma big_sepL2_sep_sepL_r {A B} (Φ : nat → A → B → PROP)
    (Ψ : nat → B → PROP) l1 l2 :
  ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2 ∗ Ψ k y2)
  ⊣⊢ ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2) ∗ ([∗ list] k↦y2 ∈ l2, Ψ k y2).
Proof.
  rewrite !(big_sepL2_flip _ _ l1). setoid_rewrite (comm bi_sep).
  by rewrite big_sepL2_sep_sepL_l.
Qed.
(* iris/bi/big_op.v *)
Lemma big_sepL_sepL2_diag {A} (Φ : nat → A → A → PROP) (l : list A) :
  ([∗ list] k↦y ∈ l, Φ k y y) ⊢
  ([∗ list] k↦y1;y2 ∈ l;l, Φ k y1 y2).
Proof.
  rewrite big_sepL2_alt. rewrite pure_True // left_id.
  rewrite zip_diag big_sepL_fmap /=. done.
Qed.
(* iris/bi/big_op.v *)
Lemma big_sepL2_ne_2 {A B : ofe}
    (Φ Ψ : nat → A → B → PROP) l1 l2 l1' l2' n :
  l1 ≡{n}≡ l1' → l2 ≡{n}≡ l2' →
  (∀ k y1 y1' y2 y2',
    l1 !! k = Some y1 → l1' !! k = Some y1' → y1 ≡{n}≡ y1' →
    l2 !! k = Some y2 → l2' !! k = Some y2' → y2 ≡{n}≡ y2' →
    Φ k y1 y2 ≡{n}≡ Ψ k y1' y2') →
  ([∗ list] k ↦ y1;y2 ∈ l1;l2, Φ k y1 y2)%I ≡{n}≡ ([∗ list] k ↦ y1;y2 ∈ l1';l2', Ψ k y1 y2)%I.
Proof.
  intros Hl1 Hl2 Hf. rewrite !big_sepL2_alt. f_equiv.
  { do 2 f_equiv; by apply: length_ne. }
  apply big_opL_ne_2; [by f_equiv|].
  intros k [x1 y1] [x2 y2] (?&?&[=<- <-]&?&?)%lookup_zip_with_Some
    (?&?&[=<- <-]&?&?)%lookup_zip_with_Some [??]; naive_solver.
Qed.
(* iris/bi/big_op.v *)
Lemma big_andL_nil Φ : ([∧ list] k↦y ∈ nil, Φ k y) ⊣⊢ True.
Proof. done. Qed.
(* iris/bi/big_op.v *)
Lemma big_andL_nil' P Φ : P ⊢ [∧ list] k↦y ∈ nil, Φ k y.
Proof. by apply pure_intro. Qed.
(* iris/bi/big_op.v *)
Lemma big_andL_cons Φ x l :
    ([∧ list] k↦y ∈ x :: l, Φ k y) ⊣⊢ Φ 0 x ∧ [∧ list] k↦y ∈ l, Φ (S k) y.
Proof. by rewrite big_opL_cons. Qed.
(* iris/bi/big_op.v *)
Lemma big_andL_singleton Φ x : ([∧ list] k↦y ∈ [x], Φ k y) ⊣⊢ Φ 0 x.
Proof. by rewrite big_opL_singleton. Qed.
(* iris/bi/big_op.v *)
Lemma big_andL_app Φ l1 l2 :
    ([∧ list] k↦y ∈ l1 ++ l2, Φ k y)
    ⊣⊢ ([∧ list] k↦y ∈ l1, Φ k y) ∧ ([∧ list] k↦y ∈ l2, Φ (length l1 + k) y).
Proof. by rewrite big_opL_app. Qed.
(* iris/bi/big_op.v *)
Lemma big_andL_snoc Φ l x :
    ([∧ list] k↦y ∈ l ++ [x], Φ k y) ⊣⊢ ([∧ list] k↦y ∈ l, Φ k y) ∧ Φ (length l) x.
Proof. by rewrite big_opL_snoc. Qed.
(* iris/bi/big_op.v *)
Lemma big_andL_submseteq (Φ : A → PROP) l1 l2 :
    l1 ⊆+ l2 → ([∧ list] y ∈ l2, Φ y) ⊢ [∧ list] y ∈ l1, Φ y.
Proof.
    intros [l ->]%submseteq_Permutation. by rewrite big_andL_app and_elim_l.
  Qed.
(* iris/bi/big_op.v *)
(* The lemmas [big_andL_mono], [big_andL_ne] and [big_andL_proper] are more
  generic than the instances as they also give [l !! k = Some y] in the premise. *)
Lemma big_andL_mono Φ Ψ l :
    (∀ k y, l !! k = Some y → Φ k y ⊢ Ψ k y) →
    ([∧ list] k ↦ y ∈ l, Φ k y) ⊢ [∧ list] k ↦ y ∈ l, Ψ k y.
Proof. apply big_opL_gen_proper; apply _. Qed.
(* iris/bi/big_op.v *)
Lemma big_andL_ne Φ Ψ l n :
    (∀ k y, l !! k = Some y → Φ k y ≡{n}≡ Ψ k y) →
    ([∧ list] k ↦ y ∈ l, Φ k y)%I ≡{n}≡ ([∧ list] k ↦ y ∈ l, Ψ k y)%I.
Proof. apply big_opL_ne. Qed.
(* iris/bi/big_op.v *)
Lemma big_andL_proper Φ Ψ l :
    (∀ k y, l !! k = Some y → Φ k y ⊣⊢ Ψ k y) →
    ([∧ list] k ↦ y ∈ l, Φ k y) ⊣⊢ ([∧ list] k ↦ y ∈ l, Ψ k y).
Proof. apply big_opL_proper. Qed.
(* iris/bi/big_op.v *)
(* No need to declare instances for non-expansiveness and properness, we
  get both from the generic [big_opL] instances. *)
Instance big_andL_mono' :
    Proper (pointwise_relation _ (pointwise_relation _ (⊢)) ==> (=) ==> (⊢))
           (big_opL (@bi_and PROP) (A:=A)).
Proof. intros f g Hf m ? <-. apply big_andL_mono; intros; apply Hf. Qed.
(* iris/bi/big_op.v *)
Instance big_andL_id_mono' :
    Proper (Forall2 (⊢) ==> (⊢)) (big_opL (@bi_and PROP) (λ _ P, P)).
Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
(* iris/bi/big_op.v *)
Instance big_andL_nil_absorbing Φ :
    Absorbing ([∧ list] k↦x ∈ [], Φ k x).
Proof. simpl; apply _. Qed.
(* iris/bi/big_op.v *)
Lemma big_andL_absorbing Φ l :
    (∀ k x, l !! k = Some x → Absorbing (Φ k x)) →
    Absorbing ([∧ list] k↦x ∈ l, Φ k x).
Proof. apply big_opL_closed; apply _. Qed.
(* iris/bi/big_op.v *)
Instance big_andL_absorbing' Φ l :
    (∀ k x, Absorbing (Φ k x)) → Absorbing ([∧ list] k↦x ∈ l, Φ k x).
Proof. intros; apply big_andL_absorbing, _. Qed.
(* iris/bi/big_op.v *)
Instance big_andL_nil_persistent Φ :
    Persistent ([∧ list] k↦x ∈ [], Φ k x).
Proof. simpl; apply _. Qed.
(* iris/bi/big_op.v *)
Lemma big_andL_persistent Φ l :
    (∀ k x, l !! k = Some x → Persistent (Φ k x)) → Persistent ([∧ list] k↦x ∈ l, Φ k x).
Proof. apply big_opL_closed; apply _. Qed.
(* iris/bi/big_op.v *)
Instance big_andL_persistent' Φ l :
    (∀ k x, Persistent (Φ k x)) → Persistent ([∧ list] k↦x ∈ l, Φ k x).
Proof. intros; apply big_andL_persistent, _. Qed.
(* iris/bi/big_op.v *)
Instance big_andL_nil_timeless Φ :
    Timeless ([∧ list] k↦x ∈ [], Φ k x).
Proof. simpl; apply _. Qed.
(* iris/bi/big_op.v *)
Lemma big_andL_timeless Φ l :
    (∀ k x, l !! k = Some x → Timeless (Φ k x)) →
    Timeless ([∧ list] k↦x ∈ l, Φ k x).
Proof. apply big_opL_closed; apply _. Qed.
(* iris/bi/big_op.v *)
Instance big_andL_timeless' Φ l :
    (∀ k x, Timeless (Φ k x)) → Timeless ([∧ list] k↦x ∈ l, Φ k x).
Proof. intros; apply big_andL_timeless, _. Qed.
(* iris/bi/big_op.v *)
Lemma big_andL_lookup Φ l i x :
    l !! i = Some x → ([∧ list] k↦y ∈ l, Φ k y) ⊢ Φ i x.
Proof.
    intros. rewrite -(take_drop_middle l i x) // big_andL_app /=.
    rewrite Nat.add_0_r length_take_le;
      eauto using lookup_lt_Some, Nat.lt_le_incl, and_elim_l', and_elim_r'.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_andL_elem_of (Φ : A → PROP) l x :
    x ∈ l → ([∧ list] y ∈ l, Φ y) ⊢ Φ x.
Proof.
    intros [i ?]%list_elem_of_lookup. by eapply (big_andL_lookup (λ _, Φ)).
  Qed.
(* iris/bi/big_op.v *)
Lemma big_andL_fmap {B} (f : A → B) (Φ : nat → B → PROP) l :
    ([∧ list] k↦y ∈ f <$> l, Φ k y) ⊣⊢ ([∧ list] k↦y ∈ l, Φ k (f y)).
Proof. by rewrite big_opL_fmap. Qed.
(* iris/bi/big_op.v *)
Lemma big_andL_bind {B} (f : A → list B) (Φ : B → PROP) l :
    ([∧ list] y ∈ l ≫= f, Φ y) ⊣⊢ ([∧ list] x ∈ l, [∧ list] y ∈ f x, Φ y).
Proof. by rewrite big_opL_bind. Qed.
(* iris/bi/big_op.v *)
Lemma big_andL_and Φ Ψ l :
    ([∧ list] k↦x ∈ l, Φ k x ∧ Ψ k x)
    ⊣⊢ ([∧ list] k↦x ∈ l, Φ k x) ∧ ([∧ list] k↦x ∈ l, Ψ k x).
Proof. by rewrite big_opL_op. Qed.
(* iris/bi/big_op.v *)
Lemma big_andL_persistently Φ l :
    <pers> ([∧ list] k↦x ∈ l, Φ k x) ⊣⊢ [∧ list] k↦x ∈ l, <pers> (Φ k x).
Proof. apply (big_opL_commute _). Qed.
(* iris/bi/big_op.v *)
Lemma big_andL_forall Φ l :
    ([∧ list] k↦x ∈ l, Φ k x) ⊣⊢ (∀ k x, ⌜l !! k = Some x⌝ → Φ k x).
Proof.
    apply (anti_symm _).
    { apply forall_intro=> k; apply forall_intro=> x.
      apply impl_intro_l, pure_elim_l=> ?; by apply: big_andL_lookup. }
    revert Φ. induction l as [|x l IH]=> Φ; [by auto using big_andL_nil'|].
    rewrite big_andL_cons. apply and_intro.
    - by rewrite (forall_elim 0) (forall_elim x) pure_True // True_impl.
    - rewrite -IH. apply forall_intro=> k; by rewrite (forall_elim (S k)).
  Qed.
(* iris/bi/big_op.v *)
Lemma big_andL_intro Φ l :
    (∀ k x, ⌜l !! k = Some x⌝ → Φ k x) ⊢ [∧ list] k↦x ∈ l, Φ k x.
Proof. rewrite big_andL_forall //. Qed.
(* iris/bi/big_op.v *)
Lemma big_andL_impl Φ Ψ m :
    ([∧ list] k↦x ∈ m, Φ k x) ∧
    (∀ k x, ⌜m !! k = Some x⌝ → Φ k x → Ψ k x) ⊢
    [∧ list] k↦x ∈ m, Ψ k x.
Proof.
    rewrite -big_andL_forall -big_andL_and.
    by setoid_rewrite bi.impl_elim_r.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_andL_pure_1 (φ : nat → A → Prop) l :
    ([∧ list] k↦x ∈ l, ⌜φ k x⌝) ⊢@{PROP} ⌜∀ k x, l !! k = Some x → φ k x⌝.
Proof.
    induction l as [|x l IH] using rev_ind.
    { apply pure_intro=>??. rewrite lookup_nil. done. }
    rewrite big_andL_snoc // IH -pure_and.
    f_equiv=>-[Hl Hx] k y /lookup_app_Some =>-[Hy|[Hlen Hy]].
    - by apply Hl.
    - apply list_lookup_singleton_Some in Hy as [Hk ->].
      replace k with (length l) by lia. done.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_andL_pure_2 (φ : nat → A → Prop) l :
    ⌜∀ k x, l !! k = Some x → φ k x⌝ ⊢@{PROP} ([∧ list] k↦x ∈ l, ⌜φ k x⌝).
Proof.
    rewrite big_andL_forall pure_forall_1. f_equiv=>k.
    rewrite pure_forall_1. f_equiv=>x. apply pure_impl_1.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_andL_pure (φ : nat → A → Prop) l :
    ([∧ list] k↦x ∈ l, ⌜φ k x⌝) ⊣⊢@{PROP} ⌜∀ k x, l !! k = Some x → φ k x⌝.
Proof.
    apply (anti_symm (⊢)); first by apply big_andL_pure_1.
    apply big_andL_pure_2.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_andL_later Φ l :
    ▷ ([∧ list] k↦x ∈ l, Φ k x) ⊣⊢ ([∧ list] k↦x ∈ l, ▷ Φ k x).
Proof. apply (big_opL_commute _). Qed.
(* iris/bi/big_op.v *)
Lemma big_andL_laterN Φ n l :
    ▷^n ([∧ list] k↦x ∈ l, Φ k x) ⊣⊢ ([∧ list] k↦x ∈ l, ▷^n Φ k x).
Proof. apply (big_opL_commute _). Qed.
(* iris/bi/big_op.v *)
Lemma big_andL_zip_seq (Φ : nat * A → PROP) n len l :
    length l ≤ len →
    ([∧ list] ky ∈ zip (seq n len) l, Φ ky)
      ⊣⊢ ([∧ list] k ↦ y ∈ l, Φ (n + k, y)).
Proof. apply big_opL_zip_seq. Qed.
(* iris/bi/big_op.v *)
Lemma big_andL_zip_seqZ (Φ : Z * A → PROP) n len l :
    length l ≤ len →
    ([∧ list] ky ∈ zip (seqZ n len) l, Φ ky)
      ⊣⊢ ([∧ list] k ↦ y ∈ l, Φ ((n + k)%Z, y)).
Proof. apply big_opL_zip_seqZ. Qed.
(* iris/bi/big_op.v *)
Lemma big_orL_nil Φ : ([∨ list] k↦y ∈ nil, Φ k y) ⊣⊢ False.
Proof. done. Qed.
(* iris/bi/big_op.v *)
Lemma big_orL_cons Φ x l :
    ([∨ list] k↦y ∈ x :: l, Φ k y) ⊣⊢ Φ 0 x ∨ [∨ list] k↦y ∈ l, Φ (S k) y.
Proof. by rewrite big_opL_cons. Qed.
(* iris/bi/big_op.v *)
Lemma big_orL_singleton Φ x : ([∨ list] k↦y ∈ [x], Φ k y) ⊣⊢ Φ 0 x.
Proof. by rewrite big_opL_singleton. Qed.
(* iris/bi/big_op.v *)
Lemma big_orL_app Φ l1 l2 :
    ([∨ list] k↦y ∈ l1 ++ l2, Φ k y)
    ⊣⊢ ([∨ list] k↦y ∈ l1, Φ k y) ∨ ([∨ list] k↦y ∈ l2, Φ (length l1 + k) y).
Proof. by rewrite big_opL_app. Qed.
(* iris/bi/big_op.v *)
Lemma big_orL_snoc Φ l x :
    ([∨ list] k↦y ∈ l ++ [x], Φ k y) ⊣⊢ ([∨ list] k↦y ∈ l, Φ k y) ∨ Φ (length l) x.
Proof. by rewrite big_opL_snoc. Qed.
(* iris/bi/big_op.v *)
Lemma big_orL_submseteq (Φ : A → PROP) l1 l2 :
    l1 ⊆+ l2 → ([∨ list] y ∈ l1, Φ y) ⊢ [∨ list] y ∈ l2, Φ y.
Proof.
    intros [l ->]%submseteq_Permutation. by rewrite big_orL_app -or_intro_l.
  Qed.
(* iris/bi/big_op.v *)
(* The lemmas [big_orL_mono], [big_orL_ne] and [big_orL_proper] are more
  generic than the instances as they also give [l !! k = Some y] in the premise. *)
Lemma big_orL_mono Φ Ψ l :
    (∀ k y, l !! k = Some y → Φ k y ⊢ Ψ k y) →
    ([∨ list] k ↦ y ∈ l, Φ k y) ⊢ [∨ list] k ↦ y ∈ l, Ψ k y.
Proof. apply big_opL_gen_proper; apply _. Qed.
(* iris/bi/big_op.v *)
Lemma big_orL_ne Φ Ψ l n :
    (∀ k y, l !! k = Some y → Φ k y ≡{n}≡ Ψ k y) →
    ([∨ list] k ↦ y ∈ l, Φ k y)%I ≡{n}≡ ([∨ list] k ↦ y ∈ l, Ψ k y)%I.
Proof. apply big_opL_ne. Qed.
(* iris/bi/big_op.v *)
Lemma big_orL_proper Φ Ψ l :
    (∀ k y, l !! k = Some y → Φ k y ⊣⊢ Ψ k y) →
    ([∨ list] k ↦ y ∈ l, Φ k y) ⊣⊢ ([∨ list] k ↦ y ∈ l, Ψ k y).
Proof. apply big_opL_proper. Qed.
(* iris/bi/big_op.v *)
(* No need to declare instances for non-expansiveness and properness, we
  get both from the generic [big_opL] instances. *)
Instance big_orL_mono' :
    Proper (pointwise_relation _ (pointwise_relation _ (⊢)) ==> (=) ==> (⊢))
           (big_opL (@bi_or PROP) (A:=A)).
Proof. intros f g Hf m ? <-. apply big_orL_mono; intros; apply Hf. Qed.
(* iris/bi/big_op.v *)
Instance big_orL_id_mono' :
    Proper (Forall2 (⊢) ==> (⊢)) (big_opL (@bi_or PROP) (λ _ P, P)).
Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
(* iris/bi/big_op.v *)
Instance big_orL_nil_persistent Φ :
    Persistent ([∨ list] k↦x ∈ [], Φ k x).
Proof. simpl; apply _. Qed.
(* iris/bi/big_op.v *)
Instance big_orL_persistent Φ l :
    (∀ k x, l !! k = Some x → Persistent (Φ k x)) →
    Persistent ([∨ list] k↦x ∈ l, Φ k x).
Proof. apply big_opL_closed; apply _. Qed.
(* iris/bi/big_op.v *)
Instance big_orL_persistent' Φ l :
    (∀ k x, Persistent (Φ k x)) → Persistent ([∨ list] k↦x ∈ l, Φ k x).
Proof. intros; apply big_orL_persistent, _. Qed.
(* iris/bi/big_op.v *)
Instance big_orL_nil_timeless Φ :
    Timeless ([∨ list] k↦x ∈ [], Φ k x).
Proof. simpl; apply _. Qed.
(* iris/bi/big_op.v *)
Instance big_orL_timeless Φ l :
    (∀ k x, l !! k = Some x → Timeless (Φ k x)) →
    Timeless ([∨ list] k↦x ∈ l, Φ k x).
Proof. apply big_opL_closed; apply _. Qed.
(* iris/bi/big_op.v *)
Instance big_orL_timeless' Φ l :
    (∀ k x, Timeless (Φ k x)) → Timeless ([∨ list] k↦x ∈ l, Φ k x).
Proof. intros; apply big_orL_timeless, _. Qed.
(* iris/bi/big_op.v *)
Lemma big_orL_intro Φ l i x :
    l !! i = Some x → Φ i x ⊢ ([∨ list] k↦y ∈ l, Φ k y).
Proof.
    intros. rewrite -(take_drop_middle l i x) // big_orL_app /=.
    rewrite Nat.add_0_r length_take_le;
      eauto using lookup_lt_Some, Nat.lt_le_incl, or_intro_l', or_intro_r'.
  Qed.
(* iris/bi/big_op.v *)
Lemma big_orL_elem_of (Φ : A → PROP) l x :
    x ∈ l → Φ x ⊢ ([∨ list] y ∈ l, Φ y).
Proof.
    intros [i ?]%list_elem_of_lookup; by eapply (big_orL_intro (λ _, Φ)).
  Qed.
(* iris/bi/big_op.v *)
Lemma big_orL_fmap {B} (f : A → B) (Φ : nat → B → PROP) l :
    ([∨ list] k↦y ∈ f <$> l, Φ k y) ⊣⊢ ([∨ list] k↦y ∈ l, Φ k (f y)).
Proof. by rewrite big_opL_fmap. Qed.