From df606e637fa06baf14073ae49823d2e5d531128c Mon Sep 17 00:00:00 2001
From: Dan Frumin <dfrumin@cs.ru.nl>
Date: Thu, 31 Jan 2019 15:35:50 +0100
Subject: [PATCH] Fix bin_log_related_tlam

---
 theories/logic/model.v        | 10 ++++++++++
 theories/typing/fundamental.v |  4 ++--
 2 files changed, 12 insertions(+), 2 deletions(-)

diff --git a/theories/logic/model.v b/theories/logic/model.v
index 56c8e1c..7dcfb67 100644
--- a/theories/logic/model.v
+++ b/theories/logic/model.v
@@ -163,6 +163,16 @@ Proof.
   - admit.
 Admitted.
 
+(* Hmmm *)
+Instance env_ltyped2_proper `{relocG Σ} :
+  Proper ((≡) ==> (=) ==> (≡)) env_ltyped2.
+Proof.
+  intros Γ Γ' HΓ ? vvs ->.
+  apply equiv_dist=>n.
+  setoid_rewrite equiv_dist in HΓ.
+  by rewrite HΓ.
+Qed.
+
 Section refinement.
   Context `{relocG Σ}.
 
diff --git a/theories/typing/fundamental.v b/theories/typing/fundamental.v
index f7dac05..5e1137c 100644
--- a/theories/typing/fundamental.v
+++ b/theories/typing/fundamental.v
@@ -298,12 +298,12 @@ Section fundamental.
     iModIntro. tp_pure j _. wp_pures. iExists _; iFrame.
     iIntros (A). iDestruct ("H" $! A) as "#H". iAlways.
     iSpecialize ("H" $! vvs with "Hs [HΓ]"); auto.
-    { rewrite -map_fmap_compose /=. admit. }
+    { by rewrite (interp_ren A Δ Γ). }
     iIntros (j' K') "Hj". iModIntro.
     wp_pures. tp_pure j' _.
     iMod ("H" $! j' K' with "Hj") as "H".
     iApply "H".
-  Admitted.
+  Qed.
 
   Lemma bin_log_related_alloc Δ Γ e e' τ :
     ({Δ;Γ} ⊨ e ≤log≤ e' : τ) -∗
-- 
GitLab