diff --git a/theories/Core/Soundness/EqualityCases.v b/theories/Core/Soundness/EqualityCases.v
index 52a1d76..3891855 100644
--- a/theories/Core/Soundness/EqualityCases.v
+++ b/theories/Core/Soundness/EqualityCases.v
@@ -169,7 +169,7 @@ Proof.
   simpl in *.
 
   repeat invert_glu_rel1.
-  clear_dups.
+  handle_functional_glu_univ_elem.
   saturate_glu_typ_from_el.
   unify_glu_univ_lvl i.
 
diff --git a/theories/Core/Soundness/LogicalRelation/Lemmas.v b/theories/Core/Soundness/LogicalRelation/Lemmas.v
index 56f4bf6..2e225bc 100644
--- a/theories/Core/Soundness/LogicalRelation/Lemmas.v
+++ b/theories/Core/Soundness/LogicalRelation/Lemmas.v
@@ -1026,7 +1026,7 @@ Ltac basic_invert_glu_ctx_env H :=
    destruct H as [? [? []]])
   + dependent destruction H.
 
-Ltac invert_glu_ctx_env H := basic_glu_ctx_env H.
+Ltac invert_glu_ctx_env H := basic_invert_glu_ctx_env H.
 
 Lemma glu_ctx_env_subtyp_sub_if : forall Γ Γ' Sb Sb' Δ σ ρ,
     {{ ⊢ Γ ⊆ Γ' }} ->