diff --git a/theories/BundledAlgorithmicTyping.v b/theories/BundledAlgorithmicTyping.v
index 57fe367..703390b 100644
--- a/theories/BundledAlgorithmicTyping.v
+++ b/theories/BundledAlgorithmicTyping.v
@@ -436,14 +436,12 @@ Section BundledConv.
       assert [Γ |-[de] M : U].
       {
         eapply algo_conv_wh in Hconv as [neM neN].
-        inversion HM ; subst ; clear HM.
-        all: solve [now inversion neM| assumption].
+        now eapply neutral_ty_inv.
       }
       assert [Γ |-[de] N : U].
       {
         eapply algo_conv_wh in Hconv as [neM neN].
-        inversion HN ; subst ; clear HN.
-        all: solve [now inversion neN| assumption].
+        now eapply neutral_ty_inv.
       }
       assert (well_typed (ta := de) Γ M) by now eexists.
       assert (well_typed (ta := de) Γ N) by now eexists.
diff --git a/theories/Decidability/Termination.v b/theories/Decidability/Termination.v
index e073710..931a83c 100644
--- a/theories/Decidability/Termination.v
+++ b/theories/Decidability/Termination.v
@@ -148,8 +148,7 @@ Proof.
     split.
     2: intros [|] ; cbn ; easy.
     eapply (IHM tt A) ; tea.
-    inversion Hty ; subst ; tea.
-    1-6:  inv_whne.
+    apply neutral_ty_inv in Hty; [|tea].
     now exists U.
   - intros * ???? ? ? wu' ?.
     apply compute_domain.
diff --git a/theories/TypeConstructorsInj.v b/theories/TypeConstructorsInj.v
index b9b6376..cbb66d3 100644
--- a/theories/TypeConstructorsInj.v
+++ b/theories/TypeConstructorsInj.v
@@ -594,6 +594,18 @@ Proof.
     * prod_splitter; tea; right; now eapply TypeTrans.
 Qed.
 
+Lemma neutral_ty_inv Γ A :
+  [Γ |- A] -> whne A -> [Γ |- A : U].
+Proof.
+  intros Hty Hne.
+  unshelve eapply TypeRefl, ty_conv_inj in Hty.
+  - now constructor.
+  - now constructor.
+  - cbn in *.
+    apply Fundamental in Hty; destruct Hty.
+    now eapply escapeTm.
+Qed.
+
 Lemma prod_ty_inv Γ A B :
   [Γ |- tProd A B] ->
   [Γ |- A] × [Γ,, A |- B].