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)

U (lemma)

udecl_prop_in_var_poly [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
uip_bool [in MetaCoq.Template.utils.MCUtils]
uip_preservation [in MetaCoq.Translations.param_generous_packed]
unfold_length [in MetaCoq.Template.utils.MCList]
unfold_one_proj_None [in MetaCoq.SafeChecker.PCUICSafeConversion]
unfold_one_proj_cored [in MetaCoq.SafeChecker.PCUICSafeConversion]
unfold_one_case_None [in MetaCoq.SafeChecker.PCUICSafeConversion]
unfold_one_case_cored [in MetaCoq.SafeChecker.PCUICSafeConversion]
unfold_one_fix_None [in MetaCoq.SafeChecker.PCUICSafeConversion]
unfold_one_fix_decompose [in MetaCoq.SafeChecker.PCUICSafeConversion]
unfold_one_fix_cored [in MetaCoq.SafeChecker.PCUICSafeConversion]
unfold_one_fix_red [in MetaCoq.SafeChecker.PCUICSafeConversion]
unfold_one_fix_red_zippx [in MetaCoq.SafeChecker.PCUICSafeConversion]
unfold_one_fix_red_zipp [in MetaCoq.SafeChecker.PCUICSafeConversion]
unfold_cofix_wf [in MetaCoq.Template.TypingWf]
unfold_fix_wf [in MetaCoq.Template.TypingWf]
unfold_cofix_type [in MetaCoq.Erasure.Prelim]
unique_sorting_equality_propositional [in MetaCoq.PCUIC.PCUICElimination]
unique_sorting_equality_sprop [in MetaCoq.PCUIC.PCUICElimination]
unique_sorting_equality_sprop_r [in MetaCoq.PCUIC.PCUICElimination]
unique_sorting_equality_sprop_l [in MetaCoq.PCUIC.PCUICElimination]
unique_sorting_equality_prop [in MetaCoq.PCUIC.PCUICElimination]
unique_sorting_equality_prop_r [in MetaCoq.PCUIC.PCUICElimination]
unique_sorting_equality_prop_l [in MetaCoq.PCUIC.PCUICElimination]
UnivConstraint.compare_spec [in MetaCoq.Template.Universes]
UnivConstraint.eq_dec [in MetaCoq.Template.Universes]
UnivConstraint.lt_compat [in MetaCoq.Template.Universes]
UnivConstraint.lt_strorder [in MetaCoq.Template.Universes]
Universe.eqb_refl [in MetaCoq.Template.Universes]
Universe.make_inj [in MetaCoq.Template.Universes]
Universe.val_make [in MetaCoq.Template.Universes]
univ_is_prop_make [in MetaCoq.PCUIC.PCUICCumulProp]
univ_exprs_map_all [in MetaCoq.PCUIC.PCUICCumulProp]
univ_epxrs_elements_map [in MetaCoq.PCUIC.PCUICCumulProp]
univ_expr_set_in_elements [in MetaCoq.PCUIC.PCUICCumulProp]
untyped_substitution_red [in MetaCoq.PCUIC.PCUICSubstitution]
untyped_subslet_length [in MetaCoq.PCUIC.PCUICSubstitution]
untyped_subslet_nth_error [in MetaCoq.PCUIC.PCUICSubstitution]
untyped_subslet_projs [in MetaCoq.PCUIC.PCUICInductives]
untyped_subslet_inds [in MetaCoq.PCUIC.PCUICCumulProp]
untyped_subslet_inds [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
untyped_subslet_length [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
untyped_subslet_lift [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
untyped_subslet_ws_cumul_ctx_pb [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
untyped_subslet_ass [in MetaCoq.PCUIC.PCUICConvCumInversion]
untyped_substitution_ws_cumul_pb_subst_conv' [in MetaCoq.PCUIC.PCUICConversion]
untyped_substitution_ws_cumul_pb_subst_conv [in MetaCoq.PCUIC.PCUICConversion]
untyped_substitution_ws_cumul_pb [in MetaCoq.PCUIC.PCUICConversion]
untyped_closed_red_subst [in MetaCoq.PCUIC.PCUICConversion]
untyped_subslet_def_tip [in MetaCoq.PCUIC.PCUICConversion]
untyped_subslet_extended_subst [in MetaCoq.PCUIC.PCUICContexts]
untyped_subslet_lift [in MetaCoq.PCUIC.PCUICContexts]
untyped_subslet_eq_subst [in MetaCoq.PCUIC.PCUICSpine]
untyped_subslet_skipn [in MetaCoq.PCUIC.PCUICSpine]
Upn_subst_consn_lt [in MetaCoq.PCUIC.PCUICSigmaCalculus]
Upn_subst_consn_ge [in MetaCoq.PCUIC.PCUICSigmaCalculus]
Upn_compose [in MetaCoq.PCUIC.PCUICSigmaCalculus]
Upn_Upn [in MetaCoq.PCUIC.PCUICSigmaCalculus]
Upn_comp [in MetaCoq.PCUIC.PCUICSigmaCalculus]
Upn_S [in MetaCoq.PCUIC.PCUICSigmaCalculus]
Upn_1 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
Upn_Up [in MetaCoq.PCUIC.PCUICSigmaCalculus]
Upn_ren_r [in MetaCoq.PCUIC.PCUICSigmaCalculus]
Upn_ren_l [in MetaCoq.PCUIC.PCUICSigmaCalculus]
Upn_ren [in MetaCoq.PCUIC.PCUICSigmaCalculus]
Upn_proper [in MetaCoq.PCUIC.PCUICSigmaCalculus]
Upn_eq [in MetaCoq.PCUIC.PCUICSigmaCalculus]
Upn_1_Up [in MetaCoq.PCUIC.PCUICSigmaCalculus]
Upn_0 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
Upn_subst_instance [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
upn_subst_instance [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
Upn_ctxmap [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
upto_names_impl_leq_term [in MetaCoq.PCUIC.PCUICEquality]
upto_names_impl_eq_term [in MetaCoq.PCUIC.PCUICEquality]
upto_names_impl [in MetaCoq.PCUIC.PCUICEquality]
upto_eq_impl [in MetaCoq.PCUIC.PCUICEquality]
upto_names_eq_term [in MetaCoq.PCUIC.PCUICAlpha]
upto_names_leq_term [in MetaCoq.PCUIC.PCUICAlpha]
upto_names_eq_term_upto_univ [in MetaCoq.PCUIC.PCUICAlpha]
upto_names_eq_term_refl [in MetaCoq.PCUIC.PCUICAlpha]
upto_names_conv_context [in MetaCoq.PCUIC.PCUICAlpha]
upto_names_check_cofix [in MetaCoq.PCUIC.PCUICAlpha]
upto_names_check_fix [in MetaCoq.PCUIC.PCUICAlpha]
upto_names_destInd [in MetaCoq.PCUIC.PCUICAlpha]
Up_comp [in MetaCoq.PCUIC.PCUICSigmaCalculus]
up_ext_closed [in MetaCoq.PCUIC.PCUICSigmaCalculus]
up_up_assoc [in MetaCoq.PCUIC.PCUICSigmaCalculus]
Up_Up_assoc [in MetaCoq.PCUIC.PCUICSigmaCalculus]
up_Upn [in MetaCoq.PCUIC.PCUICSigmaCalculus]
up_Up [in MetaCoq.PCUIC.PCUICSigmaCalculus]
up_ext [in MetaCoq.PCUIC.PCUICSigmaCalculus]
up_up [in MetaCoq.PCUIC.PCUICSigmaCalculus]
up_ext_cond [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
up_0 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
Up_subst_instance [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
Up_ctxmap [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
urename_is_open_term [in MetaCoq.PCUIC.Conversion.PCUICOnFreeVarsConv]
urename_on_free_vars_shift [in MetaCoq.PCUIC.Conversion.PCUICOnFreeVarsConv]
urenaming_strengthen [in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
urenaming_context [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
urenaming_ext [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
urenaming_vdef [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
urenaming_vass [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
urenaming_impl [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
usubst_well_subst [in MetaCoq.PCUIC.PCUICSubstitution]
usubst_up_vdef [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
usubst_up_vass [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
usubst_app_up [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
usubst_app [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
usubst_Up' [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
usubst_Up [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
usubst_ext [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
usubst_on_free_vars_shift [in MetaCoq.PCUIC.Conversion.PCUICInstConv]



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)