Minor cleanup

theories/base_logic/bi.v

@@ -23,6 +23,16 @@ Context `{I : biIndex, PROP : bi}.
 Implicit Types (P Q : monPred) (i : I).
 
 (* TODO: move to Iris *)
+Global Instance big_sepL2_objective {A B} (Φ : nat → A → B → monPred)
+  (l1 : list A) (l2 : list B)
+  `{H : ∀ n x y, Objective (Φ n x y)} :
+  @Objective I PROP ([∗ list] n↦x;y ∈ l1;l2, Φ n x y).
+Proof.
+  intros i j. rewrite big_sepL2_alt 2!monPred_at_and 2!monPred_at_pure.
+  apply bi.and_mono_r. rewrite 2!monPred_at_big_sepL.
+  apply big_sepL_mono => ???. apply H.
+Qed.
+
 (* monPred_in *)
 Lemma monPred_in_bot `{BiIndexBottom _ bot} : ⊢ ⊒bot : monPred.
 Proof. constructor. eauto. Qed.

theories/base_logic/vprop.v

@@ -55,18 +55,6 @@ Notation "'@{' V '}' P" := (view_at V P) (at level 25, format "@{ V }  P") : bi_
 Instance : Params (@view_join) 1 := {}.
 Instance : Params (@view_at) 1 := {}.
 
-(* TODO: move to Iris *)
-Global Instance big_sepL2_objective
-  {I : biIndex} {PROP : bi} {A B} (Φ : nat → A → B → monPred I PROP)
-  (l1 : list A) (l2 : list B)
-  `{H : ∀ n x y, Objective (Φ n x y)} :
-  @Objective I PROP ([∗ list] n↦x;y ∈ l1;l2, Φ n x y).
-Proof.
-  intros i j. rewrite big_sepL2_alt 2!monPred_at_and 2!monPred_at_pure.
-  apply bi.and_mono_r. rewrite 2!monPred_at_big_sepL.
-  apply big_sepL_mono => ???. apply H.
-Qed.
-(* End TODO *)
 
 Section props.
 Context `{Σ : gFunctors}.