diff --git a/opam b/opam
index 48e78749cfdd63c5d46fc7e1c17cbf843046c166..92354b9360598c891f1778d36a2ca75cad49fda0 100644
--- a/opam
+++ b/opam
@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/actris" ]
 depends: [
-  "coq-iris" { (= "dev.2020-05-24.1.76bec8b7") | (= "dev") }
+  "coq-iris" { (= "dev.2020-05-26.1.d80e7abf") | (= "dev") }
 ]
diff --git a/theories/logrel/term_typing_rules.v b/theories/logrel/term_typing_rules.v
index 1f15a0c14283b0bb85289b1e595dd937fe11fe33..acf6978141998ee6aa857cdb15aca7bdc40d3f0a 100644
--- a/theories/logrel/term_typing_rules.v
+++ b/theories/logrel/term_typing_rules.v
@@ -271,6 +271,17 @@ Section properties.
     iExists l, v; iSplit=>//. iFrame "Hv Hl".
   Qed.
 
+  Lemma ltyped_free Γ1 Γ2 e A :
+    (Γ1 ⊨ e : ref_uniq A ⫤ Γ2) -∗
+    (Γ1 ⊨ Free e : () ⫤ Γ2).
+  Proof.
+    iIntros "#He" (vs) "!> HΓ1 /=".
+    wp_bind (subst_map vs e).
+    iApply (wp_wand with "(He HΓ1)"). iIntros (v) "[Hv HΓ2]".
+    iDestruct "Hv" as (l w ->) "[Hl Hw]".
+    wp_free. by iFrame "HΓ2".
+  Qed.
+
   Lemma ltyped_load Γ (x : string) A :
     Γ !! x = Some (ref_uniq A)%lty →
     ⊢ Γ ⊨ ! x : A ⫤ <[x := (ref_uniq (copy- A))%lty]> Γ.