| 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) |
L (lemma)
Lambda_conv_cum_inv [in MetaCoq.PCUIC.PCUICConversion]last_nonempty_eq [in MetaCoq.Template.utils.MCList]
last_app [in MetaCoq.Template.utils.MCList]
last_inv [in MetaCoq.Template.utils.MCList]
leb_spec_Set [in MetaCoq.Template.utils.MCArith]
leb_S [in MetaCoq.PCUIC.PCUICParallelReduction]
leb_spect [in MetaCoq.PCUIC.PCUICFirstorder]
length_nil [in MetaCoq.PCUIC.PCUICInductiveInversion]
lenm_eq [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
leqb_univ_expr_n_spec' [in MetaCoq.Template.common.uGraph]
leqb_levelalg_n_spec [in MetaCoq.Template.common.uGraph]
leqb_levelalg_n_spec0 [in MetaCoq.Template.common.uGraph]
leqb_expr_univ_n_spec [in MetaCoq.Template.common.uGraph]
leqb_expr_univ_n_spec0 [in MetaCoq.Template.common.uGraph]
leqb_expr_n_spec [in MetaCoq.Template.common.uGraph]
leqb_expr_n_spec0 [in MetaCoq.Template.common.uGraph]
leqb_level_n_spec [in MetaCoq.Template.common.uGraph]
leqb_level_n_spec0 [in MetaCoq.Template.common.uGraph]
leqb_term_spec [in MetaCoq.SafeChecker.PCUICEqualityDec]
leq_prop_is_prop_sprop [in MetaCoq.Template.Universes]
leq_sprop_sprop [in MetaCoq.Template.Universes]
leq_prop_prop [in MetaCoq.Template.Universes]
leq_universe_sprop_l [in MetaCoq.Template.Universes]
leq_universe_prop_no_prop_sub_type [in MetaCoq.Template.Universes]
leq_universe_sprop_r [in MetaCoq.Template.Universes]
leq_universe_prop_r [in MetaCoq.Template.Universes]
leq_universe_props [in MetaCoq.Template.Universes]
leq_universe_super [in MetaCoq.Template.Universes]
leq_universe_product_mon [in MetaCoq.Template.Universes]
leq_universe_subset [in MetaCoq.Template.Universes]
leq_universe_product [in MetaCoq.Template.Universes]
leq_universe_sup_r [in MetaCoq.Template.Universes]
leq_universe_sup_l [in MetaCoq.Template.Universes]
leq_levelalg_sup0_mon [in MetaCoq.Template.Universes]
leq_levelalg_sup0_r [in MetaCoq.Template.Universes]
leq_levelalg_sup0_l [in MetaCoq.Template.Universes]
leq_universe_leq_universe_n [in MetaCoq.Template.Universes]
leq_levelalg_leq_levelalg_n [in MetaCoq.Template.Universes]
leq_cuniv_of_product_mon [in MetaCoq.Template.Universes]
leq_term_sprop_sorted_r [in MetaCoq.PCUIC.PCUICElimination]
leq_term_propositional_sorted_l [in MetaCoq.PCUIC.PCUICElimination]
leq_term_sprop_sorted_l [in MetaCoq.PCUIC.PCUICElimination]
leq_term_prop_sorted_r [in MetaCoq.PCUIC.PCUICElimination]
leq_term_prop_sorted_l [in MetaCoq.PCUIC.PCUICElimination]
leq_universe_propositional_l [in MetaCoq.PCUIC.PCUICElimination]
leq_term_mkApps [in MetaCoq.PCUIC.PCUICCumulativity]
leq_term_App [in MetaCoq.PCUIC.PCUICCumulativity]
leq_term_leq_term_napp [in MetaCoq.PCUIC.PCUICCumulativity]
leq_universe_propositional_l [in MetaCoq.Erasure.EArities]
leq_universe_propositional_r [in MetaCoq.Erasure.EArities]
leq_term_propopositional_sorted_r [in MetaCoq.Erasure.EArities]
leq_term_propositional_sorted_l [in MetaCoq.Erasure.EArities]
leq_universe_sort_of_products_mon [in MetaCoq.PCUIC.PCUICArities]
leq_term_App [in MetaCoq.Template.TermEquality]
leq_term_mkApps [in MetaCoq.Template.TermEquality]
leq_term_refl [in MetaCoq.Template.TermEquality]
leq_term_subset [in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
leq_term_eq_term_prop_impl [in MetaCoq.PCUIC.PCUICCumulProp]
leq_universe_prop_spec [in MetaCoq.PCUIC.PCUICCumulProp]
leq_levelalg_vertices [in MetaCoq.Template.common.uGraph]
leq_levelalg_vertices1 [in MetaCoq.Template.common.uGraph]
leq_levelalg_vertices0 [in MetaCoq.Template.common.uGraph]
leq_term_leq_term_napp [in MetaCoq.PCUIC.PCUICEquality]
leq_term_propositional_sorted_l [in MetaCoq.Erasure.ErasureFunction]
leq_term_empty_leq_term [in MetaCoq.PCUIC.PCUICPrincipality]
leq_term_subst_instance [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
leq_context_cumul_context [in MetaCoq.SafeChecker.PCUICSafeChecker]
leq_universe_sort_of_products [in MetaCoq.PCUIC.PCUICSpine]
leq_universeP [in MetaCoq.SafeChecker.PCUICEqualityDec]
leq0_level_n_complete [in MetaCoq.Template.common.uGraph]
LevelAlgExpr.val_make' [in MetaCoq.Template.Universes]
LevelAlgExpr.val_make [in MetaCoq.Template.Universes]
levelalg_get_is_level_correct [in MetaCoq.Template.Universes]
LevelExprSet_For_all [in MetaCoq.PCUIC.PCUICCumulProp]
LevelExpr.val_make_npl [in MetaCoq.Template.Universes]
LevelExpr.val_make [in MetaCoq.Template.Universes]
LevelIn_subst_instance [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
LevelSetsUIP.ok_irrel [in MetaCoq.Template.Reflect]
LevelSet_union_empty [in MetaCoq.Template.Universes]
LevelSet_In_fold_right_add [in MetaCoq.Template.Universes]
LevelSet_pair_In [in MetaCoq.Template.Universes]
levelset_for_all_eq [in MetaCoq.Template.common.uGraph]
LevelSet_in_union_global [in MetaCoq.PCUIC.PCUICGlobalEnv]
levels_univ_gc_declared_declared [in MetaCoq.Template.common.uGraph]
levels_gc_declared_declared [in MetaCoq.Template.common.uGraph]
levels_global_ext_constraint [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
levels_global_constraint [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
levels_global_levels_declared [in MetaCoq.SafeChecker.PCUICSafeChecker]
level_var_instance_length [in MetaCoq.PCUIC.PCUICInductiveInversion]
level_gc_declared_declared [in MetaCoq.Template.common.uGraph]
Level.eqb_spec [in MetaCoq.Template.Universes]
le_irrel [in MetaCoq.PCUIC.PCUICWcbvEval]
liftP_ctx [in MetaCoq.PCUIC.Syntax.PCUICInduction]
liftP_ctx_ind [in MetaCoq.PCUIC.Syntax.PCUICInduction]
lift_unlift_context [in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
lift_unlift_term [in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
lift_unlift [in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
lift_isLambda [in MetaCoq.Erasure.ESubstitution]
lift_inst_case_branch_context [in MetaCoq.Erasure.ESubstitution]
lift_isApp [in MetaCoq.Template.WfAst]
lift_to_wf_list [in MetaCoq.Template.WfAst]
lift_to_list [in MetaCoq.Template.WfAst]
lift_context_subst [in MetaCoq.PCUIC.PCUICInductives]
lift_context_expand_lets_ctx [in MetaCoq.PCUIC.PCUICInductives]
lift_context_subst_context_let_expand [in MetaCoq.PCUIC.PCUICInductives]
lift_context_lift_context [in MetaCoq.PCUIC.PCUICInductives]
lift_instance_length [in MetaCoq.PCUIC.PCUICInductiveInversion]
lift_iota_red [in MetaCoq.PCUIC.PCUICParallelReduction]
lift_rename' [in MetaCoq.PCUIC.PCUICParallelReduction]
lift_leq_term [in MetaCoq.PCUIC.PCUICEquality]
lift_eq_term [in MetaCoq.PCUIC.PCUICEquality]
lift_compare_context [in MetaCoq.PCUIC.PCUICEquality]
lift_compare_decls [in MetaCoq.PCUIC.PCUICEquality]
lift_compare_term [in MetaCoq.PCUIC.PCUICEquality]
lift_renaming_0 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
lift_rename [in MetaCoq.PCUIC.PCUICSigmaCalculus]
lift_renaming_0_rshift [in MetaCoq.PCUIC.PCUICSigmaCalculus]
lift_renaming_spec [in MetaCoq.PCUIC.PCUICSigmaCalculus]
lift_it_mkProd_or_LetIn [in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
lift_fix_context [in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
lift_context_lift_context [in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
lift_expand_lets_k [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
lift_closed [in MetaCoq.Erasure.ELiftSubst]
lift_mkApps [in MetaCoq.Erasure.ELiftSubst]
lift_isApp [in MetaCoq.Erasure.ELiftSubst]
lift_rel_alt [in MetaCoq.Erasure.ELiftSubst]
lift_rel_lt [in MetaCoq.Erasure.ELiftSubst]
lift_rel_ge [in MetaCoq.Erasure.ELiftSubst]
lift_declared_constant [in MetaCoq.PCUIC.Typing.PCUICWeakeningTyp]
lift_to_pred [in MetaCoq.PCUIC.PCUICConfluence]
lift_to_ws_red [in MetaCoq.PCUIC.PCUICConfluence]
lift_context_add [in MetaCoq.PCUIC.Syntax.PCUICClosed]
lift_decl_closed [in MetaCoq.PCUIC.Syntax.PCUICClosed]
lift_extended_subst' [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
lift_extended_subst [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
lift_it_mkLambda_or_LetIn [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
lift_it_mkProd_or_LetIn [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
lift_context_app [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
lift_context_alt [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
lift_context_snoc [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
lift_context_length [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
lift_decl0 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
lift_to_extended_list_k [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
lift_closed [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
lift_mkApps [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
lift_isApp [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
lift_rel_lt [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
lift_rel_ge [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
lift_context_snoc [in MetaCoq.Template.TypingWf]
lift_to_extended_list_k [in MetaCoq.Template.LiftSubst]
lift_closed [in MetaCoq.Template.LiftSubst]
lift_mkApps [in MetaCoq.Template.LiftSubst]
lift_rel_lt [in MetaCoq.Template.LiftSubst]
lift_rel_ge [in MetaCoq.Template.LiftSubst]
lift_to_extended_list_k [in MetaCoq.PCUIC.PCUICSpine]
lift_context0_app [in MetaCoq.PCUIC.PCUICSpine]
lift_context_subst_context [in MetaCoq.PCUIC.PCUICSpine]
lift0_rename [in MetaCoq.PCUIC.PCUICSigmaCalculus]
lift0_open [in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
lift0_inst [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
lift0_p [in MetaCoq.Erasure.ELiftSubst]
lift0_id [in MetaCoq.Erasure.ELiftSubst]
lift0_context [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
lift0_p [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
lift0_id [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
lift0_inst_id [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
lift0_p [in MetaCoq.Template.LiftSubst]
lift0_id [in MetaCoq.Template.LiftSubst]
ListOrderedType.compare_trans [in MetaCoq.Template.utils.MCCompare]
ListOrderedType.compare_lt_lt [in MetaCoq.Template.utils.MCCompare]
ListOrderedType.compare_sym [in MetaCoq.Template.utils.MCCompare]
ListOrderedType.compare_refl [in MetaCoq.Template.utils.MCCompare]
ListOrderedType.compare_eq [in MetaCoq.Template.utils.MCCompare]
list_size_map_hom [in MetaCoq.Template.utils.MCList]
list_size_map_le [in MetaCoq.Template.utils.MCList]
list_size_mapi_le [in MetaCoq.Template.utils.MCList]
list_size_mapi_rec_le [in MetaCoq.Template.utils.MCList]
list_size_map_eq [in MetaCoq.Template.utils.MCList]
list_size_mapi_eq [in MetaCoq.Template.utils.MCList]
list_size_mapi_rec_eq [in MetaCoq.Template.utils.MCList]
list_size_map [in MetaCoq.Template.utils.MCList]
list_size_length [in MetaCoq.Template.utils.MCList]
list_size_rev [in MetaCoq.Template.utils.MCList]
list_size_app [in MetaCoq.Template.utils.MCList]
list_rect_rev [in MetaCoq.Template.utils.MCList]
list_ind_rev [in MetaCoq.Template.utils.MCList]
list_size_length [in MetaCoq.Examples.tauto]
list_length_rev_ind [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
list_size_rev [in MetaCoq.PCUIC.Syntax.PCUICInduction]
list_size_mapi_context_hom [in MetaCoq.PCUIC.Syntax.PCUICInduction]
list_depth_mapi_rec_le [in MetaCoq.PCUIC.Syntax.PCUICDepth]
list_depth_rev [in MetaCoq.PCUIC.Syntax.PCUICDepth]
list_depth_app [in MetaCoq.PCUIC.Syntax.PCUICDepth]
list_length_ind [in MetaCoq.Template.LiftSubst]
list_map_swap_eq' [in MetaCoq.PCUIC.PCUICReduction]
list_map_swap_eq [in MetaCoq.PCUIC.PCUICReduction]
list_split_eq [in MetaCoq.PCUIC.PCUICReduction]
local_env_telescope [in MetaCoq.PCUIC.PCUICConfluence]
local_env_telescope [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
lookup_lookup_global_env_None [in MetaCoq.Template.EtaExpand]
lookup_global_env_lookup [in MetaCoq.Template.EtaExpand]
lookup_lookup_global_env [in MetaCoq.Template.EtaExpand]
lookup_lookup_env [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
lookup_env_cons_fresh [in MetaCoq.PCUIC.utils.PCUICAstUtils]
lookup_env_cons [in MetaCoq.PCUIC.utils.PCUICAstUtils]
lookup_env_nil [in MetaCoq.PCUIC.utils.PCUICAstUtils]
lookup_env_Some_fresh [in MetaCoq.PCUIC.PCUICWeakeningEnv]
lookup_global_Some_fresh [in MetaCoq.PCUIC.PCUICWeakeningEnv]
lookup_inductive_pars_constructor_pars_args [in MetaCoq.Erasure.EEtaExpandedFix]
lookup_inductive_None [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
lookup_on_global_env [in MetaCoq.Template.Typing]
lookup_projection_optimize [in MetaCoq.Erasure.EInlineProjections]
lookup_constructor_optimize [in MetaCoq.Erasure.EInlineProjections]
lookup_env_optimize [in MetaCoq.Erasure.EInlineProjections]
lookup_env_optimize_env_None [in MetaCoq.Erasure.EInlineProjections]
lookup_env_map_snd [in MetaCoq.Erasure.EInlineProjections]
lookup_env_optimize_env_Some [in MetaCoq.Erasure.EInlineProjections]
lookup_inductive_wellformed [in MetaCoq.Erasure.EInlineProjections]
lookup_constructor_transform_blocks [in MetaCoq.Erasure.EConstructorsAsBlocks]
lookup_env_transform_blocks [in MetaCoq.Erasure.EConstructorsAsBlocks]
lookup_constructor_pars_args_spec [in MetaCoq.Erasure.EConstructorsAsBlocks]
lookup_ind_decl_complete [in MetaCoq.SafeChecker.PCUICSafeRetyping]
lookup_inductive_declared [in MetaCoq.PCUIC.Syntax.PCUICCases]
lookup_projection_lookup_constructor [in MetaCoq.Erasure.ErasureProperties]
lookup_erase_global [in MetaCoq.Erasure.ErasureFunction]
lookup_env_erase [in MetaCoq.Erasure.ErasureFunction]
lookup_env_cons_disc [in MetaCoq.Erasure.ErasureFunction]
lookup_env_ext [in MetaCoq.Erasure.ErasureFunction]
lookup_env_wellformed [in MetaCoq.Erasure.EWellformed]
lookup_env_nlg [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
lookup_on_global_env [in MetaCoq.PCUIC.PCUICTyping]
lookup_env_Some_fresh [in MetaCoq.Erasure.EGlobalEnv]
lookup_constructor_pars_args_cstr_arity [in MetaCoq.Erasure.EGlobalEnv]
lookup_constructor_lookup_inductive [in MetaCoq.Erasure.EGlobalEnv]
lookup_projection_lookup_constructor [in MetaCoq.Erasure.EGlobalEnv]
lookup_env_In [in MetaCoq.Erasure.EExtends]
lookup_minductive_declared_inductive [in MetaCoq.Erasure.ERemoveParams]
lookup_minductive_declared_minductive [in MetaCoq.Erasure.ERemoveParams]
lookup_inductive_pars_spec [in MetaCoq.Erasure.ERemoveParams]
lookup_constructor_lookup_inductive_pars [in MetaCoq.Erasure.ERemoveParams]
lookup_inductive_pars_is_prop_and_pars [in MetaCoq.Erasure.ERemoveParams]
lookup_constructor_strip [in MetaCoq.Erasure.ERemoveParams]
lookup_env_strip [in MetaCoq.Erasure.ERemoveParams]
lookup_inductive_pars_constructor_pars_args [in MetaCoq.Erasure.ERemoveParams]
lookup_env_closed [in MetaCoq.Erasure.EWcbvEval]
lookup_env_extends [in MetaCoq.Template.TypingWf]
lookup_projection_gen_transform [in MetaCoq.Erasure.EGenericMapEnv]
lookup_constructor_gen_transform [in MetaCoq.Erasure.EGenericMapEnv]
lookup_env_gen_transform [in MetaCoq.Erasure.EGenericMapEnv]
lookup_env_gen_transform_env_None [in MetaCoq.Erasure.EGenericMapEnv]
lookup_env_map_snd [in MetaCoq.Erasure.EGenericMapEnv]
lookup_env_gen_transform_env_Some [in MetaCoq.Erasure.EGenericMapEnv]
lookup_constructor_optimize [in MetaCoq.Erasure.EOptimizePropDiscr]
lookup_env_optimize [in MetaCoq.Erasure.EOptimizePropDiscr]
lookup_env_optimize_env_None [in MetaCoq.Erasure.EOptimizePropDiscr]
lookup_env_map_snd [in MetaCoq.Erasure.EOptimizePropDiscr]
lookup_env_optimize_env_Some [in MetaCoq.Erasure.EOptimizePropDiscr]
Lookup.consistent_instance_length [in MetaCoq.Template.EnvironmentTyping]
Lookup.declared_projection_lookup [in MetaCoq.Template.EnvironmentTyping]
Lookup.declared_constructor_lookup [in MetaCoq.Template.EnvironmentTyping]
Lookup.declared_inductive_lookup [in MetaCoq.Template.EnvironmentTyping]
Lookup.declared_minductive_lookup [in MetaCoq.Template.EnvironmentTyping]
Lookup.declared_constant_lookup [in MetaCoq.Template.EnvironmentTyping]
Lookup.global_ext_levels_InSet [in MetaCoq.Template.EnvironmentTyping]
Lookup.global_levels_memSet [in MetaCoq.Template.EnvironmentTyping]
Lookup.global_levels_InSet [in MetaCoq.Template.EnvironmentTyping]
Lookup.lookup_projection_declared [in MetaCoq.Template.EnvironmentTyping]
Lookup.lookup_constructor_declared [in MetaCoq.Template.EnvironmentTyping]
Lookup.lookup_inductive_declared [in MetaCoq.Template.EnvironmentTyping]
Lookup.lookup_minductive_declared [in MetaCoq.Template.EnvironmentTyping]
Lookup.lookup_constant_declared [in MetaCoq.Template.EnvironmentTyping]
LSet_in_global_bounded [in MetaCoq.PCUIC.PCUICInductiveInversion]
LSet_in_poly_bounded [in MetaCoq.PCUIC.PCUICInductiveInversion]
lt_not_eq [in MetaCoq.Template.utils.ByteCompareSpec]
lt_trans [in MetaCoq.Template.utils.ByteCompareSpec]
lt_level_irrel [in MetaCoq.Template.Reflect]
| 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) |