| 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) |
D (lemma)
dearg_branch_body_rec_count_zeros [in MetaRocq.Erasure.Typed.Optimize]dearg_transform_correct [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
dearg_transform_gen_correct [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
dearg_correct [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
dearg_repeat_tBox [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
dearg_branch_body_rec_substl_correct [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
dearg_branch_body_rec_all_zeros [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
dearg_branch_body_rec_dearg [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
dearg_cunfold_cofix [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
dearg_cunfold_fix [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
dearg_substl [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
dearg_dearg_lambdas [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
dearg_elim [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
dearg_subst [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
dearg_aux_subst [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
dearg_expanded [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
dearg_expanded_aux [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
dearg_single_enough_args [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
dearg_branch_body_rec_subst [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
dearg_branch_body_rec_lift [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
dearg_lambdas_lift [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
dearg_mkApps [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
dearg_aux_mkApps [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
dearg_lambdas_correct [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
dearg_single_masked [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
dearg_lambdas_subst [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
dearg_lambdas_nil [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
DeclarationTyping.declared_projection_from_gen [in MetaRocq.Common.EnvironmentTyping]
DeclarationTyping.declared_projection_to_gen [in MetaRocq.Common.EnvironmentTyping]
DeclarationTyping.declared_constructor_from_gen [in MetaRocq.Common.EnvironmentTyping]
DeclarationTyping.declared_constructor_to_gen [in MetaRocq.Common.EnvironmentTyping]
DeclarationTyping.declared_inductive_from_gen [in MetaRocq.Common.EnvironmentTyping]
DeclarationTyping.declared_inductive_to_gen [in MetaRocq.Common.EnvironmentTyping]
DeclarationTyping.declared_minductive_from_gen [in MetaRocq.Common.EnvironmentTyping]
DeclarationTyping.declared_minductive_to_gen [in MetaRocq.Common.EnvironmentTyping]
DeclarationTyping.declared_constant_to_gen [in MetaRocq.Common.EnvironmentTyping]
DeclarationTyping.declared_constant_from_gen [in MetaRocq.Common.EnvironmentTyping]
DeclarationTyping.on_wf_global_env_impl [in MetaRocq.Common.EnvironmentTyping]
DeclarationTyping.on_wf_global_env_impl_config [in MetaRocq.Common.EnvironmentTyping]
DeclarationTyping.refine_type [in MetaRocq.Common.EnvironmentTyping]
declared_minductive_closed_inds [in MetaRocq.PCUIC.Conversion.PCUICClosedConv]
declared_projection_indices [in MetaRocq.PCUIC.PCUICSR]
declared_projection_declared_constructor [in MetaRocq.PCUIC.PCUICSR]
declared_constructor_assumption_context [in MetaRocq.Erasure.Prelim]
declared_projection_projs_nonempty [in MetaRocq.PCUIC.PCUICElimination]
declared_constructor_arity [in MetaRocq.Erasure.ErasureCorrectness]
declared_cstr_levels_sub [in MetaRocq.PCUIC.PCUICWeakeningEnv]
declared_minductive_ind_npars [in MetaRocq.PCUIC.PCUICGlobalEnv]
declared_projection_constructor [in MetaRocq.PCUIC.PCUICGlobalEnv]
declared_constructor_inductive [in MetaRocq.PCUIC.PCUICGlobalEnv]
declared_inductive_minductive' [in MetaRocq.PCUIC.PCUICGlobalEnv]
declared_inductive_minductive [in MetaRocq.PCUIC.PCUICGlobalEnv]
declared_projection_inj [in MetaRocq.PCUIC.PCUICGlobalEnv]
declared_constructor_inj [in MetaRocq.PCUIC.PCUICGlobalEnv]
declared_inductive_inj [in MetaRocq.PCUIC.PCUICGlobalEnv]
declared_constant_inj [in MetaRocq.PCUIC.PCUICGlobalEnv]
declared_inductive_closed_indices [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
declared_inductive_unique_sig [in MetaRocq.PCUIC.PCUICInductiveInversion]
declared_inductive_unique [in MetaRocq.PCUIC.PCUICInductiveInversion]
declared_constructor_valid_ty [in MetaRocq.PCUIC.PCUICInductiveInversion]
declared_constructor_ind_decl [in MetaRocq.PCUIC.PCUICProgress]
declared_projection_type_and_eq [in MetaRocq.PCUIC.PCUICInductives]
declared_projection_type [in MetaRocq.PCUIC.PCUICInductives]
declared_projections_subslet [in MetaRocq.PCUIC.PCUICInductives]
declared_projections [in MetaRocq.PCUIC.PCUICInductives]
declared_projections_subslet_ind [in MetaRocq.PCUIC.PCUICInductives]
declared_constructor_wf_pars_args [in MetaRocq.PCUIC.PCUICInductives]
declared_inductive_valid_type [in MetaRocq.PCUIC.PCUICInductives]
declared_inductive_type [in MetaRocq.PCUIC.PCUICInductives]
declared_constant_All [in MetaRocq.Erasure.EWcbvEvalNamed]
declared_constant_Forall [in MetaRocq.Erasure.EWcbvEvalNamed]
declared_constructor_wf_case_branch_context [in MetaRocq.Template.TypingWf]
declared_inductive_wf_case_predicate_context [in MetaRocq.Template.TypingWf]
declared_minductive_wf [in MetaRocq.Template.TypingWf]
declared_constant_wf [in MetaRocq.Template.TypingWf]
declared_projection_wf [in MetaRocq.Template.TypingWf]
declared_constructor_wf [in MetaRocq.Template.TypingWf]
declared_inductive_wf_params [in MetaRocq.Template.TypingWf]
declared_inductive_wf_ctors [in MetaRocq.Template.TypingWf]
declared_inductive_wf_indices [in MetaRocq.Template.TypingWf]
declared_inductive_wf [in MetaRocq.Template.TypingWf]
declared_env_extends [in MetaRocq.Template.TypingWf]
declared_inductive_wf_global_ext [in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
declared_inductive_wf_ext_wk [in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
declared_constructor_typing_spine_not_arity [in MetaRocq.Erasure.EArities]
declared_constructor_type_not_arity [in MetaRocq.Erasure.EArities]
declared_constant_dearg [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
declared_constant_trans_env [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
declared_global_uctx_global_ext_uctx [in MetaRocq.SafeChecker.PCUICTypeChecker]
declared_projection_lookup [in MetaRocq.Erasure.EGlobalEnv]
declared_constructor_lookup [in MetaRocq.Erasure.EGlobalEnv]
declared_inductive_lookup [in MetaRocq.Erasure.EGlobalEnv]
declared_minductive_lookup [in MetaRocq.Erasure.EGlobalEnv]
declared_constant_lookup [in MetaRocq.Erasure.EGlobalEnv]
declared_projection_unique [in MetaRocq.PCUIC.PCUICWcbvEval]
declared_constructor_unique [in MetaRocq.PCUIC.PCUICWcbvEval]
declared_inductive_lookup [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
declared_inductive_inj [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
declared_projection_closed_type [in MetaRocq.PCUIC.Typing.PCUICClosedTyp]
declared_constructor_closed_indices [in MetaRocq.PCUIC.Typing.PCUICClosedTyp]
declared_constructor_closed_args [in MetaRocq.PCUIC.Typing.PCUICClosedTyp]
declared_constructor_closed_type [in MetaRocq.PCUIC.Typing.PCUICClosedTyp]
declared_constructor_closed_gen_type [in MetaRocq.PCUIC.Typing.PCUICClosedTyp]
declared_minductive_closed_arities [in MetaRocq.PCUIC.Typing.PCUICClosedTyp]
declared_inductive_closed_constructors [in MetaRocq.PCUIC.Typing.PCUICClosedTyp]
declared_inductive_closed_params_inst [in MetaRocq.PCUIC.Typing.PCUICClosedTyp]
declared_inductive_closed_params [in MetaRocq.PCUIC.Typing.PCUICClosedTyp]
declared_inductive_closed_type [in MetaRocq.PCUIC.Typing.PCUICClosedTyp]
declared_constant_closed_body [in MetaRocq.PCUIC.Typing.PCUICClosedTyp]
declared_constant_closed_type [in MetaRocq.PCUIC.Typing.PCUICClosedTyp]
declared_decl_closed [in MetaRocq.PCUIC.Typing.PCUICClosedTyp]
declared_constructor_closed [in MetaRocq.PCUIC.Typing.PCUICClosedTyp]
declared_inductive_closed_pars_indices [in MetaRocq.PCUIC.Typing.PCUICClosedTyp]
declared_projection_closed [in MetaRocq.PCUIC.Typing.PCUICClosedTyp]
declared_inductive_closed [in MetaRocq.PCUIC.Typing.PCUICClosedTyp]
declared_minductive_closed [in MetaRocq.PCUIC.Typing.PCUICClosedTyp]
declared_minductive_closed_ind [in MetaRocq.PCUIC.Typing.PCUICClosedTyp]
declared_decl_closed_ind [in MetaRocq.PCUIC.Typing.PCUICClosedTyp]
declared_projection_closed_ind [in MetaRocq.PCUIC.Typing.PCUICClosedTyp]
declared_constructor_expanded [in MetaRocq.TemplatePCUIC.TemplateToPCUICExpanded]
declared_minductive_expanded [in MetaRocq.TemplatePCUIC.TemplateToPCUICExpanded]
declared_projection_inv [in MetaRocq.PCUIC.Typing.PCUICWeakeningEnvTyp]
declared_constructor_inv_decls [in MetaRocq.PCUIC.Typing.PCUICWeakeningEnvTyp]
declared_inductive_inv_decls [in MetaRocq.PCUIC.Typing.PCUICWeakeningEnvTyp]
declared_minductive_inv_decls [in MetaRocq.PCUIC.Typing.PCUICWeakeningEnvTyp]
declared_constructor_inv [in MetaRocq.PCUIC.Typing.PCUICWeakeningEnvTyp]
declared_inductive_inv [in MetaRocq.PCUIC.Typing.PCUICWeakeningEnvTyp]
declared_minductive_inv [in MetaRocq.PCUIC.Typing.PCUICWeakeningEnvTyp]
declared_constant_inv [in MetaRocq.PCUIC.Typing.PCUICWeakeningEnvTyp]
decls_prefix_wf [in MetaRocq.Erasure.ErasureFunctionProperties]
decl_type_eq_context_upto_names [in MetaRocq.PCUIC.PCUICConfluence]
decl_body_eq_context_upto_names [in MetaRocq.PCUIC.PCUICConfluence]
decl_size_map_decl_hom [in MetaRocq.PCUIC.Syntax.PCUICInduction]
decompose_prod_n_assum_extend_ctx [in MetaRocq.PCUIC.PCUICContextSubst]
decompose_stack_twice [in MetaRocq.PCUIC.Syntax.PCUICPosition]
decompose_stack_at_length [in MetaRocq.PCUIC.Syntax.PCUICPosition]
decompose_stack_at_eq [in MetaRocq.PCUIC.Syntax.PCUICPosition]
decompose_stack_appstack [in MetaRocq.PCUIC.Syntax.PCUICPosition]
decompose_stack_not_app [in MetaRocq.PCUIC.Syntax.PCUICPosition]
decompose_stack_eq [in MetaRocq.PCUIC.Syntax.PCUICPosition]
decompose_app_rec_inv2 [in MetaRocq.Erasure.Prelim]
decompose_app_wf [in MetaRocq.Examples.tauto]
decompose_app_eq [in MetaRocq.Examples.tauto]
decompose_stack_at_appstack_None [in MetaRocq.SafeChecker.PCUICSafeReduce]
decompose_prod_assum_spec [in MetaRocq.PCUIC.PCUICSubstitution]
decompose_prod_assum_it_mkProd_or_LetIn [in MetaRocq.PCUIC.PCUICSubstitution]
decompose_prod_n_assum0 [in MetaRocq.PCUIC.PCUICSubstitution]
decompose_app_subst [in MetaRocq.PCUIC.PCUICSubstitution]
decompose_app_rec_subst [in MetaRocq.PCUIC.PCUICSubstitution]
decompose_stack_stack_cat [in MetaRocq.PCUIC.PCUICSafeLemmata]
decompose_stack_noStackApp [in MetaRocq.PCUIC.PCUICSafeLemmata]
decompose_stack_closed [in MetaRocq.PCUIC.PCUICSafeLemmata]
decompose_prod_assum_it_mkProd [in MetaRocq.Template.AstUtils]
decompose_prod_n_assum_it_mkProd [in MetaRocq.Template.AstUtils]
decompose_app_mkApps [in MetaRocq.Template.AstUtils]
decompose_app_tApp_split [in MetaRocq.Erasure.EUnboxing]
decompose_app_rec_inv' [in MetaRocq.PCUIC.utils.PCUICAstUtils]
decompose_app_rec_eq [in MetaRocq.PCUIC.utils.PCUICAstUtils]
decompose_app_eq_right [in MetaRocq.PCUIC.utils.PCUICAstUtils]
decompose_app_tFix [in MetaRocq.PCUIC.utils.PCUICAstUtils]
decompose_app_rec_tFix [in MetaRocq.PCUIC.utils.PCUICAstUtils]
decompose_app_rec_head [in MetaRocq.PCUIC.utils.PCUICAstUtils]
decompose_app_eq_mkApps [in MetaRocq.PCUIC.utils.PCUICAstUtils]
decompose_app_nonnil [in MetaRocq.PCUIC.utils.PCUICAstUtils]
decompose_app_inv [in MetaRocq.PCUIC.utils.PCUICAstUtils]
decompose_app_rec_inv [in MetaRocq.PCUIC.utils.PCUICAstUtils]
decompose_app_notApp [in MetaRocq.PCUIC.utils.PCUICAstUtils]
decompose_app_rec_notApp [in MetaRocq.PCUIC.utils.PCUICAstUtils]
decompose_prod_assum_it_mkProd [in MetaRocq.PCUIC.utils.PCUICAstUtils]
decompose_prod_n_assum_it_mkProd [in MetaRocq.PCUIC.utils.PCUICAstUtils]
decompose_prod_assum_ctx [in MetaRocq.PCUIC.utils.PCUICAstUtils]
decompose_app_mkApps [in MetaRocq.PCUIC.utils.PCUICAstUtils]
decompose_app_rec_mkApps [in MetaRocq.PCUIC.utils.PCUICAstUtils]
decompose_type_of_constructor [in MetaRocq.Template.EtaExpand]
decompose_prod12 [in MetaRocq.Template.EtaExpand]
decompose_prod_lift [in MetaRocq.Template.EtaExpand]
decompose_prod_assum_upto_names' [in MetaRocq.PCUIC.PCUICAlpha]
decompose_app_upto [in MetaRocq.PCUIC.PCUICAlpha]
decompose_app_rename [in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
decompose_app_rec_rename [in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
decompose_app_tApp_split [in MetaRocq.Erasure.EEtaExpandedFix]
decompose_app_size_tApp2 [in MetaRocq.PCUIC.Syntax.PCUICInduction]
decompose_app_size_tApp1 [in MetaRocq.PCUIC.Syntax.PCUICInduction]
decompose_app_rec_length [in MetaRocq.PCUIC.Syntax.PCUICInduction]
decompose_app_rec_length_mono [in MetaRocq.PCUIC.Syntax.PCUICInduction]
decompose_prod_n_assum_inv [in MetaRocq.SafeChecker.PCUICSafeChecker]
decompose_prod_assum_it_mkProd_or_LetIn' [in MetaRocq.PCUIC.PCUICInductives]
decompose_app_inst [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
decompose_app_rec_inst [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
decompose_app_inv [in MetaRocq.Template.TypingWf]
decompose_app_mkApp [in MetaRocq.Template.TypingWf]
decompose_body_masked_spec [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
decompose_app_app [in MetaRocq.Erasure.EInduction]
decompose_app_notApp [in MetaRocq.Erasure.EInduction]
decompose_app_rec_notApp [in MetaRocq.Erasure.EInduction]
decompose_app_inv [in MetaRocq.Erasure.EInduction]
decompose_app_rec_inv [in MetaRocq.Erasure.EInduction]
decompose_app_size [in MetaRocq.Erasure.EInduction]
decompose_app_rec_size [in MetaRocq.Erasure.EInduction]
decompose_app_inst [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
decompose_prod_assum_mkApps [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
decompose_app_tApp_split [in MetaRocq.Erasure.ERemoveParams]
decompose_prod_assum_it_mkProd_or_LetIn [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
decompose_prod_assum_mkApps_nonnil [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
decompose_app_rec_inv' [in MetaRocq.Erasure.EAstUtils]
decompose_app_rec_eq [in MetaRocq.Erasure.EAstUtils]
decompose_app_eq_right [in MetaRocq.Erasure.EAstUtils]
decompose_app_notApp [in MetaRocq.Erasure.EAstUtils]
decompose_app_rec_notApp [in MetaRocq.Erasure.EAstUtils]
decompose_app_inv [in MetaRocq.Erasure.EAstUtils]
decompose_app_rec_inv [in MetaRocq.Erasure.EAstUtils]
decompose_app_mkApps [in MetaRocq.Erasure.EAstUtils]
decompose_app_rec_mkApps [in MetaRocq.Erasure.EAstUtils]
decompose_app_head_spine [in MetaRocq.Erasure.EAstUtils]
decomp_step_size [in MetaRocq.Examples.tauto]
dec_All [in MetaRocq.PCUIC.PCUICNormal]
depth_subst_instance_context [in MetaRocq.PCUIC.Syntax.PCUICDepth]
depth_subst_context [in MetaRocq.PCUIC.Syntax.PCUICDepth]
depth_subst_decl [in MetaRocq.PCUIC.Syntax.PCUICDepth]
depth_subst_instance [in MetaRocq.PCUIC.Syntax.PCUICDepth]
depth_subst [in MetaRocq.PCUIC.Syntax.PCUICDepth]
depth_lift [in MetaRocq.PCUIC.Syntax.PCUICDepth]
depth_mkApps [in MetaRocq.PCUIC.Syntax.PCUICDepth]
deriv_length_min [in MetaRocq.Erasure.Typed.WcbvEvalAux]
destArity_spec_Some [in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
destArity_spec [in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
destArity_mkApps_Ind [in MetaRocq.PCUIC.utils.PCUICAstUtils]
destArity_mkApps_None [in MetaRocq.PCUIC.utils.PCUICAstUtils]
destArity_tInd [in MetaRocq.PCUIC.utils.PCUICAstUtils]
destArity_tApp [in MetaRocq.PCUIC.utils.PCUICAstUtils]
destArity_tFix [in MetaRocq.PCUIC.utils.PCUICAstUtils]
destArity_it_mkProd_or_LetIn [in MetaRocq.PCUIC.utils.PCUICAstUtils]
destArity_app_Some [in MetaRocq.PCUIC.utils.PCUICAstUtils]
destArity_app [in MetaRocq.PCUIC.utils.PCUICAstUtils]
destArity_app_aux [in MetaRocq.PCUIC.utils.PCUICAstUtils]
destArity_alpha [in MetaRocq.PCUIC.PCUICAlpha]
destArity_it_mkProd_or_LetIn [in MetaRocq.Template.TypingWf]
destArity_spec [in MetaRocq.Template.TypingWf]
destArity_mkApps [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
destInd_spec [in MetaRocq.PCUIC.PCUICAlpha]
destInd_Some_eq [in MetaRocq.PCUIC.PCUICInductives]
destInd_head_lift_inv [in MetaRocq.PCUIC.PCUICInductives]
destInd_head_lift [in MetaRocq.PCUIC.PCUICInductives]
destInd_head_subst [in MetaRocq.PCUIC.PCUICInductives]
destInd_subst_instance [in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
diamond_pred1_rel_alpha [in MetaRocq.PCUIC.PCUICConfluence]
diamond_pred1_rel [in MetaRocq.PCUIC.PCUICConfluence]
diamond_confluent [in MetaRocq.PCUIC.PCUICConfluence]
diamond_t_t_confluent [in MetaRocq.PCUIC.PCUICConfluence]
diamond_t1n_t1n_confluent [in MetaRocq.PCUIC.PCUICConfluence]
diamond_t1n_t_confluent [in MetaRocq.PCUIC.PCUICConfluence]
distr_lift_subst_context [in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
distr_subst [in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
distr_subst_rec [in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
distr_lift_subst10 [in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
distr_lift_subst [in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
distr_lift_subst_rec [in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
distr_lift_subst_context_rec [in MetaRocq.PCUIC.Syntax.PCUICClosed]
distr_subst [in MetaRocq.Template.LiftSubst]
distr_subst_rec [in MetaRocq.Template.LiftSubst]
distr_lift_subst10 [in MetaRocq.Template.LiftSubst]
distr_lift_subst [in MetaRocq.Template.LiftSubst]
distr_lift_subst_rec [in MetaRocq.Template.LiftSubst]
distr_subst [in MetaRocq.Erasure.ELiftSubst]
distr_subst_rec [in MetaRocq.Erasure.ELiftSubst]
distr_lift_subst10 [in MetaRocq.Erasure.ELiftSubst]
distr_lift_subst [in MetaRocq.Erasure.ELiftSubst]
distr_lift_subst_rec [in MetaRocq.Erasure.ELiftSubst]
dlexmod_Acc [in MetaRocq.PCUIC.utils.PCUICUtils]
dlexprod_Acc_gen [in MetaRocq.SafeChecker.PCUICSafeReduce]
dlexprod_Acc [in MetaRocq.PCUIC.utils.PCUICUtils]
dupfree_dec_ident [in MetaRocq.Erasure.EWcbvEvalNamed]
| 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) |