| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (19204 entries) |
| Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (228 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (298 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1273 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (313 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (8163 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1514 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (52 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (352 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (534 entries) |
| Instance Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (727 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (402 entries) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (333 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (4833 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (182 entries) |
R (lemma)
rebuild_wf_env_irr [in MetaRocq.ErasurePlugin.ErasureCorrectness]redl_context_trans [in MetaRocq.PCUIC.PCUICReduction]
redl_context_impl [in MetaRocq.PCUIC.PCUICReduction]
redl_preserve [in MetaRocq.PCUIC.PCUICReduction]
reduced_proj_body_whne [in MetaRocq.SafeChecker.PCUICSafeConversion]
reduced_case_discriminee_whne [in MetaRocq.SafeChecker.PCUICSafeConversion]
reduce_to_ind_complete [in MetaRocq.SafeChecker.PCUICSafeReduce]
reduce_to_prod_complete [in MetaRocq.SafeChecker.PCUICSafeReduce]
reduce_to_sort_complete [in MetaRocq.SafeChecker.PCUICSafeReduce]
reduce_term_complete [in MetaRocq.SafeChecker.PCUICSafeReduce]
reduce_stack_whnf [in MetaRocq.SafeChecker.PCUICSafeReduce]
reduce_stack_prop [in MetaRocq.SafeChecker.PCUICSafeReduce]
reduce_term_sound [in MetaRocq.SafeChecker.PCUICSafeReduce]
reduce_stack_noLamApp [in MetaRocq.SafeChecker.PCUICSafeReduce]
reduce_stack_noApp [in MetaRocq.SafeChecker.PCUICSafeReduce]
reduce_stack_isred [in MetaRocq.SafeChecker.PCUICSafeReduce]
reduce_stack_context [in MetaRocq.SafeChecker.PCUICSafeReduce]
reduce_stack_decompose [in MetaRocq.SafeChecker.PCUICSafeReduce]
reduce_stack_sound [in MetaRocq.SafeChecker.PCUICSafeReduce]
reduce_stack_Req [in MetaRocq.SafeChecker.PCUICSafeReduce]
reduce_to_ind_irrel [in MetaRocq.SafeChecker.PCUICRetypingEnvIrrelevance]
reduce_to_sort_irrel [in MetaRocq.SafeChecker.PCUICRetypingEnvIrrelevance]
reduce_to_prod_irrel [in MetaRocq.SafeChecker.PCUICRetypingEnvIrrelevance]
reducible_head_None [in MetaRocq.SafeChecker.PCUICSafeConversion]
reducible_head_decompose [in MetaRocq.SafeChecker.PCUICSafeConversion]
reducible_head_cored [in MetaRocq.SafeChecker.PCUICSafeConversion]
reducible_head_red_zippx [in MetaRocq.SafeChecker.PCUICSafeConversion]
reducible_head_red_zipp [in MetaRocq.SafeChecker.PCUICSafeConversion]
red_terms_on_free_vars [in MetaRocq.PCUIC.PCUICNormal]
red_ctx_rel_subst [in MetaRocq.PCUIC.PCUICNormal]
red_it_mkProd_or_LetIn_smash_context [in MetaRocq.Erasure.Typed.Erasure]
red_conv_conv_inv [in MetaRocq.PCUIC.PCUICCumulativity]
red_conv_conv [in MetaRocq.PCUIC.PCUICCumulativity]
red_conv [in MetaRocq.PCUIC.PCUICCumulativity]
red_cumul_cumul_inv [in MetaRocq.PCUIC.PCUICCumulativity]
red_cumul_cumul [in MetaRocq.PCUIC.PCUICCumulativity]
red_cumul_inv [in MetaRocq.PCUIC.PCUICCumulativity]
red_cumul [in MetaRocq.PCUIC.PCUICCumulativity]
red_ctx_app_context_l [in MetaRocq.PCUIC.PCUICSR]
red_ctx_clos_rt_red1_ctx [in MetaRocq.PCUIC.PCUICSR]
red_terms_refl [in MetaRocq.PCUIC.PCUICSR]
red_one_decl_ws_cumul_ctx_pb [in MetaRocq.PCUIC.PCUICSR]
red_one_decl_red_context [in MetaRocq.PCUIC.PCUICSR]
red_one_decl_red_ctx [in MetaRocq.PCUIC.PCUICSR]
red_welltyped [in MetaRocq.SafeChecker.PCUICSafeReduce]
red_red [in MetaRocq.PCUIC.PCUICSubstitution]
red_letin_alt [in MetaRocq.PCUIC.PCUICSubstitution]
red_abs_alt [in MetaRocq.PCUIC.PCUICSubstitution]
red_expand_let [in MetaRocq.PCUIC.PCUICSpine]
red_zipc [in MetaRocq.PCUIC.PCUICSafeLemmata]
red_cored_cored [in MetaRocq.PCUIC.PCUICSafeLemmata]
red_welltyped [in MetaRocq.PCUIC.PCUICSafeLemmata]
red_neq_cored [in MetaRocq.PCUIC.PCUICSafeLemmata]
red_const [in MetaRocq.PCUIC.PCUICSafeLemmata]
red_cored_or_eq [in MetaRocq.PCUIC.PCUICSafeLemmata]
red_ws_cumul_pb_inv [in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
red_ws_cumul_pb [in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
red_ws_cumul_pb_right [in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
red_ws_cumul_pb_left [in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
red_conv [in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
red_is_open_term [in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
red_decl_refl [in MetaRocq.PCUIC.PCUICContextConversion]
red_red_ctx_inv' [in MetaRocq.PCUIC.PCUICContextConversion]
red_red_ctx_inv [in MetaRocq.PCUIC.PCUICContextConversion]
red_compare_term_r [in MetaRocq.PCUIC.PCUICContextConversion]
red_compare_term_l [in MetaRocq.PCUIC.PCUICContextConversion]
red_ctx_closed_right [in MetaRocq.PCUIC.PCUICContextConversion]
red_ctx_closed_left [in MetaRocq.PCUIC.PCUICContextConversion]
red_ctx_ws_cumul_ctx_pb [in MetaRocq.PCUIC.PCUICContextConversion]
red_ctx_on_free_vars_term [in MetaRocq.PCUIC.PCUICContextConversion]
red_red_ctx [in MetaRocq.PCUIC.PCUICContextConversion]
red_red_ctx_aux' [in MetaRocq.PCUIC.PCUICContextConversion]
red_red_ctx' [in MetaRocq.PCUIC.PCUICContextConversion]
red_ctx_on_free_vars [in MetaRocq.PCUIC.PCUICContextConversion]
red_ctx_app [in MetaRocq.PCUIC.PCUICContextConversion]
red_ctx_skip [in MetaRocq.PCUIC.PCUICContextConversion]
red_confluence [in MetaRocq.PCUIC.PCUICConfluence]
red_ws_red_left [in MetaRocq.PCUIC.PCUICConfluence]
red_mkApps_tConst_axiom [in MetaRocq.PCUIC.PCUICConfluence]
red_mkApps_tRel [in MetaRocq.PCUIC.PCUICConfluence]
red_mkApps_tInd [in MetaRocq.PCUIC.PCUICConfluence]
red_mkApps_tConstruct [in MetaRocq.PCUIC.PCUICConfluence]
red_ctx_red_ctx_alpha_trans [in MetaRocq.PCUIC.PCUICConfluence]
red_eq_context_upto_names [in MetaRocq.PCUIC.PCUICConfluence]
red_context_trans [in MetaRocq.PCUIC.PCUICConfluence]
red_ctx_red_context [in MetaRocq.PCUIC.PCUICConfluence]
red_ws_red [in MetaRocq.PCUIC.PCUICConfluence]
red_ctx_clos_rt_red1_ctx [in MetaRocq.PCUIC.PCUICConfluence]
red_trans_clos_pred1 [in MetaRocq.PCUIC.PCUICConfluence]
red_pred [in MetaRocq.PCUIC.PCUICConfluence]
red_pred' [in MetaRocq.PCUIC.PCUICConfluence]
red_eq_context_upto_r [in MetaRocq.PCUIC.PCUICConfluence]
red_eq_context_upto_l [in MetaRocq.PCUIC.PCUICConfluence]
red_eq_term_upto_univ_r [in MetaRocq.PCUIC.PCUICConfluence]
red_eq_term_upto_univ_l [in MetaRocq.PCUIC.PCUICConfluence]
red_expand_lets_ctx [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
red_context_rel_conv_extended_subst [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
red_terms_lift [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
red_context_rel_assumptions [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
red_expand_lets [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
red_subst_instance [in MetaRocq.PCUIC.PCUICInductiveInversion]
red_betas_typed [in MetaRocq.PCUIC.PCUICConversion]
red_betas [in MetaRocq.PCUIC.PCUICConversion]
red_betas0 [in MetaRocq.PCUIC.PCUICConversion]
red_terms_evar [in MetaRocq.PCUIC.PCUICConversion]
red_rel_all [in MetaRocq.PCUIC.PCUICConversion]
red_fix_or_cofix_body [in MetaRocq.PCUIC.PCUICConversion]
red_terms_ws_cumul_pb_terms [in MetaRocq.PCUIC.PCUICConversion]
red_rename [in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
red_on_free_vars [in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
red_vdefs_tProd [in MetaRocq.ErasurePlugin.ErasureCorrectness]
red_ctx_rel_red_context_rel [in MetaRocq.PCUIC.PCUICContextReduction]
red_context_rel_inv [in MetaRocq.PCUIC.PCUICContextReduction]
red_context_app_right [in MetaRocq.PCUIC.PCUICContextReduction]
red_context_trans [in MetaRocq.PCUIC.PCUICContextReduction]
red_context_rel_on_ctx_free_vars [in MetaRocq.PCUIC.PCUICContextReduction]
red_context_on_ctx_free_vars [in MetaRocq.PCUIC.PCUICContextReduction]
red_context_app_same_left [in MetaRocq.PCUIC.PCUICContextReduction]
red_context_app [in MetaRocq.PCUIC.PCUICContextReduction]
red_red_ctx [in MetaRocq.PCUIC.PCUICContextReduction]
red_context_app_same [in MetaRocq.PCUIC.PCUICContextReduction]
red_context_refl [in MetaRocq.PCUIC.PCUICContextReduction]
red_decls_refl [in MetaRocq.PCUIC.PCUICContextReduction]
red_prod_alt [in MetaRocq.PCUIC.PCUICContextReduction]
red_it_mkProd_or_LetIn_mkApps_Ind [in MetaRocq.PCUIC.PCUICInductives]
red_it_mkProd_or_LetIn_smash [in MetaRocq.PCUIC.PCUICInductives]
red_destInd [in MetaRocq.PCUIC.PCUICInductives]
red_zippx [in MetaRocq.PCUIC.PCUICReduction]
red_zipp [in MetaRocq.PCUIC.PCUICReduction]
red_context_zip [in MetaRocq.PCUIC.PCUICReduction]
red_atom [in MetaRocq.PCUIC.PCUICReduction]
red_evar [in MetaRocq.PCUIC.PCUICReduction]
red_one_evar [in MetaRocq.PCUIC.PCUICReduction]
red_prod [in MetaRocq.PCUIC.PCUICReduction]
red_prod_r [in MetaRocq.PCUIC.PCUICReduction]
red_prod_l [in MetaRocq.PCUIC.PCUICReduction]
red_primArray_congr [in MetaRocq.PCUIC.PCUICReduction]
red_primArray_type [in MetaRocq.PCUIC.PCUICReduction]
red_primArray_default [in MetaRocq.PCUIC.PCUICReduction]
red_primArray_value [in MetaRocq.PCUIC.PCUICReduction]
red_primArray_one_value [in MetaRocq.PCUIC.PCUICReduction]
red_cofix_congr [in MetaRocq.PCUIC.PCUICReduction]
red_cofix_body [in MetaRocq.PCUIC.PCUICReduction]
red_cofix_one_body [in MetaRocq.PCUIC.PCUICReduction]
red_cofix_ty [in MetaRocq.PCUIC.PCUICReduction]
red_cofix_one_ty [in MetaRocq.PCUIC.PCUICReduction]
red_fix_congr [in MetaRocq.PCUIC.PCUICReduction]
red_fix_body [in MetaRocq.PCUIC.PCUICReduction]
red_fix_one_body [in MetaRocq.PCUIC.PCUICReduction]
red_fix_ty [in MetaRocq.PCUIC.PCUICReduction]
red_fix_one_ty [in MetaRocq.PCUIC.PCUICReduction]
red_proj_c [in MetaRocq.PCUIC.PCUICReduction]
red_it_mkProd_or_LetIn [in MetaRocq.PCUIC.PCUICReduction]
red_it_mkLambda_or_LetIn [in MetaRocq.PCUIC.PCUICReduction]
red_case [in MetaRocq.PCUIC.PCUICReduction]
red_case_brs [in MetaRocq.PCUIC.PCUICReduction]
red_one_brs_red_brs [in MetaRocq.PCUIC.PCUICReduction]
red_case_one_brs [in MetaRocq.PCUIC.PCUICReduction]
red_case_c [in MetaRocq.PCUIC.PCUICReduction]
red_case_p [in MetaRocq.PCUIC.PCUICReduction]
red_case_pars [in MetaRocq.PCUIC.PCUICReduction]
red_one_param [in MetaRocq.PCUIC.PCUICReduction]
red_letin [in MetaRocq.PCUIC.PCUICReduction]
red_mkApps [in MetaRocq.PCUIC.PCUICReduction]
red_mkApps_f [in MetaRocq.PCUIC.PCUICReduction]
red_app [in MetaRocq.PCUIC.PCUICReduction]
red_app_r [in MetaRocq.PCUIC.PCUICReduction]
red_abs [in MetaRocq.PCUIC.PCUICReduction]
red_one_decl_red_ctx_rel [in MetaRocq.PCUIC.PCUICReduction]
red_one_context_redl [in MetaRocq.PCUIC.PCUICReduction]
red_ctx_congr [in MetaRocq.PCUIC.PCUICReduction]
red_contextual_closure_equiv [in MetaRocq.PCUIC.PCUICReduction]
red_contextual_closure [in MetaRocq.PCUIC.PCUICReduction]
red_trans [in MetaRocq.PCUIC.PCUICReduction]
red_step [in MetaRocq.PCUIC.PCUICReduction]
red_cumul_prop [in MetaRocq.PCUIC.PCUICCumulProp]
red_conv_prop [in MetaRocq.PCUIC.PCUICCumulProp]
red_upto_conv_ctx_prop [in MetaRocq.PCUIC.PCUICCumulProp]
red_it_mkProd_or_LetIn_smash [in MetaRocq.PCUIC.PCUICClassification]
red_ctx_rel_par_conv [in MetaRocq.PCUIC.PCUICConvCumInversion]
red_case_isproof [in MetaRocq.Erasure.EArities]
red_conv_cum_r [in MetaRocq.SafeChecker.PCUICSafeConversion]
red_conv_cum_l [in MetaRocq.SafeChecker.PCUICSafeConversion]
red_on_free_vars [in MetaRocq.PCUIC.Typing.PCUICClosedTyp]
Red1Apps.isLambda_red1 [in MetaRocq.PCUIC.PCUICEtaExpand]
Red1Apps.red_tApp [in MetaRocq.PCUIC.PCUICEtaExpand]
Red1Apps.red1_ind_all [in MetaRocq.PCUIC.PCUICEtaExpand]
red1_mkApps_tCoFix_inv [in MetaRocq.PCUIC.PCUICNormal]
red1_mkApps_tFix_inv [in MetaRocq.PCUIC.PCUICNormal]
red1_mkApps_tInd_inv [in MetaRocq.PCUIC.PCUICNormal]
red1_mkApps_tConstruct_inv [in MetaRocq.PCUIC.PCUICNormal]
red1_mkApps_r [in MetaRocq.Template.Reduction]
red1_mkApps_l [in MetaRocq.Template.Reduction]
red1_mkApp [in MetaRocq.Template.Reduction]
red1_tApp_mkApp [in MetaRocq.Template.Reduction]
red1_tApp_mkApps_l [in MetaRocq.Template.Reduction]
red1_red_ctx [in MetaRocq.PCUIC.PCUICSR]
red1_ctx_app [in MetaRocq.PCUIC.PCUICSR]
red1_it_mkLambda_or_LetIn_ctx [in MetaRocq.PCUIC.PCUICSR]
red1_is_open_term [in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
red1_red_ctx_aux [in MetaRocq.PCUIC.PCUICContextConversion]
red1_red_ctxP_app [in MetaRocq.PCUIC.PCUICContextConversion]
red1_confluent [in MetaRocq.PCUIC.PCUICConfluence]
red1_eq_context_upto_names [in MetaRocq.PCUIC.PCUICConfluence]
red1_rel_alpha_red1_rel_inv [in MetaRocq.PCUIC.PCUICConfluence]
red1_rel_alpha_red1_rel [in MetaRocq.PCUIC.PCUICConfluence]
red1_rel_alpha_pred1_rel_alpha [in MetaRocq.PCUIC.PCUICConfluence]
red1_ctx_on_free_vars [in MetaRocq.PCUIC.PCUICConfluence]
red1_ctx_pred1_ctx [in MetaRocq.PCUIC.PCUICConfluence]
red1_weak_confluence [in MetaRocq.PCUIC.PCUICConfluence]
red1_pred1 [in MetaRocq.PCUIC.PCUICConfluence]
red1_eq_term_upto_univ_r [in MetaRocq.PCUIC.PCUICConfluence]
red1_eq_context_upto_r [in MetaRocq.PCUIC.PCUICConfluence]
red1_eq_term_upto_univ_l [in MetaRocq.PCUIC.PCUICConfluence]
red1_eq_context_upto_univ_l [in MetaRocq.PCUIC.PCUICConfluence]
red1_eq_context_upto_l [in MetaRocq.PCUIC.PCUICConfluence]
red1_conv [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
red1_cumul_inv [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
red1_cumul [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
red1_cumulSpec [in MetaRocq.PCUIC.PCUICConversion]
red1_red1apps [in MetaRocq.PCUIC.PCUICEtaExpand]
red1_rename [in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
red1_red_ctx [in MetaRocq.PCUIC.PCUICContextReduction]
red1_ind_all [in MetaRocq.Template.Typing]
red1_it_mkProd_or_LetIn_smash [in MetaRocq.PCUIC.PCUICInductives]
red1_destInd [in MetaRocq.PCUIC.PCUICInductives]
red1_zippx [in MetaRocq.PCUIC.PCUICReduction]
red1_zipp [in MetaRocq.PCUIC.PCUICReduction]
red1_context [in MetaRocq.PCUIC.PCUICReduction]
red1_fill_context_hole [in MetaRocq.PCUIC.PCUICReduction]
red1_it_mkProd_or_LetIn [in MetaRocq.PCUIC.PCUICReduction]
red1_it_mkLambda_or_LetIn [in MetaRocq.PCUIC.PCUICReduction]
red1_mkApps_r [in MetaRocq.PCUIC.PCUICReduction]
red1_mkApps_f [in MetaRocq.PCUIC.PCUICReduction]
red1_red [in MetaRocq.PCUIC.PCUICReduction]
red1_ind_all [in MetaRocq.PCUIC.PCUICReduction]
red1_upto_conv_ctx_prop [in MetaRocq.PCUIC.PCUICCumulProp]
red1_isLambda [in MetaRocq.Template.TypingWf]
red1_subst_instance [in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
red1_alpha_eq [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
red1_conv [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
red1_cumul_inv [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
red1_cumul [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
red1_inst [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
red1_on_free_vars [in MetaRocq.PCUIC.Typing.PCUICClosedTyp]
reference_impl_env_iter_pop_eq [in MetaRocq.ErasurePlugin.ETransform]
reference_impl_env_iter_pop_eq' [in MetaRocq.ErasurePlugin.ETransform]
reference_pop_decls_correct [in MetaRocq.SafeChecker.PCUICWfEnvImpl]
refine_red1_Γ [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
refine_red1_r [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
refine_pred [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
refine_red1_Γ [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
refine_red1_r [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
refine_red1_Γ [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
refine_red1_r [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
reflectEq_andb_right [in MetaRocq.PCUIC.Syntax.PCUICReflect]
reflectEq_andb_left [in MetaRocq.PCUIC.Syntax.PCUICReflect]
reflectEq_andb_3 [in MetaRocq.PCUIC.Syntax.PCUICReflect]
reflectEq_andb [in MetaRocq.PCUIC.Syntax.PCUICReflect]
reflectProp_sigma_simpl [in MetaRocq.PCUIC.Syntax.PCUICReflect]
reflectProp_noConfusion [in MetaRocq.PCUIC.Syntax.PCUICReflect]
reflectProp_equiv [in MetaRocq.PCUIC.Syntax.PCUICReflect]
reflectProp_reflect [in MetaRocq.Utils.ReflectEq]
reflectT_change_left4 [in MetaRocq.SafeChecker.PCUICEqualityDec]
reflectT_change_left3 [in MetaRocq.SafeChecker.PCUICEqualityDec]
reflectT_change_left2 [in MetaRocq.SafeChecker.PCUICEqualityDec]
reflectT_pred2 [in MetaRocq.Utils.MRReflect]
reflectT_pred [in MetaRocq.Utils.MRReflect]
reflectT_subrelation' [in MetaRocq.Utils.MRReflect]
reflectT_subrelation [in MetaRocq.Utils.MRReflect]
reflectT_change_left [in MetaRocq.Utils.MRReflect]
reflectT_reflect [in MetaRocq.Utils.MRReflect]
reflectT_forallb [in MetaRocq.Erasure.EPrimitive]
reflect_equiv [in MetaRocq.Utils.ByteCompareSpec]
reflect_eq_term [in MetaRocq.SafeChecker.PCUICEqualityDec]
reflect_leq_term [in MetaRocq.SafeChecker.PCUICEqualityDec]
reflect_eqb_termp_napp [in MetaRocq.SafeChecker.PCUICEqualityDec]
reflect_eqb_ctx_gen [in MetaRocq.SafeChecker.PCUICEqualityDec]
reflect_eqb_decl_gen [in MetaRocq.SafeChecker.PCUICEqualityDec]
reflect_eq_term_upto_univ [in MetaRocq.SafeChecker.PCUICEqualityDec]
reflect_eq_context_upto_names [in MetaRocq.SafeChecker.PCUICEqualityDec]
reflect_eq_decl_upto_names [in MetaRocq.SafeChecker.PCUICEqualityDec]
reflect_cmp_global_instance [in MetaRocq.SafeChecker.PCUICEqualityDec]
reflect_cmp_global_instance' [in MetaRocq.SafeChecker.PCUICEqualityDec]
reflect_cmp_universe_instance_variance [in MetaRocq.SafeChecker.PCUICEqualityDec]
reflect_cmp_universe_instance [in MetaRocq.SafeChecker.PCUICEqualityDec]
reflect_reflectT [in MetaRocq.Utils.MRReflect]
reflect_option_default [in MetaRocq.Utils.MROption]
reflect_prop_context_decl [in MetaRocq.PCUIC.Syntax.PCUICReflect]
reflect_prop_list [in MetaRocq.PCUIC.Syntax.PCUICReflect]
reflect_reflectProp_2 [in MetaRocq.Utils.ReflectEq]
reflect_reflectProp_1 [in MetaRocq.Utils.ReflectEq]
reflect_reflectProp [in MetaRocq.Utils.ReflectEq]
refl_red [in MetaRocq.PCUIC.PCUICReduction]
relation_equivalence_inclusion [in MetaRocq.Utils.MRRelations]
reln_set_binder_name [in MetaRocq.PCUIC.PCUICSR]
reln_subst [in MetaRocq.PCUIC.PCUICSpine]
reln_alt_eq [in MetaRocq.PCUIC.utils.PCUICAstUtils]
reln_list_lift_above [in MetaRocq.PCUIC.utils.PCUICAstUtils]
reln_length [in MetaRocq.PCUIC.utils.PCUICAstUtils]
reln_lift [in MetaRocq.PCUIC.PCUICContexts]
reln_acc [in MetaRocq.PCUIC.PCUICContexts]
reln_app [in MetaRocq.PCUIC.PCUICContexts]
removelast_length [in MetaRocq.PCUIC.utils.PCUICAstUtils]
remove_last_last [in MetaRocq.Utils.MRList]
remove_last_app [in MetaRocq.Utils.MRList]
remove_match_on_box_correct [in MetaRocq.Erasure.Typed.OptimizePropDiscr]
remove_match_on_box_trans_env [in MetaRocq.Erasure.Typed.ExtractionCorrectness]
remove_match_on_box_env_lemma [in MetaRocq.Erasure.Typed.ExtractionCorrectness]
remove_match_on_box_env_expanded_fix [in MetaRocq.Erasure.EOptimizePropDiscr]
remove_match_on_box_expanded_fix_decl_irrel [in MetaRocq.Erasure.EOptimizePropDiscr]
remove_match_on_box_expanded_fix_decl [in MetaRocq.Erasure.EOptimizePropDiscr]
remove_match_on_box_expanded_fix_irrel [in MetaRocq.Erasure.EOptimizePropDiscr]
remove_match_on_box_expanded_fix [in MetaRocq.Erasure.EOptimizePropDiscr]
remove_match_on_box_env_wf [in MetaRocq.Erasure.EOptimizePropDiscr]
remove_match_on_box_decl_wf [in MetaRocq.Erasure.EOptimizePropDiscr]
remove_match_on_box_wellformed_decl_irrel [in MetaRocq.Erasure.EOptimizePropDiscr]
remove_match_on_box_env_expanded [in MetaRocq.Erasure.EOptimizePropDiscr]
remove_match_on_box_env_eq [in MetaRocq.Erasure.EOptimizePropDiscr]
remove_match_on_box_extends_env [in MetaRocq.Erasure.EOptimizePropDiscr]
remove_match_on_box_env_extends' [in MetaRocq.Erasure.EOptimizePropDiscr]
remove_match_on_box_wellformed_irrel [in MetaRocq.Erasure.EOptimizePropDiscr]
remove_match_on_box_wellformed [in MetaRocq.Erasure.EOptimizePropDiscr]
remove_match_on_box_expanded_decl_irrel [in MetaRocq.Erasure.EOptimizePropDiscr]
remove_match_on_box_expanded_decl [in MetaRocq.Erasure.EOptimizePropDiscr]
remove_match_on_box_expanded_irrel [in MetaRocq.Erasure.EOptimizePropDiscr]
remove_match_on_box_expanded [in MetaRocq.Erasure.EOptimizePropDiscr]
remove_match_on_box_correct [in MetaRocq.Erasure.EOptimizePropDiscr]
remove_match_on_box_nth [in MetaRocq.Erasure.EOptimizePropDiscr]
remove_match_on_box_cunfold_cofix [in MetaRocq.Erasure.EOptimizePropDiscr]
remove_match_on_box_cunfold_fix [in MetaRocq.Erasure.EOptimizePropDiscr]
remove_match_on_box_cofix_subst [in MetaRocq.Erasure.EOptimizePropDiscr]
remove_match_on_box_fix_subst [in MetaRocq.Erasure.EOptimizePropDiscr]
remove_match_on_box_iota_red [in MetaRocq.Erasure.EOptimizePropDiscr]
remove_match_on_box_substl [in MetaRocq.Erasure.EOptimizePropDiscr]
remove_match_on_box_csubst [in MetaRocq.Erasure.EOptimizePropDiscr]
remove_match_on_box_mkApps [in MetaRocq.Erasure.EOptimizePropDiscr]
remove_last_length' [in MetaRocq.Erasure.EWcbvEval]
remove_last_length [in MetaRocq.Erasure.EWcbvEval]
rename_telescope [in MetaRocq.PCUIC.Bidirectional.BDStrengthening]
rename_context_on_free_vars [in MetaRocq.PCUIC.Conversion.PCUICOnFreeVarsConv]
rename_on_free_vars [in MetaRocq.PCUIC.Conversion.PCUICOnFreeVarsConv]
rename_ext_cond [in MetaRocq.PCUIC.Conversion.PCUICOnFreeVarsConv]
rename_prim_type [in MetaRocq.PCUIC.Typing.PCUICRenameTyp]
rename_telescope_cons [in MetaRocq.PCUIC.Typing.PCUICRenameTyp]
rename_telescope_shiftn0 [in MetaRocq.PCUIC.Typing.PCUICRenameTyp]
rename_subst_telescope [in MetaRocq.PCUIC.Typing.PCUICRenameTyp]
rename_wf_cofixpoint [in MetaRocq.PCUIC.Typing.PCUICRenameTyp]
rename_wf_fixpoint [in MetaRocq.PCUIC.Typing.PCUICRenameTyp]
rename_check_one_cofix [in MetaRocq.PCUIC.Typing.PCUICRenameTyp]
rename_check_one_fix [in MetaRocq.PCUIC.Typing.PCUICRenameTyp]
rename_smash_context [in MetaRocq.PCUIC.Typing.PCUICRenameTyp]
rename_app_context [in MetaRocq.PCUIC.Typing.PCUICRenameTyp]
rename_decompose_prod_assum [in MetaRocq.PCUIC.Typing.PCUICRenameTyp]
rename_predicate_preturn [in MetaRocq.PCUIC.Typing.PCUICRenameTyp]
rename_case_branch_type [in MetaRocq.PCUIC.Typing.PCUICRenameTyp]
rename_case_predicate_context [in MetaRocq.PCUIC.Typing.PCUICRenameTyp]
rename_ind_predicate_context [in MetaRocq.PCUIC.Typing.PCUICRenameTyp]
rename_iota_red [in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
rename_extended_subst [in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
rename_predicate_set_preturn [in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
rename_predicate_set_pparams [in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
rename_compose [in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
rename_wf_branches [in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
rename_wf_branch [in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
rename_wf_predicate [in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
rename_it_mkProd_or_LetIn [in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
rename_mkProd_or_LetIn [in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
rename_it_mkLambda_or_LetIn [in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
rename_mkLambda_or_LetIn [in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
rename_closed_constructor_body [in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
rename_case_branch_context_gen [in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
rename_cstr_branch_context [in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
rename_inst_case_context_wf [in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
rename_inst_case_context [in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
rename_context_set_binder_name [in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
rename_to_extended_list [in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
rename_reln [in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
rename_cstr_args [in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
rename_context_subst_k [in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
rename_context_subst_instance [in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
rename_inds [in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
rename_context_lift [in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
rename_shiftnk [in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
rename_context_subst [in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
rename_subst [in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
rename_unfold_cofix [in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
rename_unfold_fix [in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
rename_closed_extended_subst [in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
rename_closedn_terms [in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
rename_closedn_ctx [in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
rename_closed_decl [in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
rename_closed [in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
rename_closedn [in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
rename_fix_context [in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
rename_context_decl_body [in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
rename_context_nth_error [in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
rename_subst10 [in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
rename_subst0 [in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
rename_context_telescope [in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
rename_context_alt [in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
rename_context_snoc [in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
rename_context_snoc0 [in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
rename_subst_instance [in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
rename_mkApps [in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
rename_context_length [in MetaRocq.PCUIC.PCUICSigmaCalculus]
rename_subst_compose3 [in MetaRocq.PCUIC.PCUICSigmaCalculus]
rename_subst_compose2 [in MetaRocq.PCUIC.PCUICSigmaCalculus]
rename_subst_compose1 [in MetaRocq.PCUIC.PCUICSigmaCalculus]
rename_idsn_idsn [in MetaRocq.PCUIC.PCUICSigmaCalculus]
rename_inst_assoc [in MetaRocq.PCUIC.PCUICSigmaCalculus]
rename_ren_id [in MetaRocq.PCUIC.PCUICSigmaCalculus]
rename_inst [in MetaRocq.PCUIC.PCUICSigmaCalculus]
rename_shiftn [in MetaRocq.PCUIC.PCUICSigmaCalculus]
rename_branches_rename_branches [in MetaRocq.PCUIC.PCUICSigmaCalculus]
rename_branch_rename_branch [in MetaRocq.PCUIC.PCUICSigmaCalculus]
rename_predicate_rename_predicate [in MetaRocq.PCUIC.PCUICSigmaCalculus]
rename_compose [in MetaRocq.PCUIC.PCUICSigmaCalculus]
rename_ext [in MetaRocq.PCUIC.PCUICSigmaCalculus]
rename_context_lift_context [in MetaRocq.PCUIC.Conversion.PCUICWeakeningConv]
rename_rho_iota_red [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
rename_rho_ctx_over [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
rename_rho_ctx [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
rename_context_inst_context [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
rename_decl_inst_decl [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
renaming_vdef [in MetaRocq.PCUIC.Typing.PCUICRenameTyp]
renaming_vass [in MetaRocq.PCUIC.Typing.PCUICRenameTyp]
renaming_extP [in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
renaming_shift_rho_fix_context [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
ren_lift_renaming [in MetaRocq.PCUIC.PCUICSigmaCalculus]
ren_subst_consn_comm [in MetaRocq.PCUIC.PCUICSigmaCalculus]
ren_rshiftk [in MetaRocq.PCUIC.PCUICSigmaCalculus]
ren_shiftk [in MetaRocq.PCUIC.PCUICSigmaCalculus]
ren_shift [in MetaRocq.PCUIC.PCUICSigmaCalculus]
ren_idsn_consn_lt [in MetaRocq.PCUIC.PCUICSigmaCalculus]
ren_ids_lt [in MetaRocq.PCUIC.PCUICSigmaCalculus]
ren_ids_length [in MetaRocq.PCUIC.PCUICSigmaCalculus]
ren_consn_lt [in MetaRocq.PCUIC.PCUICSigmaCalculus]
ren_id_ids [in MetaRocq.PCUIC.PCUICSigmaCalculus]
ren_shiftn [in MetaRocq.PCUIC.PCUICSigmaCalculus]
reorder_env_wf [in MetaRocq.Erasure.EReorderCstrs]
reorder_env_expanded_fix [in MetaRocq.Erasure.EReorderCstrs]
reorder_env_expanded [in MetaRocq.Erasure.EReorderCstrs]
reorder_branches_map [in MetaRocq.Erasure.EReorderCstrs]
reorder_list_opt_map [in MetaRocq.Erasure.EReorderCstrs]
reorder_list_length [in MetaRocq.Erasure.EReorderCstrs]
reorder_list_old_tag [in MetaRocq.Erasure.EReorderCstrs]
reorder_list_spec_inv [in MetaRocq.Erasure.EReorderCstrs]
reorder_list_spec' [in MetaRocq.Erasure.EReorderCstrs]
reorder_list_opt_spec' [in MetaRocq.Erasure.EReorderCstrs]
reorder_list_opt_In [in MetaRocq.Erasure.EReorderCstrs]
reorder_list_opt_spec [in MetaRocq.Erasure.EReorderCstrs]
repeat_snoc [in MetaRocq.PCUIC.Syntax.PCUICPosition]
represents_substl_rev [in MetaRocq.Erasure.EWcbvEvalNamed]
represents_substl [in MetaRocq.Erasure.EWcbvEvalNamed]
represents_subst_ctx [in MetaRocq.Erasure.EWcbvEvalNamed]
represents_subst [in MetaRocq.Erasure.EWcbvEvalNamed]
represents_subst' [in MetaRocq.Erasure.EWcbvEvalNamed]
represents_bound_head [in MetaRocq.Erasure.EWcbvEvalNamed]
repr_global_env_map [in MetaRocq.Template.EtaExpand]
repr_lookup_constructor [in MetaRocq.Template.EtaExpand]
Req_red [in MetaRocq.SafeChecker.PCUICSafeReduce]
Req_trans [in MetaRocq.SafeChecker.PCUICSafeReduce]
Retroknowledge.extendsT [in MetaRocq.Common.Environment]
Retroknowledge.extends_r_merge [in MetaRocq.Common.Environment]
Retroknowledge.extends_merge_idempotent [in MetaRocq.Common.Environment]
Retroknowledge.extends_l_merge [in MetaRocq.Common.Environment]
Retroknowledge.extends_spec [in MetaRocq.Common.Environment]
rev_repeat [in MetaRocq.PCUIC.Syntax.PCUICPosition]
rev_repeat [in MetaRocq.Utils.MRList]
rev_case [in MetaRocq.Utils.MRList]
rev_invol [in MetaRocq.Utils.MRList]
rev_app [in MetaRocq.Utils.MRList]
rev_map_spec [in MetaRocq.Utils.MRList]
rev_mapi [in MetaRocq.Utils.MRList]
rev_mapi_rec [in MetaRocq.Utils.MRList]
rev_ind [in MetaRocq.Utils.MRList]
rev_list_ind [in MetaRocq.Utils.MRList]
rev_map_app [in MetaRocq.Utils.MRList]
rev_map_cons [in MetaRocq.Utils.MRList]
rev_cons [in MetaRocq.Utils.MRList]
rev_inj [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
rev_subst_instance [in MetaRocq.PCUIC.Syntax.PCUICUnivSubst]
rev_rec [in MetaRocq.PCUIC.Syntax.PCUICInduction]
rev_list_ind [in MetaRocq.PCUIC.Syntax.PCUICInduction]
rev_Forall [in MetaRocq.Utils.All_Forall]
rho_inst_case_context [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
rho_All_All2_fold_inv [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
rho_triangle_All_All2_ind_terms [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
rho_triangle_All_All2_ind [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
rho_fix_subst [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
rho_cofix_subst [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
rho_ctx_app [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
rho_ctx_over_app [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
rho_lift0 [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
rho_rename [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
rho_rename_pred [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
rho_ctx_rename [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
rho_app_proj [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
rho_app_case [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
rho_fix_elim [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
rho_app_fix [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
rho_app_cofix [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
rho_app_construct [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
rho_app_lambda' [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
rho_app_lambda [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
rho_fix_context_length [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
rho_ctx_over_length [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
rho_iota_red_wf_gen [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
rho_prim_wf_rho_prim [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
rho_predicate_map_predicate [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
rho_ctx_over_wf_eq [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
rshiftk_S [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
Rtrans [in MetaRocq.SafeChecker.PCUICSafeReduce]
rtrans_clos_length [in MetaRocq.PCUIC.PCUICConversion]
rtrans_clos_incl [in MetaRocq.PCUIC.PCUICReduction]
R_Acc [in MetaRocq.SafeChecker.PCUICSafeReduce]
R_Acc_aux [in MetaRocq.SafeChecker.PCUICSafeReduce]
R_Req_R [in MetaRocq.SafeChecker.PCUICSafeReduce]
R_to_Req [in MetaRocq.SafeChecker.PCUICSafeReduce]
R_positionR [in MetaRocq.SafeChecker.PCUICSafeReduce]
R_stateR [in MetaRocq.SafeChecker.PCUICSafeConversion]
R_aux_stateR [in MetaRocq.SafeChecker.PCUICSafeConversion]
R_positionR2 [in MetaRocq.SafeChecker.PCUICSafeConversion]
R_aux_positionR2 [in MetaRocq.SafeChecker.PCUICSafeConversion]
R_cored2 [in MetaRocq.SafeChecker.PCUICSafeConversion]
R_aux_cored2 [in MetaRocq.SafeChecker.PCUICSafeConversion]
R_positionR [in MetaRocq.SafeChecker.PCUICSafeConversion]
R_aux_positionR [in MetaRocq.SafeChecker.PCUICSafeConversion]
R_cored [in MetaRocq.SafeChecker.PCUICSafeConversion]
R_irrelevance [in MetaRocq.SafeChecker.PCUICSafeConversion]
R_aux_irrelevance [in MetaRocq.SafeChecker.PCUICSafeConversion]
R_Acc [in MetaRocq.SafeChecker.PCUICSafeConversion]
R_aux_Acc [in MetaRocq.SafeChecker.PCUICSafeConversion]
| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (19204 entries) |
| Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (228 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (298 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1273 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (313 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (8163 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1514 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (52 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (352 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (534 entries) |
| Instance Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (727 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (402 entries) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (333 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (4833 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (182 entries) |