| 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 | (75519 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 | (245 entries) |
| Binder 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 | (61331 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 | (144 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 | (89 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 | (236 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 | (6913 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 | (1141 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 | (34 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 | (269 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 | (443 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 | (296 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 | (604 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 | (248 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 | (3386 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 | (140 entries) |
R (lemma)
redl_context_trans [in MetaCoq.PCUIC.PCUICReduction]redl_context_impl [in MetaCoq.PCUIC.PCUICReduction]
redl_preserve [in MetaCoq.PCUIC.PCUICReduction]
reduced_proj_body_whne [in MetaCoq.SafeChecker.PCUICSafeConversion]
reduced_case_discriminee_whne [in MetaCoq.SafeChecker.PCUICSafeConversion]
reduce_to_ind_irrel [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
reduce_to_sort_irrel [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
reduce_to_prod_irrel [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
reduce_to_ind_complete [in MetaCoq.SafeChecker.PCUICSafeReduce]
reduce_to_prod_complete [in MetaCoq.SafeChecker.PCUICSafeReduce]
reduce_to_sort_complete [in MetaCoq.SafeChecker.PCUICSafeReduce]
reduce_term_complete [in MetaCoq.SafeChecker.PCUICSafeReduce]
reduce_stack_whnf [in MetaCoq.SafeChecker.PCUICSafeReduce]
reduce_stack_prop [in MetaCoq.SafeChecker.PCUICSafeReduce]
reduce_term_sound [in MetaCoq.SafeChecker.PCUICSafeReduce]
reduce_stack_noLamApp [in MetaCoq.SafeChecker.PCUICSafeReduce]
reduce_stack_noApp [in MetaCoq.SafeChecker.PCUICSafeReduce]
reduce_stack_isred [in MetaCoq.SafeChecker.PCUICSafeReduce]
reduce_stack_context [in MetaCoq.SafeChecker.PCUICSafeReduce]
reduce_stack_decompose [in MetaCoq.SafeChecker.PCUICSafeReduce]
reduce_stack_sound [in MetaCoq.SafeChecker.PCUICSafeReduce]
reduce_stack_Req [in MetaCoq.SafeChecker.PCUICSafeReduce]
reducible_head_None [in MetaCoq.SafeChecker.PCUICSafeConversion]
reducible_head_decompose [in MetaCoq.SafeChecker.PCUICSafeConversion]
reducible_head_cored [in MetaCoq.SafeChecker.PCUICSafeConversion]
reducible_head_red_zippx [in MetaCoq.SafeChecker.PCUICSafeConversion]
reducible_head_red_zipp [in MetaCoq.SafeChecker.PCUICSafeConversion]
red_conv_conv_inv [in MetaCoq.PCUIC.PCUICCumulativity]
red_conv_conv [in MetaCoq.PCUIC.PCUICCumulativity]
red_conv [in MetaCoq.PCUIC.PCUICCumulativity]
red_cumul_cumul_inv [in MetaCoq.PCUIC.PCUICCumulativity]
red_cumul_cumul [in MetaCoq.PCUIC.PCUICCumulativity]
red_cumul_inv [in MetaCoq.PCUIC.PCUICCumulativity]
red_cumul [in MetaCoq.PCUIC.PCUICCumulativity]
red_zipc [in MetaCoq.PCUIC.PCUICSafeLemmata]
red_cored_cored [in MetaCoq.PCUIC.PCUICSafeLemmata]
red_welltyped [in MetaCoq.PCUIC.PCUICSafeLemmata]
red_neq_cored [in MetaCoq.PCUIC.PCUICSafeLemmata]
red_const [in MetaCoq.PCUIC.PCUICSafeLemmata]
red_cored_or_eq [in MetaCoq.PCUIC.PCUICSafeLemmata]
red_case_isproof [in MetaCoq.Erasure.EArities]
red_on_free_vars [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
red_red [in MetaCoq.PCUIC.PCUICSubstitution]
red_letin_alt [in MetaCoq.PCUIC.PCUICSubstitution]
red_abs_alt [in MetaCoq.PCUIC.PCUICSubstitution]
red_it_mkProd_or_LetIn_mkApps_Ind [in MetaCoq.PCUIC.PCUICInductives]
red_it_mkProd_or_LetIn_smash [in MetaCoq.PCUIC.PCUICInductives]
red_destInd [in MetaCoq.PCUIC.PCUICInductives]
red_subst_instance [in MetaCoq.PCUIC.PCUICInductiveInversion]
red_cumul_prop [in MetaCoq.PCUIC.PCUICCumulProp]
red_conv_prop [in MetaCoq.PCUIC.PCUICCumulProp]
red_upto_conv_ctx_prop [in MetaCoq.PCUIC.PCUICCumulProp]
red_terms_on_free_vars [in MetaCoq.PCUIC.PCUICNormal]
red_ctx_rel_subst [in MetaCoq.PCUIC.PCUICNormal]
red_expand_lets_ctx [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
red_context_rel_conv_extended_subst [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
red_terms_lift [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
red_context_rel_assumptions [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
red_expand_lets [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
red_ws_cumul_pb_inv [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
red_ws_cumul_pb [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
red_ws_cumul_pb_right [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
red_ws_cumul_pb_left [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
red_conv [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
red_is_open_term [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
red_ctx_rel_par_conv [in MetaCoq.PCUIC.PCUICConvCumInversion]
red_welltyped [in MetaCoq.SafeChecker.PCUICSafeReduce]
red_conv_cum_r [in MetaCoq.SafeChecker.PCUICSafeConversion]
red_conv_cum_l [in MetaCoq.SafeChecker.PCUICSafeConversion]
red_confluence [in MetaCoq.PCUIC.PCUICConfluence]
red_ws_red_left [in MetaCoq.PCUIC.PCUICConfluence]
red_mkApps_tConst_axiom [in MetaCoq.PCUIC.PCUICConfluence]
red_mkApps_tRel [in MetaCoq.PCUIC.PCUICConfluence]
red_mkApps_tInd [in MetaCoq.PCUIC.PCUICConfluence]
red_mkApps_tConstruct [in MetaCoq.PCUIC.PCUICConfluence]
red_ctx_red_ctx_alpha_trans [in MetaCoq.PCUIC.PCUICConfluence]
red_eq_context_upto_names [in MetaCoq.PCUIC.PCUICConfluence]
red_context_trans [in MetaCoq.PCUIC.PCUICConfluence]
red_ctx_red_context [in MetaCoq.PCUIC.PCUICConfluence]
red_ws_red [in MetaCoq.PCUIC.PCUICConfluence]
red_ctx_clos_rt_red1_ctx [in MetaCoq.PCUIC.PCUICConfluence]
red_trans_clos_pred1 [in MetaCoq.PCUIC.PCUICConfluence]
red_pred [in MetaCoq.PCUIC.PCUICConfluence]
red_pred' [in MetaCoq.PCUIC.PCUICConfluence]
red_eq_term_upto_univ_l [in MetaCoq.PCUIC.PCUICConfluence]
red_eq_term_upto_univ_r [in MetaCoq.PCUIC.PCUICConfluence]
red_terms_evar [in MetaCoq.PCUIC.PCUICConversion]
red_rel_all [in MetaCoq.PCUIC.PCUICConversion]
red_fix_or_cofix_body [in MetaCoq.PCUIC.PCUICConversion]
red_terms_ws_cumul_pb_terms [in MetaCoq.PCUIC.PCUICConversion]
red_it_mkProd_or_LetIn_smash [in MetaCoq.PCUIC.PCUICCanonicity]
red_decl_refl [in MetaCoq.PCUIC.PCUICContextConversion]
red_eq_context_upto_r [in MetaCoq.PCUIC.PCUICContextConversion]
red_eq_context_upto_l [in MetaCoq.PCUIC.PCUICContextConversion]
red_red_ctx_inv' [in MetaCoq.PCUIC.PCUICContextConversion]
red_red_ctx_inv [in MetaCoq.PCUIC.PCUICContextConversion]
red_compare_term_r [in MetaCoq.PCUIC.PCUICContextConversion]
red_compare_term_l [in MetaCoq.PCUIC.PCUICContextConversion]
red_ctx_closed_right [in MetaCoq.PCUIC.PCUICContextConversion]
red_ctx_closed_left [in MetaCoq.PCUIC.PCUICContextConversion]
red_ctx_ws_cumul_ctx_pb [in MetaCoq.PCUIC.PCUICContextConversion]
red_ctx_on_free_vars_term [in MetaCoq.PCUIC.PCUICContextConversion]
red_red_ctx [in MetaCoq.PCUIC.PCUICContextConversion]
red_red_ctx_aux' [in MetaCoq.PCUIC.PCUICContextConversion]
red_red_ctx' [in MetaCoq.PCUIC.PCUICContextConversion]
red_ctx_on_free_vars [in MetaCoq.PCUIC.PCUICContextConversion]
red_ctx_app [in MetaCoq.PCUIC.PCUICContextConversion]
red_ctx_skip [in MetaCoq.PCUIC.PCUICContextConversion]
red_ctx_app_context_l [in MetaCoq.PCUIC.PCUICSR]
red_ctx_clos_rt_red1_ctx [in MetaCoq.PCUIC.PCUICSR]
red_terms_refl [in MetaCoq.PCUIC.PCUICSR]
red_one_decl_ws_cumul_ctx_pb [in MetaCoq.PCUIC.PCUICSR]
red_one_decl_red_context [in MetaCoq.PCUIC.PCUICSR]
red_one_decl_red_ctx [in MetaCoq.PCUIC.PCUICSR]
red_rename [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
red_on_free_vars [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
red_ctx_rel_red_context_rel [in MetaCoq.PCUIC.PCUICContextReduction]
red_context_rel_inv [in MetaCoq.PCUIC.PCUICContextReduction]
red_context_app_right [in MetaCoq.PCUIC.PCUICContextReduction]
red_context_trans [in MetaCoq.PCUIC.PCUICContextReduction]
red_context_rel_on_ctx_free_vars [in MetaCoq.PCUIC.PCUICContextReduction]
red_context_on_ctx_free_vars [in MetaCoq.PCUIC.PCUICContextReduction]
red_context_app_same_left [in MetaCoq.PCUIC.PCUICContextReduction]
red_context_app [in MetaCoq.PCUIC.PCUICContextReduction]
red_red_ctx [in MetaCoq.PCUIC.PCUICContextReduction]
red_context_app_same [in MetaCoq.PCUIC.PCUICContextReduction]
red_context_refl [in MetaCoq.PCUIC.PCUICContextReduction]
red_decls_refl [in MetaCoq.PCUIC.PCUICContextReduction]
red_prod_alt [in MetaCoq.PCUIC.PCUICContextReduction]
red_zippx [in MetaCoq.PCUIC.PCUICReduction]
red_zipp [in MetaCoq.PCUIC.PCUICReduction]
red_context_zip [in MetaCoq.PCUIC.PCUICReduction]
red_atom [in MetaCoq.PCUIC.PCUICReduction]
red_evar [in MetaCoq.PCUIC.PCUICReduction]
red_one_evar [in MetaCoq.PCUIC.PCUICReduction]
red_prod [in MetaCoq.PCUIC.PCUICReduction]
red_prod_r [in MetaCoq.PCUIC.PCUICReduction]
red_prod_l [in MetaCoq.PCUIC.PCUICReduction]
red_cofix_congr [in MetaCoq.PCUIC.PCUICReduction]
red_cofix_body [in MetaCoq.PCUIC.PCUICReduction]
red_cofix_one_body [in MetaCoq.PCUIC.PCUICReduction]
red_cofix_ty [in MetaCoq.PCUIC.PCUICReduction]
red_cofix_one_ty [in MetaCoq.PCUIC.PCUICReduction]
red_fix_congr [in MetaCoq.PCUIC.PCUICReduction]
red_fix_body [in MetaCoq.PCUIC.PCUICReduction]
red_fix_one_body [in MetaCoq.PCUIC.PCUICReduction]
red_fix_ty [in MetaCoq.PCUIC.PCUICReduction]
red_fix_one_ty [in MetaCoq.PCUIC.PCUICReduction]
red_proj_c [in MetaCoq.PCUIC.PCUICReduction]
red_it_mkProd_or_LetIn [in MetaCoq.PCUIC.PCUICReduction]
red_it_mkLambda_or_LetIn [in MetaCoq.PCUIC.PCUICReduction]
red_case [in MetaCoq.PCUIC.PCUICReduction]
red_case_brs [in MetaCoq.PCUIC.PCUICReduction]
red_one_brs_red_brs [in MetaCoq.PCUIC.PCUICReduction]
red_case_one_brs [in MetaCoq.PCUIC.PCUICReduction]
red_case_c [in MetaCoq.PCUIC.PCUICReduction]
red_case_p [in MetaCoq.PCUIC.PCUICReduction]
red_case_pars [in MetaCoq.PCUIC.PCUICReduction]
red_one_param [in MetaCoq.PCUIC.PCUICReduction]
red_letin [in MetaCoq.PCUIC.PCUICReduction]
red_mkApps [in MetaCoq.PCUIC.PCUICReduction]
red_mkApps_f [in MetaCoq.PCUIC.PCUICReduction]
red_app [in MetaCoq.PCUIC.PCUICReduction]
red_app_r [in MetaCoq.PCUIC.PCUICReduction]
red_abs [in MetaCoq.PCUIC.PCUICReduction]
red_one_decl_red_ctx_rel [in MetaCoq.PCUIC.PCUICReduction]
red_one_context_redl [in MetaCoq.PCUIC.PCUICReduction]
red_ctx_congr [in MetaCoq.PCUIC.PCUICReduction]
red_contextual_closure_equiv [in MetaCoq.PCUIC.PCUICReduction]
red_contextual_closure [in MetaCoq.PCUIC.PCUICReduction]
red_trans [in MetaCoq.PCUIC.PCUICReduction]
red_step [in MetaCoq.PCUIC.PCUICReduction]
red_expand_let [in MetaCoq.PCUIC.PCUICSpine]
red1_eval [in MetaCoq.PCUIC.PCUICProgress]
red1_incl [in MetaCoq.PCUIC.PCUICProgress]
red1_closed [in MetaCoq.PCUIC.PCUICProgress]
red1_mkApps_left [in MetaCoq.PCUIC.PCUICProgress]
red1_alpha_eq [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
red1_conv [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
red1_cumul_inv [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
red1_cumul [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
red1_on_free_vars [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
red1_ind_all [in MetaCoq.Template.Typing]
red1_it_mkProd_or_LetIn_smash [in MetaCoq.PCUIC.PCUICInductives]
red1_destInd [in MetaCoq.PCUIC.PCUICInductives]
red1_mkApps_r [in MetaCoq.Template.Reduction]
red1_mkApps_l [in MetaCoq.Template.Reduction]
red1_mkApp [in MetaCoq.Template.Reduction]
red1_tApp_mkApp [in MetaCoq.Template.Reduction]
red1_tApp_mkApps_l [in MetaCoq.Template.Reduction]
red1_upto_conv_ctx_prop [in MetaCoq.PCUIC.PCUICCumulProp]
red1_mkApps_tCoFix_inv [in MetaCoq.PCUIC.PCUICNormal]
red1_mkApps_tFix_inv [in MetaCoq.PCUIC.PCUICNormal]
red1_mkApps_tInd_inv [in MetaCoq.PCUIC.PCUICNormal]
red1_mkApps_tConstruct_inv [in MetaCoq.PCUIC.PCUICNormal]
red1_conv [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
red1_cumul_inv [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
red1_cumul [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
red1_is_open_term [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
red1_inst [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
red1_confluent [in MetaCoq.PCUIC.PCUICConfluence]
red1_eq_context_upto_names [in MetaCoq.PCUIC.PCUICConfluence]
red1_rel_alpha_red1_rel_inv [in MetaCoq.PCUIC.PCUICConfluence]
red1_rel_alpha_red1_rel [in MetaCoq.PCUIC.PCUICConfluence]
red1_rel_alpha_pred1_rel_alpha [in MetaCoq.PCUIC.PCUICConfluence]
red1_ctx_on_free_vars [in MetaCoq.PCUIC.PCUICConfluence]
red1_ctx_pred1_ctx [in MetaCoq.PCUIC.PCUICConfluence]
red1_weak_confluence [in MetaCoq.PCUIC.PCUICConfluence]
red1_pred1 [in MetaCoq.PCUIC.PCUICConfluence]
red1_eq_term_upto_univ_r [in MetaCoq.PCUIC.PCUICConfluence]
red1_eq_context_upto_r [in MetaCoq.PCUIC.PCUICConfluence]
red1_eq_term_upto_univ_l [in MetaCoq.PCUIC.PCUICConfluence]
red1_eq_context_upto_univ_l [in MetaCoq.PCUIC.PCUICConfluence]
red1_eq_context_upto_l [in MetaCoq.PCUIC.PCUICConfluence]
red1_cumulSpec [in MetaCoq.PCUIC.PCUICConversion]
red1_red_ctx_aux [in MetaCoq.PCUIC.PCUICContextConversion]
red1_red_ctxP_app [in MetaCoq.PCUIC.PCUICContextConversion]
red1_red_ctx [in MetaCoq.PCUIC.PCUICSR]
red1_ctx_app [in MetaCoq.PCUIC.PCUICSR]
red1_it_mkLambda_or_LetIn_ctx [in MetaCoq.PCUIC.PCUICSR]
red1_subst_instance [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
red1_rename [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
red1_red_ctx [in MetaCoq.PCUIC.PCUICContextReduction]
red1_isLambda [in MetaCoq.Template.TypingWf]
red1_zippx [in MetaCoq.PCUIC.PCUICReduction]
red1_zipp [in MetaCoq.PCUIC.PCUICReduction]
red1_context [in MetaCoq.PCUIC.PCUICReduction]
red1_fill_context_hole [in MetaCoq.PCUIC.PCUICReduction]
red1_it_mkProd_or_LetIn [in MetaCoq.PCUIC.PCUICReduction]
red1_it_mkLambda_or_LetIn [in MetaCoq.PCUIC.PCUICReduction]
red1_mkApps_r [in MetaCoq.PCUIC.PCUICReduction]
red1_mkApps_f [in MetaCoq.PCUIC.PCUICReduction]
red1_red [in MetaCoq.PCUIC.PCUICReduction]
red1_ind_all [in MetaCoq.PCUIC.PCUICReduction]
reference_pop_decls_correct [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
refine_red1_Γ [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
refine_red1_r [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
refine_red1_Γ [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
refine_red1_r [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
refine_red1_Γ [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
refine_red1_r [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
refine_pred [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
reflectEq_andb_right [in MetaCoq.PCUIC.Syntax.PCUICReflect]
reflectEq_andb_left [in MetaCoq.PCUIC.Syntax.PCUICReflect]
reflectEq_andb_3 [in MetaCoq.PCUIC.Syntax.PCUICReflect]
reflectEq_andb [in MetaCoq.PCUIC.Syntax.PCUICReflect]
reflectProp_reflect [in MetaCoq.Template.utils.ReflectEq]
reflectProp_sigma_simpl [in MetaCoq.PCUIC.Syntax.PCUICReflect]
reflectProp_noConfusion [in MetaCoq.PCUIC.Syntax.PCUICReflect]
reflectProp_equiv [in MetaCoq.PCUIC.Syntax.PCUICReflect]
reflectT_pred2 [in MetaCoq.Template.utils.MCReflect]
reflectT_pred [in MetaCoq.Template.utils.MCReflect]
reflectT_subrelation' [in MetaCoq.Template.utils.MCReflect]
reflectT_subrelation [in MetaCoq.Template.utils.MCReflect]
reflectT_reflect [in MetaCoq.Template.utils.MCReflect]
reflect_reflectT [in MetaCoq.Template.utils.MCReflect]
reflect_equiv [in MetaCoq.Template.utils.ByteCompareSpec]
reflect_reflectProp_2 [in MetaCoq.Template.utils.ReflectEq]
reflect_reflectProp_1 [in MetaCoq.Template.utils.ReflectEq]
reflect_reflectProp [in MetaCoq.Template.utils.ReflectEq]
reflect_option_default [in MetaCoq.Template.utils.MCOption]
reflect_prop_context_decl [in MetaCoq.PCUIC.Syntax.PCUICReflect]
reflect_prop_list [in MetaCoq.PCUIC.Syntax.PCUICReflect]
reflect_eq_term [in MetaCoq.SafeChecker.PCUICEqualityDec]
reflect_leq_term [in MetaCoq.SafeChecker.PCUICEqualityDec]
reflect_eqb_termp_napp [in MetaCoq.SafeChecker.PCUICEqualityDec]
reflect_eqb_ctx_gen [in MetaCoq.SafeChecker.PCUICEqualityDec]
reflect_eq_term_upto_univ [in MetaCoq.SafeChecker.PCUICEqualityDec]
reflect_R_global_instance [in MetaCoq.SafeChecker.PCUICEqualityDec]
reflect_eq_ctx [in MetaCoq.SafeChecker.PCUICEqualityDec]
reflect_eq_context_IH [in MetaCoq.SafeChecker.PCUICEqualityDec]
refl_red [in MetaCoq.PCUIC.PCUICReduction]
relation_equivalence_inclusion [in MetaCoq.Template.utils.MCRelations]
reln_alt_eq [in MetaCoq.PCUIC.utils.PCUICAstUtils]
reln_list_lift_above [in MetaCoq.PCUIC.utils.PCUICAstUtils]
reln_length [in MetaCoq.PCUIC.utils.PCUICAstUtils]
reln_set_binder_name [in MetaCoq.PCUIC.PCUICSR]
reln_lift [in MetaCoq.PCUIC.PCUICContexts]
reln_acc [in MetaCoq.PCUIC.PCUICContexts]
reln_app [in MetaCoq.PCUIC.PCUICContexts]
reln_subst [in MetaCoq.PCUIC.PCUICSpine]
removelast_length [in MetaCoq.PCUIC.utils.PCUICAstUtils]
remove_last_last [in MetaCoq.Template.utils.MCList]
remove_last_app [in MetaCoq.Template.utils.MCList]
remove_last_length' [in MetaCoq.Erasure.EWcbvEval]
remove_last_length [in MetaCoq.Erasure.EWcbvEval]
rename_telescope [in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
rename_context_length [in MetaCoq.PCUIC.PCUICSigmaCalculus]
rename_subst_compose3 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
rename_subst_compose2 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
rename_subst_compose1 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
rename_idsn_idsn [in MetaCoq.PCUIC.PCUICSigmaCalculus]
rename_inst_assoc [in MetaCoq.PCUIC.PCUICSigmaCalculus]
rename_ren_id [in MetaCoq.PCUIC.PCUICSigmaCalculus]
rename_inst [in MetaCoq.PCUIC.PCUICSigmaCalculus]
rename_shiftn [in MetaCoq.PCUIC.PCUICSigmaCalculus]
rename_branches_rename_branches [in MetaCoq.PCUIC.PCUICSigmaCalculus]
rename_branch_rename_branch [in MetaCoq.PCUIC.PCUICSigmaCalculus]
rename_predicate_rename_predicate [in MetaCoq.PCUIC.PCUICSigmaCalculus]
rename_compose [in MetaCoq.PCUIC.PCUICSigmaCalculus]
rename_ext [in MetaCoq.PCUIC.PCUICSigmaCalculus]
rename_context_on_free_vars [in MetaCoq.PCUIC.Conversion.PCUICOnFreeVarsConv]
rename_on_free_vars [in MetaCoq.PCUIC.Conversion.PCUICOnFreeVarsConv]
rename_ext_cond [in MetaCoq.PCUIC.Conversion.PCUICOnFreeVarsConv]
rename_context_lift_context [in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
rename_context_inst_context [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
rename_decl_inst_decl [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
rename_telescope_cons [in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
rename_telescope_shiftn0 [in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
rename_subst_telescope [in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
rename_wf_cofixpoint [in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
rename_wf_fixpoint [in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
rename_check_one_cofix [in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
rename_check_one_fix [in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
rename_smash_context [in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
rename_app_context [in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
rename_decompose_prod_assum [in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
rename_predicate_preturn [in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
rename_case_branch_type [in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
rename_case_predicate_context [in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
rename_ind_predicate_context [in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
rename_iota_red [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
rename_extended_subst [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
rename_predicate_set_preturn [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
rename_predicate_set_pparams [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
rename_compose [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
rename_wf_branches [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
rename_wf_branch [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
rename_wf_predicate [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
rename_it_mkProd_or_LetIn [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
rename_mkProd_or_LetIn [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
rename_it_mkLambda_or_LetIn [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
rename_mkLambda_or_LetIn [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
rename_closed_constructor_body [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
rename_case_branch_context_gen [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
rename_cstr_branch_context [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
rename_inst_case_context_wf [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
rename_inst_case_context [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
rename_context_set_binder_name [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
rename_to_extended_list [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
rename_reln [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
rename_cstr_args [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
rename_context_subst_k [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
rename_context_subst_instance [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
rename_inds [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
rename_context_lift [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
rename_shiftnk [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
rename_context_subst [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
rename_subst [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
rename_unfold_cofix [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
rename_unfold_fix [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
rename_closed_extended_subst [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
rename_closedn_terms [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
rename_closedn_ctx [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
rename_closed_decl [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
rename_closed [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
rename_closedn [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
rename_fix_context [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
rename_context_decl_body [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
rename_context_nth_error [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
rename_subst10 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
rename_subst0 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
rename_context_telescope [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
rename_context_alt [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
rename_context_snoc [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
rename_context_snoc0 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
rename_subst_instance [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
rename_mkApps [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
rename_rho_iota_red [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rename_rho_ctx_over [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rename_rho_ctx [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
renaming_vdef [in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
renaming_vass [in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
renaming_extP [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
renaming_shift_rho_fix_context [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
ren_lift_renaming [in MetaCoq.PCUIC.PCUICSigmaCalculus]
ren_subst_consn_comm [in MetaCoq.PCUIC.PCUICSigmaCalculus]
ren_rshiftk [in MetaCoq.PCUIC.PCUICSigmaCalculus]
ren_shiftk [in MetaCoq.PCUIC.PCUICSigmaCalculus]
ren_shift [in MetaCoq.PCUIC.PCUICSigmaCalculus]
ren_idsn_consn_lt [in MetaCoq.PCUIC.PCUICSigmaCalculus]
ren_ids_lt [in MetaCoq.PCUIC.PCUICSigmaCalculus]
ren_ids_length [in MetaCoq.PCUIC.PCUICSigmaCalculus]
ren_consn_lt [in MetaCoq.PCUIC.PCUICSigmaCalculus]
ren_id_ids [in MetaCoq.PCUIC.PCUICSigmaCalculus]
ren_shiftn [in MetaCoq.PCUIC.PCUICSigmaCalculus]
repeat_snoc [in MetaCoq.PCUIC.Syntax.PCUICPosition]
Req_red [in MetaCoq.SafeChecker.PCUICSafeReduce]
Req_trans [in MetaCoq.SafeChecker.PCUICSafeReduce]
rev_Forall [in MetaCoq.Template.utils.All_Forall]
rev_repeat [in MetaCoq.Template.utils.MCList]
rev_case [in MetaCoq.Template.utils.MCList]
rev_invol [in MetaCoq.Template.utils.MCList]
rev_app [in MetaCoq.Template.utils.MCList]
rev_map_spec [in MetaCoq.Template.utils.MCList]
rev_mapi [in MetaCoq.Template.utils.MCList]
rev_mapi_rec [in MetaCoq.Template.utils.MCList]
rev_ind [in MetaCoq.Template.utils.MCList]
rev_list_ind [in MetaCoq.Template.utils.MCList]
rev_map_app [in MetaCoq.Template.utils.MCList]
rev_map_length [in MetaCoq.Template.utils.MCList]
rev_length [in MetaCoq.Template.utils.MCList]
rev_map_cons [in MetaCoq.Template.utils.MCList]
rev_cons [in MetaCoq.Template.utils.MCList]
rev_repeat [in MetaCoq.PCUIC.Syntax.PCUICPosition]
rev_inj [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
rev_subst_instance [in MetaCoq.PCUIC.Syntax.PCUICUnivSubst]
rev_rec [in MetaCoq.PCUIC.Syntax.PCUICInduction]
rev_list_ind [in MetaCoq.PCUIC.Syntax.PCUICInduction]
rho_inst_case_context [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho_All_All2_fold_inv [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho_triangle_All_All2_ind_terms [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho_triangle_All_All2_ind [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho_fix_subst [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho_cofix_subst [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho_ctx_app [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho_ctx_over_app [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho_lift0 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho_rename [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho_rename_pred [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho_ctx_rename [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho_app_proj [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho_app_case [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho_fix_elim [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho_app_fix [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho_app_cofix [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho_app_construct [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho_app_lambda' [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho_app_lambda [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho_fix_context_length [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho_ctx_over_length [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho_iota_red_wf_gen [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho_predicate_map_predicate [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho_ctx_over_wf_eq [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rshiftk_S [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
Rtrans [in MetaCoq.SafeChecker.PCUICSafeReduce]
rtrans_clos_length [in MetaCoq.PCUIC.PCUICConversion]
rtrans_clos_incl [in MetaCoq.PCUIC.PCUICReduction]
R_global_instance_refl [in MetaCoq.Template.TermEquality]
R_universe_instance_impl' [in MetaCoq.Template.TermEquality]
R_universe_instance_impl [in MetaCoq.Template.TermEquality]
R_global_instance_weaken_env [in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
R_eq_univ_prop_consistent_instances [in MetaCoq.PCUIC.PCUICCumulProp]
R_opt_variance_impl [in MetaCoq.PCUIC.PCUICCumulProp]
R_global_instance_flip [in MetaCoq.PCUIC.PCUICEquality]
R_universe_instance_eq [in MetaCoq.PCUIC.PCUICEquality]
R_universe_instance_antisym [in MetaCoq.PCUIC.PCUICEquality]
R_global_instance_sym [in MetaCoq.PCUIC.PCUICEquality]
R_global_instance_refl [in MetaCoq.PCUIC.PCUICEquality]
R_universe_instance_impl' [in MetaCoq.PCUIC.PCUICEquality]
R_universe_instance_impl [in MetaCoq.PCUIC.PCUICEquality]
R_Acc [in MetaCoq.SafeChecker.PCUICSafeReduce]
R_Acc_aux [in MetaCoq.SafeChecker.PCUICSafeReduce]
R_Req_R [in MetaCoq.SafeChecker.PCUICSafeReduce]
R_to_Req [in MetaCoq.SafeChecker.PCUICSafeReduce]
R_positionR [in MetaCoq.SafeChecker.PCUICSafeReduce]
R_stateR [in MetaCoq.SafeChecker.PCUICSafeConversion]
R_aux_stateR [in MetaCoq.SafeChecker.PCUICSafeConversion]
R_positionR2 [in MetaCoq.SafeChecker.PCUICSafeConversion]
R_aux_positionR2 [in MetaCoq.SafeChecker.PCUICSafeConversion]
R_cored2 [in MetaCoq.SafeChecker.PCUICSafeConversion]
R_aux_cored2 [in MetaCoq.SafeChecker.PCUICSafeConversion]
R_positionR [in MetaCoq.SafeChecker.PCUICSafeConversion]
R_aux_positionR [in MetaCoq.SafeChecker.PCUICSafeConversion]
R_cored [in MetaCoq.SafeChecker.PCUICSafeConversion]
R_irrelevance [in MetaCoq.SafeChecker.PCUICSafeConversion]
R_aux_irrelevance [in MetaCoq.SafeChecker.PCUICSafeConversion]
R_Acc [in MetaCoq.SafeChecker.PCUICSafeConversion]
R_aux_Acc [in MetaCoq.SafeChecker.PCUICSafeConversion]
R_global_instance_empty_universe_instance [in MetaCoq.PCUIC.PCUICPrincipality]
R_global_instance_nl [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
R_universe_instance_flip [in MetaCoq.PCUIC.PCUICConfluence]
R_universe_instance_variance_irrelevant [in MetaCoq.PCUIC.PCUICConversion]
R_global_instance_length [in MetaCoq.PCUIC.PCUICConversion]
R_global_instance_cstr_irrelevant [in MetaCoq.PCUIC.PCUICSR]
R_global_instance_refl_wf [in MetaCoq.SafeChecker.PCUICEqualityDec]
| 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 | (75519 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 | (245 entries) |
| Binder 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 | (61331 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 | (144 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 | (89 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 | (236 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 | (6913 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 | (1141 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 | (34 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 | (269 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 | (443 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 | (296 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 | (604 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 | (248 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 | (3386 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 | (140 entries) |