Typing rule for `Free`.

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") }
 ]

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]> Γ.