`interp_env` and `bin_log_related` are non-expansive (in Δ)

theories/logrel/logrel_binary.v

@@ -18,6 +18,10 @@ Section bin_log_def.
   Global Instance interp_env_persistent Γ E1 E2 Δ vvs :
     Persistent (interp_env Γ E1 E2 Δ vvs) := _.
 
+  Global Instance interp_env_ne n Γ E1 E2 :
+    Proper (dist n ==> (=) ==> dist n) (interp_env Γ E1 E2).
+  Proof. solve_proper. Qed.
+
   (* TODO: get rid of the box before interp_env? *)
   Definition bin_log_related_def (E1 E2 : coPset)
       (Δ : list D) (Γ : stringmap type)
@@ -30,6 +34,10 @@ Section bin_log_def.
   Definition bin_log_related := unseal bin_log_related_aux.
   Definition bin_log_related_eq : bin_log_related = bin_log_related_def :=
     seal_eq bin_log_related_aux.
+
+  Global Instance bin_log_related_ne E1 E2 n :
+    Proper (dist n ==> (=) ==> (=) ==> (=) ==> (=) ==> dist n) (bin_log_related E1 E2).
+  Proof. rewrite bin_log_related_eq. solve_proper. Qed.
 End bin_log_def.
 
 Notation "⟦ Γ ⟧*" := (interp_env Γ).