From be63a88847dc59aad8f1aa9cb2c509468c63dfd6 Mon Sep 17 00:00:00 2001 From: Andrej Dudenhefner Date: Wed, 8 May 2024 14:10:31 +0200 Subject: [PATCH] replace slow firstorder by appropriate constructor --- pcuic/theories/PCUICSR.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/pcuic/theories/PCUICSR.v b/pcuic/theories/PCUICSR.v index 862263758..74a55f889 100644 --- a/pcuic/theories/PCUICSR.v +++ b/pcuic/theories/PCUICSR.v @@ -1626,7 +1626,7 @@ Proof. - (* LetIn value *) assert (X1' : lift_typing typing Σ Γ (j_vdef na r b_ty)). - { unshelve eapply lift_judgment_SR with (1 := X1); tea. firstorder. } + { unshelve eapply lift_judgment_SR with (1 := X1); tea. now constructor; [|right]. } eapply type_Cumul_alt. econstructor; eauto. unshelve eapply (closed_context_conversion _ typeb'). pcuic. @@ -1639,7 +1639,7 @@ Proof. - (* LetIn type annotation *) assert (X1' : lift_typing typing Σ Γ (j_vdef na b r)). - { unshelve eapply lift_judgment_SR with (1 := X1); tea. firstorder. } + { unshelve eapply lift_judgment_SR with (1 := X1); tea. now constructor; [|left]. } eapply type_Cumul_alt. econstructor; eauto. unshelve eapply (closed_context_conversion _ typeb'). pcuic.