| 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) |
F (lemma)
fake_params_length [in MetaRocq.PCUIC.PCUICNormal]Fast.strip_env_fast [in MetaRocq.Erasure.ERemoveParams]
Fast.strip_fast [in MetaRocq.Erasure.ERemoveParams]
Fast.strip_acc_opt [in MetaRocq.Erasure.ERemoveParams]
fill_context_hole_inj [in MetaRocq.PCUIC.Syntax.PCUICPosition]
fill_eq [in MetaRocq.PCUIC.PCUICContextConversion]
fill_le [in MetaRocq.PCUIC.PCUICContextConversion]
fill_pb [in MetaRocq.PCUIC.PCUICContextConversion]
fill_mkApps_context [in MetaRocq.PCUIC.PCUICReduction]
filter_length [in MetaRocq.Utils.MRList]
filter_deps_filter [in MetaRocq.Erasure.ErasureFunctionProperties]
filter_deps_ext [in MetaRocq.Erasure.Typed.ExtractionCorrectness]
find_index_inj [in MetaRocq.Utils.MRListable]
find_index_iff [in MetaRocq.Utils.MRListable]
find_tag_wf [in MetaRocq.Erasure.EReorderCstrs]
find_tag_None [in MetaRocq.Erasure.EReorderCstrs]
firstn_length_le_inv [in MetaRocq.Utils.MRList]
firstn_app_left [in MetaRocq.Utils.MRList]
firstn_app_left_rem [in MetaRocq.Utils.MRList]
firstn_add [in MetaRocq.Utils.MRList]
firstn_firstn_firstn [in MetaRocq.Utils.MRList]
firstn_0 [in MetaRocq.Utils.MRList]
firstn_ge [in MetaRocq.Utils.MRList]
firstn_map [in MetaRocq.Utils.MRList]
firstn_all_app_eq [in MetaRocq.SafeChecker.PCUICSafeChecker]
firstn_subst_context [in MetaRocq.PCUIC.PCUICClassification]
firstorder_value_irred [in MetaRocq.PCUIC.PCUICNormalization]
firstorder_value_alpha [in MetaRocq.PCUIC.PCUICFirstorder]
firstorder_value_spec [in MetaRocq.PCUIC.PCUICFirstorder]
firstorder_args [in MetaRocq.PCUIC.PCUICFirstorder]
firstorder_mutind_ext [in MetaRocq.PCUIC.PCUICFirstorder]
firstorder_spine_let [in MetaRocq.PCUIC.PCUICFirstorder]
firstorder_ind_propositional [in MetaRocq.PCUIC.PCUICFirstorder]
firstorder_value_inds [in MetaRocq.PCUIC.PCUICFirstorder]
firstorder_lookup_inv [in MetaRocq.PCUIC.PCUICFirstorder]
firstorder_evalue_extends [in MetaRocq.Erasure.ErasureFunctionProperties]
firstorder_erases_deterministic [in MetaRocq.Erasure.ErasureFunctionProperties]
firstorder_evalue_block_transform [in MetaRocq.ErasurePlugin.ErasureCorrectness]
firstorder_evalue_block_elim [in MetaRocq.ErasurePlugin.ErasureCorrectness]
fix_context_fix_context_alt [in MetaRocq.PCUIC.Syntax.PCUICPosition]
fix_subst_nth [in MetaRocq.Erasure.Prelim]
fix_context_pres_let_bodies [in MetaRocq.PCUIC.PCUICRedTypeIrrelevance]
Fix_F_prop [in MetaRocq.SafeChecker.PCUICSafeReduce]
fix_context_subst_instance [in MetaRocq.Erasure.ErasureProperties]
fix_context_nth_error [in MetaRocq.PCUIC.PCUICAlpha]
fix_context_length [in MetaRocq.Template.Typing]
fix_subst_length [in MetaRocq.Template.Typing]
fix_context_map_fix [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
fix_context_fold [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
fix_context_assumption_context [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
fix_context_gen_assumption_context [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
fix_env_length [in MetaRocq.Erasure.EWcbvEvalNamed]
fix_app_is_constructor [in MetaRocq.PCUIC.PCUICClassification]
fix_context_subst_instance [in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
fix_subst_instance_subst [in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
fix_subst_dearg [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
fix_context_length [in MetaRocq.PCUIC.Syntax.PCUICCases]
fix_subst_length [in MetaRocq.PCUIC.Syntax.PCUICCases]
fix_subst_length [in MetaRocq.Erasure.EGlobalEnv]
flip_PreOrder [in MetaRocq.PCUIC.PCUICConfluence]
flip_Transitive [in MetaRocq.Utils.MRRelations]
flip_Symmetric [in MetaRocq.Utils.MRRelations]
flip_Reflexive [in MetaRocq.Utils.MRRelations]
fold_left_andb_forallb [in MetaRocq.Utils.MRList]
fold_left_eq [in MetaRocq.Erasure.ErasureFunction]
fold_context_k_defs_length [in MetaRocq.Template.EtaExpand]
fold_right_ext [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
fold_right_map [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
fold_context_k_map_comm [in MetaRocq.Common.BasicAst]
fold_context_k_map [in MetaRocq.Common.BasicAst]
fold_context_k_ext [in MetaRocq.Common.BasicAst]
fold_context_k_compose [in MetaRocq.Common.BasicAst]
fold_context_k_id [in MetaRocq.Common.BasicAst]
fold_context_In_spec [in MetaRocq.Common.BasicAst]
fold_context_length [in MetaRocq.Common.BasicAst]
fold_context_k_app [in MetaRocq.Common.BasicAst]
fold_context_k_snoc0 [in MetaRocq.Common.BasicAst]
fold_context_k_length [in MetaRocq.Common.BasicAst]
fold_context_k_tip [in MetaRocq.Common.BasicAst]
fold_context_k_alt [in MetaRocq.Common.BasicAst]
fold_max_le' [in MetaRocq.Utils.wGraph]
fold_max_le [in MetaRocq.Utils.wGraph]
fold_max_In [in MetaRocq.Utils.wGraph]
fold_context_cst [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
fold_fix_context_rho_ctx [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
fold_fix_context_over_acc [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
fold_context_mapi_context [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
fold_fix_context_app [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
fold_fix_context_rev [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
fold_fix_context_rev_mapi [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
fold_fix_context_wf_fold [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
fold_fix_context_length [in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
fold_left_add_gc_Some_subset [in MetaRocq.Common.uGraph]
fold_left_add_gc_None [in MetaRocq.Common.uGraph]
fold_left_comm_ext3 [in MetaRocq.Common.uGraph]
fold_left_comm_ext2 [in MetaRocq.Common.uGraph]
fold_left_comm_ext [in MetaRocq.Common.uGraph]
fold_left_max_spec' [in MetaRocq.Common.uGraph]
fold_left_max_spec [in MetaRocq.Common.uGraph]
fold_left_false [in MetaRocq.Common.uGraph]
fold_right_xpred0 [in MetaRocq.Common.uGraph]
forallbi_impl [in MetaRocq.ErasurePlugin.ErasureCorrectness]
forallbi_Alli [in MetaRocq.ErasurePlugin.ErasureCorrectness]
forallbi_Alli [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
forallbi_nth_error [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
forallbP [in MetaRocq.Utils.All_Forall]
forallbP_cond [in MetaRocq.Utils.All_Forall]
forallb_repeat [in MetaRocq.Utils.MRList]
forallb_InP_spec [in MetaRocq.Utils.MRList]
forallb_mapi [in MetaRocq.Utils.MRList]
forallb_unfold [in MetaRocq.Utils.MRList]
forallb_rev [in MetaRocq.Utils.MRList]
forallb_true [in MetaRocq.SafeChecker.PCUICEqualityDec]
forallb_mapi_ext [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
forallb_closed_upwards [in MetaRocq.PCUIC.PCUICInductiveInversion]
forallb_forallbi [in MetaRocq.ErasurePlugin.ErasureCorrectness]
forallb_mapi_forallbi [in MetaRocq.ErasurePlugin.ErasureCorrectness]
forallb_last [in MetaRocq.Erasure.EEtaExpandedFix]
forallb_remove_last [in MetaRocq.Erasure.EEtaExpandedFix]
forallb_firstn [in MetaRocq.Erasure.EEtaExpandedFix]
forallb_iff [in MetaRocq.Utils.All_Forall]
forallb_impl [in MetaRocq.Utils.All_Forall]
forallb_nth' [in MetaRocq.Utils.All_Forall]
forallb_nth [in MetaRocq.Utils.All_Forall]
forallb_skipn [in MetaRocq.Utils.All_Forall]
forallb_Forall' [in MetaRocq.Utils.All_Forall]
forallb_mapi_impl [in MetaRocq.Utils.All_Forall]
forallb_mapi [in MetaRocq.Utils.All_Forall]
forallb_map [in MetaRocq.Utils.All_Forall]
forallb_All [in MetaRocq.Utils.All_Forall]
forallb_nth_error [in MetaRocq.Utils.All_Forall]
forallb_ext [in MetaRocq.Utils.All_Forall]
forallb_Forall [in MetaRocq.Utils.All_Forall]
forallb_in [in MetaRocq.Common.uGraph]
forallb_spec [in MetaRocq.Common.uGraph]
forallb_map_spec [in MetaRocq.PCUIC.Conversion.PCUICInstConv]
forallb2P [in MetaRocq.Utils.All_Forall]
forallb2_Forall2 [in MetaRocq.Utils.All_Forall]
forallb2_length [in MetaRocq.Utils.All_Forall]
forallb2_app [in MetaRocq.Utils.All_Forall]
forallb2_All2 [in MetaRocq.Utils.All_Forall]
forallb2_map [in MetaRocq.Utils.All_Forall]
forallb2_refl [in MetaRocq.Utils.All_Forall]
forallb3P [in MetaRocq.Utils.All_Forall]
forallb3_Forall3 [in MetaRocq.Utils.All_Forall]
forallb3_All3 [in MetaRocq.Utils.All_Forall]
Forall_Forall2_diag [in MetaRocq.SafeChecker.PCUICEqualityDec]
Forall_mapi [in MetaRocq.Erasure.Typed.TypeAnnotations]
Forall_filter [in MetaRocq.Erasure.ErasureFunctionProperties]
Forall_typing_spine_Forall [in MetaRocq.Template.EtaExpand]
Forall_erases_deps_cofix_subst [in MetaRocq.Erasure.EDeps]
Forall_erases_deps_fix_subst [in MetaRocq.Erasure.EDeps]
forall_nth_error_All2i [in MetaRocq.PCUIC.PCUICInductiveInversion]
Forall_existsb_false [in MetaRocq.Erasure.Typed.Utils]
Forall_repeat [in MetaRocq.Erasure.Typed.Utils]
Forall_snoc [in MetaRocq.Erasure.Typed.Utils]
Forall_Forall2_and' [in MetaRocq.Utils.All_Forall]
Forall_Forall2_and [in MetaRocq.Utils.All_Forall]
Forall_True [in MetaRocq.Utils.All_Forall]
Forall_Forall2 [in MetaRocq.Utils.All_Forall]
Forall_forallb [in MetaRocq.Utils.All_Forall]
Forall_forallb_eq_forallb [in MetaRocq.Utils.All_Forall]
Forall_last [in MetaRocq.Utils.All_Forall]
Forall_app [in MetaRocq.Utils.All_Forall]
Forall_impl [in MetaRocq.Utils.All_Forall]
Forall_impl_Forall [in MetaRocq.Utils.All_Forall]
Forall_map_inv [in MetaRocq.Utils.All_Forall]
Forall_map [in MetaRocq.Utils.All_Forall]
forall_forallb_forallb_spec [in MetaRocq.Utils.All_Forall]
forall_forallb_map_spec [in MetaRocq.Utils.All_Forall]
forall_nth_error_Alli [in MetaRocq.Utils.All_Forall]
forall_nth_error_All [in MetaRocq.Utils.All_Forall]
Forall_All [in MetaRocq.Utils.All_Forall]
Forall_firstn [in MetaRocq.Utils.All_Forall]
Forall_skipn [in MetaRocq.Utils.All_Forall]
Forall_mix [in MetaRocq.Utils.All_Forall]
forall_map_id_spec [in MetaRocq.Utils.All_Forall]
forall_map_spec [in MetaRocq.Utils.All_Forall]
Forall_elements_in [in MetaRocq.PCUIC.PCUICCumulProp]
Forall_decls_on_global_wf [in MetaRocq.Template.TypingWf]
Forall_closed_repeat_tBox [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
Forall_masked [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
Forall_valid_cases_cofix_subst [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
Forall_valid_cases_fix_subst [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
Forall_closed_cofix_subst [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
Forall_closed_fix_subst [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
Forall_is_expanded_cofix_subst [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
Forall_is_expanded_fix_subst [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
Forall_In [in MetaRocq.PCUIC.PCUICWfUniverses]
Forall_nth_def [in MetaRocq.SafeChecker.PCUICTypeChecker]
forall_decls_declared_projection [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
forall_decls_declared_constructor [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
forall_decls_declared_inductive [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
forall_decls_declared_minductive [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
forall_decls_declared_constant [in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
Forall2_forallb2 [in MetaRocq.SafeChecker.PCUICEqualityDec]
Forall2_nth_error_left [in MetaRocq.Erasure.EDeps]
Forall2_Forall2_Forall3 [in MetaRocq.Utils.All_Forall]
Forall2_sym [in MetaRocq.Utils.All_Forall]
Forall2_same [in MetaRocq.Utils.All_Forall]
Forall2_map' [in MetaRocq.Utils.All_Forall]
Forall2_eq [in MetaRocq.Utils.All_Forall]
Forall2_symP [in MetaRocq.Utils.All_Forall]
Forall2_dep_nth_error [in MetaRocq.Utils.All_Forall]
Forall2_dep_from_nth_error [in MetaRocq.Utils.All_Forall]
Forall2_nth_error [in MetaRocq.Utils.All_Forall]
Forall2_from_nth_error [in MetaRocq.Utils.All_Forall]
Forall2_Forall_right [in MetaRocq.Utils.All_Forall]
Forall2_mapi [in MetaRocq.Utils.All_Forall]
Forall2_rev [in MetaRocq.Utils.All_Forall]
Forall2_trans [in MetaRocq.Utils.All_Forall]
Forall2_nth_error_None_l [in MetaRocq.Utils.All_Forall]
Forall2_nth_error_Some_r [in MetaRocq.Utils.All_Forall]
Forall2_nth_error_Some_l [in MetaRocq.Utils.All_Forall]
Forall2_nth [in MetaRocq.Utils.All_Forall]
Forall2_and [in MetaRocq.Utils.All_Forall]
Forall2_map_right [in MetaRocq.Utils.All_Forall]
Forall2_map [in MetaRocq.Utils.All_Forall]
Forall2_True [in MetaRocq.Utils.All_Forall]
Forall2_Forall [in MetaRocq.Utils.All_Forall]
Forall2_impl' [in MetaRocq.Utils.All_Forall]
Forall2_impl [in MetaRocq.Utils.All_Forall]
Forall2_nth_error_Some [in MetaRocq.Utils.All_Forall]
Forall2_skipn [in MetaRocq.Utils.All_Forall]
Forall2_tip_l [in MetaRocq.Utils.All_Forall]
Forall2_map_inv [in MetaRocq.Utils.All_Forall]
Forall2_app_r [in MetaRocq.Utils.All_Forall]
Forall2_triv [in MetaRocq.Utils.All_Forall]
Forall2_length [in MetaRocq.Utils.All_Forall]
Forall2_non_nil [in MetaRocq.Utils.All_Forall]
Forall2_right [in MetaRocq.Utils.All_Forall]
Forall2_undep [in MetaRocq.Utils.All_Forall]
Forall2_All2 [in MetaRocq.Utils.All_Forall]
Forall3_map [in MetaRocq.Utils.All_Forall]
Forall3_map_inv [in MetaRocq.Utils.All_Forall]
Forall3_antisymP [in MetaRocq.Utils.All_Forall]
Forall3_transP [in MetaRocq.Utils.All_Forall]
Forall3_symP [in MetaRocq.Utils.All_Forall]
Forall3_Forall2_right [in MetaRocq.Utils.All_Forall]
Forall3_Forall2_edges [in MetaRocq.Utils.All_Forall]
Forall3_Forall2_left [in MetaRocq.Utils.All_Forall]
Forall3_impl [in MetaRocq.Utils.All_Forall]
Forall3_All3 [in MetaRocq.Utils.All_Forall]
forget_inlining_info_transformation_ext' [in MetaRocq.Erasure.EInlining]
forget_inlining_info_transformation_ext [in MetaRocq.Erasure.EInlining]
forget_types_map_context [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
forget_types_map_context [in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
forget_types_mapi_context [in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
forget_types_fold_context_k [in MetaRocq.Common.BasicAst]
forget_types_length [in MetaRocq.Common.BasicAst]
forget_types_subst_instance [in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
forget_types_map_context [in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
forget_types_inst_case_context [in MetaRocq.PCUIC.PCUICCasesHelper]
foron_free_vars_extended_subst [in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
foroptb_impl [in MetaRocq.Utils.MROption]
for_all_elements [in MetaRocq.Common.Universes]
fo_v [in MetaRocq.ErasurePlugin.ErasureCorrectness]
fresh_globals_cons_inv [in MetaRocq.Template.TemplateEnvMap]
fresh_global_map_on_snd [in MetaRocq.Erasure.EImplementBox]
fresh_globals_erase_global_decl_rec [in MetaRocq.Erasure.Typed.Extraction]
fresh_global_erase_global_decl_rec [in MetaRocq.Erasure.Typed.Extraction]
fresh_global_In [in MetaRocq.Erasure.ErasureFunction]
fresh_global_app [in MetaRocq.PCUIC.PCUICFirstorder]
fresh_global_app [in MetaRocq.Erasure.ErasureFunctionProperties]
fresh_global_map [in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
fresh_global_gen_transform_env [in MetaRocq.Erasure.EGenericGlobalMap]
fresh_global_subset [in MetaRocq.Erasure.EExtends]
fresh_global_filter_deps [in MetaRocq.Erasure.Typed.ExtractionCorrectness]
fresh_global_remove_match_on_box_env [in MetaRocq.Erasure.EOptimizePropDiscr]
fresh_global_gen_transform_env [in MetaRocq.Erasure.EGenericMapEnv]
fresh_global_trans [in MetaRocq.ErasurePlugin.ETransform]
fresh_subset [in MetaRocq.Erasure.EWcbvEvalNamed]
fresh_globals_cons_inv [in MetaRocq.Erasure.EEnvMap]
fresh_global_strip_env [in MetaRocq.Erasure.ERemoveParams]
fresh_global_trans_env [in MetaRocq.Erasure.ECoInductiveToInductive]
FSets.WFactsExtra_fun.Equiv_alt_iff [in MetaRocq.Utils.MRFSets]
fst_decompose_app_rec [in MetaRocq.Erasure.Prelim]
fst_decompose_app_rec [in MetaRocq.Erasure.EImplementBox]
fst_decompose_stack_nil [in MetaRocq.PCUIC.PCUICSafeLemmata]
fst_decompose_app_rec [in MetaRocq.PCUIC.utils.PCUICAstUtils]
fst_erase_pcuic_program' [in MetaRocq.ErasurePlugin.ErasureCorrectness]
fst_erase_pcuic_program [in MetaRocq.ErasurePlugin.ErasureCorrectness]
fst_decompose_app_rec [in MetaRocq.Erasure.EConstructorsAsBlocks]
fst_pair [in MetaRocq.Utils.MRProd]
| 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) |