| 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) |
E (lemma)
ecofix_subst_nth [in MetaCoq.Erasure.Prelim]efix_subst_nth [in MetaCoq.Erasure.Prelim]
einfering_sort_isType [in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
elimP [in MetaCoq.Template.utils.ReflectEq]
elimT [in MetaCoq.Template.utils.MCReflect]
elim_restriction_works_proj [in MetaCoq.PCUIC.PCUICElimination]
elim_restriction_works_proj_kelim1 [in MetaCoq.PCUIC.PCUICElimination]
elim_restriction_works [in MetaCoq.PCUIC.PCUICElimination]
elim_restriction_works_kelim [in MetaCoq.PCUIC.PCUICElimination]
elim_sort_intype [in MetaCoq.PCUIC.PCUICElimination]
elim_restriction_works_kelim1 [in MetaCoq.PCUIC.PCUICElimination]
elim_inspect [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
elookup_env_cons_disc [in MetaCoq.Erasure.ErasureFunction]
elookup_env_cons_fresh [in MetaCoq.Erasure.EGlobalEnv]
emkApps_snoc [in MetaCoq.Erasure.Prelim]
empty_contextset_subset [in MetaCoq.Template.Universes]
Environment.All_decls_to_alpha [in MetaCoq.Template.Environment]
Environment.All_decls_alpha_impl [in MetaCoq.Template.Environment]
Environment.All_decls_impl [in MetaCoq.Template.Environment]
Environment.app_context_length [in MetaCoq.Template.Environment]
Environment.app_context_cons [in MetaCoq.Template.Environment]
Environment.app_context_assoc [in MetaCoq.Template.Environment]
Environment.app_context_nil_l [in MetaCoq.Template.Environment]
Environment.arities_context_length [in MetaCoq.Template.Environment]
Environment.context_assumptions_lift_context [in MetaCoq.Template.Environment]
Environment.context_assumptions_subst_context [in MetaCoq.Template.Environment]
Environment.context_assumptions_subst_instance [in MetaCoq.Template.Environment]
Environment.context_assumptions_mapi [in MetaCoq.Template.Environment]
Environment.context_assumptions_app [in MetaCoq.Template.Environment]
Environment.context_assumptions_map [in MetaCoq.Template.Environment]
Environment.context_assumptions_length_bound [in MetaCoq.Template.Environment]
Environment.context_assumptions_fold [in MetaCoq.Template.Environment]
Environment.eta_global_env [in MetaCoq.Template.Environment]
Environment.expand_lets_ctx_length [in MetaCoq.Template.Environment]
Environment.expand_lets_k_ctx_length [in MetaCoq.Template.Environment]
Environment.extended_subst_length [in MetaCoq.Template.Environment]
Environment.extends_refl [in MetaCoq.Template.Environment]
Environment.ind_projs_map [in MetaCoq.Template.Environment]
Environment.ind_pars_map [in MetaCoq.Template.Environment]
Environment.ind_ctors_map [in MetaCoq.Template.Environment]
Environment.ind_type_map [in MetaCoq.Template.Environment]
Environment.it_mkProd_or_LetIn_app [in MetaCoq.Template.Environment]
Environment.lift_context_length [in MetaCoq.Template.Environment]
Environment.lift_context_alt [in MetaCoq.Template.Environment]
Environment.map_cst_body [in MetaCoq.Template.Environment]
Environment.map_cst_type [in MetaCoq.Template.Environment]
Environment.nth_error_lt [in MetaCoq.Template.Environment]
Environment.nth_error_ge [in MetaCoq.Template.Environment]
Environment.nth_error_fold_context_k_eq [in MetaCoq.Template.Environment]
Environment.nth_error_fold_context_k [in MetaCoq.Template.Environment]
Environment.nth_error_app_context_lt [in MetaCoq.Template.Environment]
Environment.nth_error_app_context_ge [in MetaCoq.Template.Environment]
Environment.projs_length [in MetaCoq.Template.Environment]
Environment.reln_alt_eq [in MetaCoq.Template.Environment]
Environment.reln_list_lift_above [in MetaCoq.Template.Environment]
Environment.reln_fold [in MetaCoq.Template.Environment]
Environment.smash_context_app [in MetaCoq.Template.Environment]
Environment.smash_context_length [in MetaCoq.Template.Environment]
Environment.subst_instance_length [in MetaCoq.Template.Environment]
Environment.subst_context_snoc [in MetaCoq.Template.Environment]
Environment.subst_context_alt [in MetaCoq.Template.Environment]
Environment.subst_context_nil [in MetaCoq.Template.Environment]
Environment.subst_context_length [in MetaCoq.Template.Environment]
Environment.to_extended_list_k_cons [in MetaCoq.Template.Environment]
Environment.to_extended_list_lift_above [in MetaCoq.Template.Environment]
Environment.to_extended_list_k_spec [in MetaCoq.Template.Environment]
EnvMap.fold_left_cons [in MetaCoq.Template.EnvMap]
EnvMap.gso [in MetaCoq.Template.EnvMap]
EnvMap.gss [in MetaCoq.Template.EnvMap]
EnvMap.lookup_spec [in MetaCoq.Template.EnvMap]
EnvMap.lookup_add_other [in MetaCoq.Template.EnvMap]
EnvMap.lookup_add [in MetaCoq.Template.EnvMap]
EnvMap.of_global_env_cons [in MetaCoq.Template.EnvMap]
EnvMap.remove_add_o [in MetaCoq.Template.EnvMap]
EnvMap.remove_add_eq [in MetaCoq.Template.EnvMap]
EnvMap.repr_add [in MetaCoq.Template.EnvMap]
EnvMap.repr_global_env [in MetaCoq.Template.EnvMap]
EnvMap.unfold_equal [in MetaCoq.Template.EnvMap]
EnvTyping.All_local_env_size_app [in MetaCoq.Template.EnvironmentTyping]
EnvTyping.All_local_env_size_pos [in MetaCoq.Template.EnvironmentTyping]
EnvTyping.All_local_rel_app [in MetaCoq.Template.EnvironmentTyping]
EnvTyping.All_local_app_rel [in MetaCoq.Template.EnvironmentTyping]
EnvTyping.All_local_local_rel [in MetaCoq.Template.EnvironmentTyping]
EnvTyping.All_local_rel_local [in MetaCoq.Template.EnvironmentTyping]
EnvTyping.All_local_env_skipn [in MetaCoq.Template.EnvironmentTyping]
EnvTyping.All_local_env_impl_ind [in MetaCoq.Template.EnvironmentTyping]
EnvTyping.All_local_env_impl [in MetaCoq.Template.EnvironmentTyping]
EnvTyping.All_local_env_fold [in MetaCoq.Template.EnvironmentTyping]
EnvTyping.ctx_inst_impl [in MetaCoq.Template.EnvironmentTyping]
EnvTyping.infer_typing_sort_impl [in MetaCoq.Template.EnvironmentTyping]
EnvTyping.infer_sort_impl [in MetaCoq.Template.EnvironmentTyping]
EnvTyping.lift_typing_impl [in MetaCoq.Template.EnvironmentTyping]
EnvTyping.lift_judgment_impl [in MetaCoq.Template.EnvironmentTyping]
env_eq [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
env_prop_sigma [in MetaCoq.Template.Typing]
env_prop_wf_local [in MetaCoq.Template.Typing]
env_prop_typing [in MetaCoq.Template.Typing]
env_prop_sigma [in MetaCoq.PCUIC.PCUICTyping]
env_prop_wf_local [in MetaCoq.PCUIC.PCUICTyping]
env_prop_typing [in MetaCoq.PCUIC.PCUICTyping]
eqb_true_iff [in MetaCoq.Template.Universes]
eqb_annot_reflect [in MetaCoq.PCUIC.utils.PCUICAstUtils]
eqb_refl [in MetaCoq.Template.utils.ReflectEq]
eqb_eq [in MetaCoq.Template.utils.ReflectEq]
eqb_specT [in MetaCoq.Template.utils.ReflectEq]
eqb_universe_instance_complete [in MetaCoq.SafeChecker.PCUICSafeConversion]
eqb_universe_instance_spec [in MetaCoq.SafeChecker.PCUICSafeConversion]
eqb_ctx_spec [in MetaCoq.SafeChecker.PCUICEqualityDec]
eqb_term_refl [in MetaCoq.SafeChecker.PCUICEqualityDec]
eqb_term_spec [in MetaCoq.SafeChecker.PCUICEqualityDec]
eqb_termp_napp_spec [in MetaCoq.SafeChecker.PCUICEqualityDec]
eqb_binder_annot_spec [in MetaCoq.SafeChecker.PCUICEqualityDec]
eqb_term_upto_univ_refl [in MetaCoq.SafeChecker.PCUICEqualityDec]
eqb_term_upto_univ_impl [in MetaCoq.SafeChecker.PCUICEqualityDec]
eqb_annots_reflect [in MetaCoq.SafeChecker.PCUICEqualityDec]
eqb_annots_spec [in MetaCoq.SafeChecker.PCUICEqualityDec]
eqb_annot_refl [in MetaCoq.SafeChecker.PCUICEqualityDec]
eqb_annot_reflect [in MetaCoq.SafeChecker.PCUICEqualityDec]
eqb_annot_spec [in MetaCoq.SafeChecker.PCUICEqualityDec]
eqt_eqterm [in MetaCoq.SafeChecker.PCUICSafeConversion]
Equal_graph_edges [in MetaCoq.Template.common.uGraph]
equal_subst_instance_cstrs_mono [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
equiv_reflectT [in MetaCoq.Template.utils.MCReflect]
equiv_contr_contr [in MetaCoq.Translations.MiniHoTT]
equiv_inverse [in MetaCoq.Translations.MiniHoTT]
equiv_contr_contr [in MetaCoq.Translations.MiniHoTT_paths]
equiv_inverse [in MetaCoq.Translations.MiniHoTT_paths]
eq_universe_subset [in MetaCoq.Template.Universes]
eq_leq_universe [in MetaCoq.Template.Universes]
eq_leq_levelalg [in MetaCoq.Template.Universes]
eq_term_eq_termp [in MetaCoq.PCUIC.PCUICCumulativity]
eq_term_mkApps [in MetaCoq.PCUIC.PCUICCumulativity]
eq_term_eq_term_napp [in MetaCoq.PCUIC.PCUICCumulativity]
eq_term_App [in MetaCoq.PCUIC.PCUICCumulativity]
eq_names_subst_instance_pcuic [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
eq_names_subst_context_pcuic [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
eq_binder_trans [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
eq_names_subst_instance [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
eq_names_subst_context [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
eq_pair_transport [in MetaCoq.PCUIC.Syntax.PCUICViews]
eq_annots_cstr_branch_context [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
eq_annots_ind_predicate_context [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
eq_annots_expand_lets_ctx [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
eq_binder_annot_eq_context_gen_set_binder_name [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
eq_term_upto_univ_mkApps [in MetaCoq.Template.TermEquality]
eq_term_App [in MetaCoq.Template.TermEquality]
eq_term_upto_univ_App [in MetaCoq.Template.TermEquality]
eq_term_leq_term [in MetaCoq.Template.TermEquality]
eq_term_upto_univ_morphism [in MetaCoq.Template.TermEquality]
eq_term_upto_univ_morphism0 [in MetaCoq.Template.TermEquality]
eq_term_refl [in MetaCoq.Template.TermEquality]
eq_term_upto_univ_refl [in MetaCoq.Template.TermEquality]
eq_term_subset [in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
eq_term_set_binder_name [in MetaCoq.PCUIC.PCUICValidity]
eq_binder_annots_eq_ctx [in MetaCoq.PCUIC.PCUICValidity]
eq_context_upto_map2_set_binder_name [in MetaCoq.PCUIC.PCUICCumulProp]
eq_term_upto_univ_napp_leq [in MetaCoq.PCUIC.PCUICCumulProp]
eq_term_prop_mkApps_inv [in MetaCoq.PCUIC.PCUICCumulProp]
eq_term_eq_term_prop_impl [in MetaCoq.PCUIC.PCUICCumulProp]
eq_term_prop_impl [in MetaCoq.PCUIC.PCUICCumulProp]
eq_rect_transport [in MetaCoq.Template.utils.MCEquality]
eq_annots_inst_case_context [in MetaCoq.PCUIC.PCUICEquality]
eq_annots_subst_instance_ctx [in MetaCoq.PCUIC.PCUICEquality]
eq_annots_lift_context [in MetaCoq.PCUIC.PCUICEquality]
eq_annots_subst_context [in MetaCoq.PCUIC.PCUICEquality]
eq_annots_fold [in MetaCoq.PCUIC.PCUICEquality]
eq_context_gen_binder_annot [in MetaCoq.PCUIC.PCUICEquality]
eq_univ_make [in MetaCoq.PCUIC.PCUICEquality]
eq_term_upto_univ_napp_flip [in MetaCoq.PCUIC.PCUICEquality]
eq_term_upto_univ_mkApps_inv [in MetaCoq.PCUIC.PCUICEquality]
eq_term_it_mkLambda_or_LetIn_inv [in MetaCoq.PCUIC.PCUICEquality]
eq_term_it_mkProd_or_LetIn [in MetaCoq.PCUIC.PCUICEquality]
eq_term_upto_univ_it_mkProd_or_LetIn [in MetaCoq.PCUIC.PCUICEquality]
eq_term_it_mkLambda_or_LetIn [in MetaCoq.PCUIC.PCUICEquality]
eq_term_upto_univ_it_mkLambda_or_LetIn_r [in MetaCoq.PCUIC.PCUICEquality]
eq_term_upto_univ_it_mkLambda_or_LetIn [in MetaCoq.PCUIC.PCUICEquality]
eq_context_impl [in MetaCoq.PCUIC.PCUICEquality]
eq_context_upto_nth_error [in MetaCoq.PCUIC.PCUICEquality]
eq_context_upto_smash_context [in MetaCoq.PCUIC.PCUICEquality]
eq_context_upto_subst_context [in MetaCoq.PCUIC.PCUICEquality]
eq_context_upto_length [in MetaCoq.PCUIC.PCUICEquality]
eq_context_upto_rev' [in MetaCoq.PCUIC.PCUICEquality]
eq_context_upto_rev [in MetaCoq.PCUIC.PCUICEquality]
eq_context_upto_cat [in MetaCoq.PCUIC.PCUICEquality]
eq_context_upto_sym [in MetaCoq.PCUIC.PCUICEquality]
eq_context_upto_refl [in MetaCoq.PCUIC.PCUICEquality]
eq_term_upto_univ_isApp [in MetaCoq.PCUIC.PCUICEquality]
eq_term_upto_univ_mkApps_r_inv [in MetaCoq.PCUIC.PCUICEquality]
eq_term_upto_univ_mkApps_l_inv [in MetaCoq.PCUIC.PCUICEquality]
eq_term_upto_univ_mkApps [in MetaCoq.PCUIC.PCUICEquality]
eq_term_upto_univ_napp_mkApps_r_inv [in MetaCoq.PCUIC.PCUICEquality]
eq_term_upto_univ_napp_mkApps_l_inv [in MetaCoq.PCUIC.PCUICEquality]
eq_term_upto_univ_napp_mkApps [in MetaCoq.PCUIC.PCUICEquality]
eq_term_eq_term_napp [in MetaCoq.PCUIC.PCUICEquality]
eq_term_upto_univ_subst [in MetaCoq.PCUIC.PCUICEquality]
eq_term_upto_univ_substs [in MetaCoq.PCUIC.PCUICEquality]
eq_term_upto_univ_lift [in MetaCoq.PCUIC.PCUICEquality]
eq_term_upto_univ_antisym [in MetaCoq.PCUIC.PCUICEquality]
eq_binder_relevances_refl [in MetaCoq.PCUIC.PCUICEquality]
eq_context_gen_impl [in MetaCoq.PCUIC.PCUICEquality]
eq_context_upto_names_gen [in MetaCoq.PCUIC.PCUICEquality]
eq_projection_refl [in MetaCoq.Template.Kernames]
eq_inductive_refl [in MetaCoq.Template.Kernames]
eq_kername_refl [in MetaCoq.Template.Kernames]
eq_term_valid_pos [in MetaCoq.PCUIC.Syntax.PCUICPosition]
eq_term_upto_valid_pos [in MetaCoq.PCUIC.Syntax.PCUICPosition]
eq_context_upto_context_choice_term [in MetaCoq.PCUIC.Syntax.PCUICPosition]
eq_term_upto_univ_napp_0 [in MetaCoq.PCUIC.PCUICAlpha]
eq_context_conversion [in MetaCoq.PCUIC.PCUICAlpha]
eq_binder_annots_eq_context_gen_ctx [in MetaCoq.PCUIC.PCUICAlpha]
eq_context_gen_upto [in MetaCoq.PCUIC.PCUICAlpha]
eq_context_upto_subst_instance [in MetaCoq.PCUIC.PCUICAlpha]
eq_context_upto_lift_context [in MetaCoq.PCUIC.PCUICAlpha]
eq_context_upto_map2_set_binder_name [in MetaCoq.PCUIC.PCUICAlpha]
eq_context_upto_conv_context_rel [in MetaCoq.PCUIC.PCUICAlpha]
eq_context_upto_empty_impl [in MetaCoq.PCUIC.PCUICAlpha]
eq_prod_refl [in MetaCoq.Template.utils.ReflectEq]
eq_annots_expand_lets_ctx [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
eq_names_subst_instance_pcuic [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
eq_names_subst_context_pcuic [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
eq_term_upto_univ_expand_lets [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
eq_context_upto_context_assumptions [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
eq_context_gen_smash_context [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
eq_context_gen_extended_subst [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
eq_binder_trans [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
eq_names_smash_context [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
eq_termp_mkApps_inv [in MetaCoq.PCUIC.PCUICConvCumInversion]
eq_term_upto_univ_napp_nonind [in MetaCoq.PCUIC.PCUICConvCumInversion]
eq_term_eq_termp [in MetaCoq.PCUIC.PCUICConvCumInversion]
eq_term_upto_univ_inst [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
eq_term_valid_pos [in MetaCoq.SafeChecker.PCUICSafeConversion]
eq_context_upto_inst_case_context [in MetaCoq.PCUIC.PCUICPrincipality]
eq_term_upto_univ_napp_leq [in MetaCoq.PCUIC.PCUICPrincipality]
eq_context_empty_eq_context [in MetaCoq.PCUIC.PCUICPrincipality]
eq_term_empty_eq_term [in MetaCoq.PCUIC.PCUICPrincipality]
eq_term_empty_leq_term [in MetaCoq.PCUIC.PCUICPrincipality]
eq_term_leq_term [in MetaCoq.PCUIC.PCUICPrincipality]
eq_form [in MetaCoq.Examples.tauto]
eq_var [in MetaCoq.Examples.tauto]
eq_term_nl_eq [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
eq_context_nl [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
eq_context_nl_IH [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
eq_context_gen_upto [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
eq_term_upto_univ_napp_on_free_vars [in MetaCoq.PCUIC.PCUICConfluence]
eq_context_upto_names_red_ctx_alpha [in MetaCoq.PCUIC.PCUICConfluence]
eq_context_upto_names_red_ctx [in MetaCoq.PCUIC.PCUICConfluence]
eq_context_upto_names_app [in MetaCoq.PCUIC.PCUICConfluence]
eq_context_upto_names_on_free_vars [in MetaCoq.PCUIC.PCUICConfluence]
eq_context_upto_flip [in MetaCoq.PCUIC.PCUICConfluence]
eq_context_upto_univ_subst_instance' [in MetaCoq.PCUIC.PCUICConfluence]
eq_context_upto_univ_subst_instance [in MetaCoq.PCUIC.PCUICConfluence]
eq_term_upto_univ_subst_instance' [in MetaCoq.PCUIC.PCUICConfluence]
eq_context_gen_eq_univ_subst_preserved [in MetaCoq.PCUIC.PCUICConfluence]
eq_context_gen_eq_context_upto [in MetaCoq.PCUIC.PCUICConfluence]
eq_context_extended_subst [in MetaCoq.PCUIC.PCUICConfluence]
eq_context_gen_context_assumptions [in MetaCoq.PCUIC.PCUICConfluence]
eq_term_inds [in MetaCoq.PCUIC.PCUICConversion]
eq_term_compare_term [in MetaCoq.PCUIC.PCUICConversion]
eq_context_upto_ws_cumul_ctx_pb [in MetaCoq.PCUIC.PCUICConversion]
eq_term_fix_or_cofix [in MetaCoq.PCUIC.PCUICConversion]
eq_context_gen_inst_case_context [in MetaCoq.PCUIC.PCUICConversion]
eq_context_gen_subst_context [in MetaCoq.PCUIC.PCUICConversion]
eq_term_upto_univ_conv_arity_r [in MetaCoq.PCUIC.PCUICConversion]
eq_term_upto_univ_conv_arity_l [in MetaCoq.PCUIC.PCUICConversion]
eq_terms_ws_cumul_pb_terms [in MetaCoq.PCUIC.PCUICConversion]
eq_term_upto_univ_cumulSpec [in MetaCoq.PCUIC.PCUICConversion]
eq_term_upto_univ_napp_cumulSpec [in MetaCoq.PCUIC.PCUICConversion]
eq_binder_annots_eq [in MetaCoq.PCUIC.PCUICCasesContexts]
eq_names_subst_instance [in MetaCoq.PCUIC.PCUICCasesContexts]
eq_names_subst_context [in MetaCoq.PCUIC.PCUICCasesContexts]
eq_context_upto_univ_cumul_context [in MetaCoq.PCUIC.PCUICContextConversion]
eq_context_upto_univ_conv_context [in MetaCoq.PCUIC.PCUICContextConversion]
eq_context_upto_empty_conv_context [in MetaCoq.PCUIC.PCUICContextConversion]
eq_context_upto_cumul_context [in MetaCoq.PCUIC.PCUICContextConversion]
eq_context_upto_conv_context [in MetaCoq.PCUIC.PCUICContextConversion]
eq_leq_context_upto [in MetaCoq.PCUIC.PCUICContextConversion]
eq_context_upto_impl [in MetaCoq.PCUIC.PCUICContextConversion]
eq_context_upto_names_upto_names [in MetaCoq.PCUIC.PCUICSR]
eq_ws_cumul_pb_terms_trans [in MetaCoq.PCUIC.PCUICSR]
eq_ws_cumul_pb_trans [in MetaCoq.PCUIC.PCUICSR]
eq_context_alpha_to_extended_list [in MetaCoq.PCUIC.PCUICSR]
eq_context_alpha_reln [in MetaCoq.PCUIC.PCUICSR]
eq_context_alpha_conv [in MetaCoq.PCUIC.PCUICSR]
eq_term_subst_instance [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
eq_term_upto_univ_subst_instance [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
eq_valuation [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
eq_term_upto_univ_rename [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
eq_context_upto_univ_cumul_context [in MetaCoq.SafeChecker.PCUICSafeChecker]
eq_context_upto_cumul_context [in MetaCoq.SafeChecker.PCUICSafeChecker]
eq_decl_upto_refl [in MetaCoq.SafeChecker.PCUICSafeChecker]
eq_decl_eq_decl_upto [in MetaCoq.SafeChecker.PCUICSafeChecker]
eq_tip_skipn [in MetaCoq.Template.TypingWf]
eq_decompose_app [in MetaCoq.Template.TypingWf]
eq_names_subst_instance [in MetaCoq.PCUIC.PCUICContexts]
eq_names_subst_context [in MetaCoq.PCUIC.PCUICContexts]
eq_context_alpha_conv [in MetaCoq.PCUIC.PCUICSpine]
eq_universeP [in MetaCoq.SafeChecker.PCUICEqualityDec]
eq_dec_to_bool_refl [in MetaCoq.SafeChecker.PCUICEqualityDec]
eq_context_gen_wf_branch [in MetaCoq.SafeChecker.PCUICTypeChecker]
eq_context_gen_wf_predicate [in MetaCoq.SafeChecker.PCUICTypeChecker]
eq0_leq0_levelalg [in MetaCoq.Template.Universes]
eqáµ—_unit_unit [in MetaCoq.Translations.times_bool_fun]
erasable_tBox_value [in MetaCoq.Erasure.ErasureFunction]
erases_subst0 [in MetaCoq.Erasure.ESubstitution]
erases_subst [in MetaCoq.Erasure.ESubstitution]
erases_eq [in MetaCoq.Erasure.ESubstitution]
erases_weakening [in MetaCoq.Erasure.ESubstitution]
erases_weakening' [in MetaCoq.Erasure.ESubstitution]
erases_ctx_ext [in MetaCoq.Erasure.ESubstitution]
erases_extends [in MetaCoq.Erasure.ESubstitution]
erases_global_wf_glob [in MetaCoq.Erasure.ErasureCorrectness]
erases_mutual_inductive_body_wf [in MetaCoq.Erasure.ErasureCorrectness]
erases_global_decls_fresh [in MetaCoq.Erasure.ErasureCorrectness]
erases_global_closed_env [in MetaCoq.Erasure.ErasureCorrectness]
erases_correct [in MetaCoq.Erasure.ErasureCorrectness]
erases_global_erases_deps [in MetaCoq.Erasure.EDeps]
erases_global_all_deps [in MetaCoq.Erasure.EDeps]
erases_deps_single [in MetaCoq.Erasure.EDeps]
erases_declared_constructor [in MetaCoq.Erasure.EDeps]
erases_deps_cons [in MetaCoq.Erasure.EDeps]
erases_deps_forall_ind [in MetaCoq.Erasure.EDeps]
erases_deps_eval [in MetaCoq.Erasure.EDeps]
erases_deps_cunfold_cofix [in MetaCoq.Erasure.EDeps]
erases_deps_cunfold_fix [in MetaCoq.Erasure.EDeps]
erases_deps_substl [in MetaCoq.Erasure.EDeps]
erases_deps_csubst [in MetaCoq.Erasure.EDeps]
erases_deps_subst1 [in MetaCoq.Erasure.EDeps]
erases_deps_subst [in MetaCoq.Erasure.EDeps]
erases_deps_lift [in MetaCoq.Erasure.EDeps]
erases_deps_mkApps_inv [in MetaCoq.Erasure.EDeps]
erases_deps_mkApps [in MetaCoq.Erasure.EDeps]
erases_forall_list_ind [in MetaCoq.Erasure.Extract]
erases_wellformed [in MetaCoq.Erasure.ErasureProperties]
erases_closed [in MetaCoq.Erasure.ErasureProperties]
erases_subst_instance_decl [in MetaCoq.Erasure.ErasureProperties]
erases_subst_instance'' [in MetaCoq.Erasure.ErasureProperties]
erases_subst_instance [in MetaCoq.Erasure.ErasureProperties]
erases_subst_instance0 [in MetaCoq.Erasure.ErasureProperties]
erases_context_conversion [in MetaCoq.Erasure.ErasureProperties]
erases_isLambda [in MetaCoq.Erasure.ErasureProperties]
erases_mkApps_inv [in MetaCoq.Erasure.ErasureProperties]
erases_mkApps [in MetaCoq.Erasure.ErasureProperties]
erases_App [in MetaCoq.Erasure.ErasureProperties]
erases_ext_eq [in MetaCoq.Erasure.ErasureProperties]
erases_wf_fixpoints [in MetaCoq.Erasure.ErasureFunction]
erases_deps_wellformed [in MetaCoq.Erasure.ErasureFunction]
erases_deps_erase_weaken [in MetaCoq.Erasure.ErasureFunction]
erases_deps_erase [in MetaCoq.Erasure.ErasureFunction]
erases_mutual [in MetaCoq.Erasure.ErasureFunction]
erases_deps_weaken [in MetaCoq.Erasure.ErasureFunction]
erases_weakeninv_env [in MetaCoq.Erasure.ErasureFunction]
erases_erase [in MetaCoq.Erasure.ErasureFunction]
erase_wellformed_fast [in MetaCoq.Erasure.ErasureFunction]
erase_global_fast_wf_glob [in MetaCoq.Erasure.ErasureFunction]
erase_global_deps_fast_spec [in MetaCoq.Erasure.ErasureFunction]
erase_global_deps_fast_spec_gen [in MetaCoq.Erasure.ErasureFunction]
erase_correct_strong [in MetaCoq.Erasure.ErasureFunction]
erase_correct_strong' [in MetaCoq.Erasure.ErasureFunction]
erase_eval_to_box_eager [in MetaCoq.Erasure.ErasureFunction]
erase_eval_to_box [in MetaCoq.Erasure.ErasureFunction]
erase_global_decls_wf_glob [in MetaCoq.Erasure.ErasureFunction]
erase_global_ind_decl_wf_glob [in MetaCoq.Erasure.ErasureFunction]
erase_global_cst_decl_wf_glob [in MetaCoq.Erasure.ErasureFunction]
erase_constant_body_correct'' [in MetaCoq.Erasure.ErasureFunction]
erase_wellformed_weaken [in MetaCoq.Erasure.ErasureFunction]
erase_wellformed [in MetaCoq.Erasure.ErasureFunction]
erase_wf_fixpoints [in MetaCoq.Erasure.ErasureFunction]
erase_global_closed [in MetaCoq.Erasure.ErasureFunction]
erase_cofix_eq [in MetaCoq.Erasure.ErasureFunction]
erase_fix_eq [in MetaCoq.Erasure.ErasureFunction]
erase_brs_eq [in MetaCoq.Erasure.ErasureFunction]
erase_global_decls_fresh [in MetaCoq.Erasure.ErasureFunction]
erase_global_declared_constructor [in MetaCoq.Erasure.ErasureFunction]
erase_mkApps [in MetaCoq.Erasure.ErasureFunction]
erase_correct [in MetaCoq.Erasure.ErasureFunction]
erase_global_includes [in MetaCoq.Erasure.ErasureFunction]
erase_constant_body_correct' [in MetaCoq.Erasure.ErasureFunction]
erase_constant_body_correct [in MetaCoq.Erasure.ErasureFunction]
erase_global_erases_deps [in MetaCoq.Erasure.ErasureFunction]
erase_global_decls_irr [in MetaCoq.Erasure.ErasureFunction]
erase_constant_body_suffix [in MetaCoq.Erasure.ErasureFunction]
erase_irrel_global_env [in MetaCoq.Erasure.ErasureFunction]
erase_to_box [in MetaCoq.Erasure.ErasureFunction]
erase_terms_eq [in MetaCoq.Erasure.ErasureFunction]
erase_irrel [in MetaCoq.Erasure.ErasureFunction]
etaExp_fixsubst [in MetaCoq.Erasure.EEtaExpandedFix]
etaExp_csubst [in MetaCoq.Erasure.EEtaExpandedFix]
etaExp_csubst' [in MetaCoq.Erasure.EEtaExpandedFix]
etaExp_csubst [in MetaCoq.Erasure.EEtaExpanded]
eta_expand_global_env_expanded [in MetaCoq.Template.EtaExpand]
eta_expand_global_decl_expanded [in MetaCoq.Template.EtaExpand]
eta_context_length [in MetaCoq.Template.EtaExpand]
eta_expand_context_sorts [in MetaCoq.Template.EtaExpand]
eta_expand_context [in MetaCoq.Template.EtaExpand]
eta_declared_constructor [in MetaCoq.Template.EtaExpand]
eta_lookup_global_error [in MetaCoq.Template.EtaExpand]
eta_lookup_global [in MetaCoq.Template.EtaExpand]
eta_expand_expanded [in MetaCoq.Template.EtaExpand]
eta_global_env [in MetaCoq.Erasure.ErasureFunction]
eta_expand_erase [in MetaCoq.Erasure.ErasureFunction]
eta_pair [in MetaCoq.SafeChecker.PCUICSafeConversion]
eta_template_global_env [in MetaCoq.PCUIC.TemplateToPCUICExpanded]
eta_global_env [in MetaCoq.PCUIC.TemplateToPCUICExpanded]
eval_tCase [in MetaCoq.PCUIC.PCUICProgress]
eval_opt_to_target [in MetaCoq.Erasure.EEtaExpandedFix]
eval_app_cong_mkApps [in MetaCoq.Erasure.EEtaExpandedFix]
eval_value_cong [in MetaCoq.Erasure.EEtaExpandedFix]
eval_app_cong_tApp' [in MetaCoq.Erasure.EEtaExpandedFix]
eval_stuck_fix_eq [in MetaCoq.Erasure.EEtaExpandedFix]
eval_etaexp [in MetaCoq.Erasure.EEtaExpandedFix]
eval_app_cong_tApp [in MetaCoq.Erasure.EEtaExpandedFix]
eval_tCase [in MetaCoq.Erasure.EArities]
eval_Const [in MetaCoq.PCUIC.PCUICWcbvEval]
eval_LetIn [in MetaCoq.PCUIC.PCUICWcbvEval]
eval_unique [in MetaCoq.PCUIC.PCUICWcbvEval]
eval_deterministic [in MetaCoq.PCUIC.PCUICWcbvEval]
eval_unique_sig [in MetaCoq.PCUIC.PCUICWcbvEval]
eval_mkApps_tCoFix [in MetaCoq.PCUIC.PCUICWcbvEval]
eval_tEvar [in MetaCoq.PCUIC.PCUICWcbvEval]
eval_tVar [in MetaCoq.PCUIC.PCUICWcbvEval]
eval_tRel [in MetaCoq.PCUIC.PCUICWcbvEval]
eval_closed [in MetaCoq.PCUIC.PCUICWcbvEval]
eval_stuck_fix [in MetaCoq.PCUIC.PCUICWcbvEval]
eval_mkApps_cong [in MetaCoq.PCUIC.PCUICWcbvEval]
eval_stuck_Fix [in MetaCoq.PCUIC.PCUICWcbvEval]
eval_mkApps_tInd [in MetaCoq.PCUIC.PCUICWcbvEval]
eval_mkApps_CoFix [in MetaCoq.PCUIC.PCUICWcbvEval]
eval_mkApps_Construct [in MetaCoq.PCUIC.PCUICWcbvEval]
eval_to_value [in MetaCoq.PCUIC.PCUICWcbvEval]
eval_mkApps_Construct_inv [in MetaCoq.Erasure.EConstructorsAsBlocks]
eval_etaexp [in MetaCoq.Erasure.EWcbvEvalEtaInd]
eval_preserve_mkApps_ind [in MetaCoq.Erasure.EWcbvEvalEtaInd]
eval_wt [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
eval_mkApps_rect [in MetaCoq.Erasure.EWcbvEvalInd]
eval_proj_eval_inv_discr [in MetaCoq.Erasure.ErasureProperties]
eval_case_eval_inv_discr [in MetaCoq.Erasure.ErasureProperties]
eval_case_eval_discr [in MetaCoq.Erasure.ErasureProperties]
eval_case_tBox_inv [in MetaCoq.Erasure.ErasureProperties]
eval_empty_brs [in MetaCoq.Erasure.ErasureProperties]
eval_mkApps_cong [in MetaCoq.Template.WcbvEval]
eval_Const [in MetaCoq.Template.WcbvEval]
eval_LetIn [in MetaCoq.Template.WcbvEval]
eval_to_stuck_fix_inv [in MetaCoq.Template.WcbvEval]
eval_atom_inj [in MetaCoq.Template.WcbvEval]
eval_to_value [in MetaCoq.Template.WcbvEval]
eval_wf [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
eval_mkApps_cong [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
eval_mkApps_fix [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
eval_mkApps_value_cong [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
eval_value_cong [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
eval_stuck_fix [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
eval_to_stuck_fix_inv [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
eval_mkApps [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
eval_tApp [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
eval_eval [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
eval_mkApps_inv [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
eval_ind_canonical [in MetaCoq.PCUIC.PCUICCanonicity]
eval_whne [in MetaCoq.PCUIC.PCUICCanonicity]
eval_box_apps [in MetaCoq.Erasure.EWcbvEval]
eval_construct_size [in MetaCoq.Erasure.EWcbvEval]
eval_mkApps_Construct_size [in MetaCoq.Erasure.EWcbvEval]
eval_mkApps_inv_size [in MetaCoq.Erasure.EWcbvEval]
eval_mkApps_Construct_block_inv [in MetaCoq.Erasure.EWcbvEval]
eval_mkApps_Construct_inv [in MetaCoq.Erasure.EWcbvEval]
eval_mkApps_inv' [in MetaCoq.Erasure.EWcbvEval]
eval_mkApps_tFix_inv_size_unguarded [in MetaCoq.Erasure.EWcbvEval]
eval_mkApps_tFix_inv_size [in MetaCoq.Erasure.EWcbvEval]
eval_wellformed [in MetaCoq.Erasure.EWcbvEval]
eval_closed [in MetaCoq.Erasure.EWcbvEval]
eval_mkApps_inv [in MetaCoq.Erasure.EWcbvEval]
eval_trans [in MetaCoq.Erasure.EWcbvEval]
eval_trans' [in MetaCoq.Erasure.EWcbvEval]
eval_deterministic_all [in MetaCoq.Erasure.EWcbvEval]
eval_deterministic [in MetaCoq.Erasure.EWcbvEval]
eval_unique [in MetaCoq.Erasure.EWcbvEval]
eval_unique_sig [in MetaCoq.Erasure.EWcbvEval]
eval_mkApps_cong [in MetaCoq.Erasure.EWcbvEval]
eval_mkApps_tBox [in MetaCoq.Erasure.EWcbvEval]
eval_mkApps_CoFix [in MetaCoq.Erasure.EWcbvEval]
eval_mkApps_Construct_block [in MetaCoq.Erasure.EWcbvEval]
eval_mkApps_Construct [in MetaCoq.Erasure.EWcbvEval]
eval_stuck_Fix [in MetaCoq.Erasure.EWcbvEval]
eval_to_mkApps_tBox_inv [in MetaCoq.Erasure.EWcbvEval]
eval_mkApps_tFix_inv [in MetaCoq.Erasure.EWcbvEval]
eval_mkApps_tCoFix [in MetaCoq.Erasure.EWcbvEval]
eval_to_value [in MetaCoq.Erasure.EWcbvEval]
eval_Construct_inv [in MetaCoq.Erasure.EWcbvEval]
eval_is_box [in MetaCoq.Erasure.EOptimizePropDiscr]
exists_neg_forall [in MetaCoq.Template.common.uGraph]
exist_irrel_eq [in MetaCoq.PCUIC.utils.PCUICPrimitive]
expanded_decl_env_irrel [in MetaCoq.Template.EtaExpand]
expanded_context_env_irrel [in MetaCoq.Template.EtaExpand]
expanded_env_irrel [in MetaCoq.Template.EtaExpand]
expanded_eta_single_tRel_app [in MetaCoq.Template.EtaExpand]
expanded_lift' [in MetaCoq.Template.EtaExpand]
expanded_lift [in MetaCoq.Template.EtaExpand]
expanded_unlift [in MetaCoq.Template.EtaExpand]
expanded_mkApps [in MetaCoq.Template.EtaExpand]
expanded_mkApps_inv [in MetaCoq.Template.EtaExpand]
expanded_tApps_inv [in MetaCoq.Template.EtaExpand]
expanded_tApp_args [in MetaCoq.Template.EtaExpand]
expanded_mkApps_tFix_inv [in MetaCoq.Template.EtaExpand]
expanded_mkApps_tFix [in MetaCoq.Template.EtaExpand]
expanded_mkApps_tConstruct [in MetaCoq.Template.EtaExpand]
expanded_fold_lambda [in MetaCoq.Template.EtaExpand]
expanded_ind [in MetaCoq.Template.EtaExpand]
expanded_global_env_isEtaExp_env [in MetaCoq.Erasure.EEtaExpandedFix]
expanded_isEtaExp [in MetaCoq.Erasure.EEtaExpandedFix]
expanded_isEtaExp_app_ [in MetaCoq.Erasure.EEtaExpandedFix]
expanded_weakening [in MetaCoq.Erasure.EEtaExpandedFix]
expanded_closed [in MetaCoq.Erasure.EEtaExpandedFix]
expanded_ind [in MetaCoq.Erasure.EEtaExpandedFix]
expanded_erases [in MetaCoq.Erasure.ErasureCorrectness]
expanded_weakening [in MetaCoq.PCUIC.PCUICEtaExpand]
expanded_subst_instance [in MetaCoq.PCUIC.PCUICEtaExpand]
expanded_let_expansion [in MetaCoq.PCUIC.PCUICEtaExpand]
expanded_subst [in MetaCoq.PCUIC.PCUICEtaExpand]
expanded_lift [in MetaCoq.PCUIC.PCUICEtaExpand]
expanded_mkApps_expanded [in MetaCoq.PCUIC.PCUICEtaExpand]
expanded_ind [in MetaCoq.PCUIC.PCUICEtaExpand]
expanded_expand_lets_program [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
expanded_global_env_expand_lets [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
expanded_smash_context [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
expanded_trans_local [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
expanded_expand_lets [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
expanded_erase_fast [in MetaCoq.Erasure.ErasureFunction]
expanded_erase_global_fast [in MetaCoq.Erasure.ErasureFunction]
expanded_erase_global [in MetaCoq.Erasure.ErasureFunction]
expanded_erase [in MetaCoq.Erasure.ErasureFunction]
expanded_weakening_global [in MetaCoq.Erasure.ErasureFunction]
expanded_eprogram_env_expanded_eprogram_cstrs [in MetaCoq.Erasure.ETransform]
expanded_erase_program [in MetaCoq.Erasure.ETransform]
expanded_mkApps_expanded [in MetaCoq.Erasure.EEtaExpanded]
expanded_global_env_isEtaExp_env [in MetaCoq.Erasure.EEtaExpanded]
expanded_isEtaExp [in MetaCoq.Erasure.EEtaExpanded]
expanded_isEtaExp_app_ [in MetaCoq.Erasure.EEtaExpanded]
expanded_ind [in MetaCoq.Erasure.EEtaExpanded]
expanded_trans_program [in MetaCoq.PCUIC.TemplateToPCUICExpanded]
expanded_trans_global_env [in MetaCoq.PCUIC.TemplateToPCUICExpanded]
expanded_trans_local [in MetaCoq.PCUIC.TemplateToPCUICExpanded]
expanded_bcontext [in MetaCoq.PCUIC.TemplateToPCUICExpanded]
expanded_context_weakening [in MetaCoq.PCUIC.TemplateToPCUICExpanded]
expanded_weakening [in MetaCoq.PCUIC.TemplateToPCUICExpanded]
expanded_inds [in MetaCoq.PCUIC.TemplateToPCUICExpanded]
expanded_context_subst [in MetaCoq.PCUIC.TemplateToPCUICExpanded]
expanded_let_expansion [in MetaCoq.PCUIC.TemplateToPCUICExpanded]
expanded_extended_subst [in MetaCoq.PCUIC.TemplateToPCUICExpanded]
expanded_context_map2_bias_left [in MetaCoq.PCUIC.TemplateToPCUICExpanded]
expand_lets_subst_comm' [in MetaCoq.PCUIC.PCUICSubstitution]
expand_lets_eq [in MetaCoq.Template.TermEquality]
expand_lets_ctx_app [in MetaCoq.PCUIC.PCUICInductives]
expand_lets_k_0 [in MetaCoq.PCUIC.PCUICInductives]
expand_lets_k_to_extended_list_k [in MetaCoq.PCUIC.PCUICInductives]
expand_lets_k_subst_comm [in MetaCoq.PCUIC.PCUICInductives]
expand_lets_ctx_tip [in MetaCoq.PCUIC.PCUICInductives]
expand_lets_ctx_snoc [in MetaCoq.PCUIC.PCUICInductives]
expand_lets_k_ctx_snoc [in MetaCoq.PCUIC.PCUICInductives]
expand_lets_ctx_lift [in MetaCoq.PCUIC.PCUICInductives]
expand_lets_lift [in MetaCoq.PCUIC.PCUICInductives]
expand_lets_app [in MetaCoq.PCUIC.PCUICInductiveInversion]
expand_lets_k_app [in MetaCoq.PCUIC.PCUICInductiveInversion]
expand_lets_subst_comm [in MetaCoq.PCUIC.PCUICSigmaCalculus]
expand_lets_ctx_assumption_context [in MetaCoq.PCUIC.PCUICSigmaCalculus]
expand_lets_assumption_context [in MetaCoq.PCUIC.PCUICSigmaCalculus]
expand_lets_tRel [in MetaCoq.PCUIC.PCUICSigmaCalculus]
expand_lets_mkApps [in MetaCoq.PCUIC.PCUICSigmaCalculus]
expand_lets_k_mkApps [in MetaCoq.PCUIC.PCUICSigmaCalculus]
expand_lets_it_mkProd_or_LetIn [in MetaCoq.PCUIC.PCUICSigmaCalculus]
expand_lets_nil [in MetaCoq.PCUIC.PCUICSigmaCalculus]
expand_lets_vdef [in MetaCoq.PCUIC.PCUICSigmaCalculus]
expand_lets_k_vdef [in MetaCoq.PCUIC.PCUICSigmaCalculus]
expand_lets_vass [in MetaCoq.PCUIC.PCUICSigmaCalculus]
expand_lets_k_vass [in MetaCoq.PCUIC.PCUICSigmaCalculus]
expand_lets_sound [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
expand_lets_expand_lets [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
expand_lets_smash_context_id [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
expand_lets_ctx_lift_context_cancel [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
expand_lets_comm [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
expand_lets_k_lift [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
expand_lets_set_binder_name [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
expand_lets_k_subst_comm [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
expand_lets_subst_comm [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
expand_lets_lift_cancel [in MetaCoq.PCUIC.PCUICSR]
expand_lets_eq_map [in MetaCoq.PCUIC.PCUICSR]
expand_lets_eq [in MetaCoq.PCUIC.PCUICSR]
expand_lets_subst_instance [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
expand_lets_ctx_nil [in MetaCoq.PCUIC.PCUICContexts]
expand_lets_k_ctx_nil [in MetaCoq.PCUIC.PCUICContexts]
expand_lets_smash_context [in MetaCoq.PCUIC.PCUICContexts]
expand_lets_k_ctx_subst_id' [in MetaCoq.PCUIC.PCUICSpine]
expand_lets_ctx_o_lets [in MetaCoq.PCUIC.PCUICSpine]
expand_lets_erasure [in MetaCoq.Erasure.Prelim]
expr_set_forall_map [in MetaCoq.PCUIC.PCUICCumulProp]
expr_gc_declared_declared [in MetaCoq.Template.common.uGraph]
extended_subst_shiftn_impl [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
extended_subst_shiftn_aboveP [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
extended_subst_shiftn [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
extended_subst_lift_context [in MetaCoq.PCUIC.PCUICInductives]
extended_subst_set_binder_name [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
extended_subst_app [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
extended_subst_to_extended_list_k [in MetaCoq.PCUIC.PCUICContexts]
extends_decls_wf [in MetaCoq.PCUIC.PCUICWeakeningEnv]
extends_lookup [in MetaCoq.PCUIC.PCUICWeakeningEnv]
extends_wf_universe [in MetaCoq.PCUIC.PCUICWeakeningEnv]
extends_trans [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
extends_trans_global_decls_acc [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
extends_lookup_projection [in MetaCoq.Erasure.EInlineProjections]
extends_decls_trans [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
extends_trans [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
extends_lookup_env [in MetaCoq.Erasure.ErasureFunction]
extends_wf_global_decl [in MetaCoq.Erasure.EWellformed]
extends_wellformed [in MetaCoq.Erasure.EWellformed]
extends_is_propositional [in MetaCoq.Erasure.EWellformed]
extends_constructor_isprop_pars_decl [in MetaCoq.Erasure.EWellformed]
extends_lookup_constructor [in MetaCoq.Erasure.EWellformed]
extends_lookup [in MetaCoq.Erasure.EWellformed]
extends_wf_glob [in MetaCoq.Erasure.EExtends]
extends_decls_trans [in MetaCoq.PCUIC.TemplateToPCUICExpanded]
extends_lookup_inductive_pars [in MetaCoq.Erasure.ERemoveParams]
extends_lookup_projection [in MetaCoq.Erasure.EGenericMapEnv]
extends_inductive_isprop_and_pars [in MetaCoq.Erasure.EOptimizePropDiscr]
extends_wf_cofixpoint [in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
extends_wf_fixpoint [in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
extends_check_recursivity_kind [in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
extends_wf_local [in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
ext_lift [in MetaCoq.Template.EtaExpand]
| 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) |