From 6b0f250faeb84dfd29110b039109eb687c26859a Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 12 Sep 2018 11:48:56 +0200
Subject: [PATCH] Move theorems about `envs_` to `environments.v` where also
 these operations are defined.

---
 theories/proofmode/coq_tactics.v  | 362 -----------------------------
 theories/proofmode/environments.v | 372 ++++++++++++++++++++++++++++++
 2 files changed, 372 insertions(+), 362 deletions(-)

diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index c6c962f52..9d5a5bc66 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -5,8 +5,6 @@ Set Default Proof Using "Type".
 Import bi.
 Import env_notations.
 
-Local Notation "b1 && b2" := (if b1 then b2 else false) : bool_scope.
-
 (* Coq versions of the tactics *)
 Section bi_tactics.
 Context {PROP : bi}.
@@ -14,366 +12,6 @@ Implicit Types Γ : env PROP.
 Implicit Types Δ : envs PROP.
 Implicit Types P Q : PROP.
 
-Lemma of_envs_eq Δ :
-  of_envs Δ = (⌜envs_wf Δ⌝ ∧ □ [∧] env_intuitionistic Δ ∗ [∗] env_spatial Δ)%I.
-Proof. done. Qed.
-(** An environment is a ∗ of something intuitionistic and the spatial environment.
-TODO: Can we define it as such? *)
-Lemma of_envs_eq' Δ :
-  of_envs Δ ⊣⊢ (⌜envs_wf Δ⌝ ∧ □ [∧] env_intuitionistic Δ) ∗ [∗] env_spatial Δ.
-Proof. rewrite of_envs_eq persistent_and_sep_assoc //. Qed.
-
-Lemma envs_delete_persistent Δ i : envs_delete false i true Δ = Δ. 
-Proof. by destruct Δ. Qed.
-Lemma envs_delete_spatial Δ i :
-  envs_delete false i false Δ = envs_delete true i false Δ.
-Proof. by destruct Δ. Qed.
-
-Lemma envs_lookup_delete_Some Δ Δ' rp i p P :
-  envs_lookup_delete rp i Δ = Some (p,P,Δ')
-  ↔ envs_lookup i Δ = Some (p,P) ∧ Δ' = envs_delete rp i p Δ.
-Proof.
-  rewrite /envs_lookup /envs_delete /envs_lookup_delete.
-  destruct Δ as [Γp Γs]; rewrite /= !env_lookup_delete_correct.
-  destruct (Γp !! i), (Γs !! i); naive_solver.
-Qed.
-
-Lemma envs_lookup_sound' Δ rp i p P :
-  envs_lookup i Δ = Some (p,P) →
-  of_envs Δ ⊢ □?p P ∗ of_envs (envs_delete rp i p Δ).
-Proof.
-  rewrite /envs_lookup /envs_delete /of_envs=>?. apply pure_elim_l=> Hwf.
-  destruct Δ as [Γp Γs], (Γp !! i) eqn:?; simplify_eq/=.
-  - rewrite pure_True ?left_id; last (destruct Hwf, rp; constructor;
-      naive_solver eauto using env_delete_wf, env_delete_fresh).
-    destruct rp.
-    + rewrite (env_lookup_perm Γp) //= intuitionistically_and.
-      by rewrite and_sep_intuitionistically -assoc.
-    + rewrite {1}intuitionistically_sep_dup {1}(env_lookup_perm Γp) //=.
-      by rewrite intuitionistically_and and_elim_l -assoc.
-  - destruct (Γs !! i) eqn:?; simplify_eq/=.
-    rewrite pure_True ?left_id; last (destruct Hwf; constructor;
-      naive_solver eauto using env_delete_wf, env_delete_fresh).
-    rewrite (env_lookup_perm Γs) //=. by rewrite !assoc -(comm _ P).
-Qed.
-Lemma envs_lookup_sound Δ i p P :
-  envs_lookup i Δ = Some (p,P) →
-  of_envs Δ ⊢ □?p P ∗ of_envs (envs_delete true i p Δ).
-Proof. apply envs_lookup_sound'. Qed.
-Lemma envs_lookup_persistent_sound Δ i P :
-  envs_lookup i Δ = Some (true,P) → of_envs Δ ⊢ □ P ∗ of_envs Δ.
-Proof. intros ?%(envs_lookup_sound' _ false). by destruct Δ. Qed.
-Lemma envs_lookup_sound_2 Δ i p P :
-  envs_wf Δ → envs_lookup i Δ = Some (p,P) →
-  □?p P ∗ of_envs (envs_delete true i p Δ) ⊢ of_envs Δ.
-Proof.
-  rewrite /envs_lookup /of_envs=>Hwf ?. rewrite [⌜envs_wf Δ⌝%I]pure_True // left_id.
-  destruct Δ as [Γp Γs], (Γp !! i) eqn:?; simplify_eq/=.
-  - rewrite (env_lookup_perm Γp) //= intuitionistically_and
-      and_sep_intuitionistically and_elim_r.
-    cancel [â–¡ P]%I. solve_sep_entails.
-  - destruct (Γs !! i) eqn:?; simplify_eq/=.
-    rewrite (env_lookup_perm Γs) //= and_elim_r.
-    cancel [P]. solve_sep_entails.
-Qed.
-
-Lemma envs_lookup_split Δ i p P :
-  envs_lookup i Δ = Some (p,P) → of_envs Δ ⊢ □?p P ∗ (□?p P -∗ of_envs Δ).
-Proof.
-  intros. apply pure_elim with (envs_wf Δ).
-  { rewrite of_envs_eq. apply and_elim_l. }
-  intros. rewrite {1}envs_lookup_sound//.
-  apply sep_mono_r. apply wand_intro_l, envs_lookup_sound_2; done.
-Qed.
-
-Lemma envs_lookup_delete_sound Δ Δ' rp i p P :
-  envs_lookup_delete rp i Δ = Some (p,P,Δ') → of_envs Δ ⊢ □?p P ∗ of_envs Δ'.
-Proof. intros [? ->]%envs_lookup_delete_Some. by apply envs_lookup_sound'. Qed.
-
-Lemma envs_lookup_delete_list_sound Δ Δ' rp js p Ps :
-  envs_lookup_delete_list rp js Δ = Some (p,Ps,Δ') →
-  of_envs Δ ⊢ □?p [∗] Ps ∗ of_envs Δ'.
-Proof.
-  revert Δ Δ' p Ps. induction js as [|j js IH]=> Δ Δ'' p Ps ?; simplify_eq/=.
-  { by rewrite intuitionistically_emp left_id. }
-  destruct (envs_lookup_delete rp j Δ) as [[[q1 P] Δ']|] eqn:Hj; simplify_eq/=.
-  apply envs_lookup_delete_Some in Hj as [Hj ->].
-  destruct (envs_lookup_delete_list _ js _) as [[[q2 Ps'] ?]|] eqn:?; simplify_eq/=.
-  rewrite -intuitionistically_if_sep_2 -assoc.
-  rewrite envs_lookup_sound' //; rewrite IH //.
-  repeat apply sep_mono=>//; apply intuitionistically_if_flag_mono; by destruct q1.
-Qed.
-
-Lemma envs_lookup_delete_list_cons Δ Δ' Δ'' rp j js p1 p2 P Ps :
-  envs_lookup_delete rp j Δ = Some (p1, P, Δ') →
-  envs_lookup_delete_list rp js Δ' = Some (p2, Ps, Δ'') →
-  envs_lookup_delete_list rp (j :: js) Δ = Some (p1 && p2, (P :: Ps), Δ'').
-Proof. rewrite //= => -> //= -> //=. Qed.
-
-Lemma envs_lookup_delete_list_nil Δ rp :
-  envs_lookup_delete_list rp [] Δ = Some (true, [], Δ).
-Proof. done. Qed.
-
-Lemma envs_lookup_snoc Δ i p P :
-  envs_lookup i Δ = None → envs_lookup i (envs_snoc Δ p i P) = Some (p, P).
-Proof.
-  rewrite /envs_lookup /envs_snoc=> ?.
-  destruct Δ as [Γp Γs], p, (Γp !! i); simplify_eq; by rewrite env_lookup_snoc.
-Qed.
-Lemma envs_lookup_snoc_ne Δ i j p P :
-  i ≠ j → envs_lookup i (envs_snoc Δ p j P) = envs_lookup i Δ.
-Proof.
-  rewrite /envs_lookup /envs_snoc=> ?.
-  destruct Δ as [Γp Γs], p; simplify_eq; by rewrite env_lookup_snoc_ne.
-Qed.
-
-Lemma envs_snoc_sound Δ p i P :
-  envs_lookup i Δ = None → of_envs Δ ⊢ □?p P -∗ of_envs (envs_snoc Δ p i P).
-Proof.
-  rewrite /envs_lookup /envs_snoc /of_envs=> ?; apply pure_elim_l=> Hwf.
-  destruct Δ as [Γp Γs], (Γp !! i) eqn:?, (Γs !! i) eqn:?; simplify_eq/=.
-  apply wand_intro_l; destruct p; simpl.
-  - apply and_intro; [apply pure_intro|].
-    + destruct Hwf; constructor; simpl; eauto using Esnoc_wf.
-      intros j; destruct (ident_beq_reflect j i); naive_solver.
-    + by rewrite intuitionistically_and and_sep_intuitionistically assoc.
-  - apply and_intro; [apply pure_intro|].
-    + destruct Hwf; constructor; simpl; eauto using Esnoc_wf.
-      intros j; destruct (ident_beq_reflect j i); naive_solver.
-    + solve_sep_entails.
-Qed.
-
-Lemma envs_app_sound Δ Δ' p Γ :
-  envs_app p Γ Δ = Some Δ' →
-  of_envs Δ ⊢ (if p then □ [∧] Γ else [∗] Γ) -∗ of_envs Δ'.
-Proof.
-  rewrite /of_envs /envs_app=> ?; apply pure_elim_l=> Hwf.
-  destruct Δ as [Γp Γs], p; simplify_eq/=.
-  - destruct (env_app Γ Γs) eqn:Happ,
-      (env_app Γ Γp) as [Γp'|] eqn:?; simplify_eq/=.
-    apply wand_intro_l, and_intro; [apply pure_intro|].
-    + destruct Hwf; constructor; simpl; eauto using env_app_wf.
-      intros j. apply (env_app_disjoint _ _ _ j) in Happ.
-      naive_solver eauto using env_app_fresh.
-    + rewrite (env_app_perm _ _ Γp') //.
-      rewrite big_opL_app intuitionistically_and and_sep_intuitionistically.
-      solve_sep_entails.
-  - destruct (env_app Γ Γp) eqn:Happ,
-      (env_app Γ Γs) as [Γs'|] eqn:?; simplify_eq/=.
-    apply wand_intro_l, and_intro; [apply pure_intro|].
-    + destruct Hwf; constructor; simpl; eauto using env_app_wf.
-      intros j. apply (env_app_disjoint _ _ _ j) in Happ.
-      naive_solver eauto using env_app_fresh.
-    + rewrite (env_app_perm _ _ Γs') // big_opL_app. solve_sep_entails.
-Qed.
-
-Lemma envs_app_singleton_sound Δ Δ' p j Q :
-  envs_app p (Esnoc Enil j Q) Δ = Some Δ' → of_envs Δ ⊢ □?p Q -∗ of_envs Δ'.
-Proof. move=> /envs_app_sound. destruct p; by rewrite /= right_id. Qed.
-
-Lemma envs_simple_replace_sound' Δ Δ' i p Γ :
-  envs_simple_replace i p Γ Δ = Some Δ' →
-  of_envs (envs_delete true i p Δ) ⊢ (if p then □ [∧] Γ else [∗] Γ) -∗ of_envs Δ'.
-Proof.
-  rewrite /envs_simple_replace /envs_delete /of_envs=> ?.
-  apply pure_elim_l=> Hwf. destruct Δ as [Γp Γs], p; simplify_eq/=.
-  - destruct (env_app Γ Γs) eqn:Happ,
-      (env_replace i Γ Γp) as [Γp'|] eqn:?; simplify_eq/=.
-    apply wand_intro_l, and_intro; [apply pure_intro|].
-    + destruct Hwf; constructor; simpl; eauto using env_replace_wf.
-      intros j. apply (env_app_disjoint _ _ _ j) in Happ.
-      destruct (decide (i = j)); try naive_solver eauto using env_replace_fresh.
-    + rewrite (env_replace_perm _ _ Γp') //.
-      rewrite big_opL_app intuitionistically_and and_sep_intuitionistically.
-      solve_sep_entails.
-  - destruct (env_app Γ Γp) eqn:Happ,
-      (env_replace i Γ Γs) as [Γs'|] eqn:?; simplify_eq/=.
-    apply wand_intro_l, and_intro; [apply pure_intro|].
-    + destruct Hwf; constructor; simpl; eauto using env_replace_wf.
-      intros j. apply (env_app_disjoint _ _ _ j) in Happ.
-      destruct (decide (i = j)); try naive_solver eauto using env_replace_fresh.
-    + rewrite (env_replace_perm _ _ Γs') // big_opL_app. solve_sep_entails.
-Qed.
-
-Lemma envs_simple_replace_singleton_sound' Δ Δ' i p j Q :
-  envs_simple_replace i p (Esnoc Enil j Q) Δ = Some Δ' →
-  of_envs (envs_delete true i p Δ) ⊢ □?p Q -∗ of_envs Δ'.
-Proof. move=> /envs_simple_replace_sound'. destruct p; by rewrite /= right_id. Qed.
-
-Lemma envs_simple_replace_sound Δ Δ' i p P Γ :
-  envs_lookup i Δ = Some (p,P) → envs_simple_replace i p Γ Δ = Some Δ' →
-  of_envs Δ ⊢ □?p P ∗ ((if p then □ [∧] Γ else [∗] Γ) -∗ of_envs Δ').
-Proof. intros. by rewrite envs_lookup_sound// envs_simple_replace_sound'//. Qed.
-
-Lemma envs_simple_replace_maybe_sound Δ Δ' i p P Γ :
-  envs_lookup i Δ = Some (p,P) → envs_simple_replace i p Γ Δ = Some Δ' →
-  of_envs Δ ⊢ □?p P ∗ (((if p then □ [∧] Γ else [∗] Γ) -∗ of_envs Δ') ∧ (□?p P -∗ of_envs Δ)).
-Proof.
-  intros. apply pure_elim with (envs_wf Δ).
-  { rewrite of_envs_eq. apply and_elim_l. }
-  intros. rewrite {1}envs_lookup_sound//. apply sep_mono_r, and_intro.
-  - rewrite envs_simple_replace_sound'//.
-  - apply wand_intro_l, envs_lookup_sound_2; done.
-Qed.
-
-Lemma envs_simple_replace_singleton_sound Δ Δ' i p P j Q :
-  envs_lookup i Δ = Some (p,P) →
-  envs_simple_replace i p (Esnoc Enil j Q) Δ = Some Δ' →
-  of_envs Δ ⊢ □?p P ∗ (□?p Q -∗ of_envs Δ').
-Proof.
-  intros. by rewrite envs_lookup_sound// envs_simple_replace_singleton_sound'//.
-Qed.
-
-Lemma envs_replace_sound' Δ Δ' i p q Γ :
-  envs_replace i p q Γ Δ = Some Δ' →
-  of_envs (envs_delete true i p Δ) ⊢ (if q then □ [∧] Γ else [∗] Γ) -∗ of_envs Δ'.
-Proof.
-  rewrite /envs_replace; destruct (beq _ _) eqn:Hpq.
-  - apply eqb_prop in Hpq as ->. apply envs_simple_replace_sound'.
-  - apply envs_app_sound.
-Qed.
-
-Lemma envs_replace_singleton_sound' Δ Δ' i p q j Q :
-  envs_replace i p q (Esnoc Enil j Q) Δ = Some Δ' →
-  of_envs (envs_delete true i p Δ) ⊢ □?q Q -∗ of_envs Δ'.
-Proof. move=> /envs_replace_sound'. destruct q; by rewrite /= ?right_id. Qed.
-
-Lemma envs_replace_sound Δ Δ' i p q P Γ :
-  envs_lookup i Δ = Some (p,P) → envs_replace i p q Γ Δ = Some Δ' →
-  of_envs Δ ⊢ □?p P ∗ ((if q then □ [∧] Γ else [∗] Γ) -∗ of_envs Δ').
-Proof. intros. by rewrite envs_lookup_sound// envs_replace_sound'//. Qed.
-
-Lemma envs_replace_singleton_sound Δ Δ' i p q P j Q :
-  envs_lookup i Δ = Some (p,P) →
-  envs_replace i p q (Esnoc Enil j Q) Δ = Some Δ' →
-  of_envs Δ ⊢ □?p P ∗ (□?q Q -∗ of_envs Δ').
-Proof. intros. by rewrite envs_lookup_sound// envs_replace_singleton_sound'//. Qed.
-
-Lemma envs_lookup_envs_clear_spatial Δ j :
-  envs_lookup j (envs_clear_spatial Δ)
-  = ''(p,P) ← envs_lookup j Δ; if p : bool then Some (p,P) else None.
-Proof.
-  rewrite /envs_lookup /envs_clear_spatial.
-  destruct Δ as [Γp Γs]; simpl; destruct (Γp !! j) eqn:?; simplify_eq/=; auto.
-  by destruct (Γs !! j).
-Qed.
-
-Lemma envs_clear_spatial_sound Δ :
-  of_envs Δ ⊢ of_envs (envs_clear_spatial Δ) ∗ [∗] env_spatial Δ.
-Proof.
-  rewrite /of_envs /envs_clear_spatial /=. apply pure_elim_l=> Hwf.
-  rewrite right_id -persistent_and_sep_assoc. apply and_intro; [|done].
-  apply pure_intro. destruct Hwf; constructor; simpl; auto using Enil_wf.
-Qed.
-
-Lemma env_spatial_is_nil_intuitionistically Δ :
-  env_spatial_is_nil Δ = true → of_envs Δ ⊢ □ of_envs Δ.
-Proof.
-  intros. unfold of_envs; destruct Δ as [? []]; simplify_eq/=.
-  rewrite !right_id /bi_intuitionistically {1}affinely_and_r persistently_and.
-  by rewrite persistently_affinely_elim persistently_idemp persistently_pure.
-Qed.
-
-Lemma envs_lookup_envs_delete Δ i p P :
-  envs_wf Δ →
-  envs_lookup i Δ = Some (p,P) → envs_lookup i (envs_delete true i p Δ) = None.
-Proof.
-  rewrite /envs_lookup /envs_delete=> -[?? Hdisj] Hlookup.
-  destruct Δ as [Γp Γs], p; simplify_eq/=.
-  - rewrite env_lookup_env_delete //. revert Hlookup.
-    destruct (Hdisj i) as [->| ->]; [|done]. by destruct (Γs !! _).
-  - rewrite env_lookup_env_delete //. by destruct (Γp !! _).
-Qed.
-Lemma envs_lookup_envs_delete_ne Δ rp i j p :
-  i ≠ j → envs_lookup i (envs_delete rp j p Δ) = envs_lookup i Δ.
-Proof.
-  rewrite /envs_lookup /envs_delete=> ?. destruct Δ as [Γp Γs],p; simplify_eq/=.
-  - destruct rp=> //. by rewrite env_lookup_env_delete_ne.
-  - destruct (Γp !! i); simplify_eq/=; by rewrite ?env_lookup_env_delete_ne.
-Qed.
-
-Lemma envs_split_go_sound js Δ1 Δ2 Δ1' Δ2' :
-  (∀ j P, envs_lookup j Δ1 = Some (false, P) → envs_lookup j Δ2 = None) →
-  envs_split_go js Δ1 Δ2 = Some (Δ1',Δ2') →
-  of_envs Δ1 ∗ of_envs Δ2 ⊢ of_envs Δ1' ∗ of_envs Δ2'.
-Proof.
-  revert Δ1 Δ2.
-  induction js as [|j js IH]=> Δ1 Δ2 Hlookup HΔ; simplify_eq/=; [done|].
-  apply pure_elim with (envs_wf Δ1)=> [|Hwf].
-  { by rewrite /of_envs !and_elim_l sep_elim_l. }
-  destruct (envs_lookup_delete _ j Δ1)
-    as [[[[] P] Δ1'']|] eqn:Hdel; simplify_eq/=; auto.
-  apply envs_lookup_delete_Some in Hdel as [??]; subst.
-  rewrite envs_lookup_sound //; rewrite /= (comm _ P) -assoc.
-  rewrite -(IH _ _ _ HΔ); last first.
-   { intros j' P'; destruct (decide (j = j')) as [->|].
-     - by rewrite (envs_lookup_envs_delete _ _ _ P).
-     - rewrite envs_lookup_envs_delete_ne // envs_lookup_snoc_ne //. eauto. }
-  rewrite (envs_snoc_sound Δ2 false j P) /= ?wand_elim_r; eauto.
-Qed.
-Lemma envs_split_sound Δ d js Δ1 Δ2 :
-  envs_split d js Δ = Some (Δ1,Δ2) → of_envs Δ ⊢ of_envs Δ1 ∗ of_envs Δ2.
-Proof.
-  rewrite /envs_split=> ?. rewrite -(idemp bi_and (of_envs Δ)).
-  rewrite {2}envs_clear_spatial_sound.
-  rewrite (env_spatial_is_nil_intuitionistically (envs_clear_spatial _)) //.
-  rewrite -persistently_and_intuitionistically_sep_l.
-  rewrite (and_elim_l (<pers> _)%I)
-          persistently_and_intuitionistically_sep_r intuitionistically_elim.
-  destruct (envs_split_go _ _) as [[Δ1' Δ2']|] eqn:HΔ; [|done].
-  apply envs_split_go_sound in HΔ as ->; last first.
-  { intros j P. by rewrite envs_lookup_envs_clear_spatial=> ->. }
-  destruct d; simplify_eq/=; solve_sep_entails.
-Qed.
-
-Lemma prop_of_env_sound Γ : prop_of_env Γ ⊣⊢ [∗] Γ.
-Proof.
-  destruct Γ as [|Γ ? P]; simpl; first done.
-  revert P. induction Γ as [|Γ IH ? Q]=>P; simpl.
-  - by rewrite right_id.
-  - rewrite /= IH (comm _ Q _) assoc. done.
-Qed.
-
-Global Instance envs_Forall2_refl (R : relation PROP) :
-  Reflexive R → Reflexive (envs_Forall2 R).
-Proof. by constructor. Qed.
-Global Instance envs_Forall2_sym (R : relation PROP) :
-  Symmetric R → Symmetric (envs_Forall2 R).
-Proof. intros ??? [??]; by constructor. Qed.
-Global Instance envs_Forall2_trans (R : relation PROP) :
-  Transitive R → Transitive (envs_Forall2 R).
-Proof. intros ??? [??] [??] [??]; constructor; etrans; eauto. Qed.
-Global Instance envs_Forall2_antisymm (R R' : relation PROP) :
-  AntiSymm R R' → AntiSymm (envs_Forall2 R) (envs_Forall2 R').
-Proof. intros ??? [??] [??]; constructor; by eapply (anti_symm _). Qed.
-Lemma envs_Forall2_impl (R R' : relation PROP) Δ1 Δ2 :
-  envs_Forall2 R Δ1 Δ2 → (∀ P Q, R P Q → R' P Q) → envs_Forall2 R' Δ1 Δ2.
-Proof. intros [??] ?; constructor; eauto using env_Forall2_impl. Qed.
-
-Global Instance of_envs_mono : Proper (envs_Forall2 (⊢) ==> (⊢)) (@of_envs PROP).
-Proof.
-  intros [Γp1 Γs1] [Γp2 Γs2] [Hp Hs]; apply and_mono; simpl in *.
-  - apply pure_mono=> -[???]. constructor;
-      naive_solver eauto using env_Forall2_wf, env_Forall2_fresh.
-  - by repeat f_equiv.
-Qed.
-Global Instance of_envs_proper :
-  Proper (envs_Forall2 (⊣⊢) ==> (⊣⊢)) (@of_envs PROP).
-Proof.
-  intros Δ1 Δ2 HΔ; apply (anti_symm (⊢)); apply of_envs_mono;
-    eapply (envs_Forall2_impl (⊣⊢)); [| |symmetry|]; eauto using equiv_entails.
-Qed.
-Global Instance Envs_proper (R : relation PROP) :
-  Proper (env_Forall2 R ==> env_Forall2 R ==> eq ==> envs_Forall2 R) (@Envs PROP).
-Proof. by constructor. Qed.
-
-Global Instance envs_entails_proper :
-  Proper (envs_Forall2 (⊣⊢) ==> (⊣⊢) ==> iff) (@envs_entails PROP).
-Proof. rewrite envs_entails_eq. solve_proper. Qed.
-Global Instance envs_entails_flip_mono :
-  Proper (envs_Forall2 (⊢) ==> flip (⊢) ==> flip impl) (@envs_entails PROP).
-Proof. rewrite envs_entails_eq=> Δ1 Δ2 ? P1 P2 <- <-. by f_equiv. Qed.
-
 (** * Adequacy *)
 Lemma tac_adequate P : envs_entails (Envs Enil Enil 1) P → P.
 Proof.
diff --git a/theories/proofmode/environments.v b/theories/proofmode/environments.v
index cdca5f137..a1e363e75 100644
--- a/theories/proofmode/environments.v
+++ b/theories/proofmode/environments.v
@@ -1,7 +1,9 @@
 From iris.proofmode Require Import base.
 From iris.algebra Require Export base.
 From iris.bi Require Export bi.
+From iris.bi Require Import tactics.
 Set Default Proof Using "Type".
+Import bi.
 
 Inductive env (A : Type) : Type :=
   | Enil : env A
@@ -22,6 +24,9 @@ Module env_notations.
   Notation "x ← y ; z" := (y ≫= λ x, z).
   Notation "' x1 .. xn ← y ; z" := (y ≫= (λ x1, .. (λ xn, z) .. )).
   Notation "Γ !! j" := (env_lookup j Γ).
+
+  (* andb will not be simplified by pm_reduce *)
+  Notation "b1 && b2" := (if b1 then b2 else false) : bool_scope.
 End env_notations.
 Import env_notations.
 
@@ -335,3 +340,370 @@ Definition prop_of_env {PROP : bi} (Γ : env PROP) : PROP :=
     match Γ with Enil => acc | Esnoc Γ _ P => aux Γ (P ∗ acc)%I end
   in
   match Γ with Enil => emp%I | Esnoc Γ _ P => aux Γ P end.
+
+Section envs.
+Context {PROP : bi}.
+Implicit Types Γ : env PROP.
+Implicit Types Δ : envs PROP.
+Implicit Types P Q : PROP.
+
+Lemma of_envs_eq Δ :
+  of_envs Δ = (⌜envs_wf Δ⌝ ∧ □ [∧] env_intuitionistic Δ ∗ [∗] env_spatial Δ)%I.
+Proof. done. Qed.
+(** An environment is a ∗ of something intuitionistic and the spatial environment.
+TODO: Can we define it as such? *)
+Lemma of_envs_eq' Δ :
+  of_envs Δ ⊣⊢ (⌜envs_wf Δ⌝ ∧ □ [∧] env_intuitionistic Δ) ∗ [∗] env_spatial Δ.
+Proof. rewrite of_envs_eq persistent_and_sep_assoc //. Qed.
+
+Lemma envs_delete_persistent Δ i : envs_delete false i true Δ = Δ.
+Proof. by destruct Δ. Qed.
+Lemma envs_delete_spatial Δ i :
+  envs_delete false i false Δ = envs_delete true i false Δ.
+Proof. by destruct Δ. Qed.
+
+Lemma envs_lookup_delete_Some Δ Δ' rp i p P :
+  envs_lookup_delete rp i Δ = Some (p,P,Δ')
+  ↔ envs_lookup i Δ = Some (p,P) ∧ Δ' = envs_delete rp i p Δ.
+Proof.
+  rewrite /envs_lookup /envs_delete /envs_lookup_delete.
+  destruct Δ as [Γp Γs]; rewrite /= !env_lookup_delete_correct.
+  destruct (Γp !! i), (Γs !! i); naive_solver.
+Qed.
+
+Lemma envs_lookup_sound' Δ rp i p P :
+  envs_lookup i Δ = Some (p,P) →
+  of_envs Δ ⊢ □?p P ∗ of_envs (envs_delete rp i p Δ).
+Proof.
+  rewrite /envs_lookup /envs_delete /of_envs=>?. apply pure_elim_l=> Hwf.
+  destruct Δ as [Γp Γs], (Γp !! i) eqn:?; simplify_eq/=.
+  - rewrite pure_True ?left_id; last (destruct Hwf, rp; constructor;
+      naive_solver eauto using env_delete_wf, env_delete_fresh).
+    destruct rp.
+    + rewrite (env_lookup_perm Γp) //= intuitionistically_and.
+      by rewrite and_sep_intuitionistically -assoc.
+    + rewrite {1}intuitionistically_sep_dup {1}(env_lookup_perm Γp) //=.
+      by rewrite intuitionistically_and and_elim_l -assoc.
+  - destruct (Γs !! i) eqn:?; simplify_eq/=.
+    rewrite pure_True ?left_id; last (destruct Hwf; constructor;
+      naive_solver eauto using env_delete_wf, env_delete_fresh).
+    rewrite (env_lookup_perm Γs) //=. by rewrite !assoc -(comm _ P).
+Qed.
+Lemma envs_lookup_sound Δ i p P :
+  envs_lookup i Δ = Some (p,P) →
+  of_envs Δ ⊢ □?p P ∗ of_envs (envs_delete true i p Δ).
+Proof. apply envs_lookup_sound'. Qed.
+Lemma envs_lookup_persistent_sound Δ i P :
+  envs_lookup i Δ = Some (true,P) → of_envs Δ ⊢ □ P ∗ of_envs Δ.
+Proof. intros ?%(envs_lookup_sound' _ false). by destruct Δ. Qed.
+Lemma envs_lookup_sound_2 Δ i p P :
+  envs_wf Δ → envs_lookup i Δ = Some (p,P) →
+  □?p P ∗ of_envs (envs_delete true i p Δ) ⊢ of_envs Δ.
+Proof.
+  rewrite /envs_lookup /of_envs=>Hwf ?. rewrite [⌜envs_wf Δ⌝%I]pure_True // left_id.
+  destruct Δ as [Γp Γs], (Γp !! i) eqn:?; simplify_eq/=.
+  - rewrite (env_lookup_perm Γp) //= intuitionistically_and
+      and_sep_intuitionistically and_elim_r.
+    cancel [â–¡ P]%I. solve_sep_entails.
+  - destruct (Γs !! i) eqn:?; simplify_eq/=.
+    rewrite (env_lookup_perm Γs) //= and_elim_r.
+    cancel [P]. solve_sep_entails.
+Qed.
+
+Lemma envs_lookup_split Δ i p P :
+  envs_lookup i Δ = Some (p,P) → of_envs Δ ⊢ □?p P ∗ (□?p P -∗ of_envs Δ).
+Proof.
+  intros. apply pure_elim with (envs_wf Δ).
+  { rewrite of_envs_eq. apply and_elim_l. }
+  intros. rewrite {1}envs_lookup_sound//.
+  apply sep_mono_r. apply wand_intro_l, envs_lookup_sound_2; done.
+Qed.
+
+Lemma envs_lookup_delete_sound Δ Δ' rp i p P :
+  envs_lookup_delete rp i Δ = Some (p,P,Δ') → of_envs Δ ⊢ □?p P ∗ of_envs Δ'.
+Proof. intros [? ->]%envs_lookup_delete_Some. by apply envs_lookup_sound'. Qed.
+
+Lemma envs_lookup_delete_list_sound Δ Δ' rp js p Ps :
+  envs_lookup_delete_list rp js Δ = Some (p,Ps,Δ') →
+  of_envs Δ ⊢ □?p [∗] Ps ∗ of_envs Δ'.
+Proof.
+  revert Δ Δ' p Ps. induction js as [|j js IH]=> Δ Δ'' p Ps ?; simplify_eq/=.
+  { by rewrite intuitionistically_emp left_id. }
+  destruct (envs_lookup_delete rp j Δ) as [[[q1 P] Δ']|] eqn:Hj; simplify_eq/=.
+  apply envs_lookup_delete_Some in Hj as [Hj ->].
+  destruct (envs_lookup_delete_list _ js _) as [[[q2 Ps'] ?]|] eqn:?; simplify_eq/=.
+  rewrite -intuitionistically_if_sep_2 -assoc.
+  rewrite envs_lookup_sound' //; rewrite IH //.
+  repeat apply sep_mono=>//; apply intuitionistically_if_flag_mono; by destruct q1.
+Qed.
+
+Lemma envs_lookup_delete_list_cons Δ Δ' Δ'' rp j js p1 p2 P Ps :
+  envs_lookup_delete rp j Δ = Some (p1, P, Δ') →
+  envs_lookup_delete_list rp js Δ' = Some (p2, Ps, Δ'') →
+  envs_lookup_delete_list rp (j :: js) Δ = Some (p1 && p2, (P :: Ps), Δ'').
+Proof. rewrite //= => -> //= -> //=. Qed.
+
+Lemma envs_lookup_delete_list_nil Δ rp :
+  envs_lookup_delete_list rp [] Δ = Some (true, [], Δ).
+Proof. done. Qed.
+
+Lemma envs_lookup_snoc Δ i p P :
+  envs_lookup i Δ = None → envs_lookup i (envs_snoc Δ p i P) = Some (p, P).
+Proof.
+  rewrite /envs_lookup /envs_snoc=> ?.
+  destruct Δ as [Γp Γs], p, (Γp !! i); simplify_eq; by rewrite env_lookup_snoc.
+Qed.
+Lemma envs_lookup_snoc_ne Δ i j p P :
+  i ≠ j → envs_lookup i (envs_snoc Δ p j P) = envs_lookup i Δ.
+Proof.
+  rewrite /envs_lookup /envs_snoc=> ?.
+  destruct Δ as [Γp Γs], p; simplify_eq; by rewrite env_lookup_snoc_ne.
+Qed.
+
+Lemma envs_snoc_sound Δ p i P :
+  envs_lookup i Δ = None → of_envs Δ ⊢ □?p P -∗ of_envs (envs_snoc Δ p i P).
+Proof.
+  rewrite /envs_lookup /envs_snoc /of_envs=> ?; apply pure_elim_l=> Hwf.
+  destruct Δ as [Γp Γs], (Γp !! i) eqn:?, (Γs !! i) eqn:?; simplify_eq/=.
+  apply wand_intro_l; destruct p; simpl.
+  - apply and_intro; [apply pure_intro|].
+    + destruct Hwf; constructor; simpl; eauto using Esnoc_wf.
+      intros j; destruct (ident_beq_reflect j i); naive_solver.
+    + by rewrite intuitionistically_and and_sep_intuitionistically assoc.
+  - apply and_intro; [apply pure_intro|].
+    + destruct Hwf; constructor; simpl; eauto using Esnoc_wf.
+      intros j; destruct (ident_beq_reflect j i); naive_solver.
+    + solve_sep_entails.
+Qed.
+
+Lemma envs_app_sound Δ Δ' p Γ :
+  envs_app p Γ Δ = Some Δ' →
+  of_envs Δ ⊢ (if p then □ [∧] Γ else [∗] Γ) -∗ of_envs Δ'.
+Proof.
+  rewrite /of_envs /envs_app=> ?; apply pure_elim_l=> Hwf.
+  destruct Δ as [Γp Γs], p; simplify_eq/=.
+  - destruct (env_app Γ Γs) eqn:Happ,
+      (env_app Γ Γp) as [Γp'|] eqn:?; simplify_eq/=.
+    apply wand_intro_l, and_intro; [apply pure_intro|].
+    + destruct Hwf; constructor; simpl; eauto using env_app_wf.
+      intros j. apply (env_app_disjoint _ _ _ j) in Happ.
+      naive_solver eauto using env_app_fresh.
+    + rewrite (env_app_perm _ _ Γp') //.
+      rewrite big_opL_app intuitionistically_and and_sep_intuitionistically.
+      solve_sep_entails.
+  - destruct (env_app Γ Γp) eqn:Happ,
+      (env_app Γ Γs) as [Γs'|] eqn:?; simplify_eq/=.
+    apply wand_intro_l, and_intro; [apply pure_intro|].
+    + destruct Hwf; constructor; simpl; eauto using env_app_wf.
+      intros j. apply (env_app_disjoint _ _ _ j) in Happ.
+      naive_solver eauto using env_app_fresh.
+    + rewrite (env_app_perm _ _ Γs') // big_opL_app. solve_sep_entails.
+Qed.
+
+Lemma envs_app_singleton_sound Δ Δ' p j Q :
+  envs_app p (Esnoc Enil j Q) Δ = Some Δ' → of_envs Δ ⊢ □?p Q -∗ of_envs Δ'.
+Proof. move=> /envs_app_sound. destruct p; by rewrite /= right_id. Qed.
+
+Lemma envs_simple_replace_sound' Δ Δ' i p Γ :
+  envs_simple_replace i p Γ Δ = Some Δ' →
+  of_envs (envs_delete true i p Δ) ⊢ (if p then □ [∧] Γ else [∗] Γ) -∗ of_envs Δ'.
+Proof.
+  rewrite /envs_simple_replace /envs_delete /of_envs=> ?.
+  apply pure_elim_l=> Hwf. destruct Δ as [Γp Γs], p; simplify_eq/=.
+  - destruct (env_app Γ Γs) eqn:Happ,
+      (env_replace i Γ Γp) as [Γp'|] eqn:?; simplify_eq/=.
+    apply wand_intro_l, and_intro; [apply pure_intro|].
+    + destruct Hwf; constructor; simpl; eauto using env_replace_wf.
+      intros j. apply (env_app_disjoint _ _ _ j) in Happ.
+      destruct (decide (i = j)); try naive_solver eauto using env_replace_fresh.
+    + rewrite (env_replace_perm _ _ Γp') //.
+      rewrite big_opL_app intuitionistically_and and_sep_intuitionistically.
+      solve_sep_entails.
+  - destruct (env_app Γ Γp) eqn:Happ,
+      (env_replace i Γ Γs) as [Γs'|] eqn:?; simplify_eq/=.
+    apply wand_intro_l, and_intro; [apply pure_intro|].
+    + destruct Hwf; constructor; simpl; eauto using env_replace_wf.
+      intros j. apply (env_app_disjoint _ _ _ j) in Happ.
+      destruct (decide (i = j)); try naive_solver eauto using env_replace_fresh.
+    + rewrite (env_replace_perm _ _ Γs') // big_opL_app. solve_sep_entails.
+Qed.
+
+Lemma envs_simple_replace_singleton_sound' Δ Δ' i p j Q :
+  envs_simple_replace i p (Esnoc Enil j Q) Δ = Some Δ' →
+  of_envs (envs_delete true i p Δ) ⊢ □?p Q -∗ of_envs Δ'.
+Proof. move=> /envs_simple_replace_sound'. destruct p; by rewrite /= right_id. Qed.
+
+Lemma envs_simple_replace_sound Δ Δ' i p P Γ :
+  envs_lookup i Δ = Some (p,P) → envs_simple_replace i p Γ Δ = Some Δ' →
+  of_envs Δ ⊢ □?p P ∗ ((if p then □ [∧] Γ else [∗] Γ) -∗ of_envs Δ').
+Proof. intros. by rewrite envs_lookup_sound// envs_simple_replace_sound'//. Qed.
+
+Lemma envs_simple_replace_maybe_sound Δ Δ' i p P Γ :
+  envs_lookup i Δ = Some (p,P) → envs_simple_replace i p Γ Δ = Some Δ' →
+  of_envs Δ ⊢ □?p P ∗ (((if p then □ [∧] Γ else [∗] Γ) -∗ of_envs Δ') ∧ (□?p P -∗ of_envs Δ)).
+Proof.
+  intros. apply pure_elim with (envs_wf Δ).
+  { rewrite of_envs_eq. apply and_elim_l. }
+  intros. rewrite {1}envs_lookup_sound//. apply sep_mono_r, and_intro.
+  - rewrite envs_simple_replace_sound'//.
+  - apply wand_intro_l, envs_lookup_sound_2; done.
+Qed.
+
+Lemma envs_simple_replace_singleton_sound Δ Δ' i p P j Q :
+  envs_lookup i Δ = Some (p,P) →
+  envs_simple_replace i p (Esnoc Enil j Q) Δ = Some Δ' →
+  of_envs Δ ⊢ □?p P ∗ (□?p Q -∗ of_envs Δ').
+Proof.
+  intros. by rewrite envs_lookup_sound// envs_simple_replace_singleton_sound'//.
+Qed.
+
+Lemma envs_replace_sound' Δ Δ' i p q Γ :
+  envs_replace i p q Γ Δ = Some Δ' →
+  of_envs (envs_delete true i p Δ) ⊢ (if q then □ [∧] Γ else [∗] Γ) -∗ of_envs Δ'.
+Proof.
+  rewrite /envs_replace; destruct (beq _ _) eqn:Hpq.
+  - apply eqb_prop in Hpq as ->. apply envs_simple_replace_sound'.
+  - apply envs_app_sound.
+Qed.
+
+Lemma envs_replace_singleton_sound' Δ Δ' i p q j Q :
+  envs_replace i p q (Esnoc Enil j Q) Δ = Some Δ' →
+  of_envs (envs_delete true i p Δ) ⊢ □?q Q -∗ of_envs Δ'.
+Proof. move=> /envs_replace_sound'. destruct q; by rewrite /= ?right_id. Qed.
+
+Lemma envs_replace_sound Δ Δ' i p q P Γ :
+  envs_lookup i Δ = Some (p,P) → envs_replace i p q Γ Δ = Some Δ' →
+  of_envs Δ ⊢ □?p P ∗ ((if q then □ [∧] Γ else [∗] Γ) -∗ of_envs Δ').
+Proof. intros. by rewrite envs_lookup_sound// envs_replace_sound'//. Qed.
+
+Lemma envs_replace_singleton_sound Δ Δ' i p q P j Q :
+  envs_lookup i Δ = Some (p,P) →
+  envs_replace i p q (Esnoc Enil j Q) Δ = Some Δ' →
+  of_envs Δ ⊢ □?p P ∗ (□?q Q -∗ of_envs Δ').
+Proof. intros. by rewrite envs_lookup_sound// envs_replace_singleton_sound'//. Qed.
+
+Lemma envs_lookup_envs_clear_spatial Δ j :
+  envs_lookup j (envs_clear_spatial Δ)
+  = ''(p,P) ← envs_lookup j Δ; if p : bool then Some (p,P) else None.
+Proof.
+  rewrite /envs_lookup /envs_clear_spatial.
+  destruct Δ as [Γp Γs]; simpl; destruct (Γp !! j) eqn:?; simplify_eq/=; auto.
+  by destruct (Γs !! j).
+Qed.
+
+Lemma envs_clear_spatial_sound Δ :
+  of_envs Δ ⊢ of_envs (envs_clear_spatial Δ) ∗ [∗] env_spatial Δ.
+Proof.
+  rewrite /of_envs /envs_clear_spatial /=. apply pure_elim_l=> Hwf.
+  rewrite right_id -persistent_and_sep_assoc. apply and_intro; [|done].
+  apply pure_intro. destruct Hwf; constructor; simpl; auto using Enil_wf.
+Qed.
+
+Lemma env_spatial_is_nil_intuitionistically Δ :
+  env_spatial_is_nil Δ = true → of_envs Δ ⊢ □ of_envs Δ.
+Proof.
+  intros. unfold of_envs; destruct Δ as [? []]; simplify_eq/=.
+  rewrite !right_id /bi_intuitionistically {1}affinely_and_r persistently_and.
+  by rewrite persistently_affinely_elim persistently_idemp persistently_pure.
+Qed.
+
+Lemma envs_lookup_envs_delete Δ i p P :
+  envs_wf Δ →
+  envs_lookup i Δ = Some (p,P) → envs_lookup i (envs_delete true i p Δ) = None.
+Proof.
+  rewrite /envs_lookup /envs_delete=> -[?? Hdisj] Hlookup.
+  destruct Δ as [Γp Γs], p; simplify_eq/=.
+  - rewrite env_lookup_env_delete //. revert Hlookup.
+    destruct (Hdisj i) as [->| ->]; [|done]. by destruct (Γs !! _).
+  - rewrite env_lookup_env_delete //. by destruct (Γp !! _).
+Qed.
+Lemma envs_lookup_envs_delete_ne Δ rp i j p :
+  i ≠ j → envs_lookup i (envs_delete rp j p Δ) = envs_lookup i Δ.
+Proof.
+  rewrite /envs_lookup /envs_delete=> ?. destruct Δ as [Γp Γs],p; simplify_eq/=.
+  - destruct rp=> //. by rewrite env_lookup_env_delete_ne.
+  - destruct (Γp !! i); simplify_eq/=; by rewrite ?env_lookup_env_delete_ne.
+Qed.
+
+Lemma envs_split_go_sound js Δ1 Δ2 Δ1' Δ2' :
+  (∀ j P, envs_lookup j Δ1 = Some (false, P) → envs_lookup j Δ2 = None) →
+  envs_split_go js Δ1 Δ2 = Some (Δ1',Δ2') →
+  of_envs Δ1 ∗ of_envs Δ2 ⊢ of_envs Δ1' ∗ of_envs Δ2'.
+Proof.
+  revert Δ1 Δ2.
+  induction js as [|j js IH]=> Δ1 Δ2 Hlookup HΔ; simplify_eq/=; [done|].
+  apply pure_elim with (envs_wf Δ1)=> [|Hwf].
+  { by rewrite /of_envs !and_elim_l sep_elim_l. }
+  destruct (envs_lookup_delete _ j Δ1)
+    as [[[[] P] Δ1'']|] eqn:Hdel; simplify_eq/=; auto.
+  apply envs_lookup_delete_Some in Hdel as [??]; subst.
+  rewrite envs_lookup_sound //; rewrite /= (comm _ P) -assoc.
+  rewrite -(IH _ _ _ HΔ); last first.
+   { intros j' P'; destruct (decide (j = j')) as [->|].
+     - by rewrite (envs_lookup_envs_delete _ _ _ P).
+     - rewrite envs_lookup_envs_delete_ne // envs_lookup_snoc_ne //. eauto. }
+  rewrite (envs_snoc_sound Δ2 false j P) /= ?wand_elim_r; eauto.
+Qed.
+Lemma envs_split_sound Δ d js Δ1 Δ2 :
+  envs_split d js Δ = Some (Δ1,Δ2) → of_envs Δ ⊢ of_envs Δ1 ∗ of_envs Δ2.
+Proof.
+  rewrite /envs_split=> ?. rewrite -(idemp bi_and (of_envs Δ)).
+  rewrite {2}envs_clear_spatial_sound.
+  rewrite (env_spatial_is_nil_intuitionistically (envs_clear_spatial _)) //.
+  rewrite -persistently_and_intuitionistically_sep_l.
+  rewrite (and_elim_l (<pers> _)%I)
+          persistently_and_intuitionistically_sep_r intuitionistically_elim.
+  destruct (envs_split_go _ _) as [[Δ1' Δ2']|] eqn:HΔ; [|done].
+  apply envs_split_go_sound in HΔ as ->; last first.
+  { intros j P. by rewrite envs_lookup_envs_clear_spatial=> ->. }
+  destruct d; simplify_eq/=; solve_sep_entails.
+Qed.
+
+Lemma prop_of_env_sound Γ : prop_of_env Γ ⊣⊢ [∗] Γ.
+Proof.
+  destruct Γ as [|Γ ? P]; simpl; first done.
+  revert P. induction Γ as [|Γ IH ? Q]=>P; simpl.
+  - by rewrite right_id.
+  - rewrite /= IH (comm _ Q _) assoc. done.
+Qed.
+
+Global Instance envs_Forall2_refl (R : relation PROP) :
+  Reflexive R → Reflexive (envs_Forall2 R).
+Proof. by constructor. Qed.
+Global Instance envs_Forall2_sym (R : relation PROP) :
+  Symmetric R → Symmetric (envs_Forall2 R).
+Proof. intros ??? [??]; by constructor. Qed.
+Global Instance envs_Forall2_trans (R : relation PROP) :
+  Transitive R → Transitive (envs_Forall2 R).
+Proof. intros ??? [??] [??] [??]; constructor; etrans; eauto. Qed.
+Global Instance envs_Forall2_antisymm (R R' : relation PROP) :
+  AntiSymm R R' → AntiSymm (envs_Forall2 R) (envs_Forall2 R').
+Proof. intros ??? [??] [??]; constructor; by eapply (anti_symm _). Qed.
+Lemma envs_Forall2_impl (R R' : relation PROP) Δ1 Δ2 :
+  envs_Forall2 R Δ1 Δ2 → (∀ P Q, R P Q → R' P Q) → envs_Forall2 R' Δ1 Δ2.
+Proof. intros [??] ?; constructor; eauto using env_Forall2_impl. Qed.
+
+Global Instance of_envs_mono : Proper (envs_Forall2 (⊢) ==> (⊢)) (@of_envs PROP).
+Proof.
+  intros [Γp1 Γs1] [Γp2 Γs2] [Hp Hs]; apply and_mono; simpl in *.
+  - apply pure_mono=> -[???]. constructor;
+      naive_solver eauto using env_Forall2_wf, env_Forall2_fresh.
+  - by repeat f_equiv.
+Qed.
+Global Instance of_envs_proper :
+  Proper (envs_Forall2 (⊣⊢) ==> (⊣⊢)) (@of_envs PROP).
+Proof.
+  intros Δ1 Δ2 HΔ; apply (anti_symm (⊢)); apply of_envs_mono;
+    eapply (envs_Forall2_impl (⊣⊢)); [| |symmetry|]; eauto using equiv_entails.
+Qed.
+Global Instance Envs_proper (R : relation PROP) :
+  Proper (env_Forall2 R ==> env_Forall2 R ==> eq ==> envs_Forall2 R) (@Envs PROP).
+Proof. by constructor. Qed.
+
+Global Instance envs_entails_proper :
+  Proper (envs_Forall2 (⊣⊢) ==> (⊣⊢) ==> iff) (@envs_entails PROP).
+Proof. rewrite envs_entails_eq. solve_proper. Qed.
+Global Instance envs_entails_flip_mono :
+  Proper (envs_Forall2 (⊢) ==> flip (⊢) ==> flip impl) (@envs_entails PROP).
+Proof. rewrite envs_entails_eq=> Δ1 Δ2 ? P1 P2 <- <-. by f_equiv. Qed.
+End envs.
-- 
GitLab