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)

F (lemma)

fake_params_length [in MetaCoq.PCUIC.PCUICNormal]
Fast.strip_env_fast [in MetaCoq.Erasure.ERemoveParams]
Fast.strip_fast [in MetaCoq.Erasure.ERemoveParams]
Fast.strip_acc_opt [in MetaCoq.Erasure.ERemoveParams]
fill_context_hole_inj [in MetaCoq.PCUIC.Syntax.PCUICPosition]
fill_eq [in MetaCoq.PCUIC.PCUICContextConversion]
fill_le [in MetaCoq.PCUIC.PCUICContextConversion]
fill_mkApps_context [in MetaCoq.PCUIC.PCUICReduction]
firstn_length_le_inv [in MetaCoq.Template.utils.MCList]
firstn_app_left [in MetaCoq.Template.utils.MCList]
firstn_app_left_rem [in MetaCoq.Template.utils.MCList]
firstn_add [in MetaCoq.Template.utils.MCList]
firstn_firstn_firstn [in MetaCoq.Template.utils.MCList]
firstn_0 [in MetaCoq.Template.utils.MCList]
firstn_ge [in MetaCoq.Template.utils.MCList]
firstn_map [in MetaCoq.Template.utils.MCList]
firstn_subst_context [in MetaCoq.PCUIC.PCUICCanonicity]
firstn_all_app_eq [in MetaCoq.SafeChecker.PCUICSafeChecker]
firstorder_value_irred [in MetaCoq.PCUIC.PCUICProgress]
firstorder_value_spec [in MetaCoq.PCUIC.PCUICFirstorder]
firstorder_args [in MetaCoq.PCUIC.PCUICFirstorder]
firstorder_mutind_ext [in MetaCoq.PCUIC.PCUICFirstorder]
firstorder_spine_let [in MetaCoq.PCUIC.PCUICFirstorder]
firstorder_ind_propositional [in MetaCoq.PCUIC.PCUICFirstorder]
firstorder_value_inds [in MetaCoq.PCUIC.PCUICFirstorder]
firstorder_erases_deterministic [in MetaCoq.Erasure.ErasureFunction]
fix_context_pres_let_bodies [in MetaCoq.PCUIC.PCUICRedTypeIrrelevance]
fix_context_length [in MetaCoq.Template.Typing]
fix_subst_length [in MetaCoq.Template.Typing]
fix_context_fix_context_alt [in MetaCoq.PCUIC.Syntax.PCUICPosition]
fix_context_nth_error [in MetaCoq.PCUIC.PCUICAlpha]
fix_context_length [in MetaCoq.PCUIC.Syntax.PCUICCases]
fix_subst_length [in MetaCoq.PCUIC.Syntax.PCUICCases]
fix_context_subst_instance [in MetaCoq.Erasure.ErasureProperties]
Fix_F_prop [in MetaCoq.SafeChecker.PCUICSafeReduce]
fix_subst_length [in MetaCoq.Erasure.EGlobalEnv]
fix_app_is_constructor [in MetaCoq.PCUIC.PCUICCanonicity]
fix_context_subst_instance [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
fix_subst_instance_subst [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
fix_context_map_fix [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
fix_context_fold [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
fix_context_assumption_context [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
fix_context_gen_assumption_context [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
fix_subst_nth [in MetaCoq.Erasure.Prelim]
flip_Transitive [in MetaCoq.Template.utils.MCRelations]
flip_Symmetric [in MetaCoq.Template.utils.MCRelations]
flip_Reflexive [in MetaCoq.Template.utils.MCRelations]
fold_context_k_defs_length [in MetaCoq.Template.EtaExpand]
fold_context_k_map_comm [in MetaCoq.Template.BasicAst]
fold_context_k_map [in MetaCoq.Template.BasicAst]
fold_context_k_ext [in MetaCoq.Template.BasicAst]
fold_context_k_compose [in MetaCoq.Template.BasicAst]
fold_context_k_id [in MetaCoq.Template.BasicAst]
fold_context_In_spec [in MetaCoq.Template.BasicAst]
fold_context_length [in MetaCoq.Template.BasicAst]
fold_context_k_app [in MetaCoq.Template.BasicAst]
fold_context_k_snoc0 [in MetaCoq.Template.BasicAst]
fold_context_k_length [in MetaCoq.Template.BasicAst]
fold_context_k_tip [in MetaCoq.Template.BasicAst]
fold_context_k_alt [in MetaCoq.Template.BasicAst]
fold_left_andb_forallb [in MetaCoq.Template.utils.MCList]
fold_left_add_gc_Some_subset [in MetaCoq.Template.common.uGraph]
fold_left_add_gc_None [in MetaCoq.Template.common.uGraph]
fold_left_comm_ext3 [in MetaCoq.Template.common.uGraph]
fold_left_comm_ext2 [in MetaCoq.Template.common.uGraph]
fold_left_comm_ext [in MetaCoq.Template.common.uGraph]
fold_left_max_spec' [in MetaCoq.Template.common.uGraph]
fold_left_max_spec [in MetaCoq.Template.common.uGraph]
fold_left_false [in MetaCoq.Template.common.uGraph]
fold_right_xpred0 [in MetaCoq.Template.common.uGraph]
fold_right_ext [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
fold_right_map [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
fold_max_le' [in MetaCoq.Template.utils.wGraph]
fold_max_le [in MetaCoq.Template.utils.wGraph]
fold_max_In [in MetaCoq.Template.utils.wGraph]
fold_context_cst [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
fold_fix_context_rho_ctx [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
fold_fix_context_over_acc [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
fold_context_mapi_context [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
fold_fix_context_app [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
fold_fix_context_rev [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
fold_fix_context_rev_mapi [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
fold_fix_context_wf_fold [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
fold_fix_context_length [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
forallbP [in MetaCoq.Template.utils.All_Forall]
forallbP_cond [in MetaCoq.Template.utils.All_Forall]
forallb_last [in MetaCoq.Erasure.EEtaExpandedFix]
forallb_remove_last [in MetaCoq.Erasure.EEtaExpandedFix]
forallb_firstn [in MetaCoq.Erasure.EEtaExpandedFix]
forallb_iff [in MetaCoq.Template.utils.All_Forall]
forallb_impl [in MetaCoq.Template.utils.All_Forall]
forallb_nth' [in MetaCoq.Template.utils.All_Forall]
forallb_nth [in MetaCoq.Template.utils.All_Forall]
forallb_skipn [in MetaCoq.Template.utils.All_Forall]
forallb_Forall' [in MetaCoq.Template.utils.All_Forall]
forallb_map [in MetaCoq.Template.utils.All_Forall]
forallb_All [in MetaCoq.Template.utils.All_Forall]
forallb_nth_error [in MetaCoq.Template.utils.All_Forall]
forallb_ext [in MetaCoq.Template.utils.All_Forall]
forallb_Forall [in MetaCoq.Template.utils.All_Forall]
forallb_repeat [in MetaCoq.Template.utils.MCList]
forallb_InP_spec [in MetaCoq.Template.utils.MCList]
forallb_mapi [in MetaCoq.Template.utils.MCList]
forallb_unfold [in MetaCoq.Template.utils.MCList]
forallb_rev [in MetaCoq.Template.utils.MCList]
forallb_closed_upwards [in MetaCoq.PCUIC.PCUICInductiveInversion]
forallb_in [in MetaCoq.Template.common.uGraph]
forallb_spec [in MetaCoq.Template.common.uGraph]
forallb_mapi_ext [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
forallb_map_spec [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
forallb_true [in MetaCoq.SafeChecker.PCUICEqualityDec]
forallb2P [in MetaCoq.Template.utils.All_Forall]
forallb2_Forall2 [in MetaCoq.Template.utils.All_Forall]
forallb2_length [in MetaCoq.Template.utils.All_Forall]
forallb2_app [in MetaCoq.Template.utils.All_Forall]
forallb2_All2 [in MetaCoq.Template.utils.All_Forall]
forallb2_map [in MetaCoq.Template.utils.All_Forall]
forallb2_refl [in MetaCoq.Template.utils.All_Forall]
forallb2_bcompare_decl_All2_fold [in MetaCoq.SafeChecker.PCUICEqualityDec]
Forall_typing_spine_Forall [in MetaCoq.Template.EtaExpand]
Forall_Forall2_and' [in MetaCoq.Template.utils.All_Forall]
Forall_Forall2_and [in MetaCoq.Template.utils.All_Forall]
Forall_True [in MetaCoq.Template.utils.All_Forall]
Forall_Forall2 [in MetaCoq.Template.utils.All_Forall]
Forall_forallb [in MetaCoq.Template.utils.All_Forall]
Forall_forallb_eq_forallb [in MetaCoq.Template.utils.All_Forall]
Forall_last [in MetaCoq.Template.utils.All_Forall]
Forall_app [in MetaCoq.Template.utils.All_Forall]
Forall_impl [in MetaCoq.Template.utils.All_Forall]
Forall_map_inv [in MetaCoq.Template.utils.All_Forall]
Forall_map [in MetaCoq.Template.utils.All_Forall]
forall_forallb_forallb_spec [in MetaCoq.Template.utils.All_Forall]
forall_forallb_map_spec [in MetaCoq.Template.utils.All_Forall]
forall_nth_error_Alli [in MetaCoq.Template.utils.All_Forall]
forall_nth_error_All [in MetaCoq.Template.utils.All_Forall]
Forall_All [in MetaCoq.Template.utils.All_Forall]
Forall_firstn [in MetaCoq.Template.utils.All_Forall]
Forall_skipn [in MetaCoq.Template.utils.All_Forall]
Forall_mix [in MetaCoq.Template.utils.All_Forall]
forall_map_id_spec [in MetaCoq.Template.utils.All_Forall]
forall_map_spec [in MetaCoq.Template.utils.All_Forall]
Forall_In [in MetaCoq.PCUIC.PCUICWfUniverses]
forall_decls_declared_projection [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
forall_decls_declared_constructor [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
forall_decls_declared_inductive [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
forall_decls_declared_minductive [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
forall_decls_declared_constant [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
Forall_erases_deps_cofix_subst [in MetaCoq.Erasure.EDeps]
Forall_erases_deps_fix_subst [in MetaCoq.Erasure.EDeps]
forall_nth_error_All2i [in MetaCoq.PCUIC.PCUICInductiveInversion]
Forall_elements_in [in MetaCoq.PCUIC.PCUICCumulProp]
Forall_decls_on_global_wf [in MetaCoq.Template.TypingWf]
Forall_Forall2_diag [in MetaCoq.SafeChecker.PCUICEqualityDec]
Forall_nth_def [in MetaCoq.SafeChecker.PCUICTypeChecker]
Forall2_sym [in MetaCoq.Template.utils.All_Forall]
Forall2_same [in MetaCoq.Template.utils.All_Forall]
Forall2_map' [in MetaCoq.Template.utils.All_Forall]
Forall2_eq [in MetaCoq.Template.utils.All_Forall]
Forall2_Forall_right [in MetaCoq.Template.utils.All_Forall]
Forall2_mapi [in MetaCoq.Template.utils.All_Forall]
Forall2_rev [in MetaCoq.Template.utils.All_Forall]
Forall2_trans [in MetaCoq.Template.utils.All_Forall]
Forall2_nth_error_None_l [in MetaCoq.Template.utils.All_Forall]
Forall2_nth_error_Some_r [in MetaCoq.Template.utils.All_Forall]
Forall2_nth_error_Some_l [in MetaCoq.Template.utils.All_Forall]
Forall2_nth [in MetaCoq.Template.utils.All_Forall]
Forall2_and [in MetaCoq.Template.utils.All_Forall]
Forall2_map_right [in MetaCoq.Template.utils.All_Forall]
Forall2_map [in MetaCoq.Template.utils.All_Forall]
Forall2_True [in MetaCoq.Template.utils.All_Forall]
Forall2_Forall [in MetaCoq.Template.utils.All_Forall]
Forall2_impl' [in MetaCoq.Template.utils.All_Forall]
Forall2_impl [in MetaCoq.Template.utils.All_Forall]
Forall2_nth_error_Some [in MetaCoq.Template.utils.All_Forall]
Forall2_skipn [in MetaCoq.Template.utils.All_Forall]
Forall2_map_inv [in MetaCoq.Template.utils.All_Forall]
Forall2_app_r [in MetaCoq.Template.utils.All_Forall]
Forall2_length [in MetaCoq.Template.utils.All_Forall]
Forall2_non_nil [in MetaCoq.Template.utils.All_Forall]
Forall2_right [in MetaCoq.Template.utils.All_Forall]
Forall2_All2 [in MetaCoq.Template.utils.All_Forall]
Forall2_nth_error_left [in MetaCoq.Erasure.EDeps]
Forall2_flip [in MetaCoq.PCUIC.PCUICConfluence]
Forall2_forallb2 [in MetaCoq.SafeChecker.PCUICEqualityDec]
forget_types_fold_context_k [in MetaCoq.Template.BasicAst]
forget_types_length [in MetaCoq.Template.BasicAst]
forget_types_map_context [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
forget_types_map_context [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
forget_types_subst_instance [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
forget_types_map_context [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
forget_types_mapi_context [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
foron_free_vars_extended_subst [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
foroptb_impl [in MetaCoq.Template.utils.MCOption]
for_all_elements [in MetaCoq.Template.Universes]
FreeTheorems.param_map [in MetaCoq.Translations.param_binary]
FreeTheorems.rel_map_map [in MetaCoq.Translations.param_binary]
fresh_global_optimize_env [in MetaCoq.Erasure.EInlineProjections]
fresh_global_app [in MetaCoq.PCUIC.PCUICFirstorder]
fresh_global_map [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
fresh_globals_cons_inv [in MetaCoq.Erasure.EEnvMap]
fresh_global_subset [in MetaCoq.Erasure.EExtends]
fresh_global_strip_env [in MetaCoq.Erasure.ERemoveParams]
fresh_global_gen_transform_env [in MetaCoq.Erasure.EGenericMapEnv]
fresh_global_optimize_env [in MetaCoq.Erasure.EOptimizePropDiscr]
fst_decompose_app_rec [in MetaCoq.PCUIC.utils.PCUICAstUtils]
fst_decompose_stack_nil [in MetaCoq.PCUIC.PCUICSafeLemmata]
fst_decompose_app_rec [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)