Merge pull request #1154 from MetaCoq/cherry-picks-on-9.0

Cherry picks on 9.0

Author: mattam82

erasure/theories/EArities.v

@@ -858,7 +858,7 @@ Proof.
   eapply PCUICSpine.inversion_it_mkProd_or_LetIn in ty; eauto.
   epose proof (typing_spine_proofs _ _ [] _ _ _ [] _ _ wfΣ ty).
   forward H0 by constructor. eapply has_sort_isType; eauto.
-  simpl. now eapply has_sort_isType. eapply PCUICConversion.ws_cumul_pb_eq_le_gen, PCUICSR.wt_cumul_pb_refl; eauto.
+  simpl. now eapply has_sort_isType. eapply ws_cumul_eq_pb, PCUICSR.wt_cumul_pb_refl; eauto.
   destruct H0 as [_ sorts].
   specialize (sorts _ _ decli c) as [sorts sorts'].
   forward sorts' by constructor.

pcuic/theories/PCUICAlpha.v

@@ -338,7 +338,7 @@ Section Alpha.
     eapply eq_term_mkApps.
     - eapply eq_term_upto_univ_lift.
       rewrite /ptm /ptm'.
-      eapply eq_term_upto_univ_it_mkLambda_or_LetIn. tc.
+      eapply eq_term_upto_univ_it_mkLambda_or_LetIn; tc.
       eapply eq_context_upto_empty_impl; tea.
       eapply eq_term_upto_univ_empty_impl; tea; tc.
     - eapply All2_app.
@@ -425,7 +425,7 @@ Section Alpha.
     2:{ eapply All2_refl. reflexivity. }
     len. eapply eq_term_upto_univ_lift.
     eapply eq_term_upto_univ_impl; revgoals.
-    eapply eq_term_upto_univ_it_mkLambda_or_LetIn; tea.
+    eapply eq_term_upto_univ_it_mkLambda_or_LetIn; tea. 1,2: tc.
     reflexivity. lia. all:tc.
   Qed.
 

pcuic/theories/PCUICConfluence.v

@@ -834,7 +834,7 @@ Proof.
   ].
   (* tLambda and tProd *)
   idtac.
-  10,15:solve [
+  15:solve [
     dependent destruction e ;
     edestruct (IHh pb) as [? [? ?]] ; [ .. | tea | ] ; eauto;
     clear h;
@@ -857,16 +857,38 @@ Proof.
       eapply eq_term_upto_univ_leq ; eauto
     ]
   ].
+  10:solve [
+    dependent destruction e ;
+    edestruct (IHh Conv) as [? [? ?]] ; [ .. | tea | ] ; tc ; eauto;
+    clear h;
+    lazymatch goal with
+    | r : red1 _ (?Γ,, vass ?na ?A) ?u ?v,
+      e :  eq_term_upto_univ_napp _ _ _ _ _ ?A ?B
+      |- _ =>
+      let hh := fresh "hh" in
+      eapply red1_eq_context_upto_l in r as hh ; revgoals;
+      [ constructor ; [
+          eapply (eq_context_upto_refl _ _ _ Conv); eauto ; tc
+        | constructor; tea
+        ]
+      | tc ..];
+      destruct hh as [? [? ?]]
+    end;
+    eexists ; split; [ solve [ econstructor ; eauto ]
+    | constructor ; eauto ;
+      eapply eq_term_upto_univ_trans ; eauto ; tc
+    ]
+  ].
   - dependent destruction e. dependent destruction e1.
     eexists. split.
     + constructor.
     + eapply eq_term_upto_univ_substs ; eauto.
-      eapply leq_term_leq_term_napp; eauto.
+      eapply eq_term_upto_univ_leq; tea; eauto with arith.
   - dependent destruction e.
     eexists. split.
     + constructor.
     + eapply eq_term_upto_univ_substs ; try assumption.
