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)

T (lemma)

tApp_mkApps_inj [in MetaCoq.PCUIC.utils.PCUICAstUtils]
tApp_mkApps [in MetaCoq.PCUIC.utils.PCUICAstUtils]
tApp_mkApps [in MetaCoq.SafeChecker.PCUICSafeReduce]
target_edge_of_level [in MetaCoq.Template.common.uGraph]
tauto_sound [in MetaCoq.Examples.tauto]
tCoFix_no_Type [in MetaCoq.Erasure.EArities]
tConstruct_no_Type [in MetaCoq.Erasure.EArities]
template_to_pcuic_typing [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
template_to_pcuic_env_ext [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
template_to_pcuic_env [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
template_to_pcuic [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
template_wf_cons_inv [in MetaCoq.PCUIC.TemplateToPCUICExpanded]
TermSpineView.view_mkApps [in MetaCoq.Erasure.ESpineView]
term_forall_list_ind [in MetaCoq.Erasure.EInduction]
term_noccur_between_list_ind [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
term_closedn_list_ind [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
term_wf_forall_list_ind [in MetaCoq.Template.WfAst]
term_on_free_vars_ind [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
term_subterm_redp [in MetaCoq.SafeChecker.PCUICWfReduction]
term_subterm_red1 [in MetaCoq.SafeChecker.PCUICWfReduction]
term_global_deps_spec [in MetaCoq.Erasure.ErasureFunction]
term_ind_size_app [in MetaCoq.PCUIC.Syntax.PCUICInduction]
term_forall_ctx_list_ind [in MetaCoq.PCUIC.Syntax.PCUICInduction]
term_forall_mkApps_ind [in MetaCoq.PCUIC.Syntax.PCUICInduction]
term_forall_list_ind [in MetaCoq.PCUIC.Syntax.PCUICInduction]
term_ind_depth_app [in MetaCoq.PCUIC.Syntax.PCUICDepth]
term_forall_ctx_list_ind [in MetaCoq.PCUIC.Syntax.PCUICDepth]
term_forall_list_rect [in MetaCoq.Template.Induction]
term_forall_list_ind [in MetaCoq.Template.Induction]
test [in MetaCoq.Examples.tauto]
test_decl_map_decl [in MetaCoq.Template.BasicAst]
test_decl_impl [in MetaCoq.Template.BasicAst]
test_context_app [in MetaCoq.PCUIC.PCUICWfUniverses]
test_context_k_ctx [in MetaCoq.PCUIC.PCUICWfUniverses]
test_context_mapi [in MetaCoq.PCUIC.PCUICWfUniverses]
test_context_k_impl [in MetaCoq.PCUIC.utils.PCUICOnOne]
test_context_k_closed_on_free_vars_ctx [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
test_context_k_on_free_vars_ctx [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
test_context_k_ctx [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
test_context_map [in MetaCoq.PCUIC.PCUICAst]
test_context_k_eq [in MetaCoq.PCUIC.PCUICAst]
test_context_k_eq_spec [in MetaCoq.PCUIC.PCUICAst]
test_context_k_eqP_eq_spec [in MetaCoq.PCUIC.PCUICAst]
test_context_k_eqP_id_spec [in MetaCoq.PCUIC.PCUICAst]
test_decl_conv_decls_map [in MetaCoq.PCUIC.PCUICConversion]
test_context_k_map [in MetaCoq.PCUIC.Syntax.PCUICClosed]
test_context_k_mapi [in MetaCoq.PCUIC.Syntax.PCUICClosed]
test_decl_map_decl [in MetaCoq.PCUIC.Syntax.PCUICClosed]
test_context_k_app [in MetaCoq.PCUIC.Syntax.PCUICClosed]
test2 [in MetaCoq.Examples.tauto]
tfix_map_spec [in MetaCoq.Template.BasicAst]
tfix_forallb_map_spec [in MetaCoq.Template.Ast]
to_extended_list_k_map_subst [in MetaCoq.Template.EtaExpand]
to_extended_list_k_cons [in MetaCoq.PCUIC.utils.PCUICAstUtils]
to_extended_list_lift_above [in MetaCoq.PCUIC.utils.PCUICAstUtils]
to_extended_list_k_spec [in MetaCoq.PCUIC.utils.PCUICAstUtils]
to_extended_list_k_length [in MetaCoq.PCUIC.utils.PCUICAstUtils]
to_extended_list_k_map_subst [in MetaCoq.PCUIC.PCUICSubstitution]
to_N_inj [in MetaCoq.Template.utils.bytestring]
to_extended_list_k_expand_lets [in MetaCoq.PCUIC.PCUICInductives]
to_extended_list_k_map_lift [in MetaCoq.PCUIC.PCUICInductives]
to_extended_list_map_lift [in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
to_extended_list_smash_context_eq [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
to_Z_bounded_bool [in MetaCoq.PCUIC.TemplateToPCUIC]
to_extended_list_case_branch_context [in MetaCoq.PCUIC.PCUICSR]
to_extended_list_set_binder_name [in MetaCoq.PCUIC.PCUICSR]
to_extended_list_k_subst [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
to_extended_list_subst_instance [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
to_extended_list_rename [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
to_extended_list_subst_context_let_expand [in MetaCoq.PCUIC.PCUICContexts]
to_extended_list_length [in MetaCoq.PCUIC.PCUICContexts]
to_extended_list_k_lift_context [in MetaCoq.PCUIC.PCUICContexts]
to_extended_list_k_fold_context_k [in MetaCoq.PCUIC.PCUICContexts]
to_extended_list_k_app [in MetaCoq.PCUIC.PCUICContexts]
tProd_it_mkProd_or_LetIn [in MetaCoq.PCUIC.PCUICConversion]
transform_blocks_eval [in MetaCoq.Erasure.EConstructorsAsBlocks]
transform_wf_global [in MetaCoq.Erasure.EConstructorsAsBlocks]
transform_wellformed [in MetaCoq.Erasure.EConstructorsAsBlocks]
transform_blocks_extends [in MetaCoq.Erasure.EConstructorsAsBlocks]
transform_wellformed' [in MetaCoq.Erasure.EConstructorsAsBlocks]
transform_blocks_declared_constant [in MetaCoq.Erasure.EConstructorsAsBlocks]
transform_blocks_isConstructApp [in MetaCoq.Erasure.EConstructorsAsBlocks]
transform_blocks_tApp [in MetaCoq.Erasure.EConstructorsAsBlocks]
transform_blocks_nth [in MetaCoq.Erasure.EConstructorsAsBlocks]
transform_blocks_cunfold_cofix [in MetaCoq.Erasure.EConstructorsAsBlocks]
transform_blocks_cunfold_fix [in MetaCoq.Erasure.EConstructorsAsBlocks]
transform_blocks_cofix_subst [in MetaCoq.Erasure.EConstructorsAsBlocks]
transform_blocks_fix_subst [in MetaCoq.Erasure.EConstructorsAsBlocks]
transform_blocks_iota_red [in MetaCoq.Erasure.EConstructorsAsBlocks]
transform_blocks_substl [in MetaCoq.Erasure.EConstructorsAsBlocks]
transform_blocks_csubst [in MetaCoq.Erasure.EConstructorsAsBlocks]
transform_blocks_mkApps_eta_fn [in MetaCoq.Erasure.EConstructorsAsBlocks]
transform_blocks_mkApps_eta [in MetaCoq.Erasure.EConstructorsAsBlocks]
transform_blocks_decompose [in MetaCoq.Erasure.EConstructorsAsBlocks]
transform_blocks_mkApps [in MetaCoq.Erasure.EConstructorsAsBlocks]
transportD_compose [in MetaCoq.Translations.MiniHoTT]
transportD_compose [in MetaCoq.Translations.MiniHoTT_paths]
transport_pr1_path_sigma_uncurried [in MetaCoq.Translations.MiniHoTT]
transport_precompose [in MetaCoq.Translations.MiniHoTT]
transport_apD_transportD [in MetaCoq.Translations.MiniHoTT]
transport_compose [in MetaCoq.Translations.MiniHoTT]
transport_pr1_path_sigma_uncurried [in MetaCoq.Translations.MiniHoTT_paths]
transport_precompose [in MetaCoq.Translations.MiniHoTT_paths]
transport_apD_transportD [in MetaCoq.Translations.MiniHoTT_paths]
transport_compose [in MetaCoq.Translations.MiniHoTT_paths]
trans_template_program_wt [in MetaCoq.PCUIC.PCUICTransform]
trans_subst_instance_decl [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
trans_case_branch_type [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
trans_it_mkLambda_or_LetIn [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
trans_wf_cofixpoint [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
trans_wf_fixpoint [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
trans_check_rec_kind [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
trans_check_one_cofix [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
trans_check_one_fix [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
trans_decompose_app [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
trans_destInd [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
trans_nisApp [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
trans_isApp [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
trans_decompose_prod_assum [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
trans_mfix_All2 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
trans_mfix_All [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
trans_branches [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
trans_wf_local_env [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
trans_wf_local' [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
trans_cumul [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
trans_leq_term [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
trans_eq_term_upto_univ [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
trans_eq_context_gen_eq_binder_annot [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
trans_R_global_instance [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
trans_red1 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
trans_bcontext [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
trans_eq_binder_annot [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
trans_case_predicate_context [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
trans_local_set_binder_name_eq [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
trans_local_set_binder [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
trans_set_binder [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
trans_wf [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
trans_cstr_branch_context_eq [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
trans_ind_predicate_context_eq [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
trans_ind_predicate_context [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
trans_to_extended_list [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
trans_reln [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
trans_inst_case_branch_context [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
trans_cstr_branch_context_inst [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
trans_cstr_branch_context [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
trans_inds [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
trans_expand_lets_ctx [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
trans_expand_lets [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
trans_expand_lets_k [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
trans_extended_subst [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
trans_smash_context [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
trans_lift_context [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
trans_subst_context [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
trans_fix_context [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
trans_is_constructor [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
trans_unfold_cofix [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
trans_unfold_fix [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
trans_isLambda [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
trans_nth [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
trans_it_mkProd_or_LetIn [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
trans_mkProd_or_LetIn [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
trans_destr_arity [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
trans_declared_projection [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
trans_dbody [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
trans_dtype [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
trans_type_of_constructor [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
trans_ind_type [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
trans_cst_type [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
trans_subst_instance_ctx [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
trans_subst_instance [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
trans_subst10 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
trans_subst [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
trans_decl_type [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
trans_mkApps [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
trans_declared_constructor [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
trans_declared_inductive [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
trans_consistent_instance_ext [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
trans_constraintSet_in [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
trans_declared_constant [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
trans_lookup [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
trans_in_level_set [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
trans_mem_level_set [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
trans_global_ext_constraints [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
trans_global_ext_levels [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
trans_lift [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
trans_local_app [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
trans_on_global_env [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
trans_consistent_instance_ext_gen [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
trans_env_env_universes [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
trans_projs [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
trans_check_ind_sorts [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
trans_type_local_ctx [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
trans_ind_respects_variance [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
trans_cstr_respects_variance [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
trans_ind_arities [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
trans_cumul_ctx_rel [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
trans_closedn [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
trans_subst_telescope [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
trans_arities_context [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
trans_wf_universe [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
trans_case_branch_type [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
trans_cumulSpec_typed [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
trans_cumulSpec [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
trans_consistent_instance_ext [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
trans_global_decl_universes [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
trans_wf_cofixpoint [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
trans_wf_fixpoint [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
trans_check_rec_kind [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
trans_check_one_cofix [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
trans_check_one_fix [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
trans_decompose_prod_assum [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
trans_decompose_app [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
trans_wf_local_env [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
trans_wf_local [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
trans_cumul_gen [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
trans_red1 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
trans_case_branch_context [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
trans_cstr_branch_context_alpha [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
trans_ind_predicate_context [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
trans_case_predicate_context [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
trans_local_app [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
trans_inst_case_context [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
trans_is_constructor [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
trans_unfold_cofix [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
trans_unfold_fix [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
trans_isLambda [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
trans_iota_red [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
trans_cstr_branch_context [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
trans_smash_context [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
trans_expand_lets_ctx [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
trans_lift_context [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
trans_subst_context [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
trans_expand_lets [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
trans_expand_lets_k [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
trans_extended_subst [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
trans_nth [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
trans_eq_term_list [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
trans_eq_term [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
trans_leq_term [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
trans_eq_term_upto_univ [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
trans_R_global_instance [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
trans_to_extended_list [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
trans_reln [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
trans_ind_npars [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
trans_ind_params_length [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
trans_ind_bodies_length [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
trans_ind_bodies [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
trans_ind_params [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
trans_local_subst_instance [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
trans_it_mkLambda_or_LetIn [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
trans_it_mkProd_or_LetIn [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
trans_inds [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
trans_destArity [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
trans_subst_instance [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
trans_subst [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
trans_mkApps [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
trans_mkApp [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
trans_lift [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
trans_lookup [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
trans_global_decl_weaken [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
trans_ind_body_weakening [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
trans_local_weakening [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
trans_local_length [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
trans_decl_weakening [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
trans_weakening [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
trans_lookup_env [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
trans_global_decls_app [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
trans_lookup_inductive [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
trans_lookup_minductive [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
trans_isFix [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_isRel [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_isConstruct [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_wcbveval [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_closedn [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_csubst [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_wf_ext [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_wf [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_on_udecl [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_projs [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_on_context [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_type_local_ctx [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_cumul_ctx_rel' [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_convSpec' [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_conv' [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_cumul' [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_cumul_ctx_rel [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_convSpec [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_cumulSpec [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_ind_realargs [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_destArity [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_cstr_concl_eq [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_ctx_inst_expand_lets [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_local_subst_telescope [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_global_constraints [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_global_levels [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_case_branch_context [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_subst_telescope [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_arities_context [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_wf_predicate [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_eq_annots [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_type_of_constructor [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_case_branch_type [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_it_mkLambda_or_LetIn [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_wf_cofixpoint [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_wf_fixpoint [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_check_rec_kind [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_check_one_cofix [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_check_one_fix [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_decompose_app [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_destInd [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_nisApp [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_isApp [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_decompose_prod_assum [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_mfix_All [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_branches [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_wf_local_env [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_wf_local' [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_cumul [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_conv [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_leq_term [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_compare_term [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_eq_term_upto_univ [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_eq_context_gen [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_eq_context_gen_eq_binder_annot [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_R_global_instance [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_red1 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_untyped_subslet [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_is_closed_context [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_bbody [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_bcontext [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_eq_binder_annot [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_case_predicate_context [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_local_set_binder_name_eq [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_local_set_binder [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_set_binder [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_cstr_branch_context_eq [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_ind_predicate_context_eq [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_ind_predicate_context [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_to_extended_list [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_reln [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_inst_case_branch_context [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_inst_case_branch_context_gen [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_assumption_context [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_cstr_branch_context_inst [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_cstr_branch_context [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_expand_lets_ctx [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_expand_lets_map [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_expand_lets [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_expand_lets_k [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_extended_subst [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_smash_context [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_lift_context [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_lift_decl [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_subst_context [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_subst_decl [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_fix_context [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_is_constructor [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_unfold_cofix [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_unfold_fix [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_isLambda [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_nth [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_it_mkProd_or_LetIn [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_mkProd_or_LetIn [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_destr_arity [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_declared_projection [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_inds [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_dbody [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_dtype [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_ind_type [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_cst_type [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_subst_instance_ctx [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_subst_instance [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_subst10 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_subst_ctx [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_subst [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_decl_type [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_mkApps [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_declared_constructor [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_declared_inductive [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_consistent_instance_ext [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_constraintSet_in [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_declared_constant [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_lookup [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_in_level_set [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_mem_level_set [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_global_ext_constraints [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_global_ext_levels [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_lift [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_on_free_vars_ctx [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_on_free_vars [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_local_app [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
trans_lookup_projection [in MetaCoq.Erasure.ErasureProperties]
trans_lookup_constructor [in MetaCoq.Erasure.ErasureProperties]
trans_lookup_inductive [in MetaCoq.Erasure.ErasureProperties]
trans_lookup_constant [in MetaCoq.Erasure.ErasureProperties]
trans_wcbvEval [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
trans_cunfold_cofix [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
trans_cunfold_fix [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
trans_cofix_subst [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
trans_fix_subst [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
trans_substl [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
trans_csubst [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
trans_global_env_cons [in MetaCoq.PCUIC.TemplateToPCUICExpanded]
trans_expanded [in MetaCoq.PCUIC.TemplateToPCUICExpanded]
trans_red [in MetaCoq.PCUIC.PCUICReduction]
triangle [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
triangle_gen [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
tsize_downlift_le [in MetaCoq.Examples.tauto]
tsize_downlift [in MetaCoq.Examples.tauto]
tsize_lift [in MetaCoq.Examples.tauto]
tsize_decompose_app [in MetaCoq.Examples.tauto]
tsize_nonzero [in MetaCoq.Examples.tauto]
TT_typing_spine_app [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
typecheck_closed [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
typed_subst [in MetaCoq.PCUIC.PCUICSubstitution]
typed_inst [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
typed_subst_abstract_instance [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
type_inst [in MetaCoq.PCUIC.Typing.PCUICInstTyp]
type_app [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
type_mkApps_napp [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
type_mkApps_tConstruct_n_conv_arity [in MetaCoq.Erasure.EArities]
type_it_mkProd_or_LetIn_sorts [in MetaCoq.PCUIC.PCUICArities]
type_it_mkProd_or_LetIn [in MetaCoq.PCUIC.PCUICArities]
type_mkProd_or_LetIn [in MetaCoq.PCUIC.PCUICArities]
type_ws_cumul_pb [in MetaCoq.PCUIC.PCUICArities]
type_local_ctx_wf [in MetaCoq.PCUIC.PCUICWfUniverses]
type_is_open_term [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
type_closed [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
type_Prop_wf [in MetaCoq.Template.Typing]
type_Prop [in MetaCoq.Template.Typing]
type_local_ctx_wf [in MetaCoq.PCUIC.PCUICInductives]
type_local_ctx_cum [in MetaCoq.PCUIC.PCUICInductives]
type_mkApps_arity [in MetaCoq.PCUIC.PCUICValidity]
type_App' [in MetaCoq.PCUIC.PCUICValidity]
type_ctx_wf_univ [in MetaCoq.PCUIC.PCUICValidity]
type_tCoFix_inv [in MetaCoq.PCUIC.PCUICInductiveInversion]
type_tFix_inv [in MetaCoq.PCUIC.PCUICInductiveInversion]
type_it_mkProd_or_LetIn_smash_middle [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
type_mkApps_napp [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
type_closed_subst [in MetaCoq.Erasure.ErasureProperties]
type_it_mkLambda_or_LetIn [in MetaCoq.PCUIC.PCUICGeneration]
type_mkApps [in MetaCoq.PCUIC.PCUICGeneration]
type_Cumul' [in MetaCoq.PCUIC.PCUICTyping]
type_Prop [in MetaCoq.PCUIC.PCUICTyping]
type_Prop_wf [in MetaCoq.PCUIC.PCUICTyping]
type_reduction_closed [in MetaCoq.PCUIC.PCUICSR]
type_reduction [in MetaCoq.PCUIC.PCUICSR]
type_Cumul_alt [in MetaCoq.PCUIC.PCUICSR]
type_local_ctx_Pclosed [in MetaCoq.PCUIC.Conversion.PCUICClosedConv]
type_local_ctx_All_local_env [in MetaCoq.PCUIC.Conversion.PCUICClosedConv]
type_smash [in MetaCoq.SafeChecker.PCUICSafeChecker]
type_local_ctx_instantiate [in MetaCoq.PCUIC.PCUICContexts]
type_local_ctx_wf_local [in MetaCoq.PCUIC.PCUICContexts]
type_mkApps [in MetaCoq.PCUIC.PCUICSpine]
type_it_mkProd_or_LetIn_inv [in MetaCoq.PCUIC.PCUICSpine]
typing_wf_fixpoint [in MetaCoq.Template.EtaExpand]
typing_renaming_cond_P [in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
typing_value_head [in MetaCoq.PCUIC.PCUICProgress]
typing_value_head_napp [in MetaCoq.PCUIC.PCUICProgress]
typing_spine_sort [in MetaCoq.PCUIC.PCUICProgress]
typing_constructor_arity [in MetaCoq.PCUIC.PCUICProgress]
typing_constructor_arity_exact [in MetaCoq.PCUIC.PCUICProgress]
typing_spine_length [in MetaCoq.PCUIC.PCUICProgress]
typing_ind_env [in MetaCoq.PCUIC.PCUICProgress]
typing_ind_env_app_size [in MetaCoq.PCUIC.PCUICProgress]
typing_spine_pred_strengthen [in MetaCoq.PCUIC.PCUICProgress]
typing_spine_proofs [in MetaCoq.PCUIC.PCUICElimination]
typing_spine_it_mkProd_or_LetIn_full_inv [in MetaCoq.PCUIC.PCUICElimination]
typing_spine_case_predicate [in MetaCoq.PCUIC.PCUICElimination]
typing_spine_app [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
typing_spine_weaken_concl_size [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
typing_spine_weaken_concl [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
typing_spine_inj [in MetaCoq.Erasure.EArities]
typing_spine_wat [in MetaCoq.Erasure.EArities]
typing_spine_Is_conv_to_Arity [in MetaCoq.Erasure.EArities]
typing_spine_mkApps_Ind_ex [in MetaCoq.Erasure.EArities]
typing_spine_red [in MetaCoq.Erasure.EArities]
typing_spine_isType_dom [in MetaCoq.PCUIC.PCUICArities]
typing_spine_WAT_concl [in MetaCoq.PCUIC.PCUICArities]
typing_spine_prod [in MetaCoq.PCUIC.PCUICArities]
typing_spine_weaken_concl [in MetaCoq.PCUIC.PCUICArities]
typing_spine_letin [in MetaCoq.PCUIC.PCUICArities]
typing_spine_letin_inv [in MetaCoq.PCUIC.PCUICArities]
typing_spine_isType_codom [in MetaCoq.PCUIC.PCUICArities]
typing_wf_universe [in MetaCoq.PCUIC.PCUICWfUniverses]
typing_wf_universes [in MetaCoq.PCUIC.PCUICWfUniverses]
typing_closed_context [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
typing_wf_wf [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
typing_ind_env [in MetaCoq.Template.Typing]
typing_wf_local_size [in MetaCoq.Template.Typing]
typing_wf_local [in MetaCoq.Template.Typing]
typing_size_pos [in MetaCoq.Template.Typing]
typing_expand_lets_gen [in MetaCoq.PCUIC.PCUICInductives]
typing_spine_to_extended_list [in MetaCoq.PCUIC.PCUICInductives]
typing_spine_to_extended_list_k_app [in MetaCoq.PCUIC.PCUICInductiveInversion]
typing_spine_to_extended_list_app [in MetaCoq.PCUIC.PCUICInductiveInversion]
typing_leq_term_prop [in MetaCoq.PCUIC.PCUICCumulProp]
typing_ws_cumul_pb [in MetaCoq.PCUIC.PCUICInversion]
typing_closed_ctx [in MetaCoq.PCUIC.PCUICInversion]
typing_alpha [in MetaCoq.PCUIC.PCUICAlpha]
typing_alpha_prop [in MetaCoq.PCUIC.PCUICAlpha]
typing_spine_arity_spine [in MetaCoq.PCUIC.PCUICFirstorder]
typing_spine_wt [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
typing_subst_instance_decl [in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
typing_subst_instance_ctx [in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
typing_subst_instance'' [in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
typing_subst_instance_wf_local [in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
typing_subst_instance' [in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
typing_subst_instance [in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
typing_wellformed [in MetaCoq.Erasure.ErasureProperties]
typing_eq_term [in MetaCoq.PCUIC.PCUICPrincipality]
typing_leq_term [in MetaCoq.PCUIC.PCUICPrincipality]
typing_ind_env [in MetaCoq.PCUIC.PCUICTyping]
typing_ind_env_app_size [in MetaCoq.PCUIC.PCUICTyping]
typing_wf_local_size [in MetaCoq.PCUIC.PCUICTyping]
typing_wf_local [in MetaCoq.PCUIC.PCUICTyping]
typing_size_pos [in MetaCoq.PCUIC.PCUICTyping]
typing_cofix_coind [in MetaCoq.PCUIC.PCUICCanonicity]
typing_evar [in MetaCoq.PCUIC.PCUICCanonicity]
typing_var [in MetaCoq.PCUIC.PCUICCanonicity]
typing_spine_nth_error_None_prod [in MetaCoq.PCUIC.PCUICCanonicity]
typing_spine_nth_error_None [in MetaCoq.PCUIC.PCUICCanonicity]
typing_spine_more_inv [in MetaCoq.PCUIC.PCUICCanonicity]
typing_spine_all_inv [in MetaCoq.PCUIC.PCUICCanonicity]
typing_spine_nth_error [in MetaCoq.PCUIC.PCUICCanonicity]
typing_spine_smash [in MetaCoq.PCUIC.PCUICCanonicity]
typing_spine_arity_mkApps_Ind [in MetaCoq.PCUIC.PCUICCanonicity]
typing_closed_red [in MetaCoq.PCUIC.PCUICSR]
typing_closed_red1 [in MetaCoq.PCUIC.PCUICSR]
typing_rename [in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
typing_rename_P [in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
typing_rename_prop [in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
typing_spine_it_mkProd_or_LetIn_ext_list_inv [in MetaCoq.SafeChecker.PCUICSafeChecker]
typing_spine_it_mkProd_or_LetIn_ext_list_inv_gen [in MetaCoq.SafeChecker.PCUICSafeChecker]
typing_spine_prod_inv [in MetaCoq.SafeChecker.PCUICSafeChecker]
typing_spine_letin_inv' [in MetaCoq.SafeChecker.PCUICSafeChecker]
typing_spine_it_mkProd_or_LetIn_inv [in MetaCoq.SafeChecker.PCUICSafeChecker]
typing_wf [in MetaCoq.Template.TypingWf]
typing_wf_sigma [in MetaCoq.Template.TypingWf]
typing_all_wf_decl [in MetaCoq.Template.TypingWf]
typing_wf_gen [in MetaCoq.Template.TypingWf]
typing_expand_lets [in MetaCoq.PCUIC.PCUICContexts]
typing_spine_ctx_inst_smash [in MetaCoq.PCUIC.PCUICSpine]
typing_spine_nth_error [in MetaCoq.PCUIC.PCUICSpine]
typing_spine_app [in MetaCoq.PCUIC.PCUICSpine]
typing_spine_ctx_inst [in MetaCoq.PCUIC.PCUICSpine]
typing_spine_inv [in MetaCoq.PCUIC.PCUICSpine]
typing_spine_wf_local [in MetaCoq.PCUIC.PCUICSpine]
typing_spine_it_mkProd_or_LetIn_close [in MetaCoq.PCUIC.PCUICSpine]
typing_spine_it_mkProd_or_LetIn_close_make_subst [in MetaCoq.PCUIC.PCUICSpine]
typing_spine_it_mkProd_or_LetIn' [in MetaCoq.PCUIC.PCUICSpine]
typing_spine_it_mkProd_or_LetIn [in MetaCoq.PCUIC.PCUICSpine]
typing_spine_it_mkProd_or_LetIn_gen [in MetaCoq.PCUIC.PCUICSpine]
typing_spine_refl [in MetaCoq.PCUIC.PCUICSpine]
typing_spine_strengthen [in MetaCoq.PCUIC.PCUICSpine]
typing_spine_eq [in MetaCoq.PCUIC.PCUICSpine]
typing_infer_ind [in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
typing_infer_prod [in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
typing_infering_sort [in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
typing_checking [in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
typing_infering [in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
typing_spine_eval [in MetaCoq.Erasure.Prelim]
typing_spine_wt [in MetaCoq.Erasure.Prelim]
typing_spine_inv [in MetaCoq.Erasure.Prelim]



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)