| 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) |
C (lemma)
Case_Construct_ind_eq [in MetaRocq.PCUIC.PCUICSafeLemmata]case_predicate_context_alpha [in MetaRocq.PCUIC.PCUICInductiveInversion]
case_branch_type_eq_context_gen_2 [in MetaRocq.PCUIC.PCUICAlpha]
case_branch_type_eq_context_gen_1 [in MetaRocq.PCUIC.PCUICAlpha]
case_branch_type_equiv [in MetaRocq.PCUIC.PCUICAlpha]
case_branch_context_equiv [in MetaRocq.PCUIC.PCUICAlpha]
case_predicate_context_equiv [in MetaRocq.PCUIC.PCUICAlpha]
case_brs_forallb_map_spec [in MetaRocq.PCUIC.PCUICAst]
case_brs_map_k_spec [in MetaRocq.PCUIC.PCUICAst]
case_brs_map_spec_cond [in MetaRocq.PCUIC.PCUICAst]
case_brs_map_spec [in MetaRocq.PCUIC.PCUICAst]
case_branch_type_length [in MetaRocq.PCUIC.Syntax.PCUICCases]
case_branches_contexts_length [in MetaRocq.PCUIC.Syntax.PCUICCases]
case_branch_context_assumptions [in MetaRocq.PCUIC.Syntax.PCUICCases]
case_branch_context_length_args [in MetaRocq.PCUIC.Syntax.PCUICCases]
case_branch_context_length [in MetaRocq.PCUIC.Syntax.PCUICCases]
case_predicate_context_length_indices [in MetaRocq.PCUIC.Syntax.PCUICCases]
case_predicate_context_length [in MetaRocq.PCUIC.Syntax.PCUICCases]
case_branch_type_fst [in MetaRocq.PCUIC.Syntax.PCUICCases]
case_conv_preds_inv [in MetaRocq.SafeChecker.PCUICSafeConversion]
case_conv_brs_inv [in MetaRocq.SafeChecker.PCUICSafeConversion]
case_branch_context_assumptions [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
case_branch_context_assumptions [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
case_brs_forallb_map_spec [in MetaRocq.Template.Ast]
case_brs_map_k_spec [in MetaRocq.Template.Ast]
case_brs_map_spec [in MetaRocq.Template.Ast]
case_branch_type_beta_typed [in MetaRocq.PCUIC.PCUICCasesHelper]
case_branch_type_conv_beta [in MetaRocq.PCUIC.PCUICCasesHelper]
case_branch_type_beta [in MetaRocq.PCUIC.PCUICCasesHelper]
case_branch_context_unfold [in MetaRocq.PCUIC.PCUICCasesHelper]
case_branch_type_split [in MetaRocq.PCUIC.PCUICCasesHelper]
case_branch_type_gen_split [in MetaRocq.PCUIC.PCUICCasesHelper]
checking_typing [in MetaRocq.PCUIC.Bidirectional.BDToPCUIC]
check_ind_sorts_is_propositional [in MetaRocq.PCUIC.PCUICElimination]
check_constructors_smallerP [in MetaRocq.SafeChecker.PCUICSafeChecker]
check_dearging_precond_spec [in MetaRocq.ErasurePlugin.ETransform]
check_constraints_complete [in MetaRocq.SafeChecker.PCUICWfEnv]
check_constraints_spec [in MetaRocq.SafeChecker.PCUICWfEnv]
check_recursivity_kind_inj [in MetaRocq.PCUIC.PCUICClassification]
check_eqb_sort_complete_gen [in MetaRocq.Common.uGraph]
check_eqb_sort_spec_gen' [in MetaRocq.Common.uGraph]
check_leqb_sort_complete_gen [in MetaRocq.Common.uGraph]
check_leqb_sort_spec_gen' [in MetaRocq.Common.uGraph]
check_constraints_complete_gen [in MetaRocq.Common.uGraph]
check_constraints_spec_gen [in MetaRocq.Common.uGraph]
check_gc_constraints_complete_gen [in MetaRocq.Common.uGraph]
check_gc_constraint_complete_gen [in MetaRocq.Common.uGraph]
check_eqb_universe_complete_gen [in MetaRocq.Common.uGraph]
check_eqb_universe_spec_gen' [in MetaRocq.Common.uGraph]
check_leqb_universe_complete_gen [in MetaRocq.Common.uGraph]
check_leqb_universe_spec_gen' [in MetaRocq.Common.uGraph]
check_eqb_sort_spec_gen [in MetaRocq.Common.uGraph]
check_eqb_sort_refl_gen [in MetaRocq.Common.uGraph]
check_gc_constraints_spec_gen [in MetaRocq.Common.uGraph]
check_gc_constraint_spec_gen [in MetaRocq.Common.uGraph]
check_eqb_universe_spec_gen [in MetaRocq.Common.uGraph]
check_leqb_universe_spec_gen [in MetaRocq.Common.uGraph]
chop_all [in MetaRocq.Erasure.EImplementBox]
chop_eq [in MetaRocq.Erasure.EImplementBox]
chop_firstn_skipn [in MetaRocq.Erasure.EImplementBox]
chop_n_app [in MetaRocq.Utils.MRList]
chop_map [in MetaRocq.Utils.MRList]
chop_all [in MetaRocq.Erasure.EConstructorsAsBlocks]
chop_eq [in MetaRocq.Erasure.EConstructorsAsBlocks]
chop_firstn_skipn [in MetaRocq.Erasure.EConstructorsAsBlocks]
chop_firstn_skipn [in MetaRocq.SafeChecker.PCUICTypeChecker]
classification [in MetaRocq.PCUIC.PCUICProgress]
closedn_ctx_subst_forall [in MetaRocq.PCUIC.PCUICContextSubst]
closedn_ctx_lift_inv [in MetaRocq.PCUIC.Bidirectional.BDStrengthening]
closedn_All_local_closed [in MetaRocq.PCUIC.Conversion.PCUICClosedConv]
closedn_All_local_env [in MetaRocq.PCUIC.Conversion.PCUICClosedConv]
closedn_ctx_alpha [in MetaRocq.PCUIC.Conversion.PCUICClosedConv]
closedn_zip [in MetaRocq.PCUIC.Syntax.PCUICPosition]
closedn_fill_hole [in MetaRocq.PCUIC.Syntax.PCUICPosition]
closedn_expand_lets [in MetaRocq.PCUIC.PCUICSR]
closedn_subst0 [in MetaRocq.Erasure.Typed.ClosedAux]
closedn_subst [in MetaRocq.Erasure.Typed.ClosedAux]
closedn_lift [in MetaRocq.Erasure.Typed.ClosedAux]
closedn_mkApps [in MetaRocq.Erasure.Typed.ClosedAux]
closedn_to_extended_list [in MetaRocq.PCUIC.Syntax.PCUICClosed]
closedn_to_extended_list_k [in MetaRocq.PCUIC.Syntax.PCUICClosed]
closedn_to_extended_list_k_up [in MetaRocq.PCUIC.Syntax.PCUICClosed]
closedn_expand_lets_eq [in MetaRocq.PCUIC.Syntax.PCUICClosed]
closedn_expand_lets [in MetaRocq.PCUIC.Syntax.PCUICClosed]
closedn_ctx_upwards [in MetaRocq.PCUIC.Syntax.PCUICClosed]
closedn_ctx_expand_lets [in MetaRocq.PCUIC.Syntax.PCUICClosed]
closedn_extended_subst [in MetaRocq.PCUIC.Syntax.PCUICClosed]
closedn_extended_subst_gen [in MetaRocq.PCUIC.Syntax.PCUICClosed]
closedn_ctx_subst [in MetaRocq.PCUIC.Syntax.PCUICClosed]
closedn_ctx_lift [in MetaRocq.PCUIC.Syntax.PCUICClosed]
closedn_ctx_decl [in MetaRocq.PCUIC.Syntax.PCUICClosed]
closedn_mapi_rec_ext [in MetaRocq.PCUIC.Syntax.PCUICClosed]
closedn_smash_context [in MetaRocq.PCUIC.Syntax.PCUICClosed]
closedn_ctx_spec [in MetaRocq.PCUIC.Syntax.PCUICClosed]
closedn_subst_instance_context [in MetaRocq.PCUIC.Syntax.PCUICClosed]
closedn_it_mkLambda_or_LetIn [in MetaRocq.PCUIC.Syntax.PCUICClosed]
closedn_it_mkProd_or_LetIn [in MetaRocq.PCUIC.Syntax.PCUICClosed]
closedn_mkLambda_or_LetIn [in MetaRocq.PCUIC.Syntax.PCUICClosed]
closedn_mkProd_or_LetIn [in MetaRocq.PCUIC.Syntax.PCUICClosed]
closedn_ctx_tip [in MetaRocq.PCUIC.Syntax.PCUICClosed]
closedn_subst_instance [in MetaRocq.PCUIC.Syntax.PCUICClosed]
closedn_subst0 [in MetaRocq.PCUIC.Syntax.PCUICClosed]
closedn_subst [in MetaRocq.PCUIC.Syntax.PCUICClosed]
closedn_subst_eq' [in MetaRocq.PCUIC.Syntax.PCUICClosed]
closedn_subst_eq [in MetaRocq.PCUIC.Syntax.PCUICClosed]
closedn_mkApps [in MetaRocq.PCUIC.Syntax.PCUICClosed]
closedn_lift_inv [in MetaRocq.PCUIC.Syntax.PCUICClosed]
closedn_lift [in MetaRocq.PCUIC.Syntax.PCUICClosed]
closedn_ctx_app [in MetaRocq.PCUIC.Syntax.PCUICClosed]
closedn_ctx_cons [in MetaRocq.PCUIC.Syntax.PCUICClosed]
closedn_trans [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
closedn_ctx_on_free_vars [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
closedn_expand'' [in MetaRocq.PCUIC.PCUICInductiveInversion]
closedn_expand' [in MetaRocq.PCUIC.PCUICInductiveInversion]
closedn_expand [in MetaRocq.PCUIC.PCUICInductiveInversion]
closedn_mkApps [in MetaRocq.Erasure.EEtaExpandedFix]
closedn_ctx_snoc [in MetaRocq.PCUIC.PCUICContexts]
closedn_mkApps [in MetaRocq.Erasure.EWcbvEval]
closedn_mkApps [in MetaRocq.PCUIC.PCUICClassification]
closedn_dearg_aux [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
closedn_dearg_case_branch_body_rec [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
closedn_subst [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
closedn_dearg_lambdas [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
closedn_dearg_single [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
closedn_ctx_cstr_branch_context [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
closedn_ctx_expand_lets [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
closedn_mkApps [in MetaRocq.Erasure.ERemoveParams]
closedn_ctx_on_free_vars_shift [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
closedn_ctx_on_free_vars [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
closedn_on_free_vars [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
closedn_subst [in MetaRocq.Erasure.ELiftSubst]
closedn_subst_eq [in MetaRocq.Erasure.ELiftSubst]
closedn_lift [in MetaRocq.Erasure.ELiftSubst]
closedP_shiftnP_eq [in MetaRocq.PCUIC.PCUICSR]
closedP_mon [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
closedP_xpredT [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
closedP_shiftnP_impl [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
closedP_shiftnP [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
closedP_on_free_vars [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
closedu_subst_instance [in MetaRocq.Common.Universes]
closedu_subst_instance_univ [in MetaRocq.Common.Universes]
closedu_subst_instance_level_expr [in MetaRocq.Common.Universes]
closedu_subst_instance_level [in MetaRocq.Common.Universes]
closedu_subst_instance_cstrs_lift [in MetaRocq.PCUIC.PCUICInductiveInversion]
closedu_subst_instance_cstrs_app [in MetaRocq.PCUIC.PCUICInductiveInversion]
closedu_subst_instance_lift [in MetaRocq.PCUIC.PCUICInductiveInversion]
closedu_subst_instance_app [in MetaRocq.PCUIC.PCUICInductiveInversion]
closedu_subst_instance_level_expr_app [in MetaRocq.PCUIC.PCUICInductiveInversion]
closedu_subst_instance_level_lift [in MetaRocq.PCUIC.PCUICInductiveInversion]
closedu_subst_instance_level_app [in MetaRocq.PCUIC.PCUICInductiveInversion]
closedu_subst_instance [in MetaRocq.PCUIC.Syntax.PCUICUnivSubst]
closedu_subst_instance [in MetaRocq.Template.UnivSubst]
closedu_inds [in MetaRocq.PCUIC.PCUICWfUniverses]
closedu_to_extended_list_k [in MetaRocq.PCUIC.PCUICWfUniverses]
closedu_reln [in MetaRocq.PCUIC.PCUICWfUniverses]
closedu_smash_context [in MetaRocq.PCUIC.PCUICWfUniverses]
closedu_smash_context_gen [in MetaRocq.PCUIC.PCUICWfUniverses]
closedu_expand_lets_ctx [in MetaRocq.PCUIC.PCUICWfUniverses]
closedu_extended_subst [in MetaRocq.PCUIC.PCUICWfUniverses]
closedu_lift_context [in MetaRocq.PCUIC.PCUICWfUniverses]
closedu_subst_context [in MetaRocq.PCUIC.PCUICWfUniverses]
closedu_subst [in MetaRocq.PCUIC.PCUICWfUniverses]
closedu_lift [in MetaRocq.PCUIC.PCUICWfUniverses]
closedu_abstract_instance [in MetaRocq.PCUIC.PCUICWfUniverses]
closedu_mkApps [in MetaRocq.PCUIC.PCUICWfUniverses]
closedu_compare_decls [in MetaRocq.PCUIC.PCUICWfUniverses]
closed_fake_params [in MetaRocq.PCUIC.PCUICNormal]
closed_cstr_branch_context_gen [in MetaRocq.PCUIC.Conversion.PCUICClosedConv]
closed_red1_case_branch_type [in MetaRocq.PCUIC.PCUICSR]
closed_red1_mkApps_left [in MetaRocq.PCUIC.PCUICSR]
closed_red1_it_mkLambda_or_LetIn [in MetaRocq.PCUIC.PCUICSR]
closed_red1_ws_cumul_pb [in MetaRocq.PCUIC.PCUICSR]
closed_red1_eq_context_upto_names [in MetaRocq.PCUIC.PCUICSR]
closed_red1_ind [in MetaRocq.PCUIC.PCUICSR]
closed_nlctx [in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
closed_nl [in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
closed_ctx_IH [in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
closed_upwards [in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
closed_implement_box [in MetaRocq.Erasure.EImplementBox]
closed_csubst [in MetaRocq.Erasure.Typed.ClosedAux]
closed_mkApps_args [in MetaRocq.Erasure.Typed.ClosedAux]
closed_mkApps_head [in MetaRocq.Erasure.Typed.ClosedAux]
closed_mkApps_inv [in MetaRocq.Erasure.Typed.ClosedAux]
closed_mkApps [in MetaRocq.Erasure.Typed.ClosedAux]
closed_tele_subst [in MetaRocq.PCUIC.PCUICSubstitution]
closed_ctx_subst [in MetaRocq.PCUIC.PCUICSubstitution]
closed_ctx_app [in MetaRocq.PCUIC.Syntax.PCUICClosed]
closed_ind_closed_cstrs [in MetaRocq.PCUIC.Syntax.PCUICClosed]
closed_inds [in MetaRocq.PCUIC.Syntax.PCUICClosed]
closed_ind_predicate_context [in MetaRocq.PCUIC.Syntax.PCUICClosed]
closed_ctx_decl [in MetaRocq.PCUIC.Syntax.PCUICClosed]
closed_ctx_expand_lets [in MetaRocq.PCUIC.Syntax.PCUICClosed]
closed_declared_ind [in MetaRocq.PCUIC.Syntax.PCUICClosed]
closed_smash_context_unfold [in MetaRocq.PCUIC.Syntax.PCUICClosed]
closed_smash_context_gen [in MetaRocq.PCUIC.Syntax.PCUICClosed]
closed_subst_context [in MetaRocq.PCUIC.Syntax.PCUICClosed]
closed_map_subst_instance [in MetaRocq.PCUIC.Syntax.PCUICClosed]
closed_ctx_lift [in MetaRocq.PCUIC.Syntax.PCUICClosed]
closed_decl_upwards [in MetaRocq.PCUIC.Syntax.PCUICClosed]
closed_spine_subst_inst [in MetaRocq.PCUIC.PCUICSpine]
closed_spine_subst [in MetaRocq.PCUIC.PCUICSpine]
closed_subslet [in MetaRocq.PCUIC.PCUICSpine]
closed_subst_map_lift [in MetaRocq.PCUIC.PCUICSpine]
closed_ctx_subst [in MetaRocq.PCUIC.PCUICSpine]
closed_k_ctx_subst [in MetaRocq.PCUIC.PCUICSpine]
closed_red1_red [in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
closed_red_open_right [in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
closed_red1_open_right [in MetaRocq.PCUIC.PCUICWellScopedCumulativity]
closed_substl [in MetaRocq.Erasure.ECSubst]
closed_csubst [in MetaRocq.Erasure.ECSubst]
closed_subst [in MetaRocq.Erasure.ECSubst]
closed_context_conversion [in MetaRocq.PCUIC.Typing.PCUICContextConversionTyp]
closed_context_cumulativity [in MetaRocq.PCUIC.Typing.PCUICContextConversionTyp]
closed_context_conv_conv [in MetaRocq.PCUIC.Typing.PCUICContextConversionTyp]
closed_context_cumul_cumul [in MetaRocq.PCUIC.Typing.PCUICContextConversionTyp]
closed_red_ctx_refl [in MetaRocq.PCUIC.PCUICContextConversion]
closed_red_refl [in MetaRocq.PCUIC.PCUICContextConversion]
closed_red_eq_context_upto_r [in MetaRocq.PCUIC.PCUICContextConversion]
closed_red_eq_context_upto_l [in MetaRocq.PCUIC.PCUICContextConversion]
closed_red_confluence [in MetaRocq.PCUIC.PCUICContextConversion]
closed_red_red_ctx [in MetaRocq.PCUIC.PCUICContextConversion]
closed_red_compare_term_r [in MetaRocq.PCUIC.PCUICContextConversion]
closed_red_compare_term_l [in MetaRocq.PCUIC.PCUICContextConversion]
closed_red_ctx_red_ctx [in MetaRocq.PCUIC.PCUICContextConversion]
closed_cunfold_cofix [in MetaRocq.Erasure.Typed.WcbvEvalAux]
closed_cunfold_fix [in MetaRocq.Erasure.Typed.WcbvEvalAux]
closed_iota_red [in MetaRocq.Erasure.Typed.WcbvEvalAux]
closed_unfold_cofix [in MetaRocq.Erasure.Typed.WcbvEvalAux]
closed_unfold_fix [in MetaRocq.Erasure.Typed.WcbvEvalAux]
closed_constant [in MetaRocq.Erasure.Typed.WcbvEvalAux]
closed_inst_case_context [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
closed_ctx_is_closed_context [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
closed_csubst [in MetaRocq.PCUIC.PCUICCSubst]
closed_subst [in MetaRocq.PCUIC.PCUICCSubst]
closed_upwards [in MetaRocq.Template.LiftSubst]
closed_red_mkApps [in MetaRocq.PCUIC.PCUICInductiveInversion]
closed_red_rel_all [in MetaRocq.PCUIC.PCUICConversion]
closed_red_subst [in MetaRocq.PCUIC.PCUICConversion]
closed_red1_mkApps_left [in MetaRocq.PCUIC.PCUICConversion]
closed_red_terms_open_right [in MetaRocq.PCUIC.PCUICConversion]
closed_red_terms_open_left [in MetaRocq.PCUIC.PCUICConversion]
closed_red_prod_codom [in MetaRocq.PCUIC.PCUICConversion]
closed_red_prod [in MetaRocq.PCUIC.PCUICConversion]
closed_red_letin_body [in MetaRocq.PCUIC.PCUICConversion]
closed_red_letin [in MetaRocq.PCUIC.PCUICConversion]
closed_red_ind [in MetaRocq.PCUIC.PCUICConversion]
closed_red_untyped_substitution0 [in MetaRocq.PCUIC.PCUICConversion]
closed_red_untyped_substitution [in MetaRocq.PCUIC.PCUICConversion]
closed_red_red_subst0 [in MetaRocq.PCUIC.PCUICConversion]
closed_red_red_subst [in MetaRocq.PCUIC.PCUICConversion]
closed_red_clos [in MetaRocq.PCUIC.PCUICConversion]
closed_prod_type [in MetaRocq.ErasurePlugin.ErasureCorrectness]
closed_iota_red [in MetaRocq.Erasure.EOptimizePropDiscr]
closed_remove_match_on_box [in MetaRocq.Erasure.EOptimizePropDiscr]
closed_iota_red [in MetaRocq.Erasure.EReorderCstrs]
closed_transform_blocks [in MetaRocq.Erasure.EConstructorsAsBlocks]
closed_cunfold_cofix [in MetaRocq.Erasure.EWcbvEval]
closed_cunfold_fix [in MetaRocq.Erasure.EWcbvEval]
closed_cofix_subst [in MetaRocq.Erasure.EWcbvEval]
closed_fix_subst [in MetaRocq.Erasure.EWcbvEval]
closed_unfold_cofix_cunfold_eq [in MetaRocq.Erasure.EWcbvEval]
closed_cofix_substl_subst_eq [in MetaRocq.Erasure.EWcbvEval]
closed_unfold_fix_cunfold_eq [in MetaRocq.Erasure.EWcbvEval]
closed_fix_substl_subst_eq [in MetaRocq.Erasure.EWcbvEval]
closed_ctx_lift [in MetaRocq.PCUIC.Conversion.PCUICWeakeningConv]
closed_red_upto_conv_ctx_prop [in MetaRocq.PCUIC.PCUICCumulProp]
closed_red1_upto_conv_ctx_prop [in MetaRocq.PCUIC.PCUICCumulProp]
closed_iota_red [in MetaRocq.Erasure.EInlineProjections]
closed_ind_predicate_context [in MetaRocq.PCUIC.PCUICWfUniverses]
closed_red_zipp [in MetaRocq.SafeChecker.PCUICSafeConversion]
closed_red_mkApps_tConst_axiom [in MetaRocq.SafeChecker.PCUICSafeConversion]
closed_unfold_cofix [in MetaRocq.PCUIC.PCUICWcbvEval]
closed_unfold_cofix_cunfold_eq [in MetaRocq.PCUIC.PCUICWcbvEval]
closed_unfold_fix_cunfold_eq [in MetaRocq.PCUIC.PCUICWcbvEval]
closed_cofix_substl_subst_eq [in MetaRocq.PCUIC.PCUICWcbvEval]
closed_fix_substl_subst_eq [in MetaRocq.PCUIC.PCUICWcbvEval]
closed_unfold_fix [in MetaRocq.PCUIC.PCUICWcbvEval]
closed_arg [in MetaRocq.PCUIC.PCUICWcbvEval]
closed_iota [in MetaRocq.PCUIC.PCUICWcbvEval]
closed_def [in MetaRocq.PCUIC.PCUICWcbvEval]
closed_beta [in MetaRocq.PCUIC.PCUICWcbvEval]
closed_subst_up_vdef [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
closed_subst_up_vass [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
closed_subst_app_up [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
closed_subst_app [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
closed_subst_Up' [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
closed_subst_Up [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
closed_subst_ext [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
closed_ctx_args [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
closed_tele_inst [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
closed_strip [in MetaRocq.Erasure.ERemoveParams]
closed_ctx_on_free_vars [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
closed_decl_on_free_vars [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
closed_on_free_vars [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
closed_on_free_vars_none [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
closed_arities_context [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
closed_ind_predicate_context [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
closed_cstr_branch_context_npars [in MetaRocq.PCUIC.Typing.PCUICClosedTyp]
closed_cstr_branch_context [in MetaRocq.PCUIC.Typing.PCUICClosedTyp]
closed_ctx_on_ctx_free_vars [in MetaRocq.PCUIC.Typing.PCUICClosedTyp]
closed_wf_local [in MetaRocq.PCUIC.Typing.PCUICClosedTyp]
closed_upwards [in MetaRocq.Erasure.ELiftSubst]
closed_iota_red [in MetaRocq.Erasure.ECoInductiveToInductive]
closed_trans [in MetaRocq.Erasure.ECoInductiveToInductive]
clos_rt_red1_red1_rel_alpha [in MetaRocq.PCUIC.PCUICConfluence]
clos_refl_trans_ctx_to_1n [in MetaRocq.PCUIC.PCUICConfluence]
clos_rt_red1_alpha_out' [in MetaRocq.PCUIC.PCUICConfluence]
clos_rt_red1_alpha_out [in MetaRocq.PCUIC.PCUICConfluence]
clos_rt_red1_eq_context_upto_names [in MetaRocq.PCUIC.PCUICConfluence]
clos_rt_red1_rel_red1 [in MetaRocq.PCUIC.PCUICConfluence]
clos_rt_red1_rel_ws_red1 [in MetaRocq.PCUIC.PCUICConfluence]
clos_red_rel_out_inv [in MetaRocq.PCUIC.PCUICConfluence]
clos_red_rel_out [in MetaRocq.PCUIC.PCUICConfluence]
clos_refl_trans_out [in MetaRocq.PCUIC.PCUICConfluence]
clos_refl_trans_red1_ctx_eq_length [in MetaRocq.PCUIC.PCUICConfluence]
clos_refl_trans_prod_r [in MetaRocq.PCUIC.PCUICConfluence]
clos_refl_trans_prod_l_sigma [in MetaRocq.PCUIC.PCUICConfluence]
clos_rt_red1_rel_rt_ctx [in MetaRocq.PCUIC.PCUICConfluence]
clos_rt_red1_rel_ctx_rt_ctx_red1_rel [in MetaRocq.PCUIC.PCUICConfluence]
clos_refl_trans_ctx_length [in MetaRocq.PCUIC.PCUICConfluence]
clos_refl_trans_ctx_on_free_vars [in MetaRocq.PCUIC.PCUICConfluence]
clos_refl_trans_ctx_t_prod_r [in MetaRocq.PCUIC.PCUICConfluence]
clos_refl_trans_ctx_t_prod_l [in MetaRocq.PCUIC.PCUICConfluence]
clos_rt_ctx_t_disjunction_right [in MetaRocq.PCUIC.PCUICConfluence]
clos_rt_ctx_t_disjunction_left [in MetaRocq.PCUIC.PCUICConfluence]
clos_rt_OnOne2_local_env_ctx_incl [in MetaRocq.PCUIC.PCUICConfluence]
clos_rt_proper [in MetaRocq.PCUIC.PCUICConfluence]
clos_rt_OnOne2_local_env_incl [in MetaRocq.PCUIC.PCUICConfluence]
clos_t_rt_equiv [in MetaRocq.Utils.MRRelations]
clos_t_rt_incl [in MetaRocq.Utils.MRRelations]
clos_rt_t_incl [in MetaRocq.Utils.MRRelations]
clos_refl_trans_prod_r [in MetaRocq.Utils.MRRelations]
clos_refl_trans_prod_l [in MetaRocq.Utils.MRRelations]
clos_rt_disjunction_right [in MetaRocq.Utils.MRRelations]
clos_rt_disjunction_left [in MetaRocq.Utils.MRRelations]
clos_t_rt [in MetaRocq.Utils.MRRelations]
cmpb_term_correct [in MetaRocq.SafeChecker.PCUICSafeConversion]
cmp_global_instance_cstr_irrelevant [in MetaRocq.PCUIC.PCUICSR]
cmp_global_instance_nl [in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
cmp_global_instance_flip [in MetaRocq.PCUIC.PCUICEquality]
cmp_universe_instance_flip [in MetaRocq.PCUIC.PCUICEquality]
cmp_universe_instance_variance_flip [in MetaRocq.PCUIC.PCUICEquality]
cmp_universe_variance_flip [in MetaRocq.PCUIC.PCUICEquality]
cmp_universe_instance_eq [in MetaRocq.PCUIC.PCUICEquality]
cmp_universe_instance_variance_antisym [in MetaRocq.PCUIC.PCUICEquality]
cmp_universe_variance_antisym [in MetaRocq.PCUIC.PCUICEquality]
cmp_universe_instance_antisym [in MetaRocq.PCUIC.PCUICEquality]
cmp_universe_instance_variance_impl [in MetaRocq.PCUIC.PCUICEquality]
cmp_universe_variance_impl [in MetaRocq.PCUIC.PCUICEquality]
cmp_universe_instance_impl' [in MetaRocq.PCUIC.PCUICEquality]
cmp_universe_instance_impl [in MetaRocq.PCUIC.PCUICEquality]
cmp_opt_variance_or_impl [in MetaRocq.PCUIC.PCUICEquality]
cmp_opt_variance_length [in MetaRocq.PCUIC.PCUICEquality]
cmp_opt_variance_var_dec [in MetaRocq.PCUIC.PCUICEquality]
cmp_instance_opt_variance [in MetaRocq.PCUIC.PCUICEquality]
cmp_instance_variance [in MetaRocq.PCUIC.PCUICEquality]
cmp_universe_universe_variance [in MetaRocq.PCUIC.PCUICEquality]
cmp_sort_config_impl [in MetaRocq.Common.Universes]
cmp_universe_config_impl [in MetaRocq.Common.Universes]
cmp_sort_subset [in MetaRocq.Common.Universes]
cmp_universe_subset [in MetaRocq.Common.Universes]
cmp_global_instance_weaken_env [in MetaRocq.PCUIC.Conversion.PCUICWeakeningEnvConv]
cmp_global_instance_refl [in MetaRocq.Template.TermEquality]
cmp_universe_instance_refl [in MetaRocq.Template.TermEquality]
cmp_universe_instance_variance_impl [in MetaRocq.Template.TermEquality]
cmp_universe_instance_impl' [in MetaRocq.Template.TermEquality]
cmp_universe_instance_impl [in MetaRocq.Template.TermEquality]
cmp_opt_variance_var_dec [in MetaRocq.Template.TermEquality]
cmp_instance_variance [in MetaRocq.Template.TermEquality]
cmp_universe_universe_variance [in MetaRocq.Template.TermEquality]
cmp_instance_opt_variance [in MetaRocq.Template.TermEquality]
cmp_global_instance_refl_wf [in MetaRocq.SafeChecker.PCUICEqualityDec]
cmp_universe_instance_refl_wf [in MetaRocq.SafeChecker.PCUICEqualityDec]
cmp_global_instance_ind_inv [in MetaRocq.PCUIC.PCUICInductiveInversion]
cmp_universe_instance_variance_irrelevant [in MetaRocq.PCUIC.PCUICConversion]
cmp_global_instance_length [in MetaRocq.PCUIC.PCUICConversion]
cmp_True_instance [in MetaRocq.PCUIC.PCUICCumulProp]
cmp_True_subst_instance [in MetaRocq.PCUIC.PCUICCumulProp]
cofix_subst_nth [in MetaRocq.Erasure.Prelim]
cofix_subst_length [in MetaRocq.Template.Typing]
cofix_subst_instance_subst [in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
cofix_subst_dearg [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
cofix_subst_length [in MetaRocq.PCUIC.Syntax.PCUICCases]
cofix_subst_length [in MetaRocq.Erasure.EGlobalEnv]
combine_map_id [in MetaRocq.Utils.MRList]
common_typing [in MetaRocq.PCUIC.PCUICPrincipality]
commutes_disj_joinable [in MetaRocq.PCUIC.PCUICConfluence]
commutes_diamonds_diamond [in MetaRocq.PCUIC.PCUICConfluence]
commut_lift_subst [in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
commut_lift_subst_rec [in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
commut_lift_subst [in MetaRocq.Template.LiftSubst]
commut_lift_subst_rec [in MetaRocq.Template.LiftSubst]
commut_lift_subst [in MetaRocq.Erasure.ELiftSubst]
commut_lift_subst_rec [in MetaRocq.Erasure.ELiftSubst]
CompareSpec_Proper [in MetaRocq.Utils.MRCompare]
compare_eq_refl [in MetaRocq.Utils.ByteCompareSpec]
compare_spec [in MetaRocq.Utils.ByteCompareSpec]
compare_eq [in MetaRocq.Utils.ByteCompareSpec]
compare_opp [in MetaRocq.Utils.ByteCompareSpec]
compare_equiv [in MetaRocq.Utils.ByteCompareSpec]
compare_decls_lift_decl [in MetaRocq.PCUIC.PCUICEquality]
compare_decl_map [in MetaRocq.PCUIC.PCUICEquality]
compare_decl_impl_ondecl [in MetaRocq.PCUIC.PCUICEquality]
compare_decls_impl [in MetaRocq.PCUIC.PCUICEquality]
compare_cont_trans [in MetaRocq.Utils.MRCompare]
compare_cont_CompOpp [in MetaRocq.Utils.MRCompare]
compare_sort_type [in MetaRocq.Common.Universes]
compare_context_subset [in MetaRocq.PCUIC.Conversion.PCUICWeakeningEnvConv]
compare_decl_subset [in MetaRocq.PCUIC.Conversion.PCUICWeakeningEnvConv]
compare_term_subset [in MetaRocq.PCUIC.Conversion.PCUICWeakeningEnvConv]
compare_sortP_gen [in MetaRocq.SafeChecker.PCUICEqualityDec]
compare_universeP_gen [in MetaRocq.SafeChecker.PCUICEqualityDec]
compare_global_instance_refl [in MetaRocq.SafeChecker.PCUICEqualityDec]
compare_global_instance_impl [in MetaRocq.SafeChecker.PCUICEqualityDec]
compare_context_cumul_pb_context [in MetaRocq.PCUIC.PCUICContextConversion]
compare_sort_subst_instance [in MetaRocq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
compare_term_mkApps_r_inv [in MetaRocq.PCUIC.PCUICConversion]
compare_term_mkApps_l_inv [in MetaRocq.PCUIC.PCUICConversion]
compare_term_subst_instance [in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
compare_context_config_impl [in MetaRocq.PCUIC.Conversion.PCUICWeakeningConfigConv]
compare_decl_config_impl [in MetaRocq.PCUIC.Conversion.PCUICWeakeningConfigConv]
compare_term_config_impl [in MetaRocq.PCUIC.Conversion.PCUICWeakeningConfigConv]
compare_universe_instance_variance_complete [in MetaRocq.SafeChecker.PCUICSafeConversion]
compare_universe_variance_complete [in MetaRocq.SafeChecker.PCUICSafeConversion]
compare_universeb_make_complete [in MetaRocq.SafeChecker.PCUICSafeConversion]
compare_universeb_complete [in MetaRocq.SafeChecker.PCUICSafeConversion]
compile_value_erase_mkApps [in MetaRocq.Erasure.ErasureFunctionProperties]
compile_evalue_strip [in MetaRocq.ErasurePlugin.ErasureCorrectness]
compile_evalue_box_firstorder [in MetaRocq.ErasurePlugin.ErasureCorrectness]
compile_evalue_erase [in MetaRocq.ErasurePlugin.ErasureCorrectness]
compile_evalue_box_mkApps [in MetaRocq.ErasurePlugin.ErasureCorrectness]
compile_evalue_box_strip_mkApps [in MetaRocq.ErasurePlugin.ErasureCorrectness]
compile_value_box_mkApps [in MetaRocq.ErasurePlugin.ErasureCorrectness]
complete_ctx_mask_length [in MetaRocq.Erasure.Typed.Optimize]
compose_transforms_correct [in MetaRocq.Erasure.Typed.Transform]
compose_ren [in MetaRocq.PCUIC.PCUICSigmaCalculus]
compose_ids_l [in MetaRocq.PCUIC.PCUICSigmaCalculus]
compose_ids_r [in MetaRocq.PCUIC.PCUICSigmaCalculus]
compose_map_decl [in MetaRocq.Common.BasicAst]
compose_map_def [in MetaRocq.Common.BasicAst]
compose_on_snd [in MetaRocq.Utils.MRProd]
compose_map_def [in MetaRocq.Erasure.ELiftSubst]
concat_sing [in MetaRocq.Erasure.EWcbvEvalNamed]
confluent_union [in MetaRocq.PCUIC.PCUICConfluence]
consistent_extension_on_union [in MetaRocq.Common.Universes]
consistent_extension_on_empty [in MetaRocq.Common.Universes]
consistent_instance_wf_sort [in MetaRocq.SafeChecker.PCUICEqualityDec]
consistent_extension_on_iff [in MetaRocq.Common.UniversesDec]
consistent_extension_on_iff_subgraph_helper [in MetaRocq.Common.UniversesDec]
consistent_extension_on_iff_declare_and_uniquify_and_combine_levels [in MetaRocq.Common.UniversesDec]
consistent_instance_valid [in MetaRocq.PCUIC.PCUICInductiveInversion]
consistent_instance_poly_length [in MetaRocq.PCUIC.PCUICInductiveInversion]
consistent_extension_on_global [in MetaRocq.SafeChecker.PCUICSafeChecker]
consistent_instance_ext_subst_abs_inds [in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
consistent_instance_ext_subst_abs_univ [in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
consistent_instance_ext_subst_abs [in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
consistent_instance_ext_subst_abs_level [in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
consistent_instance_ext_abstract_instance [in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
consistent_instance_valid_constraints [in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
consistent_ext_trans [in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
consistent_ext_trans_polymorphic_cases [in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
consistent_ext_trans_polymorphic_case_aux [in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
consistent_instance_declared [in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
consistent_instance_ext_wf [in MetaRocq.PCUIC.PCUICWfUniverses]
consistent_instance_ext_wf [in MetaRocq.SafeChecker.PCUICSafeConversion]
consistent_ext_on_full_ext [in MetaRocq.Common.uGraph]
consistent_ext_on_full_ext0 [in MetaRocq.Common.uGraph]
ConstraintSetsUIP.ok_irrel [in MetaRocq.Common.Reflect]
ConstraintSet_In__declare_and_uniquify_levels_2__1 [in MetaRocq.Common.UniversesDec]
ConstraintSet_In__declare_and_uniquify_and_combine_levels_2__0 [in MetaRocq.Common.UniversesDec]
ConstraintSet_In__declare_and_uniquify_and_combine_levels_1__1 [in MetaRocq.Common.UniversesDec]
ConstraintSet_In__declare_and_uniquify_and_combine_levels_1__0 [in MetaRocq.Common.UniversesDec]
ConstraintSet_In_fold_add [in MetaRocq.Common.UniversesDec]
ConstraintType.compare_spec [in MetaRocq.Common.Universes]
ConstraintType.eq_dec [in MetaRocq.Common.Universes]
constraint_lt_irrel [in MetaRocq.Common.Reflect]
constraint_type_lt_level_irrel [in MetaRocq.Common.Reflect]
constructor_isprop_pars_decl_params [in MetaRocq.Erasure.EImplementBox]
constructor_declared [in MetaRocq.Template.EtaExpand]
constructor_isprop_pars_decl_constructor [in MetaRocq.Erasure.EGenericGlobalMap]
constructor_isprop_pars_decl_inductive [in MetaRocq.Erasure.EGenericGlobalMap]
constructor_cumulative_indices [in MetaRocq.PCUIC.PCUICInductiveInversion]
constructor_isprop_pars_decl_inductive [in MetaRocq.Erasure.EOptimizePropDiscr]
constructor_isprop_pars_decl_constructor [in MetaRocq.Erasure.EGenericMapEnv]
constructor_isprop_pars_decl_inductive [in MetaRocq.Erasure.EGenericMapEnv]
constructor_isprop_pars_decl_constructor [in MetaRocq.Erasure.EReorderCstrs]
constructor_isprop_pars_decl_inductive [in MetaRocq.Erasure.EReorderCstrs]
constructor_isprop_pars_decl_params [in MetaRocq.Erasure.EConstructorsAsBlocks]
constructor_isprop_pars_decl_in_env [in MetaRocq.Erasure.EWcbvEvalNamed]
constructor_isprop_pars_decl_constructor [in MetaRocq.Erasure.EInlineProjections]
constructor_isprop_pars_decl_inductive [in MetaRocq.Erasure.EInlineProjections]
constructor_isprop_pars_decl_trans_env_debox_types [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
constructor_isprop_pars_decl_trans_env_dearg_env [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
constructor_isprop_pars_inductive_pars [in MetaRocq.Erasure.ERemoveParams]
constructor_isprop_pars_decl_lookup [in MetaRocq.Erasure.ERemoveParams]
constructor_isprop_pars_decl_constructor [in MetaRocq.Erasure.ECoInductiveToInductive]
constructor_isprop_pars_decl_inductive [in MetaRocq.Erasure.ECoInductiveToInductive]
Construct_Ind_ind_eq' [in MetaRocq.PCUIC.PCUICInductiveInversion]
Construct_Ind_ind_eq [in MetaRocq.PCUIC.PCUICInductiveInversion]
construct_cofix_rename [in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
construct_cofix_discr_match [in MetaRocq.PCUIC.Syntax.PCUICViews]
cons_prefix [in MetaRocq.Utils.MRList]
ContextSet.equal_spec [in MetaRocq.Common.Universes]
ContextSet.subsetP [in MetaRocq.Common.Universes]
ContextSet.subset_spec [in MetaRocq.Common.Universes]
contextual_closure_red [in MetaRocq.PCUIC.PCUICReduction]
context_subst_subst_expand_lets [in MetaRocq.PCUIC.PCUICContextSubst]
context_subst_subst_extended_subst [in MetaRocq.PCUIC.PCUICContextSubst]
context_subst_app [in MetaRocq.PCUIC.PCUICContextSubst]
context_subst_fun' [in MetaRocq.PCUIC.PCUICContextSubst]
context_subst_fun [in MetaRocq.PCUIC.PCUICContextSubst]
context_subst_length2 [in MetaRocq.PCUIC.PCUICContextSubst]
context_subst_assumptions_length [in MetaRocq.PCUIC.PCUICContextSubst]
context_subst_length [in MetaRocq.PCUIC.PCUICContextSubst]
context_position_valid [in MetaRocq.PCUIC.Syntax.PCUICPosition]
context_position_atpos [in MetaRocq.PCUIC.Syntax.PCUICPosition]
context_assumptions_bound [in MetaRocq.PCUIC.PCUICSR]
context_assumptions_expand_lets_k_ctx [in MetaRocq.PCUIC.PCUICSR]
context_pres_let_bodies_red [in MetaRocq.PCUIC.PCUICRedTypeIrrelevance]
context_pres_let_bodies_red1 [in MetaRocq.PCUIC.PCUICRedTypeIrrelevance]
context_position_nlctx [in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
context_assumptions_subst [in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
context_assumptions_subst [in MetaRocq.PCUIC.PCUICSpine]
context_assumptions_lift [in MetaRocq.PCUIC.PCUICSpine]
context_assumptions_subst_telescope [in MetaRocq.PCUIC.PCUICSpine]
context_subst_subst [in MetaRocq.PCUIC.PCUICSpine]
context_subst_app_inv [in MetaRocq.PCUIC.PCUICSpine]
context_conversion [in MetaRocq.PCUIC.Typing.PCUICContextConversionTyp]
context_cumulativity [in MetaRocq.PCUIC.Typing.PCUICContextConversionTyp]
context_cumulativity_prop [in MetaRocq.PCUIC.Typing.PCUICContextConversionTyp]
context_assumptions_expand_lets_ctx [in MetaRocq.PCUIC.utils.PCUICAstUtils]
context_assumptions_smash_context [in MetaRocq.PCUIC.utils.PCUICAstUtils]
context_cumulativity_app [in MetaRocq.PCUIC.PCUICContextConversion]
context_cumulativity_wf_app [in MetaRocq.PCUIC.PCUICContextConversion]
context_assumptions_lift [in MetaRocq.Template.EtaExpand]
context_assumptions_lift' [in MetaRocq.Template.EtaExpand]
context_assumptions_fold_context_k_defs [in MetaRocq.Template.EtaExpand]
context_assumptions_firstn [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
context_cumulativity_spec [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
context_assumptions_set_binder_name [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
context_assumptions_map [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
context_subst_extended_subst [in MetaRocq.PCUIC.PCUICContexts]
context_subst_lift [in MetaRocq.PCUIC.PCUICContexts]
context_assumptions_context [in MetaRocq.PCUIC.PCUICSigmaCalculus]
context_assumptions_mapi_context [in MetaRocq.PCUIC.PCUICAst]
context_depth_inst_case_context [in MetaRocq.PCUIC.Syntax.PCUICDepth]
context_subst_to_extended_list_k [in MetaRocq.PCUIC.PCUICInductives]
context_conversion_cumul_prop [in MetaRocq.PCUIC.PCUICCumulProp]
context_assumptions_fake_params [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
context_assumptions_smash [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
context_assumptions_smash_context'' [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
context_assumptions_smash_context' [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
context_assumptions_fold_context_term [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
context_cumulativity_wt_decl [in MetaRocq.SafeChecker.PCUICTypeChecker]
context_cumulativity_welltyped [in MetaRocq.SafeChecker.PCUICTypeChecker]
context_assumptions_map2_set_binder_name [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
context_assumptions_map [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
context_assumptions_map [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
Conversion.All_decls_alpha_pb_impl [in MetaRocq.Common.EnvironmentTyping]
convSpec_renameP [in MetaRocq.PCUIC.Typing.PCUICRenameTyp]
convSpec_subst_instance [in MetaRocq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
convSpec_convAlgo_curry [in MetaRocq.PCUIC.PCUICConversion]
convSpec_convAlgo [in MetaRocq.PCUIC.PCUICConversion]
convSpec_cumulSpec [in MetaRocq.PCUIC.PCUICConversion]
convSpec0_ind_all [in MetaRocq.PCUIC.PCUICCumulativitySpec]
conv_arity_Is_conv_to_Arity [in MetaRocq.Erasure.Typed.Erasure]
conv_cumul_inv [in MetaRocq.PCUIC.PCUICCumulativity]
conv_cumul [in MetaRocq.PCUIC.PCUICCumulativity]
conv_cumul2 [in MetaRocq.PCUIC.PCUICCumulativity]
conv_ctx_set_binder_name [in MetaRocq.PCUIC.PCUICSR]
conv_refl' [in MetaRocq.PCUIC.PCUICSR]
conv_context_rel_to_extended_list [in MetaRocq.PCUIC.PCUICSR]
conv_context_rel_reln [in MetaRocq.PCUIC.PCUICSR]
conv_context_smash_end [in MetaRocq.PCUIC.PCUICSR]
conv_context_app [in MetaRocq.Erasure.Prelim]
conv_arity_Is_conv_to_Arity [in MetaRocq.SafeChecker.PCUICSafeReduce]
conv_cum_zipp [in MetaRocq.PCUIC.PCUICSafeLemmata]
conv_alt_it_mkProd_or_LetIn [in MetaRocq.PCUIC.PCUICSafeLemmata]
conv_alt_it_mkLambda_or_LetIn [in MetaRocq.PCUIC.PCUICSafeLemmata]
conv_context_wf_local_app [in MetaRocq.Erasure.ErasureProperties]
conv_context_app_same [in MetaRocq.PCUIC.PCUICContextConversion]
conv_cumul_context [in MetaRocq.PCUIC.PCUICContextConversion]
conv_alt_red_ctx_inv [in MetaRocq.PCUIC.PCUICContextConversion]
conv_alt_red_ctx [in MetaRocq.PCUIC.PCUICContextConversion]
conv_leq_context_upto_inv [in MetaRocq.PCUIC.PCUICContextConversion]
conv_leq_context_upto [in MetaRocq.PCUIC.PCUICContextConversion]
conv_eq_context_upto [in MetaRocq.PCUIC.PCUICContextConversion]
conv_decorate_hetero [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
conv_decorate [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
conv_ctx_subst_instance [in MetaRocq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
conv_decls_subst_instance [in MetaRocq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
conv_betas_typed [in MetaRocq.PCUIC.PCUICInductiveInversion]
conv_decls_fix_context [in MetaRocq.PCUIC.PCUICInductiveInversion]
conv_decls_fix_context_gen [in MetaRocq.PCUIC.PCUICInductiveInversion]
conv_eq_ctx [in MetaRocq.PCUIC.PCUICInductiveInversion]
conv_betas [in MetaRocq.PCUIC.PCUICConversion]
conv_inds [in MetaRocq.PCUIC.PCUICConversion]
conv_cum_Lambda [in MetaRocq.PCUIC.PCUICConversion]
conv_cum_red_conv_iff [in MetaRocq.PCUIC.PCUICConversion]
conv_cum_red_iff [in MetaRocq.PCUIC.PCUICConversion]
conv_cum_red_conv_inv [in MetaRocq.PCUIC.PCUICConversion]
conv_cum_red_inv [in MetaRocq.PCUIC.PCUICConversion]
conv_cum_red_conv [in MetaRocq.PCUIC.PCUICConversion]
conv_cum_red [in MetaRocq.PCUIC.PCUICConversion]
conv_cum_conv_ctx [in MetaRocq.PCUIC.PCUICConversion]
conv_red_conv [in MetaRocq.PCUIC.PCUICConversion]
conv_Prod_inv [in MetaRocq.PCUIC.PCUICConversion]
conv_renameP [in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
conv_context_smash [in MetaRocq.PCUIC.PCUICContexts]
conv_refl' [in MetaRocq.Template.Typing]
conv_lift_judgment_univ [in MetaRocq.PCUIC.Bidirectional.BDFromPCUIC]
conv_lift_judgment [in MetaRocq.PCUIC.Bidirectional.BDFromPCUIC]
conv_infer_ind [in MetaRocq.PCUIC.Bidirectional.BDFromPCUIC]
conv_infer_prod [in MetaRocq.PCUIC.Bidirectional.BDFromPCUIC]
conv_infer_sort [in MetaRocq.PCUIC.Bidirectional.BDFromPCUIC]
conv_check [in MetaRocq.PCUIC.Bidirectional.BDFromPCUIC]
conv_ctx_prop_app [in MetaRocq.PCUIC.PCUICCumulProp]
conv_ctx_prop_refl [in MetaRocq.PCUIC.PCUICCumulProp]
conv_sort_inv [in MetaRocq.PCUIC.PCUICCumulProp]
conv_cum_tProj_inv [in MetaRocq.PCUIC.PCUICConvCumInversion]
conv_cum_tCoFix_inv [in MetaRocq.PCUIC.PCUICConvCumInversion]
conv_cum_tFix_inv [in MetaRocq.PCUIC.PCUICConvCumInversion]
conv_cum_tCase_inv [in MetaRocq.PCUIC.PCUICConvCumInversion]
conv_cum_mkApps_inv [in MetaRocq.PCUIC.PCUICConvCumInversion]
conv_conv_cum_r [in MetaRocq.PCUIC.PCUICConvCumInversion]
conv_conv_cum_l [in MetaRocq.PCUIC.PCUICConvCumInversion]
conv_cum_alt [in MetaRocq.PCUIC.PCUICConvCumInversion]
conv_to_arity_cumul [in MetaRocq.Erasure.EArities]
conv_cum_red_inv [in MetaRocq.SafeChecker.PCUICSafeConversion]
conv_cum_red_conv_inv [in MetaRocq.SafeChecker.PCUICSafeConversion]
conv_context_decl [in MetaRocq.SafeChecker.PCUICSafeConversion]
conv_decls_irrel_sec [in MetaRocq.SafeChecker.PCUICTypeChecker]
cored_prod_r [in MetaRocq.Erasure.Typed.Erasure]
cored_prod_l [in MetaRocq.Erasure.Typed.Erasure]
cored_welltyped [in MetaRocq.SafeChecker.PCUICSafeReduce]
cored_zipc [in MetaRocq.PCUIC.PCUICSafeLemmata]
cored_red_cored [in MetaRocq.PCUIC.PCUICSafeLemmata]
cored_const [in MetaRocq.PCUIC.PCUICSafeLemmata]
cored_context [in MetaRocq.PCUIC.PCUICSafeLemmata]
cored_red [in MetaRocq.PCUIC.PCUICSafeLemmata]
cored_proj [in MetaRocq.PCUIC.PCUICSafeLemmata]
cored_case [in MetaRocq.PCUIC.PCUICSafeLemmata]
cored_red_trans [in MetaRocq.PCUIC.PCUICSafeLemmata]
cored_trans' [in MetaRocq.PCUIC.PCUICSafeLemmata]
cored_welltyped [in MetaRocq.PCUIC.PCUICSafeLemmata]
cored_it_mkLambda_or_LetIn [in MetaRocq.PCUIC.PCUICSafeLemmata]
cored_extends [in MetaRocq.Erasure.ErasureFunctionProperties]
cored_cored' [in MetaRocq.PCUIC.PCUICSN]
cored_eq_context_upto_names [in MetaRocq.PCUIC.PCUICSN]
cored_upto [in MetaRocq.PCUIC.PCUICSN]
cored_alt [in MetaRocq.PCUIC.PCUICSN]
cored_redp [in MetaRocq.SafeChecker.PCUICWfReduction]
cored'_postpone [in MetaRocq.PCUIC.PCUICSN]
correct_valuation_of_labelling_satisfies [in MetaRocq.Common.uGraph]
correct_labelling_of_valuation_satisfies_iff [in MetaRocq.Common.uGraph]
count_zeros_nth_error [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
count_ones_zeros [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
count_zeros_distr_app [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
count_zeros_repeat [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
count_zeros_rev [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
count_zeros_le [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
csort_sup_mon [in MetaRocq.Common.Universes]
csort_sup_not_uproplevel [in MetaRocq.Common.Universes]
csort_sup_comm [in MetaRocq.Common.Universes]
cstr_branch_context_assumptions [in MetaRocq.PCUIC.PCUICProgress]
cstr_branch_context_length [in MetaRocq.Template.TypingWf]
cstr_branch_context_assumptions [in MetaRocq.PCUIC.Syntax.PCUICCases]
cstr_branch_context_length [in MetaRocq.PCUIC.Syntax.PCUICCases]
cstr_branch_context_assumptions [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
cstr_branch_context_assumptions [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
cstr_indices_length [in MetaRocq.PCUIC.PCUICCasesHelper]
csubst_closed [in MetaRocq.Erasure.ECSubst]
csubst_mkApps [in MetaRocq.Erasure.ECSubst]
csubst_mkApps [in MetaRocq.TemplatePCUIC.TemplateToPCUICWcbvEval]
csubst_mkApps [in MetaRocq.Erasure.EEtaExpandedFix]
csubst_closed [in MetaRocq.Erasure.EOptimizePropDiscr]
csubst_mkApps [in MetaRocq.Erasure.EOptimizePropDiscr]
csubst_closed [in MetaRocq.Erasure.ECoInductiveToInductive]
csubst_mkApps [in MetaRocq.Erasure.ECoInductiveToInductive]
CS_For_all_add [in MetaRocq.Common.Universes]
CS_For_all_union [in MetaRocq.Common.Universes]
CS_union_empty [in MetaRocq.Common.Universes]
ctxmap_fix_subst [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
ctxmap_cofix_subst [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
ctxmap_ext [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
ctx_inst_merge' [in MetaRocq.PCUIC.PCUICSR]
ctx_inst_merge [in MetaRocq.PCUIC.PCUICSR]
ctx_inst_eq_context [in MetaRocq.PCUIC.PCUICSpine]
ctx_inst_open_terms [in MetaRocq.PCUIC.PCUICSpine]
ctx_inst_smash [in MetaRocq.PCUIC.PCUICSpine]
ctx_inst_smash_acc [in MetaRocq.PCUIC.PCUICSpine]
ctx_inst_cumul [in MetaRocq.PCUIC.PCUICSpine]
ctx_inst_sub_subst [in MetaRocq.PCUIC.PCUICSpine]
ctx_inst_sub_to_extended_list_k [in MetaRocq.PCUIC.PCUICSpine]
ctx_inst_spine_subst [in MetaRocq.PCUIC.PCUICSpine]
ctx_inst_ass [in MetaRocq.PCUIC.PCUICSpine]
ctx_inst_def [in MetaRocq.PCUIC.PCUICSpine]
ctx_inst_app_sub [in MetaRocq.PCUIC.PCUICSpine]
ctx_inst_sub_eq [in MetaRocq.PCUIC.PCUICSpine]
ctx_inst_app_inv [in MetaRocq.PCUIC.PCUICSpine]
ctx_inst_app [in MetaRocq.PCUIC.PCUICSpine]
ctx_inst_subst_length [in MetaRocq.PCUIC.PCUICSpine]
ctx_inst_sub_spec [in MetaRocq.PCUIC.PCUICSpine]
ctx_inst_weaken [in MetaRocq.PCUIC.PCUICSpine]
ctx_inst_subst [in MetaRocq.PCUIC.PCUICSpine]
ctx_inst_length [in MetaRocq.PCUIC.PCUICSpine]
ctx_inst_inst [in MetaRocq.PCUIC.PCUICSpine]
ctx_inst_on_universes [in MetaRocq.SafeChecker.PCUICEqualityDec]
ctx_inst_wt [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
ctx_inst_expand_lets [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
ctx_inst_bd_typing [in MetaRocq.PCUIC.Bidirectional.BDToPCUIC]
ctx_inst_impl [in MetaRocq.PCUIC.Bidirectional.BDToPCUIC]
ctx_inst_app_weak [in MetaRocq.PCUIC.PCUICInductiveInversion]
ctx_inst_eq_context [in MetaRocq.PCUIC.PCUICAlpha]
ctx_length_rev_ind [in MetaRocq.PCUIC.Syntax.PCUICInduction]
ctx_length_ind [in MetaRocq.PCUIC.Syntax.PCUICInduction]
ctx_inst_wt [in MetaRocq.SafeChecker.PCUICSafeChecker]
ctx_inst_smash [in MetaRocq.SafeChecker.PCUICSafeChecker]
ctx_inst_typing_bd [in MetaRocq.PCUIC.Bidirectional.BDFromPCUIC]
ctx_inst_app_impl [in MetaRocq.PCUIC.Bidirectional.BDFromPCUIC]
ctx_inst_length [in MetaRocq.PCUIC.Bidirectional.BDFromPCUIC]
ctx_inst_wt [in MetaRocq.SafeChecker.PCUICTypeChecker]
ctx_inst_closed [in MetaRocq.PCUIC.Typing.PCUICClosedTyp]
cumulAlgo_cumulSpec [in MetaRocq.PCUIC.PCUICConversion]
cumulSpec_renameP [in MetaRocq.PCUIC.Typing.PCUICRenameTyp]
cumulSpec_subst_instance [in MetaRocq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
cumulSpec_typed_cumulAlgo [in MetaRocq.PCUIC.PCUICConversion]
cumulSpec_cumulAlgo_curry [in MetaRocq.PCUIC.PCUICConversion]
cumulSpec_cumulAlgo [in MetaRocq.PCUIC.PCUICConversion]
cumulSpec0_rect [in MetaRocq.PCUIC.PCUICCumulativitySpec]
cumul_App_l [in MetaRocq.PCUIC.PCUICCumulativity]
cumul_alt [in MetaRocq.PCUIC.PCUICCumulativity]
cumul_Sort_Prod_discr [in MetaRocq.Erasure.Prelim]
cumul_sprop2 [in MetaRocq.PCUIC.PCUICElimination]
cumul_sprop1 [in MetaRocq.PCUIC.PCUICElimination]
cumul_prop2 [in MetaRocq.PCUIC.PCUICElimination]
cumul_prop1 [in MetaRocq.PCUIC.PCUICElimination]
cumul_prop_inv [in MetaRocq.PCUIC.PCUICElimination]
cumul_context_Algo_Spec [in MetaRocq.PCUIC.Typing.PCUICContextConversionTyp]
cumul_context_app_same [in MetaRocq.PCUIC.PCUICContextConversion]
cumul_alt_red_ctx_inv [in MetaRocq.PCUIC.PCUICContextConversion]
cumul_alt_red_ctx [in MetaRocq.PCUIC.PCUICContextConversion]
cumul_pb_alt_red_ctx_inv [in MetaRocq.PCUIC.PCUICContextConversion]
cumul_pb_alt_red_ctx [in MetaRocq.PCUIC.PCUICContextConversion]
cumul_eq_context_upto [in MetaRocq.PCUIC.PCUICContextConversion]
cumul_leq_context_upto [in MetaRocq.PCUIC.PCUICContextConversion]
cumul_pb_compare_context_inv [in MetaRocq.PCUIC.PCUICContextConversion]
cumul_pb_compare_context [in MetaRocq.PCUIC.PCUICContextConversion]
cumul_trans_red_leqterm [in MetaRocq.PCUIC.PCUICContextConversion]
cumul_red_ctx_inv [in MetaRocq.PCUIC.PCUICContextConversion]
cumul_decorate_hetero [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
cumul_type_irrelevance [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
cumul_context_Spec_Algo [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
cumul_decorate [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
cumul_decls_subst_instance [in MetaRocq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
cumul_ctx_relSpec_Algo [in MetaRocq.PCUIC.PCUICInductiveInversion]
cumul_Prod_inv [in MetaRocq.PCUIC.PCUICConversion]
cumul_mkApps [in MetaRocq.PCUIC.PCUICConversion]
cumul_renameP [in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
cumul_predicate_undep [in MetaRocq.PCUIC.PCUICCumulativitySpec]
cumul_ctx_rel_close' [in MetaRocq.SafeChecker.PCUICSafeChecker]
cumul_refl' [in MetaRocq.Template.Typing]
cumul_prop_is_open [in MetaRocq.PCUIC.PCUICCumulProp]
cumul_prop_mkApps_Ind_inv [in MetaRocq.PCUIC.PCUICCumulProp]
cumul_prop_mkApps [in MetaRocq.PCUIC.PCUICCumulProp]
cumul_prop_tLetIn [in MetaRocq.PCUIC.PCUICCumulProp]
cumul_prop_tProd [in MetaRocq.PCUIC.PCUICCumulProp]
cumul_prop_subst_instance [in MetaRocq.PCUIC.PCUICCumulProp]
cumul_prop_args [in MetaRocq.PCUIC.PCUICCumulProp]
cumul_prop_prod_inv [in MetaRocq.PCUIC.PCUICCumulProp]
cumul_prop_cum_pb_r [in MetaRocq.PCUIC.PCUICCumulProp]
cumul_prop_cumul_pb_l [in MetaRocq.PCUIC.PCUICCumulProp]
cumul_prop_trans [in MetaRocq.PCUIC.PCUICCumulProp]
cumul_prop_sym [in MetaRocq.PCUIC.PCUICCumulProp]
cumul_sprop_props [in MetaRocq.PCUIC.PCUICCumulProp]
cumul_prop_props [in MetaRocq.PCUIC.PCUICCumulProp]
cumul_prop_sort [in MetaRocq.PCUIC.PCUICCumulProp]
cumul_prop_alt [in MetaRocq.PCUIC.PCUICCumulProp]
cumul_pb_cumul_prop [in MetaRocq.PCUIC.PCUICCumulProp]
cumul_ind_confluence [in MetaRocq.PCUIC.PCUICCumulProp]
cumul_sort_confluence [in MetaRocq.PCUIC.PCUICCumulProp]
cumul_it_mkProd_or_LetIn_smash [in MetaRocq.PCUIC.PCUICClassification]
cumul_subst_instance [in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
cumul_prop2' [in MetaRocq.Erasure.EArities]
cumul_prop1' [in MetaRocq.Erasure.EArities]
cumul_propositional [in MetaRocq.Erasure.EArities]
cumul_sprop2 [in MetaRocq.Erasure.EArities]
cumul_sprop1 [in MetaRocq.Erasure.EArities]
cumul_prop2 [in MetaRocq.Erasure.EArities]
cumul_prop1 [in MetaRocq.Erasure.EArities]
cumul_ctx_rel_cons [in MetaRocq.SafeChecker.PCUICTypeChecker]
cumul_decls_irrel_sec [in MetaRocq.SafeChecker.PCUICTypeChecker]
cumul_decorate [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
| 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) |