diff --git a/theories/typing/interp.v b/theories/typing/interp.v
index aa03ce92face9894ab7ec1224aa65df9dad617fd..2845ffcf974a91657c318d4ea695e8045046ce76 100644
--- a/theories/typing/interp.v
+++ b/theories/typing/interp.v
@@ -39,7 +39,7 @@ Section semtypes.
     | TExists τ' => λne Δ, lrel_exists (λ τ, interp τ' (τ::Δ))
     | Tref τ => λne Δ, lrel_ref (interp τ Δ)
     end.
-  Solve Obligations with (intros I τ τ' n Δ Δ' HΔ' ??; solve_proper).
+  Solve Obligations with (intros I τ τ' n Δ Δ' HΔ' ??; try solve_proper).
   Next Obligation.
     intros I τ τ' n Δ Δ' HΔ' ??.
     apply lrel_rec_ne=> X /=.