diff --git a/theories/examples/termination/logrel.v b/theories/examples/termination/logrel.v
index 8e171fc1e3e1ad54468515efe906b38d8ac5177c..a2a5dddb26b62ea07d5fea4189c9ebe000573c5c 100644
--- a/theories/examples/termination/logrel.v
+++ b/theories/examples/termination/logrel.v
@@ -520,9 +520,9 @@ Section semantic_model.
   Implicit Types (θ τ: gmap string val).
 
   Definition subst_cons δ X A := <[X := A]> δ.
-  Definition subst_ty (T: lptype) (X: string) U : lptype := λ δ, T (subst_cons δ X (U δ)).
+  Definition subst_ty (T: lptype) (X: string) (U: lptype) : lptype := λ δ, T (subst_cons δ X (U δ)).
   Definition well_formed Ω δ : iProp Σ := (⌜Ω ≡ dom (gset string) δ⌝)%I.
-  Definition well_formed_type Ω T : Prop := (∀ δ δ', (∀ X, X ∈ Ω → δ !! X = δ' !! X) → T δ = T δ').
+  Definition well_formed_type Ω T : Prop := (∀ δ δ', (∀ X, X ∈ Ω → δ !! X ≡ δ' !! X) → T δ ≡ T δ').
   Definition well_formed_ctx Ω Π : Prop := (∀ x T, Π !! x = Some T → well_formed_type Ω T).
   Definition env_lptyped Π δ θ : iProp Σ := (env_ltyped (fmap (λ T, T δ) Π) θ)%I.
   Definition lptyped Ω Π e T := ⊢ (∃ α, $ α -∗ ∀ δ, well_formed Ω δ -∗ ∀ θ, env_lptyped Π δ θ -∗ SEQ subst_map θ e [{ v, (T δ) v }])%I.
@@ -541,8 +541,8 @@ Section semantic_model.
   Definition lpput T : lptype := λ δ, lput (T δ).
   Definition lptensor T U : lptype := λ δ, ltensor (T δ) (U δ).
   Definition lparr T U : lptype := λ δ, larr (T δ) (U δ).
-  Definition lpforall X (T: lptype) : lptype := λ δ f, (∀ U, SEQ (f #()) [{ u, (subst_ty T X U) δ u }])%I.
-  Definition lpexists X (T: lptype) : lptype := λ δ v, (∃ U, (subst_ty T X U) δ v)%I.
+  Definition lpforall X (T: lptype) : lptype := λ δ f, (∀ U: lptype, SEQ (f #()) [{ u, (subst_ty T X U) δ u }])%I.
+  Definition lpexists X (T: lptype) : lptype := λ δ v, (∃ U: lptype, (subst_ty T X U) δ v)%I.
 
   Definition tlam e : expr := λ: <>, e.
   Definition tapp e : expr := e #().
@@ -593,7 +593,7 @@ Section semantic_model.
     iExists v; iSplit; auto.
     feed pose proof (Hwf _ _ HYB δ (<[X:=T δ]> δ)) as HB.
     { intros Z Hx'. assert (X ≠ Z) by  set_solver. by rewrite lookup_insert_ne. }
-    by erewrite HB.
+    by erewrite (HB v).
   Qed.
 
 
@@ -839,7 +839,7 @@ Section semantic_model.
       iApply (env_lptyped_update_type_map with "HΞ"); eauto.
     - feed pose proof (HwfU δ (<[X := (T' δ)]> δ)).
       { intros Z Hx'. assert (X ≠ Z) by set_solver. by rewrite lookup_insert_ne. }
-      iIntros (w) "[$ HU] !>". by rewrite -H.
+      iIntros (w) "[$ HU] !>". by rewrite -(H w).
   Qed.
 
 End polymorphic_logical_relation.