From 909ddcabd0b83a7647aefbf283e730b7eee2cc38 Mon Sep 17 00:00:00 2001
From: Dan Frumin <dfrumin@cs.ru.nl>
Date: Fri, 12 Jun 2020 13:00:35 +0200
Subject: [PATCH] logrel_ctxequiv -> refines_sound_open

---
 theories/typing/soundness.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/typing/soundness.v b/theories/typing/soundness.v
index bd26acb..c7613a1 100644
--- a/theories/typing/soundness.v
+++ b/theories/typing/soundness.v
@@ -56,7 +56,7 @@ Proof.
   eapply logrel_adequate; eauto.
 Qed.
 
-Lemma logrel_ctxequiv Σ `{relocPreG Σ} Γ e e' τ :
+Lemma refines_sound_open Σ `{relocPreG Σ} Γ e e' τ :
   (∀ `{relocG Σ} Δ, ⊢ {⊤;Δ;Γ} ⊨ e ≤log≤ e' : τ) →
   Γ ⊨ e ≤ctx≤ e' : τ.
 Proof.
@@ -73,7 +73,7 @@ Lemma refines_sound Σ `{relocPreG Σ} e e' τ :
   (∀ `{relocG Σ} Δ, ⊢ REL e << e' : (interp τ Δ)) →
   ∅ ⊨ e ≤ctx≤ e' : τ.
 Proof.
-  intros Hlog. eapply logrel_ctxequiv. apply _.
+  intros Hlog. eapply refines_sound_open. apply _.
   iIntros (? Δ vs).
   rewrite fmap_empty env_ltyped2_empty_inv.
   iIntros (->).
-- 
GitLab