diff --git a/theories/logic/model.v b/theories/logic/model.v
index a46721f3354d2623a7f4fbeec5abca7f18a6a448..53373432f6a71417f996580538cbf86e7245ec15 100644
--- a/theories/logic/model.v
+++ b/theories/logic/model.v
@@ -113,6 +113,11 @@ Section semtypes.
   Definition lty2_exists (C : lty2 Σ → lty2 Σ) : lty2 Σ := Lty2 (λ w1 w2,
     ∃ A, C A w1 w2)%I.
 
+  Definition lty2_forall (C : lty2 Σ → lty2 Σ) : lty2 Σ := Lty2 (λ w1 w2,
+    □ ∀ A : lty2 Σ, (lty2_arr lty2_unit (C A))%lty2 w1 w2)%I.
+
+  Definition lty2_true : lty2 Σ := Lty2 (λ w1 w2, True)%I.
+
   (** The lty2 constructors are non-expansive *)
   Global Instance lty2_prod_ne n : Proper (dist n ==> dist n ==> dist n) lty2_prod.
   Proof. solve_proper. Qed.
@@ -147,6 +152,8 @@ Infix "+" := lty2_sum : lty_scope.
 Notation "'ref' A" := (lty2_ref A) : lty_scope.
 Notation "∃ A1 .. An , C" :=
   (lty2_exists (λ A1, .. (lty2_exists (λ An, C%lty2)) ..)) : lty_scope.
+Notation "∀ A1 .. An , C" :=
+  (lty2_forall (λ A1, .. (lty2_forall (λ An, C%lty2)) ..)) : lty_scope.
 
 Section semtypes_properties.
   Context `{relocG Σ}.
diff --git a/theories/typing/interp.v b/theories/typing/interp.v
index 1ff154fcf3cab603555b3690c7c8fd432ce57a39..2dca5f7db887b55a06ce2bb05d13df89ee0dbff2 100644
--- a/theories/typing/interp.v
+++ b/theories/typing/interp.v
@@ -10,15 +10,6 @@ From Autosubst Require Import Autosubst.
 (** * Interpretation of types *)
 Section semtypes.
   Context `{relocG Σ}.
-  (** Type-level lambdas are interpreted as closures *)
-  (** DF: lty2_forall is defined here because it depends on TApp *)
-  Definition lty2_forall (C : lty2 Σ → lty2 Σ) : lty2 Σ := Lty2 (λ w1 w2,
-    □ ∀ A : lty2 Σ, (() → C A)%lty2 w1 w2)%I.
-  Lemma lty2_forall_spec (C : lty2 Σ → lty2 Σ) w1 w2 :
-    lty2_forall C w1 w2 -∗ ∀ A, (() → C A)%lty2 w1 w2.
-  Proof. eauto with iFrame. Qed.
-
-  Definition lty2_true : lty2 Σ := Lty2 (λ w1 w2, True)%I.
 
   Program Definition ctx_lookup (x : var) : listC (lty2C Σ) -n> (lty2C Σ)
     := λne Δ, (from_option id lty2_true (Δ !! x))%I.
@@ -71,7 +62,7 @@ Section semtypes.
     interp τ Δ v v' -∗ ⌜v = v'⌝.
   Proof.
     intros HÏ„; revert v v'; induction HÏ„; iIntros (v v') "#H1 /=".
-    - by iDestruct "H1" as "[% %]"; subst.
+    - by iDestruct "H1" as %[-> ->].
     - by iDestruct "H1" as (n) "[% %]"; subst.
     - by iDestruct "H1" as (b) "[% %]"; subst.
     - iDestruct "H1" as (?? ??) "[% [% [H1 H2]]]"; simplify_eq/=.
@@ -85,9 +76,6 @@ Section semtypes.
   Qed.
 End semtypes.
 
-Notation "∀ A1 .. An , C" :=
-  (lty2_forall (λ A1, .. (lty2_forall (λ An, C%lty2)) ..)) : lty_scope.
-
 (** ** Properties of the type inrpretation w.r.t. the substitutions *)
 Section interp_ren.
   Context `{relocG Σ}.
@@ -190,7 +178,7 @@ Section env_typed.
   (** Substitution [vs] is well-typed w.r.t. [Γ] *)
   Definition env_ltyped2 (Γ : gmap string (lty2 Σ))
     (vs : gmap string (val*val)) : iProp Σ :=
-    (⌜ ∀ x, is_Some (Γ !! x) ↔ is_Some (vs !! x) ⌝ ∧ (* TODO why not equality of `dom`s? *)
+    (⌜ ∀ x, is_Some (Γ !! x) ↔ is_Some (vs !! x) ⌝ ∧
     [∗ map] i ↦ Avv ∈ map_zip Γ vs, lty2_car Avv.1 Avv.2.1 Avv.2.2)%I.
 
   Notation "⟦ Γ ⟧*" := (env_ltyped2 Γ).