-      eapply leq_term_leq_term_napp; eauto.
+      eapply eq_term_upto_univ_leq; tea; eauto with arith.
       auto.
   - dependent destruction e.
     eexists. split.
@@ -990,7 +1012,7 @@ Proof.
     + eapply eq_term_upto_univ_leq ; eauto.
       eapply eq_term_eq_term_napp; auto.
   - dependent destruction e.
-    edestruct IHh as [? [? ?]] ; [ .. | eassumption | ] ; eauto.
+    edestruct IHh as [? [? ?]] ; [ .. | eassumption | ] ; tc ; eauto.
     clear h.
     lazymatch goal with
     | r : red1 _ (?Γ,, vdef ?na ?a ?A) ?u ?v,
@@ -1010,7 +1032,6 @@ Proof.
     + eapply letin_red_body ; eauto.
     + constructor ; eauto.
       eapply eq_term_upto_univ_trans ; eauto ; tc.
-      eapply eq_term_upto_univ_leq ; eauto.
   - dependent destruction e.
     destruct e as [? [? [? ?]]].
     eapply OnOne2_prod_inv in X as [_ X].

pcuic/theories/PCUICConversion.v

@@ -2684,22 +2684,14 @@ Section ConvRedConv.
     Σ ;;; Γ ⊢ tCoFix mfix idx = tCoFix mfix' idx.
   Proof using wfΣ. eapply (ws_cumul_pb_fix_or_cofix (b:=false)). Qed.
 
-  Lemma ws_cumul_pb_eq_le_gen {pb Γ T U} :
-    Σ ;;; Γ ⊢ T = U ->
-    Σ ;;; Γ ⊢ T ≤[pb] U.
-  Proof using Type.
-    destruct pb => //.
-    eapply ws_cumul_pb_eq_le.
-  Qed.
-
   Lemma ws_cumul_pb_Lambda_l {Γ na A b na' A' pb} :
     eq_binder_annot na na' ->
     is_open_term (Γ ,, vass na A) b ->
     Σ ;;; Γ ⊢ A = A' ->
     Σ ;;; Γ ⊢ tLambda na A b ≤[pb] tLambda na' A' b.
   Proof using wfΣ.
     intros hna hb h.
