Work around COQBUG(rocq-prover/rocq#5481)

Author: JasonGross

pcuic/theories/PCUICExpandLetsCorrectness.v

@@ -1468,7 +1468,7 @@ Qed.
 Lemma OnOne2All_map2_map_all {A B I I'} {P} {i : list I} {l l' : list A} (g : B -> I -> I') (f : A -> B) :
   OnOne2All (fun i x y => P (g (f x) i) (f x) (f y)) i l l' -> OnOne2All P (map2 g (map f l) i) (map f l) (map f l').
 Proof.
-  induction 1; simpl; constructor; try congruence. len.
+  induction 1; simpl; constructor; try congruence; try assumption. len.
   now rewrite map2_length !map_length.
 Qed.
 
@@ -5545,4 +5545,4 @@ Proof.
   cbn in *.
   now eapply expanded_expand_lets in etat.
   Unshelve. all:eauto. destruct wfΣ; eauto.
-Qed.
+Qed.

pcuic/theories/PCUICParallelReduction.v

@@ -2220,7 +2220,7 @@ Section ParallelSubstitution.
         rewrite !inst_inst_case_context_wf //.
         eapply on_free_vars_ctx_inst_case_context; tea; solve_all.
         eapply pred1_pred1_ctx in X7.
-        eapply on_contexts_app_inv => //. now rewrite /id.
+        eapply on_contexts_app_inv => //. now rewrite /id; (* congruence is enough in monomorphic mode, but we have to work around COQBUG(https://github.com/coq/coq/issues/5481) *) cbv [pcontext] in *; repeat destruct ?; cbn in *; subst; assumption.
         eapply (on_contexts_length X).
         rewrite /id. rewrite {2}H1.
         apply: X6; tea. 3:now len.
@@ -2351,7 +2351,7 @@ Section ParallelSubstitution.
         rewrite !inst_inst_case_context_wf //.
         eapply on_free_vars_ctx_inst_case_context; tea; solve_all.
         eapply pred1_pred1_ctx in X3 => //.
-        eapply on_contexts_app_inv => //. now rewrite /id.
+        eapply on_contexts_app_inv => //. now rewrite /id; (* congruence is enough in monomorphic mode, but we have to work around COQBUG(https://github.com/coq/coq/issues/5481) *) cbv [pcontext] in *; repeat destruct ?; cbn in *; subst; assumption.
         eapply (on_contexts_length X). 2:len; lia.
         now rewrite {2}H0.
       + solve_all. rewrite /inst_case_branch_context in a1 *.

template-pcuic/theories/PCUICToTemplateCorrectness.v

@@ -1210,7 +1210,7 @@ Qed.
 Lemma OnOne2All_map2_map_all {A B I I'} {P} {i : list I} {l l' : list A} (g : B -> I -> I') (f : A -> B) :
   OnOne2All (fun i x y => P (g (f x) i) (f x) (f y)) i l l' -> OnOne2All P (map2 g (map f l) i) (map f l) (map f l').
 Proof.
-  induction 1; simpl; constructor; try congruence. len.
+  induction 1; simpl; constructor; try congruence; try assumption. len.
   now rewrite map2_length !map_length.
 Qed.