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)

A (lemma)

Acc_fun [in MetaCoq.PCUIC.PCUICSafeLemmata]
acc_dlexmod [in MetaCoq.PCUIC.utils.PCUICUtils]
acc_dlexprod [in MetaCoq.PCUIC.utils.PCUICUtils]
Acc_no_loop [in MetaCoq.SafeChecker.PCUICWfReduction]
Acc_cored_cored' [in MetaCoq.PCUIC.PCUICSN]
Acc_impl [in MetaCoq.PCUIC.PCUICSN]
Acc_no_loop [in MetaCoq.Erasure.ErasureFunction]
acc_dlexprod_gen [in MetaCoq.SafeChecker.PCUICSafeReduce]
acyclic_no_loop_add_uctx [in MetaCoq.Template.common.uGraph]
addnP_strengthen_lift [in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
addnP_shiftnP_k [in MetaCoq.PCUIC.PCUICSubstitution]
addnP_shiftnP_comm [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
addnP_orP [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
addnP_shiftnP [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
addnP_add [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
addnP_xpredT [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
addnP_closedP [in MetaCoq.PCUIC.PCUICContextReduction]
addnP0 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
add_uctx_make_graph2 [in MetaCoq.Template.common.uGraph]
add_gc_of_constraint_spec [in MetaCoq.Template.common.uGraph]
add_uctx_subgraph [in MetaCoq.Template.common.uGraph]
add_uctx_make_graph [in MetaCoq.Template.common.uGraph]
add_level_edges_add_cstrs_comm [in MetaCoq.Template.common.uGraph]
add_level_edges_union [in MetaCoq.Template.common.uGraph]
add_cstrs_union [in MetaCoq.Template.common.uGraph]
add_level_edges_spec [in MetaCoq.Template.common.uGraph]
add_cstrs_spec [in MetaCoq.Template.common.uGraph]
add_suffix_cons [in MetaCoq.Erasure.ErasureFunction]
allbiP [in MetaCoq.Template.utils.All_Forall]
Alli_impl_le [in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
alli_fold_context_k_prop [in MetaCoq.Template.BasicAst]
Alli_rev_All_fold [in MetaCoq.Template.utils.All_Forall]
Alli_All_fold [in MetaCoq.Template.utils.All_Forall]
Alli_map_option_out_mapi_Some_spec [in MetaCoq.Template.utils.All_Forall]
Alli_map_id [in MetaCoq.Template.utils.All_Forall]
Alli_mapi_id [in MetaCoq.Template.utils.All_Forall]
Alli_mapi_spec [in MetaCoq.Template.utils.All_Forall]
Alli_All_mix [in MetaCoq.Template.utils.All_Forall]
Alli_shiftn_inv [in MetaCoq.Template.utils.All_Forall]
Alli_shiftn [in MetaCoq.Template.utils.All_Forall]
Alli_rev_nth_error [in MetaCoq.Template.utils.All_Forall]
Alli_app_inv [in MetaCoq.Template.utils.All_Forall]
Alli_rev_inv [in MetaCoq.Template.utils.All_Forall]
Alli_rev [in MetaCoq.Template.utils.All_Forall]
Alli_shift [in MetaCoq.Template.utils.All_Forall]
Alli_mapi [in MetaCoq.Template.utils.All_Forall]
Alli_nth_error [in MetaCoq.Template.utils.All_Forall]
Alli_app [in MetaCoq.Template.utils.All_Forall]
Alli_All [in MetaCoq.Template.utils.All_Forall]
Alli_mix [in MetaCoq.Template.utils.All_Forall]
Alli_impl [in MetaCoq.Template.utils.All_Forall]
alli_mapi [in MetaCoq.Template.utils.All_Forall]
alli_map [in MetaCoq.Template.utils.All_Forall]
alli_shift [in MetaCoq.Template.utils.All_Forall]
alli_app [in MetaCoq.Template.utils.All_Forall]
alli_shiftn [in MetaCoq.Template.utils.All_Forall]
alli_Alli [in MetaCoq.Template.utils.All_Forall]
alli_impl [in MetaCoq.Template.utils.All_Forall]
alli_ext [in MetaCoq.Template.utils.All_Forall]
Alli_All_mix [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
Alli_map [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
Alli_map_option_out_mapi_Some_spec [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
Alli_map_option_out_mapi_Some_spec' [in MetaCoq.PCUIC.PCUICSubstitution]
alli_subst_instance [in MetaCoq.PCUIC.PCUICFirstorder]
Alli_map [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
Alli_nth_hyp [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
Alli_nth_hyp_ind [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
alli_fold_context_k [in MetaCoq.PCUIC.Syntax.PCUICClosed]
Alli_helper [in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
Alli_id [in MetaCoq.Template.TypingWf]
allowed_eliminations_subset_impl [in MetaCoq.Template.Universes]
All_fold_fold_context_k_defs [in MetaCoq.Template.EtaExpand]
All_local_assum_subst [in MetaCoq.PCUIC.PCUICElimination]
All_local_assum_app [in MetaCoq.PCUIC.PCUICElimination]
All_eval_etaexp [in MetaCoq.Erasure.EEtaExpandedFix]
all_isEtaExp_closedn [in MetaCoq.Erasure.EEtaExpandedFix]
All_map_All [in MetaCoq.Template.utils.All_Forall]
All_remove_last [in MetaCoq.Template.utils.All_Forall]
All_fold_All2_fold [in MetaCoq.Template.utils.All_Forall]
All_fold_All2_fold_impl [in MetaCoq.Template.utils.All_Forall]
All_fold_prod [in MetaCoq.Template.utils.All_Forall]
All_fold_Alli_rev [in MetaCoq.Template.utils.All_Forall]
All_fold_app [in MetaCoq.Template.utils.All_Forall]
All_fold_impl [in MetaCoq.Template.utils.All_Forall]
All_fold_app_inv [in MetaCoq.Template.utils.All_Forall]
All_forall [in MetaCoq.Template.utils.All_Forall]
All_In [in MetaCoq.Template.utils.All_Forall]
All_All2_refl [in MetaCoq.Template.utils.All_Forall]
All_sq [in MetaCoq.Template.utils.All_Forall]
All_prod [in MetaCoq.Template.utils.All_Forall]
All_pair [in MetaCoq.Template.utils.All_Forall]
All_prod_inv [in MetaCoq.Template.utils.All_Forall]
All_forallb_eq_forallb [in MetaCoq.Template.utils.All_Forall]
All_forallb_forallb_spec [in MetaCoq.Template.utils.All_Forall]
All_forallb_map_spec [in MetaCoq.Template.utils.All_Forall]
All_All2_All2_mix [in MetaCoq.Template.utils.All_Forall]
All_All2 [in MetaCoq.Template.utils.All_Forall]
All_repeat [in MetaCoq.Template.utils.All_Forall]
All_All_All2 [in MetaCoq.Template.utils.All_Forall]
All_All2_flex [in MetaCoq.Template.utils.All_Forall]
All_Alli [in MetaCoq.Template.utils.All_Forall]
All_mapi [in MetaCoq.Template.utils.All_Forall]
All_forallb' [in MetaCoq.Template.utils.All_Forall]
All_map_id' [in MetaCoq.Template.utils.All_Forall]
All_safe_nth [in MetaCoq.Template.utils.All_Forall]
All_map_id [in MetaCoq.Template.utils.All_Forall]
All_map_eq [in MetaCoq.Template.utils.All_Forall]
All_nth_error [in MetaCoq.Template.utils.All_Forall]
All_map_inv [in MetaCoq.Template.utils.All_Forall]
All_map [in MetaCoq.Template.utils.All_Forall]
All_impl [in MetaCoq.Template.utils.All_Forall]
All_rev_inv [in MetaCoq.Template.utils.All_Forall]
All_rev [in MetaCoq.Template.utils.All_Forall]
All_rev_map [in MetaCoq.Template.utils.All_Forall]
All_refl [in MetaCoq.Template.utils.All_Forall]
All_mix [in MetaCoq.Template.utils.All_Forall]
All_tip [in MetaCoq.Template.utils.All_Forall]
All_True [in MetaCoq.Template.utils.All_Forall]
All_app_inv [in MetaCoq.Template.utils.All_Forall]
All_app [in MetaCoq.Template.utils.All_Forall]
All_skipn [in MetaCoq.Template.utils.All_Forall]
All_firstn [in MetaCoq.Template.utils.All_Forall]
All_forallb [in MetaCoq.Template.utils.All_Forall]
All_Forall [in MetaCoq.Template.utils.All_Forall]
All_over_All [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
All_All2_refl [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
All_map_option_out_map_Some_spec [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
All_map2 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
All_local_env_map [in MetaCoq.Template.Typing]
All_local_env_app [in MetaCoq.Template.Typing]
All_local_env_lookup [in MetaCoq.Template.Typing]
All_local_env_app_inv [in MetaCoq.Template.Typing]
All_local_env_inst [in MetaCoq.PCUIC.PCUICSubstitution]
All_local_env_subst [in MetaCoq.PCUIC.PCUICSubstitution]
All_fold_tip [in MetaCoq.PCUIC.PCUICEtaExpand]
All_tip [in MetaCoq.PCUIC.PCUICEtaExpand]
all_rels_smash [in MetaCoq.PCUIC.PCUICInductives]
All_decls_on_free_vars_map_impl [in MetaCoq.PCUIC.PCUICParallelReduction]
All_fold_fold_context_k [in MetaCoq.PCUIC.PCUICParallelReduction]
All_decls_on_free_vars_impl [in MetaCoq.PCUIC.PCUICParallelReduction]
All_decls_map [in MetaCoq.PCUIC.PCUICParallelReduction]
All_decls_alpha_pb_ws_decl [in MetaCoq.PCUIC.PCUICAlpha]
All_over_All [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
All_fold_closed_on_free_vars_ctx [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
All_fold_map_context [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
All_fold_on_free_vars_ctx [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
All_mfix_wf [in MetaCoq.PCUIC.Typing.PCUICWeakeningTyp]
All_mapi_spec [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
All_All2_telescopei [in MetaCoq.PCUIC.PCUICConfluence]
All_All2_telescopei_gen [in MetaCoq.PCUIC.PCUICConfluence]
All_decls_alpha_pb_map [in MetaCoq.PCUIC.PCUICConversion]
All_decls_alpha_pb_impl [in MetaCoq.PCUIC.PCUICConversion]
All_local_env_lift_prod_inv [in MetaCoq.PCUIC.PCUICTyping]
All_local_env_prod_inv [in MetaCoq.PCUIC.PCUICTyping]
All_local_env_map [in MetaCoq.PCUIC.PCUICTyping]
All_local_env_lookup [in MetaCoq.PCUIC.PCUICTyping]
All_local_env_app_inv [in MetaCoq.PCUIC.PCUICTyping]
All_local_env_app [in MetaCoq.PCUIC.PCUICTyping]
All_fold_All_mix_left [in MetaCoq.PCUIC.TemplateToPCUICExpanded]
All_fold_map [in MetaCoq.PCUIC.TemplateToPCUICExpanded]
All_local_env_over_subst_instance [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
All_depth [in MetaCoq.PCUIC.Syntax.PCUICDepth]
All_decls_map_right [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
All_decls_on_free_vars_map_impl_inv [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
All_All2_telescopei_rho [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
All_All2_telescopei [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
All_All2_telescopei_gen_rho [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
All_All2_telescopei_gen [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
All_IH' [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
All_IH [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
All_local_env_Pclosed [in MetaCoq.PCUIC.Conversion.PCUICClosedConv]
All_local_env_app_l [in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
All_local_env_wf_decls [in MetaCoq.Template.TypingWf]
All_Alli [in MetaCoq.Template.TypingWf]
All_mapi [in MetaCoq.Template.TypingWf]
All_local_env_wf_decl_inv [in MetaCoq.Template.TypingWf]
All_local_env_wf_decl [in MetaCoq.Template.TypingWf]
all_rels_subst_lift [in MetaCoq.PCUIC.PCUICSpine]
all_rels_subst [in MetaCoq.PCUIC.PCUICSpine]
all_rels_lift [in MetaCoq.PCUIC.PCUICSpine]
all_rels_length [in MetaCoq.PCUIC.PCUICSpine]
All_All2_diag [in MetaCoq.SafeChecker.PCUICEqualityDec]
All2i_All2_All2 [in MetaCoq.Template.utils.All_Forall]
All2i_All2_All2i_All2i [in MetaCoq.Template.utils.All_Forall]
All2i_app_inv [in MetaCoq.Template.utils.All_Forall]
All2i_length [in MetaCoq.Template.utils.All_Forall]
All2i_app_inv_r [in MetaCoq.Template.utils.All_Forall]
All2i_app_inv_l [in MetaCoq.Template.utils.All_Forall]
All2i_nth_error_r [in MetaCoq.Template.utils.All_Forall]
All2i_nth_error_l [in MetaCoq.Template.utils.All_Forall]
All2i_nth_hyp [in MetaCoq.Template.utils.All_Forall]
All2i_nth_impl_gen [in MetaCoq.Template.utils.All_Forall]
All2i_map_right [in MetaCoq.Template.utils.All_Forall]
All2i_map [in MetaCoq.Template.utils.All_Forall]
All2i_rev_ctx_inv [in MetaCoq.Template.utils.All_Forall]
All2i_rev_ctx_gen [in MetaCoq.Template.utils.All_Forall]
All2i_rev_ctx [in MetaCoq.Template.utils.All_Forall]
All2i_len_rev [in MetaCoq.Template.utils.All_Forall]
All2i_len_impl [in MetaCoq.Template.utils.All_Forall]
All2i_len_length [in MetaCoq.Template.utils.All_Forall]
All2i_len_app [in MetaCoq.Template.utils.All_Forall]
All2i_rev [in MetaCoq.Template.utils.All_Forall]
All2i_trivial [in MetaCoq.Template.utils.All_Forall]
All2i_mapi_rec [in MetaCoq.Template.utils.All_Forall]
All2i_app [in MetaCoq.Template.utils.All_Forall]
All2i_mapi [in MetaCoq.Template.utils.All_Forall]
All2i_impl [in MetaCoq.Template.utils.All_Forall]
All2i_All_right [in MetaCoq.Template.utils.All_Forall]
All2i_All_left [in MetaCoq.Template.utils.All_Forall]
All2i_All2_mix_left [in MetaCoq.Template.utils.All_Forall]
All2i_All_mix_right [in MetaCoq.Template.utils.All_Forall]
All2i_All_mix_left [in MetaCoq.Template.utils.All_Forall]
All2i_sym [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
All2i_All2_mapi [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
All2i_map2_right [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
All2i_All2 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
All2i_sym [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
All2i_All2_mapi [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
All2i_map_left_inv [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
All2i_map_right_inv [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
All2i_map [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
All2i_All2i_mix [in MetaCoq.PCUIC.PCUICSR]
All2i_nth_error [in MetaCoq.PCUIC.PCUICSR]
All2i_prod [in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
All2i_All2 [in MetaCoq.Template.TypingWf]
All2P [in MetaCoq.Template.utils.All_Forall]
All2_fold_cst_map [in MetaCoq.Template.BasicAst]
All2_fold_map [in MetaCoq.Template.BasicAst]
All2_fold_mapi [in MetaCoq.Template.BasicAst]
All2_fold_impl_onctx [in MetaCoq.Template.BasicAst]
All2_fold_nth_ass [in MetaCoq.PCUIC.PCUICRedTypeIrrelevance]
All2_map2_left_All3 [in MetaCoq.Template.utils.All_Forall]
All2_map2_left [in MetaCoq.Template.utils.All_Forall]
All2_fold_All_fold_mix_inv [in MetaCoq.Template.utils.All_Forall]
All2_fold_All_fold_mix [in MetaCoq.Template.utils.All_Forall]
All2_fold_prod_inv [in MetaCoq.Template.utils.All_Forall]
All2_fold_prod [in MetaCoq.Template.utils.All_Forall]
All2_fold_nth_r [in MetaCoq.Template.utils.All_Forall]
All2_fold_nth [in MetaCoq.Template.utils.All_Forall]
All2_fold_forallb2 [in MetaCoq.Template.utils.All_Forall]
All2_fold_impl_len [in MetaCoq.Template.utils.All_Forall]
All2_fold_impl_ind [in MetaCoq.Template.utils.All_Forall]
All2_fold_app_inv_l [in MetaCoq.Template.utils.All_Forall]
All2_fold_app_inv [in MetaCoq.Template.utils.All_Forall]
All2_fold_sym [in MetaCoq.Template.utils.All_Forall]
All2_fold_trans [in MetaCoq.Template.utils.All_Forall]
All2_fold_refl [in MetaCoq.Template.utils.All_Forall]
All2_fold_All2 [in MetaCoq.Template.utils.All_Forall]
All2_fold_All_left [in MetaCoq.Template.utils.All_Forall]
All2_fold_All_right [in MetaCoq.Template.utils.All_Forall]
All2_fold_All_fold_mix_left_inv [in MetaCoq.Template.utils.All_Forall]
All2_fold_All_fold_mix_right [in MetaCoq.Template.utils.All_Forall]
All2_fold_All_fold_mix_left [in MetaCoq.Template.utils.All_Forall]
All2_fold_impl [in MetaCoq.Template.utils.All_Forall]
All2_fold_length [in MetaCoq.Template.utils.All_Forall]
All2_fold_app [in MetaCoq.Template.utils.All_Forall]
All2_In_right [in MetaCoq.Template.utils.All_Forall]
All2_In [in MetaCoq.Template.utils.All_Forall]
All2_app_r [in MetaCoq.Template.utils.All_Forall]
All2_sq [in MetaCoq.Template.utils.All_Forall]
All2_eq [in MetaCoq.Template.utils.All_Forall]
All2_mix_inv [in MetaCoq.Template.utils.All_Forall]
All2_mix [in MetaCoq.Template.utils.All_Forall]
All2_nth_error_Some_right [in MetaCoq.Template.utils.All_Forall]
All2_symP [in MetaCoq.Template.utils.All_Forall]
All2_sym [in MetaCoq.Template.utils.All_Forall]
All2_prod_inv [in MetaCoq.Template.utils.All_Forall]
All2_prod [in MetaCoq.Template.utils.All_Forall]
All2_same [in MetaCoq.Template.utils.All_Forall]
All2_nth_error_Some_r [in MetaCoq.Template.utils.All_Forall]
All2_nth_error_Some [in MetaCoq.Template.utils.All_Forall]
All2_impl' [in MetaCoq.Template.utils.All_Forall]
All2_firstn [in MetaCoq.Template.utils.All_Forall]
All2_swap [in MetaCoq.Template.utils.All_Forall]
All2_nth_error [in MetaCoq.Template.utils.All_Forall]
All2_from_nth_error [in MetaCoq.Template.utils.All_Forall]
All2_right_triv [in MetaCoq.Template.utils.All_Forall]
All2_skipn [in MetaCoq.Template.utils.All_Forall]
All2_mapi [in MetaCoq.Template.utils.All_Forall]
All2_nth [in MetaCoq.Template.utils.All_Forall]
All2_trans' [in MetaCoq.Template.utils.All_Forall]
All2_trans [in MetaCoq.Template.utils.All_Forall]
All2_All [in MetaCoq.Template.utils.All_Forall]
All2_impl_In [in MetaCoq.Template.utils.All_Forall]
All2_rev [in MetaCoq.Template.utils.All_Forall]
All2_app [in MetaCoq.Template.utils.All_Forall]
All2_ind_rev [in MetaCoq.Template.utils.All_Forall]
All2_rect_rev [in MetaCoq.Template.utils.All_Forall]
All2_app_inv [in MetaCoq.Template.utils.All_Forall]
All2_app_inv_r [in MetaCoq.Template.utils.All_Forall]
All2_app_inv_l [in MetaCoq.Template.utils.All_Forall]
All2_All2_mix [in MetaCoq.Template.utils.All_Forall]
All2_nth_error_None [in MetaCoq.Template.utils.All_Forall]
All2_length [in MetaCoq.Template.utils.All_Forall]
All2_All_left_pack [in MetaCoq.Template.utils.All_Forall]
All2_non_nil [in MetaCoq.Template.utils.All_Forall]
All2_map_right [in MetaCoq.Template.utils.All_Forall]
All2_map_left [in MetaCoq.Template.utils.All_Forall]
All2_map_right_equiv [in MetaCoq.Template.utils.All_Forall]
All2_map_left_equiv [in MetaCoq.Template.utils.All_Forall]
All2_Forall2 [in MetaCoq.Template.utils.All_Forall]
All2_apply_dep_All [in MetaCoq.Template.utils.All_Forall]
All2_apply_dep_arrow [in MetaCoq.Template.utils.All_Forall]
All2_apply_arrow [in MetaCoq.Template.utils.All_Forall]
All2_apply [in MetaCoq.Template.utils.All_Forall]
All2_transitivity [in MetaCoq.Template.utils.All_Forall]
All2_symmetry [in MetaCoq.Template.utils.All_Forall]
All2_reflexivity [in MetaCoq.Template.utils.All_Forall]
All2_eq_eq [in MetaCoq.Template.utils.All_Forall]
All2_impl [in MetaCoq.Template.utils.All_Forall]
All2_right [in MetaCoq.Template.utils.All_Forall]
All2_All_right [in MetaCoq.Template.utils.All_Forall]
All2_All_left [in MetaCoq.Template.utils.All_Forall]
All2_All_mix_right [in MetaCoq.Template.utils.All_Forall]
All2_All_mix_left [in MetaCoq.Template.utils.All_Forall]
All2_map_inv [in MetaCoq.Template.utils.All_Forall]
All2_map [in MetaCoq.Template.utils.All_Forall]
All2_map_equiv [in MetaCoq.Template.utils.All_Forall]
All2_refl [in MetaCoq.Template.utils.All_Forall]
All2_forallb2 [in MetaCoq.Template.utils.All_Forall]
All2_map_option_out_mapi_Some_spec [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
All2_eq_binder_expand_lets_ctx [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
All2_eq_binder_lift_context [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
All2_refl_inv [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
All2_All_map2 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
All2_map2_right [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
All2_nth_hyp [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
All2_All2_All2_All3 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
All2_map2 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
All2_map_option_out_mapi_Some_spec [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
All2_many_OnOne2 [in MetaCoq.PCUIC.utils.PCUICOnOne]
All2_eq_binder_subst_context_inst [in MetaCoq.PCUIC.PCUICValidity]
All2_sym [in MetaCoq.PCUIC.PCUICInductiveInversion]
All2_fold_context_k [in MetaCoq.PCUIC.PCUICInductiveInversion]
All2_fold_inst [in MetaCoq.PCUIC.PCUICInductiveInversion]
All2_All2_prop2_eq [in MetaCoq.PCUIC.PCUICParallelReduction]
All2_All2_prop_eq [in MetaCoq.PCUIC.PCUICParallelReduction]
All2_branch_prop [in MetaCoq.PCUIC.PCUICParallelReduction]
All2_All2_prop [in MetaCoq.PCUIC.PCUICParallelReduction]
All2_eq_context_upto [in MetaCoq.PCUIC.PCUICEquality]
All2_fold_All_right [in MetaCoq.PCUIC.PCUICAlpha]
All2_fold_All_fold_mix_right [in MetaCoq.PCUIC.PCUICAlpha]
All2_map_option_out_mapi_Some_spec [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
All2_eq_binder_expand_lets_ctx [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
All2_eq_binder_lift_context [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
All2_cumul_over_refl [in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
All2_conv_over_refl [in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
All2_nil_rev [in MetaCoq.Template.WcbvEval]
All2_nil [in MetaCoq.Template.WcbvEval]
All2_All2_fold_fix_context [in MetaCoq.PCUIC.PCUICConfluence]
All2_fold_refl [in MetaCoq.PCUIC.PCUICConfluence]
All2_fold_over_same_app [in MetaCoq.PCUIC.PCUICConversion]
All2_fold_over_same [in MetaCoq.PCUIC.PCUICConversion]
All2_fold_fold_context_k [in MetaCoq.PCUIC.PCUICConversion]
All2_many_OnOne2_pres [in MetaCoq.PCUIC.PCUICConversion]
All2_eq_binder_subst_instance [in MetaCoq.PCUIC.PCUICCasesContexts]
All2_eq_binder_subst_context [in MetaCoq.PCUIC.PCUICCasesContexts]
All2_map_left' [in MetaCoq.PCUIC.PCUICCanonicity]
All2_fold_red_refl [in MetaCoq.PCUIC.PCUICContextConversion]
All2_fold_over_red_refl [in MetaCoq.PCUIC.PCUICContextConversion]
All2_tip [in MetaCoq.PCUIC.PCUICSR]
All2_fold_fold_context_right [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
All2_fold_context_assumptions [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
All2_telescope_mapi [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
All2_prop2_eq_split [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
All2_ind_OnOne2 [in MetaCoq.PCUIC.PCUICReduction]
All2_eq [in MetaCoq.PCUIC.PCUICReduction]
All2_ctx_inst [in MetaCoq.PCUIC.PCUICSpine]
All2_fold_mapi_right [in MetaCoq.PCUIC.PCUICSpine]
All3_impl [in MetaCoq.Template.utils.All_Forall]
All3_map_all [in MetaCoq.Template.utils.All_Forall]
All3_impl [in MetaCoq.PCUIC.PCUICNormal]
All3_many_OnOne2All [in MetaCoq.PCUIC.PCUICReduction]
All3_length [in MetaCoq.PCUIC.PCUICReduction]
alpha_eq_trans [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
alpha_eq_inst_case_context [in MetaCoq.PCUIC.PCUICSafeLemmata]
alpha_eq_context_ws_cumul_ctx_pb [in MetaCoq.PCUIC.PCUICSafeLemmata]
alpha_eq_context_closed [in MetaCoq.PCUIC.PCUICSafeLemmata]
alpha_eq_subst_context [in MetaCoq.Template.TermEquality]
alpha_eq_extended_subst [in MetaCoq.Template.TermEquality]
alpha_eq_context_assumptions [in MetaCoq.Template.TermEquality]
alpha_eq_on_free_vars [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
alpha_eq_on_free_vars_ctx [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
alpha_eq_trans [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
alpha_eq_context_gen [in MetaCoq.PCUIC.PCUICConvCumInversion]
alpha_eq_subst_context [in MetaCoq.PCUIC.PCUICCasesContexts]
alpha_eq_lift_context [in MetaCoq.PCUIC.PCUICCasesContexts]
alpha_eq_smash_context [in MetaCoq.PCUIC.PCUICCasesContexts]
alpha_eq_extended_subst [in MetaCoq.PCUIC.PCUICCasesContexts]
alpha_eq_context_assumptions [in MetaCoq.PCUIC.PCUICCasesContexts]
alpha_eq_subst_instance [in MetaCoq.PCUIC.PCUICCasesContexts]
alt_into_ws_cumul_pb_terms [in MetaCoq.PCUIC.PCUICConvCumInversion]
andb_is_true [in MetaCoq.Template.common.uGraph]
andb_andI [in MetaCoq.Template.utils.MCProd]
andb_and [in MetaCoq.Template.utils.MCProd]
anonymize_two [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
apD_const [in MetaCoq.Translations.MiniHoTT]
apD_const [in MetaCoq.Translations.MiniHoTT_paths]
application_atom_mkApps [in MetaCoq.PCUIC.utils.PCUICAstUtils]
apply_expanded [in MetaCoq.Template.EtaExpand]
apply_expanded [in MetaCoq.Erasure.ErasureFunction]
app_Forall [in MetaCoq.Template.utils.All_Forall]
app_cored_r [in MetaCoq.PCUIC.PCUICSafeLemmata]
app_tip_nil [in MetaCoq.Template.utils.MCList]
app_inj_length_l [in MetaCoq.Template.utils.MCList]
app_inj_length_r [in MetaCoq.Template.utils.MCList]
app_tip_assoc [in MetaCoq.Template.utils.MCList]
app_context_push [in MetaCoq.PCUIC.PCUICArities]
app_mkApps [in MetaCoq.PCUIC.PCUICConversion]
app_inj [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
ap_path_sigma_1p [in MetaCoq.Translations.MiniHoTT]
ap_pp_concat_Vp [in MetaCoq.Translations.MiniHoTT]
ap_pp_concat_pV [in MetaCoq.Translations.MiniHoTT]
ap_transport_pV [in MetaCoq.Translations.MiniHoTT]
ap_transportD2 [in MetaCoq.Translations.MiniHoTT]
ap_transportD [in MetaCoq.Translations.MiniHoTT]
ap_transport [in MetaCoq.Translations.MiniHoTT]
ap_path_sigma_1p [in MetaCoq.Translations.MiniHoTT_paths]
ap_pp_concat_Vp [in MetaCoq.Translations.MiniHoTT_paths]
ap_pp_concat_pV [in MetaCoq.Translations.MiniHoTT_paths]
ap_transport_pV [in MetaCoq.Translations.MiniHoTT_paths]
ap_transportD2 [in MetaCoq.Translations.MiniHoTT_paths]
ap_transportD [in MetaCoq.Translations.MiniHoTT_paths]
ap_transport [in MetaCoq.Translations.MiniHoTT_paths]
arity_type_inv [in MetaCoq.Erasure.EArities]
arity_spine_case_predicate [in MetaCoq.PCUIC.PCUICInductives]
arity_spine_to_extended_list_app [in MetaCoq.PCUIC.PCUICInductiveInversion]
arity_spine_to_extended_list [in MetaCoq.PCUIC.PCUICInductiveInversion]
arity_spine_eq [in MetaCoq.PCUIC.PCUICInductiveInversion]
arity_red_to_prod_or_sort [in MetaCoq.PCUIC.PCUICConversion]
arity_spine_it_mkProd_or_LetIn_smash [in MetaCoq.PCUIC.PCUICSpine]
arity_spine_eq [in MetaCoq.PCUIC.PCUICSpine]
arity_spine_it_mkProd_or_LetIn_Sort [in MetaCoq.PCUIC.PCUICSpine]
arity_spine_it_mkProd_or_LetIn [in MetaCoq.PCUIC.PCUICSpine]
arity_typing_spine [in MetaCoq.PCUIC.PCUICSpine]
assumption_context_skipn [in MetaCoq.PCUIC.PCUICSubstitution]
assumption_context_lift_context [in MetaCoq.PCUIC.PCUICInductiveInversion]
assumption_context_subst_context [in MetaCoq.PCUIC.PCUICInductiveInversion]
assumption_context_expand_lets_ctx [in MetaCoq.PCUIC.PCUICInductiveInversion]
assumption_context_subst_instance [in MetaCoq.PCUIC.PCUICInductiveInversion]
assumption_context_map [in MetaCoq.PCUIC.PCUICInductiveInversion]
assumption_context_app [in MetaCoq.PCUIC.PCUICSigmaCalculus]
assumption_context_arities_context [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
assumption_context_assumptions [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
assumption_context_arity_ass_context [in MetaCoq.SafeChecker.PCUICSafeReduce]
assumption_context_firstn [in MetaCoq.PCUIC.PCUICCanonicity]
assumption_context_assumptions [in MetaCoq.PCUIC.PCUICCanonicity]
assumption_context_app_inv [in MetaCoq.PCUIC.Syntax.PCUICClosed]
assumption_context_fold [in MetaCoq.PCUIC.PCUICContexts]
assumption_context_length [in MetaCoq.PCUIC.PCUICContexts]
assumption_context_compare_decls [in MetaCoq.Erasure.Prelim]
assumption_context_cstr_branch_context [in MetaCoq.Erasure.Prelim]
assumption_context_map2_binders [in MetaCoq.Erasure.Prelim]
assumption_context_rev [in MetaCoq.SafeChecker.PCUICTypeChecker]
assumption_context_subst_telescope [in MetaCoq.SafeChecker.PCUICTypeChecker]
Ast_inst_case_context_assumptions [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
Ast_inst_case_context_length [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
Ast_cstr_branch_context_assumptions [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
atom_decompose_app [in MetaCoq.PCUIC.utils.PCUICAstUtils]
atom_nApp [in MetaCoq.PCUIC.PCUICWcbvEval]
atom_mkApps [in MetaCoq.PCUIC.PCUICWcbvEval]
atom_nApp [in MetaCoq.Template.WcbvEval]
atom_mkApps [in MetaCoq.Template.WcbvEval]
atom_mkApps [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
atom_nApp [in MetaCoq.Erasure.EWcbvEval]
atom_mkApps [in MetaCoq.Erasure.EWcbvEval]
atom_decompose_app [in MetaCoq.Template.AstUtils]
atpos_assoc [in MetaCoq.PCUIC.Syntax.PCUICPosition]
axiom_free_axiom_free_value [in MetaCoq.SafeChecker.PCUICConsistency]
axiom_free_value_mkApps [in MetaCoq.PCUIC.PCUICCanonicity]



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)