-    eapply ws_cumul_pb_eq_le_gen.
+    eapply ws_cumul_eq_pb.
     eapply into_ws_cumul_pb.
     { clear -h hna; induction h.
       - constructor; constructor; auto; reflexivity.
@@ -2710,7 +2702,7 @@ Section ConvRedConv.
   Qed.
 
   Lemma ws_cumul_pb_Lambda_r {pb Γ na A b b'} :
-    Σ ;;; Γ,, vass na A ⊢ b ≤[pb] b' ->
+    Σ ;;; Γ,, vass na A ⊢ b ≤[Conv] b' ->
     Σ ;;; Γ ⊢ tLambda na A b ≤[pb] tLambda na A b'.
   Proof using wfΣ.
     intros h.
@@ -2736,9 +2728,10 @@ Section ConvRedConv.
     rewrite /on_free_vars_decl /test_decl => /andP[] /= onty ont onu onu'.
     eapply into_ws_cumul_pb => //.
     { clear -h. induction h.
-      - destruct pb;
-        eapply cumul_refl; constructor.
-        all: try reflexivity; auto.
+      - eapply cumul_red_l; pcuic.
+        eapply cumul_red_r; [|pcuic].
+        eapply cumul_refl.
+        apply eq_term_upto_univ_subst; trea; tc.
       - destruct pb;
         eapply cumul_red_l; tea; pcuic.
       - destruct pb;
@@ -2748,12 +2741,12 @@ Section ConvRedConv.
   Qed.
 
   Lemma ws_cumul_pb_it_mkLambda_or_LetIn_codom {Δ Γ u v pb} :
-      Σ ;;; (Δ ,,, Γ) ⊢ u ≤[pb] v ->
+      Σ ;;; (Δ ,,, Γ) ⊢ u ≤[Conv] v ->
       Σ ;;; Δ ⊢ it_mkLambda_or_LetIn Γ u ≤[pb] it_mkLambda_or_LetIn Γ v.
   Proof using wfΣ.
     intros h. revert Δ u v h.
     induction Γ as [| [na [b|] A] Γ ih ] ; intros Δ u v h.
-    - assumption.
+    - by apply ws_cumul_eq_pb.
     - simpl. cbn. eapply ih.
       eapply ws_cumul_pb_LetIn_bo. assumption.
     - simpl. cbn. eapply ih.
@@ -2791,7 +2784,7 @@ Section ConvRedConv.
   Lemma ws_cumul_pb_Lambda {pb Γ na1 na2 A1 A2 t1 t2} :
     eq_binder_annot na1 na2 ->
     Σ ;;; Γ ⊢ A1 = A2 ->
-    Σ ;;; Γ ,, vass na1 A1 ⊢ t1 ≤[pb] t2 ->
+    Σ ;;; Γ ,, vass na1 A1 ⊢ t1 ≤[Conv] t2 ->
     Σ ;;; Γ ⊢ tLambda na1 A1 t1 ≤[pb] tLambda na2 A2 t2.
   Proof using wfΣ.
     intros eqna X.
@@ -2805,7 +2798,7 @@ Section ConvRedConv.
   Lemma conv_cum_Lambda leq Γ na1 na2 A1 A2 t1 t2 :
     eq_binder_annot na1 na2 ->
     Σ ;;; Γ ⊢ A1 = A2 ->
-    sq_ws_cumul_pb leq Σ (Γ ,, vass na1 A1) t1 t2 ->
+    sq_ws_cumul_pb Conv Σ (Γ ,, vass na1 A1) t1 t2 ->
     sq_ws_cumul_pb leq Σ Γ (tLambda na1 A1 t1) (tLambda na2 A2 t2).
   Proof using wfΣ.
     intros eqna X []; sq. now apply ws_cumul_pb_Lambda.
@@ -2857,7 +2850,7 @@ Section ConvRedConv.
     intros hna ont ona onu.
     etransitivity.
     { eapply ws_cumul_pb_LetIn_bo; tea. }
-    eapply ws_cumul_pb_eq_le_gen.
+    eapply ws_cumul_eq_pb.
     etransitivity.
     { eapply ws_cumul_pb_LetIn_ty; tea; eauto with fvs. }
     eapply ws_cumul_pb_LetIn_tm; tea; eauto with fvs.
@@ -2866,12 +2859,13 @@ Section ConvRedConv.
 
   Lemma ws_cumul_pb_it_mkLambda_or_LetIn {pb Γ Δ1 Δ2 t1 t2} :
     Σ ⊢ Γ ,,, Δ1 = Γ ,,, Δ2 ->
-    Σ ;;; Γ ,,, Δ1 ⊢ t1 ≤[pb] t2 ->
+    Σ ;;; Γ ,,, Δ1 ⊢ t1 = t2 ->
     Σ ;;; Γ ⊢ it_mkLambda_or_LetIn Δ1 t1 ≤[pb] it_mkLambda_or_LetIn Δ2 t2.
   Proof using wfΣ.
     induction Δ1 in Δ2, t1, t2 |- *; intros X Y.
     - apply All2_fold_length in X.
       destruct Δ2; cbn in *; [trivial|].
+      1: by apply ws_cumul_eq_pb.
       rewrite length_app in X; lia.
     - apply All2_fold_length in X as X'.
       destruct Δ2 as [|c Δ2]; simpl in *; [rewrite length_app in X'; lia|].
@@ -2916,7 +2910,7 @@ Section ConvRedConv.
   Lemma ws_cumul_pb_Lambda_inv :
     forall pb Γ na1 na2 A1 A2 b1 b2,
       Σ ;;; Γ ⊢ tLambda na1 A1 b1 ≤[pb] tLambda na2 A2 b2 ->
-      [× eq_binder_annot na1 na2, Σ ;;; Γ ⊢ A1 = A2 & Σ ;;; Γ ,, vass na1 A1 ⊢ b1 ≤[pb] b2].
+      [× eq_binder_annot na1 na2, Σ ;;; Γ ⊢ A1 = A2 & Σ ;;; Γ ,, vass na1 A1 ⊢ b1 = b2].
   Proof using wfΣ.
     intros *.
     move/ws_cumul_pb_red; intros (v & v' & [redv redv' eq]).
@@ -2951,7 +2945,7 @@ Section ConvRedConv.
   Lemma Lambda_conv_cum_inv :
     forall leq Γ na1 na2 A1 A2 b1 b2,
       sq_ws_cumul_pb leq Σ Γ (tLambda na1 A1 b1) (tLambda na2 A2 b2) ->
-      eq_binder_annot na1 na2 /\ ∥ Σ ;;; Γ ⊢ A1 = A2 ∥ /\ sq_ws_cumul_pb leq Σ (Γ ,, vass na1 A1) b1 b2.
+      eq_binder_annot na1 na2 /\ ∥ Σ ;;; Γ ⊢ A1 = A2 ∥ /\ sq_ws_cumul_pb Conv Σ (Γ ,, vass na1 A1) b1 b2.
   Proof using wfΣ.
     intros * []. eapply ws_cumul_pb_Lambda_inv in X as [].
     intuition auto. all:sq; auto.
@@ -3257,7 +3251,7 @@ Section ConvSubst.
       move: clctx. rewrite on_free_vars_ctx_app !app_context_length H => /andP[] //. }
     etransitivity.
     * eapply untyped_substitution_ws_cumul_pb; tea. fvs.
-    * eapply ws_cumul_pb_eq_le_gen.
+    * eapply ws_cumul_eq_pb.
       eapply (untyped_substitution_ws_cumul_pb_subst_conv (Δ := Γ0) (Δ' := Γ1)); tea; eauto.
   Qed.
 
@@ -3557,7 +3551,7 @@ Qed.
 
 Lemma ws_cumul_pb_rel_it_mkLambda_or_LetIn {cf pb Σ} {wfΣ : wf Σ} (Δ Γ Γ' : context) (B B' : term) :
   ws_cumul_ctx_pb_rel Conv Σ Δ Γ Γ' ->
-  Σ ;;; Δ ,,, Γ ⊢ B ≤[pb] B' ->
+  Σ ;;; Δ ,,, Γ ⊢ B = B' ->
   Σ ;;; Δ ⊢ it_mkLambda_or_LetIn Γ B ≤[pb] it_mkLambda_or_LetIn Γ' B'.
 Proof.
   move/ws_cumul_ctx_pb_rel_app => hc hb.
@@ -3687,7 +3681,7 @@ Section CumulSubst.
     Σ ;;; Γ ,,, subst_context s 0 Γ' ⊢ subst s #|Γ'| b ≤[pb] subst s' #|Γ'| b.
   Proof using wfΣ.
     move=> cl cl' clb eqsub subs subs'.
-    eapply ws_cumul_pb_eq_le_gen.
+    eapply ws_cumul_eq_pb.
     eapply substitution_ws_cumul_pb_subst_conv; tea; eauto with pcuic.
   Qed.
 
@@ -3957,7 +3951,7 @@ Proof.
       eapply (ws_cumul_pb_refl' (exist Γ _) (exist t _)) end.
   all: intros Γ pb; revert Γ.
   - intros; etransitivity; eauto.
-  - intros. apply ws_cumul_pb_eq_le_gen. apply symmetry.
+  - intros. apply ws_cumul_eq_pb. apply symmetry.
     eauto.
   - intros Γ t; intros. unshelve eapply (ws_cumul_pb_refl' (exist Γ _) (exist t _)); eauto.
   - intros Γ ev args args' Hargsargs' Hargsargs'_dep HΓ Hargs Hargs'. cbn in *. eapply ws_cumul_pb_Evar; eauto.
@@ -3979,7 +3973,7 @@ Proof.
   - intros Γ na na' t t' ty ty' u u' Hna _ Heqtt' _ Heqtyty' _ Hequu' HΓ HM HN.
     cbn in *. apply andb_andI in HM; apply andb_andI in HN; destruct HM as [Ht Htyu]; destruct HN as [Ht' Htyu'].
     apply andb_andI in Htyu; apply andb_andI in Htyu'; destruct Htyu as [Hty Hu]; destruct Htyu' as [Hty' Hu'].
-    eapply ws_cumul_pb_LetIn; eauto. eapply Hequu'; eauto.
+    eapply ws_cumul_pb_LetIn; eauto. apply ws_cumul_eq_pb. eapply Hequu'; eauto.
     * change (is_closed_context (Γ,, vdef na t ty)). rewrite on_free_vars_ctx_snoc. apply andb_and. split; eauto.
       rewrite /on_free_vars_decl /test_decl. apply andb_and. split; eauto.
     * rewrite shiftnP_S; eauto.
@@ -3989,7 +3983,7 @@ Proof.
     apply andb_andI in H; apply andb_andI in H'; destruct H as [Hreturn H]; destruct H' as [Hreturn' H'].
     apply andb_andI in H; apply andb_andI in H'; destruct H as [Hcontext H]; destruct H' as [Hcontext' H'].
     apply andb_andI in H; apply andb_andI in H'; destruct H as [Hc Hbrs]; destruct H' as [Hc' Hbrs'].
-    eapply ws_cumul_pb_eq_le_gen. eapply ws_cumul_pb_Case; eauto.
+    eapply ws_cumul_eq_pb. eapply ws_cumul_pb_Case; eauto.
     * rewrite is_open_case_split. repeat (apply andb_and; split); eauto.
     * rewrite is_open_case_split. repeat (apply andb_and; split); eauto.
     * unfold cumul_predicate in Hpp'. unfold ws_cumul_pb_predicate. destruct Hpp' as [Hpp' [Hinst [Hpcon Hpret]]].
@@ -4018,7 +4012,7 @@ Proof.
         rewrite <- length_app in *. tea.
   - intros; eapply ws_cumul_pb_Proj_c; eauto.
   - intros Γ mfix mfix' idx Hmfixmfix' Hmfixmfix'_dep HΓ H H'. cbn in *.
-    eapply ws_cumul_pb_eq_le_gen. eapply ws_cumul_pb_Fix; eauto. repeat toAll.
+    eapply ws_cumul_eq_pb. eapply ws_cumul_pb_Fix; eauto. repeat toAll.
     eapply All2_impl. 1: tea. cbn; intros; destruct_head'_prod.
     pose proof (Hfix := All2_length ltac:(eassumption)).
     unfold test_def in *; repeat toProp; destruct_head'_and.
@@ -4028,7 +4022,7 @@ Proof.
     * rewrite -> shiftnP_add, <- fix_context_length, <- length_app in *; tea.
     * rewrite -> shiftnP_add, <- Hfix, <- fix_context_length, <- length_app in *; tea.
   - intros Γ mfix mfix' idx Hmfixmfix' Hmfixmfix'_dep HΓ H H'. cbn in *.
-    eapply ws_cumul_pb_eq_le_gen. eapply ws_cumul_pb_CoFix; eauto. repeat toAll.
+    eapply ws_cumul_eq_pb. eapply ws_cumul_pb_CoFix; eauto. repeat toAll.
     eapply All2_impl. 1: tea. pose proof (Hfix := All2_length ltac:(eassumption)); cbn; intros. destruct_head'_prod.
     unfold test_def in *.
     repeat toProp; destruct_head'_and.

pcuic/theories/PCUICCumulativitySpec.v

@@ -115,7 +115,7 @@ Inductive cumulSpec0 {cf : checker_flags} (Σ : global_env_ext) Γ (pb : conv_pb
 | cumul_Lambda : forall na na' ty ty' t t',
     eq_binder_annot na na' ->
     Σ ;;; Γ ⊢ ty ≤s[Conv] ty' ->
-    Σ ;;; Γ ,, vass na ty ⊢ t ≤s[pb] t' ->
+    Σ ;;; Γ ,, vass na ty ⊢ t ≤s[Conv] t' ->
     Σ ;;; Γ ⊢ tLambda na ty t ≤s[pb] tLambda na' ty' t'
 
 | cumul_Prod : forall na na' a a' b b',
@@ -128,7 +128,7 @@ Inductive cumulSpec0 {cf : checker_flags} (Σ : global_env_ext) Γ (pb : conv_pb
     eq_binder_annot na na' ->
     Σ ;;; Γ ⊢ t ≤s[Conv] t' ->
     Σ ;;; Γ ⊢ ty ≤s[Conv] ty' ->
-    Σ ;;; Γ ,, vdef na t ty ⊢ u ≤s[pb] u' ->
+    Σ ;;; Γ ,, vdef na t ty ⊢ u ≤s[Conv] u' ->
     Σ ;;; Γ ⊢ tLetIn na t ty u ≤s[pb] tLetIn na' t' ty' u'
 
 | cumul_Case indn : forall p p' c c' brs brs',
@@ -358,7 +358,7 @@ Lemma cumulSpec0_rect :
     (forall (Γ : context) (pb : conv_pb) (na na' : aname) (ty ty' t t' : term)
             (Hna : eq_binder_annot na na')
             (Hty : cumulSpec0 Σ Γ Conv ty ty') (_ : P cf Σ Γ Conv ty ty' Hty)
-            (Ht : cumulSpec0 Σ (Γ ,, vass na ty) pb t t') ( _ : P cf Σ (Γ ,, vass na ty) pb t t' Ht),
+            (Ht : cumulSpec0 Σ (Γ ,, vass na ty) Conv t t') ( _ : P cf Σ (Γ ,, vass na ty) Conv t t' Ht),
         P cf Σ Γ pb (tLambda na ty t) (tLambda na' ty' t')
           (cumul_Lambda _ _ _ _ _ _ _ _ _ Hna Hty Ht)) ->
 
@@ -373,7 +373,7 @@ Lemma cumulSpec0_rect :
             (Hna : eq_binder_annot na na')
             (Ht : cumulSpec0 Σ Γ Conv t t') (_ : P cf Σ Γ Conv t t' Ht)
             (Hty : cumulSpec0 Σ Γ Conv ty ty') (_ : P cf Σ Γ Conv ty ty' Hty)
-            (Hu : cumulSpec0 Σ (Γ,, vdef na t ty) pb u u') (_ : P cf Σ (Γ,, vdef na t ty) pb u u' Hu),
+            (Hu : cumulSpec0 Σ (Γ,, vdef na t ty) Conv u u') (_ : P cf Σ (Γ,, vdef na t ty) Conv u u' Hu),
         P cf Σ Γ pb (tLetIn na t ty u) (tLetIn na' t' ty' u')
           (cumul_LetIn _ _ _ _ _ _ _ _ _ _ _ Hna Ht Hty Hu)) ->
 

pcuic/theories/PCUICEquality.v

@@ -437,7 +437,7 @@ Inductive eq_term_upto_univ_napp Σ
 | eq_Lambda : forall na na' ty ty' t t',
     eq_binder_annot na na' ->
     Σ ⊢ ty <==[ Conv , 0 ] ty' ->
-    Σ ⊢ t <==[ pb , 0 ] t' ->
+    Σ ⊢ t <==[ Conv , 0 ] t' ->
     Σ ⊢ tLambda na ty t <==[ pb , napp ] tLambda na' ty' t'
 
 | eq_Prod : forall na na' a a' b b',
@@ -450,7 +450,7 @@ Inductive eq_term_upto_univ_napp Σ
     eq_binder_annot na na' ->
     Σ ⊢ t <==[ Conv , 0 ] t' ->
     Σ ⊢ ty <==[ Conv , 0 ] ty' ->
-    Σ ⊢ u <==[ pb , 0 ] u' ->
+    Σ ⊢ u <==[ Conv , 0 ] u' ->
     Σ ⊢ tLetIn na t ty u <==[ pb , napp ] tLetIn na' t' ty' u'
 
 | eq_Case : forall indn p p' c c' brs brs',
@@ -1688,19 +1688,22 @@ Proof.
 Qed.
 
 Lemma eq_term_upto_univ_it_mkLambda_or_LetIn Σ cmp_universe cmp_sort pb :
-  Proper (eq_context_upto Σ cmp_universe cmp_sort Conv ==> eq_term_upto_univ Σ cmp_universe cmp_sort pb ==> eq_term_upto_univ Σ cmp_universe cmp_sort pb) it_mkLambda_or_LetIn.
+  RelationClasses.subrelation (cmp_universe Conv) (cmp_universe pb) ->
+  RelationClasses.subrelation (cmp_sort Conv) (cmp_sort pb) ->
+  Proper (eq_context_upto Σ cmp_universe cmp_sort Conv ==> eq_term_upto_univ Σ cmp_universe cmp_sort Conv ==> eq_term_upto_univ Σ cmp_universe cmp_sort pb) it_mkLambda_or_LetIn.
 Proof.
-  intros Γ Δ eq u v h.
+  intros ?? Γ Δ eq u v h.
   induction eq in u, v, h |- *.
-  - assumption.
+  - cbn.
+    eapply eq_term_upto_univ_leq; trea.
   - simpl. cbn. apply IHeq => //.
     destruct p; cbn; constructor ; tas; try reflexivity.
 Qed.
 
-Lemma eq_term_upto_univ_it_mkLambda_or_LetIn_r Σ cmp_universe cmp_sort pb Γ :
+Lemma eq_term_upto_univ_it_mkLambda_or_LetIn_r Σ cmp_universe cmp_sort Γ :
   RelationClasses.Reflexive (cmp_universe Conv) ->
   RelationClasses.Reflexive (cmp_sort Conv) ->
-  respectful (eq_term_upto_univ Σ cmp_universe cmp_sort pb) (eq_term_upto_univ Σ cmp_universe cmp_sort pb)
+  respectful (eq_term_upto_univ Σ cmp_universe cmp_sort Conv) (eq_term_upto_univ Σ cmp_universe cmp_sort Conv)
              (it_mkLambda_or_LetIn Γ) (it_mkLambda_or_LetIn Γ).
 Proof.
   intros univ_refl sort_refl u v h.
@@ -1719,10 +1722,10 @@ Proof.
   apply eq_term_upto_univ_it_mkLambda_or_LetIn_r; exact _.
 Qed.
 
-Lemma eq_term_upto_univ_it_mkProd_or_LetIn Σ cmp_universe cmp_sort pb Γ :
+Lemma eq_term_upto_univ_it_mkProd_or_LetIn Σ cmp_universe cmp_sort Γ :
   RelationClasses.Reflexive (cmp_universe Conv) ->
   RelationClasses.Reflexive (cmp_sort Conv) ->
-  respectful (eq_term_upto_univ Σ cmp_universe cmp_sort pb) (eq_term_upto_univ Σ cmp_universe cmp_sort pb)
+  respectful (eq_term_upto_univ Σ cmp_universe cmp_sort Conv) (eq_term_upto_univ Σ cmp_universe cmp_sort Conv)
              (it_mkProd_or_LetIn Γ) (it_mkProd_or_LetIn Γ).
 Proof.
   intros univ_refl sort_refl u v h.