Move out the `bin_log_related_seq` lemma

theories/examples/various.v

@@ -6,23 +6,6 @@ From iris.proofmode Require Import tactics.
 From iris.algebra Require Import csum agree excl.
 From iris_logrel Require Import logrel.
 
-Lemma bin_log_related_seq `{logrelG Σ} τ1 E Δ Γ e1 e2 e1' e2' τ2
-`{Closed ∅ e2} `{Closed ∅ e2'} :
-  ↑logrelN ⊆ E →
-  {E,E;Δ;Γ} ⊨ e1 ≤log≤ e1' : τ1 -∗
-  {E,E;Δ;Γ} ⊨ e2 ≤log≤ e2' : τ2 -∗
-  {E,E;Δ;Γ} ⊨ (e1;; e2) ≤log≤ (e1';; e2') : τ2.
-Proof.
-  iIntros (?) "He1 He2".
-  rel_bind_l e1.
-  rel_bind_r e1'.
-  iApply (related_bind with "He1 [He2]").
-  iIntros (?) "? /=".
-  rel_rec_l.
-  rel_rec_r.
-  done.
-Qed.
-
 Section refinement.
   Context `{logrelG Σ}.
   Notation D := (prodC valC valC -n> iProp Σ).

theories/logrel/fundamental_binary.v

@@ -197,6 +197,22 @@ Section masked.
     iApply ("Ht" with "Hj").
   Qed.
 
+  Lemma bin_log_related_seq Δ Γ e1 e2 e1' e2' τ1 τ2 `{Closed ∅ e2} `{Closed ∅ e2'} :
+    ↑logrelN ⊆ E →
+    {E,E;Δ;Γ} ⊨ e1 ≤log≤ e1' : τ1 -∗
+    {E,E;Δ;Γ} ⊨ e2 ≤log≤ e2' : τ2 -∗
+    {E,E;Δ;Γ} ⊨ (e1;; e2) ≤log≤ (e1';; e2') : τ2.
+  Proof.
+    iIntros (?) "He1 He2".
+    rel_bind_l e1.
+    rel_bind_r e1'.
+    iApply (related_bind with "He1 [He2]").
+    iIntros (?) "? /=".
+    rel_rec_l.
+    rel_rec_r.
+    done.
+  Qed.
+
   Lemma bin_log_related_injl Δ Γ e e' τ1 τ2 :
     ↑ logrelN ⊆ E →
     {E,E;Δ;Γ} ⊨ e ≤log≤ e' : τ1 -∗