Remove unneeded problematic universe constraints

MetaCoq · Sep 3, 2024 · 734acd2 · 734acd2
1 parent b1b6be2
commit 734acd2
Showing 1 changed file with 11 additions and 1 deletion.
diff --git a/pcuic/theories/PCUICConfluence.v b/pcuic/theories/PCUICConfluence.v
@@ -1403,6 +1403,16 @@ Proof.
     eapply eq_term_upto_univ_napp_flip; [..|eassumption]; tc.
 Qed.
 
+Lemma flip_PreOrder {A} (R : A -> A -> Prop) :
+  RelationClasses.PreOrder R ->
+  RelationClasses.PreOrder (flip R).
+Proof.
+  intro H.
+  split.
+  - apply H.
+  - intros x y z  r r'. eapply H. all: eassumption.
+Qed.
+
 Lemma red1_eq_term_upto_univ_r {Σ Σ' cmp_universe cmp_sort pb napp Γ u v u'} :
   RelationClasses.PreOrder (cmp_universe Conv) ->
   RelationClasses.PreOrder (cmp_universe pb) ->
@@ -1420,7 +1430,7 @@ Lemma red1_eq_term_upto_univ_r {Σ Σ' cmp_universe cmp_sort pb napp Γ u v u'}
 Proof.
   intros preorder_univ_conv preorder_sort_pb preorder_sort_conv preoder_sort_pb sub_univ sub_sort hsubst_univ hsubst_sort_conv hsubst_sort_pb h uv.
   destruct (@red1_eq_term_upto_univ_l Σ Σ' (fun pb => flip (cmp_universe pb)) (fun pb => flip (cmp_sort pb)) pb napp Γ u v u') as (v' & r & e).
-  all: eauto using RelationClasses.flip_PreOrder.
+  all: eauto using flip_PreOrder.
   1,2: intros ??; unfold flip; cbn; eauto.
   - red. intros s u1 u2 ru.
     eapply cmp_universe_instance_flip in ru; cbnr.