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)

V

val [projection, in MetaCoq.Template.Universes]
val [constructor, in MetaCoq.Template.Universes]
Valid [constructor, in MetaCoq.Examples.tauto]
valid [definition, in MetaCoq.Examples.tauto]
validity [lemma, in MetaCoq.PCUIC.PCUICValidity]
Validity [section, in MetaCoq.PCUIC.PCUICValidity]
validity_wf [lemma, in MetaCoq.PCUIC.PCUICSafeLemmata]
validity_term [abbreviation, in MetaCoq.PCUIC.PCUICValidity]
validity_env [lemma, in MetaCoq.PCUIC.PCUICValidity]
validity_wf_local [lemma, in MetaCoq.PCUIC.PCUICValidity]
validpos [definition, in MetaCoq.PCUIC.Syntax.PCUICPosition]
valid_subset [lemma, in MetaCoq.Template.Universes]
valid_constraints [definition, in MetaCoq.Template.Universes]
valid_constraints0 [definition, in MetaCoq.Template.Universes]
valid_valid_gc [lemma, in MetaCoq.Template.common.uGraph]
valid_gc_constraints_aux [lemma, in MetaCoq.Template.common.uGraph]
valid_gc_constraints_ext [definition, in MetaCoq.Template.common.uGraph]
valid_gc_constraints [definition, in MetaCoq.Template.common.uGraph]
valid_gc_constraint [definition, in MetaCoq.Template.common.uGraph]
valid_constraints_empty [lemma, in MetaCoq.PCUIC.PCUICEquality]
valid_subgoal [definition, in MetaCoq.Examples.tauto]
valuation [record, in MetaCoq.Template.Universes]
valuation_poly [projection, in MetaCoq.Template.Universes]
valuation_mono [projection, in MetaCoq.Template.Universes]
valuation_labelling_eq [lemma, in MetaCoq.Template.common.uGraph]
valuation_of_labelling [definition, in MetaCoq.Template.common.uGraph]
value [inductive, in MetaCoq.PCUIC.PCUICWcbvEval]
value [inductive, in MetaCoq.Template.WcbvEval]
value [abbreviation, in MetaCoq.Erasure.EWcbvEval]
value [inductive, in MetaCoq.Erasure.EWcbvEval]
value_mkApps_inv' [lemma, in MetaCoq.PCUIC.PCUICProgress]
value_stuck_fix [lemma, in MetaCoq.PCUIC.PCUICProgress]
value_final [lemma, in MetaCoq.PCUIC.PCUICWcbvEval]
value_head_antimon [lemma, in MetaCoq.PCUIC.PCUICWcbvEval]
value_head_final [lemma, in MetaCoq.PCUIC.PCUICWcbvEval]
value_head_spec [lemma, in MetaCoq.PCUIC.PCUICWcbvEval]
value_mkApps_values [lemma, in MetaCoq.PCUIC.PCUICWcbvEval]
value_mkApps_inv [lemma, in MetaCoq.PCUIC.PCUICWcbvEval]
value_head_nApp [lemma, in MetaCoq.PCUIC.PCUICWcbvEval]
value_values_ind [lemma, in MetaCoq.PCUIC.PCUICWcbvEval]
value_app [lemma, in MetaCoq.PCUIC.PCUICWcbvEval]
value_app_nonnil [constructor, in MetaCoq.PCUIC.PCUICWcbvEval]
value_atom [constructor, in MetaCoq.PCUIC.PCUICWcbvEval]
value_head_fix [constructor, in MetaCoq.PCUIC.PCUICWcbvEval]
value_head_cofix [constructor, in MetaCoq.PCUIC.PCUICWcbvEval]
value_head_ind [constructor, in MetaCoq.PCUIC.PCUICWcbvEval]
value_head_cstr [constructor, in MetaCoq.PCUIC.PCUICWcbvEval]
value_head [inductive, in MetaCoq.PCUIC.PCUICWcbvEval]
value_final [lemma, in MetaCoq.Template.WcbvEval]
value_head_final [lemma, in MetaCoq.Template.WcbvEval]
value_head_spec [lemma, in MetaCoq.Template.WcbvEval]
value_mkApps_values [lemma, in MetaCoq.Template.WcbvEval]
value_mkApps_inv [lemma, in MetaCoq.Template.WcbvEval]
value_head_nApp [lemma, in MetaCoq.Template.WcbvEval]
value_values_ind [lemma, in MetaCoq.Template.WcbvEval]
value_app [constructor, in MetaCoq.Template.WcbvEval]
value_atom [constructor, in MetaCoq.Template.WcbvEval]
value_head_fix [constructor, in MetaCoq.Template.WcbvEval]
value_head_ind [constructor, in MetaCoq.Template.WcbvEval]
value_head_cofix [constructor, in MetaCoq.Template.WcbvEval]
value_head_cstr [constructor, in MetaCoq.Template.WcbvEval]
value_head [inductive, in MetaCoq.Template.WcbvEval]
value_mkApps_tFix [lemma, in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
value_canonical [lemma, in MetaCoq.PCUIC.PCUICCanonicity]
value_axiom_free [lemma, in MetaCoq.PCUIC.PCUICCanonicity]
value_whnf [lemma, in MetaCoq.PCUIC.PCUICCanonicity]
value_final [lemma, in MetaCoq.Erasure.EWcbvEval]
value_app_inv [lemma, in MetaCoq.Erasure.EWcbvEval]
value_head_spec' [lemma, in MetaCoq.Erasure.EWcbvEval]
value_head_final [lemma, in MetaCoq.Erasure.EWcbvEval]
value_head_spec [lemma, in MetaCoq.Erasure.EWcbvEval]
value_mkApps_values [lemma, in MetaCoq.Erasure.EWcbvEval]
value_mkApps_inv [lemma, in MetaCoq.Erasure.EWcbvEval]
value_head_nApp [lemma, in MetaCoq.Erasure.EWcbvEval]
value_values_ind [lemma, in MetaCoq.Erasure.EWcbvEval]
value_app [lemma, in MetaCoq.Erasure.EWcbvEval]
value_head [abbreviation, in MetaCoq.Erasure.EWcbvEval]
value_app_nonnil [constructor, in MetaCoq.Erasure.EWcbvEval]
value_constructor [constructor, in MetaCoq.Erasure.EWcbvEval]
value_atom [constructor, in MetaCoq.Erasure.EWcbvEval]
value_head_fix [constructor, in MetaCoq.Erasure.EWcbvEval]
value_head_cofix [constructor, in MetaCoq.Erasure.EWcbvEval]
value_head_cstr [constructor, in MetaCoq.Erasure.EWcbvEval]
value_head [inductive, in MetaCoq.Erasure.EWcbvEval]
value'':46 [binder, in MetaCoq.Template.Transform]
value':11 [binder, in MetaCoq.Template.Transform]
value':45 [binder, in MetaCoq.Template.Transform]
value:10 [binder, in MetaCoq.Template.Transform]
value:38 [binder, in MetaCoq.Template.Transform]
value:44 [binder, in MetaCoq.Template.Transform]
val_map_succ [lemma, in MetaCoq.Template.Universes]
val_succ [lemma, in MetaCoq.Template.Universes]
val_is_prop_false [lemma, in MetaCoq.Template.Universes]
val_is_sprop [lemma, in MetaCoq.Template.Universes]
val_is_prop [lemma, in MetaCoq.Template.Universes]
val_universe_sup [lemma, in MetaCoq.Template.Universes]
val_sup [lemma, in MetaCoq.Template.Universes]
val_add [lemma, in MetaCoq.Template.Universes]
val_caract [lemma, in MetaCoq.Template.Universes]
val_le_caract [lemma, in MetaCoq.Template.Universes]
val_ge_caract [lemma, in MetaCoq.Template.Universes]
val_In_max [lemma, in MetaCoq.Template.Universes]
val_In_le [lemma, in MetaCoq.Template.Universes]
val_fold_right [lemma, in MetaCoq.Template.Universes]
val_valuation_of_labelling2 [lemma, in MetaCoq.Template.common.uGraph]
val_ge_caract' [lemma, in MetaCoq.Template.common.uGraph]
val_le_caract' [lemma, in MetaCoq.Template.common.uGraph]
val_valuation_of_labelling [lemma, in MetaCoq.Template.common.uGraph]
val_valuation_of_labelling' [lemma, in MetaCoq.Template.common.uGraph]
val_labelling_of_valuation' [lemma, in MetaCoq.Template.common.uGraph]
val_labelling_of_valuation [lemma, in MetaCoq.Template.common.uGraph]
val_level_of_variable_level [lemma, in MetaCoq.Template.common.uGraph]
val:195 [binder, in MetaCoq.Erasure.Extract]
val:482 [binder, in MetaCoq.Template.Universes]
val:75 [binder, in MetaCoq.Erasure.EDeps]
Var [constructor, in MetaCoq.Examples.tauto]
var [definition, in MetaCoq.Examples.tauto]
var [constructor, in MetaCoq.Examples.add_constructor]
VariableLevel [module, in MetaCoq.Template.common.uGraph]
VariableLevelOT [module, in MetaCoq.Template.common.uGraph]
VariableLevel.compare [definition, in MetaCoq.Template.common.uGraph]
VariableLevel.compare_trans [lemma, in MetaCoq.Template.common.uGraph]
VariableLevel.compare_sym [lemma, in MetaCoq.Template.common.uGraph]
VariableLevel.compare_eq [lemma, in MetaCoq.Template.common.uGraph]
VariableLevel.compare_refl [lemma, in MetaCoq.Template.common.uGraph]
VariableLevel.compare_spec [definition, in MetaCoq.Template.common.uGraph]
VariableLevel.eq_dec [definition, in MetaCoq.Template.common.uGraph]
VariableLevel.Evaluable [instance, in MetaCoq.Template.common.uGraph]
VariableLevel.Level [constructor, in MetaCoq.Template.common.uGraph]
VariableLevel.lt [definition, in MetaCoq.Template.common.uGraph]
VariableLevel.lt_compat [definition, in MetaCoq.Template.common.uGraph]
VariableLevel.lt_trans [definition, in MetaCoq.Template.common.uGraph]
VariableLevel.lt_strorder [instance, in MetaCoq.Template.common.uGraph]
VariableLevel.t [definition, in MetaCoq.Template.common.uGraph]
VariableLevel.to_level [definition, in MetaCoq.Template.common.uGraph]
VariableLevel.to_noprop [definition, in MetaCoq.Template.common.uGraph]
VariableLevel.t_ [inductive, in MetaCoq.Template.common.uGraph]
VariableLevel.Var [constructor, in MetaCoq.Template.common.uGraph]
_ ?= _ (var_level) [notation, in MetaCoq.Template.common.uGraph]
variable_of_level [definition, in MetaCoq.Template.common.uGraph]
Variance [module, in MetaCoq.Template.Universes]
variances:640 [binder, in MetaCoq.Template.EnvironmentTyping]
variances:648 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
variance_universes_insts [lemma, in MetaCoq.PCUIC.PCUICInductiveInversion]
variance_universes_spec [lemma, in MetaCoq.SafeChecker.PCUICSafeChecker]
Variance.Covariant [constructor, in MetaCoq.Template.Universes]
Variance.Invariant [constructor, in MetaCoq.Template.Universes]
Variance.Irrelevant [constructor, in MetaCoq.Template.Universes]
Variance.t [inductive, in MetaCoq.Template.Universes]
VarRef [constructor, in MetaCoq.Template.Kernames]
var:818 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
vass [definition, in MetaCoq.Erasure.EAst]
vass_open_decl [definition, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
vdef [definition, in MetaCoq.Erasure.EAst]
view_prod_sortc [definition, in MetaCoq.PCUIC.utils.PCUICAstUtils]
view_prod_sort_other [constructor, in MetaCoq.PCUIC.utils.PCUICAstUtils]
view_prod_sort_sort [constructor, in MetaCoq.PCUIC.utils.PCUICAstUtils]
view_prod_sort_prod [constructor, in MetaCoq.PCUIC.utils.PCUICAstUtils]
view_prod_sort [inductive, in MetaCoq.PCUIC.utils.PCUICAstUtils]
view_indc [definition, in MetaCoq.PCUIC.utils.PCUICAstUtils]
view_ind_other [constructor, in MetaCoq.PCUIC.utils.PCUICAstUtils]
view_ind_tInd [constructor, in MetaCoq.PCUIC.utils.PCUICAstUtils]
view_ind [inductive, in MetaCoq.PCUIC.utils.PCUICAstUtils]
view_prodc [definition, in MetaCoq.PCUIC.utils.PCUICAstUtils]
view_prod_other [constructor, in MetaCoq.PCUIC.utils.PCUICAstUtils]
view_prod_prod [constructor, in MetaCoq.PCUIC.utils.PCUICAstUtils]
view_prod [inductive, in MetaCoq.PCUIC.utils.PCUICAstUtils]
view_sortc [definition, in MetaCoq.PCUIC.utils.PCUICAstUtils]
view_sort_other [constructor, in MetaCoq.PCUIC.utils.PCUICAstUtils]
view_sort_sort [constructor, in MetaCoq.PCUIC.utils.PCUICAstUtils]
view_sort [inductive, in MetaCoq.PCUIC.utils.PCUICAstUtils]
view_lambda_fix_app_other [lemma, in MetaCoq.PCUIC.Syntax.PCUICViews]
view_fix_lambda [lemma, in MetaCoq.PCUIC.Syntax.PCUICViews]
view_construct0_cofix [definition, in MetaCoq.PCUIC.Syntax.PCUICViews]
view_construct_cofix [definition, in MetaCoq.PCUIC.Syntax.PCUICViews]
view_lambda_fix_app_lambda_app [lemma, in MetaCoq.PCUIC.Syntax.PCUICViews]
view_lambda_fix_app_fix_app [lemma, in MetaCoq.PCUIC.Syntax.PCUICViews]
view_lambda_fix_app_lambda_app_sigma [lemma, in MetaCoq.PCUIC.Syntax.PCUICViews]
view_lambda_fix_app_fix_app_sigma [lemma, in MetaCoq.PCUIC.Syntax.PCUICViews]
view_lambda_fix_app [lemma, in MetaCoq.PCUIC.Syntax.PCUICViews]
view_other [constructor, in MetaCoq.SafeChecker.PCUICSafeReduce]
view_construct [constructor, in MetaCoq.SafeChecker.PCUICSafeReduce]
view_other [constructor, in MetaCoq.Erasure.EEtaExpanded]
view_construct [constructor, in MetaCoq.Erasure.EEtaExpanded]
vi:53 [binder, in MetaCoq.Erasure.ESpineView]
VmCast [constructor, in MetaCoq.Template.BasicAst]
vn:55 [binder, in MetaCoq.Erasure.ESpineView]
VSet [module, in MetaCoq.Template.common.uGraph]
vset:507 [binder, in MetaCoq.Template.common.uGraph]
vset:510 [binder, in MetaCoq.Template.common.uGraph]
vsub:931 [binder, in MetaCoq.Template.utils.wGraph]
vtn [abbreviation, in MetaCoq.Template.common.uGraph]
vx:1190 [binder, in MetaCoq.Template.utils.wGraph]
Vx:613 [binder, in MetaCoq.Template.utils.wGraph]
Vx:659 [binder, in MetaCoq.Template.utils.wGraph]
vy:1191 [binder, in MetaCoq.Template.utils.wGraph]
Vy:614 [binder, in MetaCoq.Template.utils.wGraph]
Vy:660 [binder, in MetaCoq.Template.utils.wGraph]
Vy:744 [binder, in MetaCoq.Template.utils.wGraph]
v'':61 [binder, in MetaCoq.Template.Transform]
v':10 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
v':10 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
v':105 [binder, in MetaCoq.Erasure.ETransform]
v':112 [binder, in MetaCoq.PCUIC.Syntax.PCUICReflect]
v':115 [binder, in MetaCoq.Erasure.ETransform]
v':119 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
v':125 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
v':126 [binder, in MetaCoq.PCUIC.PCUICConfluence]
v':1292 [binder, in MetaCoq.PCUIC.PCUICConfluence]
v':1301 [binder, in MetaCoq.PCUIC.PCUICConfluence]
v':131 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
v':132 [binder, in MetaCoq.PCUIC.PCUICNormal]
v':137 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
v':1387 [binder, in MetaCoq.Erasure.ErasureFunction]
v':139 [binder, in MetaCoq.PCUIC.PCUICNormal]
v':1409 [binder, in MetaCoq.Erasure.ErasureFunction]
v':146 [binder, in MetaCoq.PCUIC.PCUICCumulativity]
v':147 [binder, in MetaCoq.PCUIC.PCUICConfluence]
v':148 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
v':149 [binder, in MetaCoq.PCUIC.PCUICNormal]
v':152 [binder, in MetaCoq.PCUIC.PCUICConfluence]
v':153 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
v':155 [binder, in MetaCoq.PCUIC.PCUICConfluence]
v':159 [binder, in MetaCoq.PCUIC.PCUICArities]
v':162 [binder, in MetaCoq.PCUIC.PCUICNormal]
v':162 [binder, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
V':177 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
v':18 [binder, in MetaCoq.PCUIC.PCUICTransform]
v':18 [binder, in MetaCoq.PCUIC.PCUICSN]
v':184 [binder, in MetaCoq.Erasure.EArities]
v':185 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
v':190 [binder, in MetaCoq.Erasure.EArities]
v':190 [binder, in MetaCoq.PCUIC.PCUICConfluence]
v':195 [binder, in MetaCoq.PCUIC.PCUICConfluence]
v':197 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
v':20 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
v':200 [binder, in MetaCoq.PCUIC.PCUICConfluence]
v':203 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
v':209 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
v':21 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
v':214 [binder, in MetaCoq.PCUIC.PCUICConfluence]
v':22 [binder, in MetaCoq.Template.Transform]
v':220 [binder, in MetaCoq.PCUIC.PCUICElimination]
v':226 [binder, in MetaCoq.PCUIC.PCUICElimination]
v':232 [binder, in MetaCoq.PCUIC.PCUICElimination]
v':238 [binder, in MetaCoq.PCUIC.PCUICElimination]
v':240 [binder, in MetaCoq.Template.Universes]
v':244 [binder, in MetaCoq.Template.Universes]
v':244 [binder, in MetaCoq.PCUIC.PCUICElimination]
v':248 [binder, in MetaCoq.PCUIC.PCUICConfluence]
v':253 [binder, in MetaCoq.PCUIC.PCUICConfluence]
v':258 [binder, in MetaCoq.PCUIC.PCUICConfluence]
v':272 [binder, in MetaCoq.PCUIC.PCUICConfluence]
v':288 [binder, in MetaCoq.Erasure.EWcbvEval]
v':29 [binder, in MetaCoq.PCUIC.PCUICSN]
v':29 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
v':297 [binder, in MetaCoq.Erasure.EWcbvEval]
v':300 [binder, in MetaCoq.Erasure.EWcbvEval]
v':313 [binder, in MetaCoq.PCUIC.PCUICConfluence]
v':32 [binder, in MetaCoq.Erasure.ETransform]
v':356 [binder, in MetaCoq.PCUIC.PCUICConfluence]
v':37 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
v':379 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
v':384 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
v':39 [binder, in MetaCoq.PCUIC.PCUICCumulativity]
v':399 [binder, in MetaCoq.PCUIC.PCUICConfluence]
v':4 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
v':420 [binder, in MetaCoq.PCUIC.PCUICConfluence]
v':47 [binder, in MetaCoq.Erasure.ETransform]
v':471 [binder, in MetaCoq.PCUIC.PCUICConfluence]
v':472 [binder, in MetaCoq.PCUIC.PCUICProgress]
v':480 [binder, in MetaCoq.PCUIC.PCUICProgress]
v':488 [binder, in MetaCoq.PCUIC.PCUICProgress]
v':488 [binder, in MetaCoq.Template.Universes]
v':492 [binder, in MetaCoq.PCUIC.PCUICConfluence]
v':53 [binder, in MetaCoq.PCUIC.PCUICSN]
v':541 [binder, in MetaCoq.PCUIC.PCUICConfluence]
v':551 [binder, in MetaCoq.PCUIC.PCUICConfluence]
v':572 [binder, in MetaCoq.PCUIC.PCUICConfluence]
v':59 [binder, in MetaCoq.PCUIC.PCUICConvCumInversion]
v':59 [binder, in MetaCoq.Template.Transform]
v':6 [binder, in MetaCoq.PCUIC.PCUICTransform]
v':60 [binder, in MetaCoq.Erasure.ETransform]
v':628 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
v':635 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
v':71 [binder, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
v':71 [binder, in MetaCoq.Erasure.ETransform]
v':8 [binder, in MetaCoq.Erasure.ErasureCorrectness]
v':81 [binder, in MetaCoq.Erasure.ETransform]
v':93 [binder, in MetaCoq.Erasure.ETransform]
v':959 [binder, in MetaCoq.Erasure.ErasureFunction]
v':97 [binder, in MetaCoq.PCUIC.PCUICConvCumInversion]
v':986 [binder, in MetaCoq.Erasure.ErasureFunction]
v1:1001 [binder, in MetaCoq.Template.utils.wGraph]
v1:1064 [binder, in MetaCoq.Template.utils.wGraph]
v1:178 [binder, in MetaCoq.PCUIC.PCUICSafeLemmata]
v1:2799 [binder, in MetaCoq.Translations.MiniHoTT]
v1:2807 [binder, in MetaCoq.Translations.MiniHoTT_paths]
v1:2811 [binder, in MetaCoq.Translations.MiniHoTT]
v1:2819 [binder, in MetaCoq.Translations.MiniHoTT_paths]
v1:538 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
v1:843 [binder, in MetaCoq.PCUIC.PCUICReduction]
v2:1002 [binder, in MetaCoq.Template.utils.wGraph]
v2:1065 [binder, in MetaCoq.Template.utils.wGraph]
v2:179 [binder, in MetaCoq.PCUIC.PCUICSafeLemmata]
v2:2802 [binder, in MetaCoq.Translations.MiniHoTT]
v2:2810 [binder, in MetaCoq.Translations.MiniHoTT_paths]
v2:2813 [binder, in MetaCoq.Translations.MiniHoTT]
v2:2821 [binder, in MetaCoq.Translations.MiniHoTT_paths]
v2:540 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
v2:844 [binder, in MetaCoq.PCUIC.PCUICReduction]
v:1 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
v:10 [binder, in MetaCoq.PCUIC.PCUICEquality]
v:100 [binder, in MetaCoq.Template.EtaExpand]
v:100 [binder, in MetaCoq.SafeChecker.PCUICErrors]
v:101 [binder, in MetaCoq.Template.common.uGraph]
v:104 [binder, in MetaCoq.Erasure.ETransform]
v:1056 [binder, in MetaCoq.Template.utils.All_Forall]
v:106 [binder, in MetaCoq.PCUIC.Syntax.PCUICReflect]
v:107 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
v:107 [binder, in MetaCoq.PCUIC.PCUICAst]
v:1071 [binder, in MetaCoq.Template.utils.wGraph]
v:108 [binder, in MetaCoq.Template.common.uGraph]
v:108 [binder, in MetaCoq.PCUIC.PCUICAlpha]
v:108 [binder, in MetaCoq.Erasure.EEtaExpanded]
v:1085 [binder, in MetaCoq.Template.utils.wGraph]
v:109 [binder, in MetaCoq.PCUIC.PCUICNormal]
v:11 [binder, in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
v:11 [binder, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
v:110 [binder, in MetaCoq.Erasure.EEtaExpanded]
v:111 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
v:113 [binder, in MetaCoq.PCUIC.PCUICAlpha]
v:113 [binder, in MetaCoq.Erasure.EEtaExpanded]
v:114 [binder, in MetaCoq.Erasure.ETransform]
v:117 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
v:118 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
v:1188 [binder, in MetaCoq.Template.utils.wGraph]
v:119 [binder, in MetaCoq.Template.common.uGraph]
v:1195 [binder, in MetaCoq.PCUIC.PCUICReduction]
v:12 [binder, in MetaCoq.Template.TermEquality]
v:120 [binder, in MetaCoq.SafeChecker.PCUICErrors]
v:120 [binder, in MetaCoq.Erasure.ERemoveParams]
v:122 [binder, in MetaCoq.Erasure.ERemoveParams]
v:1228 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
v:123 [binder, in MetaCoq.PCUIC.PCUICSafeLemmata]
v:123 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
v:1231 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
v:125 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
v:1261 [binder, in MetaCoq.Translations.MiniHoTT]
v:1262 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
v:1266 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
v:1269 [binder, in MetaCoq.Translations.MiniHoTT_paths]
v:127 [binder, in MetaCoq.Erasure.EConstructorsAsBlocks]
v:127 [binder, in MetaCoq.Template.common.uGraph]
v:128 [binder, in MetaCoq.Template.Universes]
v:129 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
v:1291 [binder, in MetaCoq.PCUIC.PCUICConfluence]
v:13 [binder, in MetaCoq.Template.Universes]
v:13 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
v:13 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
v:130 [binder, in MetaCoq.PCUIC.PCUICCumulativity]
v:130 [binder, in MetaCoq.Erasure.EInlineProjections]
v:130 [binder, in MetaCoq.PCUIC.PCUICNormal]
v:1300 [binder, in MetaCoq.PCUIC.PCUICConfluence]
v:131 [binder, in MetaCoq.Template.Universes]
v:131 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
v:1312 [binder, in MetaCoq.Erasure.ErasureFunction]
v:1320 [binder, in MetaCoq.Erasure.ErasureFunction]
v:133 [binder, in MetaCoq.Template.Universes]
v:1337 [binder, in MetaCoq.Erasure.ErasureFunction]
v:135 [binder, in MetaCoq.Template.Universes]
v:135 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
v:136 [binder, in MetaCoq.PCUIC.PCUICCumulativity]
v:137 [binder, in MetaCoq.Template.Universes]
v:137 [binder, in MetaCoq.PCUIC.PCUICNormal]
v:1373 [binder, in MetaCoq.Erasure.ErasureFunction]
v:139 [binder, in MetaCoq.Template.Universes]
v:1395 [binder, in MetaCoq.Erasure.ErasureFunction]
v:14 [binder, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
v:1425 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
v:145 [binder, in MetaCoq.PCUIC.PCUICCumulativity]
v:145 [binder, in MetaCoq.Erasure.EOptimizePropDiscr]
v:146 [binder, in MetaCoq.PCUIC.PCUICConfluence]
v:147 [binder, in MetaCoq.PCUIC.PCUICNormal]
v:147 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
v:148 [binder, in MetaCoq.Template.Universes]
V:151 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
v:152 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
v:1523 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
v:1529 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
v:155 [binder, in MetaCoq.Template.Universes]
v:157 [binder, in MetaCoq.Template.Universes]
v:158 [binder, in MetaCoq.PCUIC.PCUICArities]
v:16 [binder, in MetaCoq.PCUIC.PCUICCumulativity]
v:16 [binder, in MetaCoq.PCUIC.PCUICEquality]
v:16 [binder, in MetaCoq.PCUIC.PCUICSN]
v:160 [binder, in MetaCoq.Template.Universes]
v:160 [binder, in MetaCoq.PCUIC.PCUICNormal]
v:161 [binder, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
v:161 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
v:162 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
v:164 [binder, in MetaCoq.Template.Universes]
v:166 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
v:167 [binder, in MetaCoq.Template.EtaExpand]
v:167 [binder, in MetaCoq.Template.Universes]
v:169 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
v:17 [binder, in MetaCoq.PCUIC.PCUICTransform]
v:17 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
v:17 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
v:17 [binder, in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
v:173 [binder, in MetaCoq.Examples.tauto]
v:174 [binder, in MetaCoq.Template.Universes]
v:176 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
v:1763 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
v:177 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
v:1782 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
v:1787 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
v:179 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
v:1793 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
v:18 [binder, in MetaCoq.Template.Normal]
v:18 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
v:181 [binder, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
v:182 [binder, in MetaCoq.Template.Universes]
v:182 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
v:183 [binder, in MetaCoq.Erasure.EArities]
v:1849 [binder, in MetaCoq.Template.utils.All_Forall]
v:186 [binder, in MetaCoq.Template.Universes]
v:186 [binder, in MetaCoq.Template.Ast]
v:186 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
v:186 [binder, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
v:189 [binder, in MetaCoq.Erasure.EArities]
v:19 [binder, in MetaCoq.PCUIC.PCUICCumulativity]
v:19 [binder, in MetaCoq.Template.Transform]
v:190 [binder, in MetaCoq.Template.Universes]
v:191 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
v:193 [binder, in MetaCoq.Template.Universes]
v:1953 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
v:2 [binder, in MetaCoq.PCUIC.PCUICTransform]
v:2 [binder, in MetaCoq.PCUIC.Syntax.PCUICReflect]
v:20 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
v:202 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
v:207 [binder, in MetaCoq.Template.TermEquality]
v:2079 [binder, in MetaCoq.Translations.MiniHoTT]
v:208 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
v:2087 [binder, in MetaCoq.Translations.MiniHoTT]
v:2087 [binder, in MetaCoq.Translations.MiniHoTT_paths]
v:2095 [binder, in MetaCoq.Translations.MiniHoTT]
v:2095 [binder, in MetaCoq.Translations.MiniHoTT_paths]
v:21 [binder, in MetaCoq.Template.Normal]
v:21 [binder, in MetaCoq.PCUIC.PCUICSN]
v:21 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
v:21 [binder, in MetaCoq.Template.AstUtils]
v:2102 [binder, in MetaCoq.Translations.MiniHoTT]
v:2103 [binder, in MetaCoq.Translations.MiniHoTT_paths]
v:2109 [binder, in MetaCoq.Translations.MiniHoTT]
v:2110 [binder, in MetaCoq.Translations.MiniHoTT_paths]
v:2117 [binder, in MetaCoq.Translations.MiniHoTT]
v:2117 [binder, in MetaCoq.Translations.MiniHoTT_paths]
v:2125 [binder, in MetaCoq.Translations.MiniHoTT]
v:2125 [binder, in MetaCoq.Translations.MiniHoTT_paths]
v:213 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
v:213 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
v:2132 [binder, in MetaCoq.Translations.MiniHoTT]
v:2133 [binder, in MetaCoq.Translations.MiniHoTT_paths]
v:2139 [binder, in MetaCoq.Translations.MiniHoTT]
v:2140 [binder, in MetaCoq.Translations.MiniHoTT_paths]
v:2146 [binder, in MetaCoq.Translations.MiniHoTT]
v:2147 [binder, in MetaCoq.Translations.MiniHoTT_paths]
v:215 [binder, in MetaCoq.PCUIC.PCUICSafeLemmata]
v:2153 [binder, in MetaCoq.Translations.MiniHoTT]
v:2154 [binder, in MetaCoq.Translations.MiniHoTT_paths]
v:216 [binder, in MetaCoq.Erasure.EArities]
v:2160 [binder, in MetaCoq.Translations.MiniHoTT]
v:2161 [binder, in MetaCoq.Translations.MiniHoTT_paths]
v:2168 [binder, in MetaCoq.Translations.MiniHoTT_paths]
v:218 [binder, in MetaCoq.PCUIC.PCUICSafeLemmata]
v:218 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
v:219 [binder, in MetaCoq.PCUIC.PCUICElimination]
v:219 [binder, in MetaCoq.Erasure.EArities]
v:22 [binder, in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
v:22 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
v:222 [binder, in MetaCoq.PCUIC.PCUICSafeLemmata]
v:222 [binder, in MetaCoq.Erasure.EArities]
v:222 [binder, in MetaCoq.PCUIC.PCUICAlpha]
v:225 [binder, in MetaCoq.PCUIC.PCUICElimination]
v:225 [binder, in MetaCoq.PCUIC.PCUICSafeLemmata]
v:225 [binder, in MetaCoq.SafeChecker.PCUICWfEnv]
v:226 [binder, in MetaCoq.PCUIC.PCUICNormal]
v:226 [binder, in MetaCoq.PCUIC.PCUICAlpha]
v:228 [binder, in MetaCoq.PCUIC.PCUICSafeLemmata]
v:228 [binder, in MetaCoq.PCUIC.PCUICNormal]
v:23 [binder, in MetaCoq.Translations.param_original]
v:230 [binder, in MetaCoq.Template.common.uGraph]
v:230 [binder, in MetaCoq.Erasure.EWcbvEval]
v:231 [binder, in MetaCoq.PCUIC.PCUICElimination]
v:235 [binder, in MetaCoq.Erasure.EWcbvEval]
v:236 [binder, in MetaCoq.PCUIC.PCUICNormal]
v:237 [binder, in MetaCoq.PCUIC.PCUICElimination]
v:239 [binder, in MetaCoq.Template.Universes]
v:24 [binder, in MetaCoq.PCUIC.PCUICSN]
v:24 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
v:240 [binder, in MetaCoq.PCUIC.PCUICNormal]
v:241 [binder, in MetaCoq.Template.common.uGraph]
v:243 [binder, in MetaCoq.Template.Universes]
v:243 [binder, in MetaCoq.PCUIC.PCUICElimination]
v:246 [binder, in MetaCoq.Template.Environment]
v:248 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
v:249 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
v:249 [binder, in MetaCoq.Template.Environment]
v:249 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
v:25 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
v:25 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
v:256 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
v:256 [binder, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
v:259 [binder, in MetaCoq.PCUIC.PCUICAlpha]
v:262 [binder, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
v:2661 [binder, in MetaCoq.Translations.MiniHoTT]
v:2667 [binder, in MetaCoq.Translations.MiniHoTT]
v:2669 [binder, in MetaCoq.Translations.MiniHoTT_paths]
v:2673 [binder, in MetaCoq.Translations.MiniHoTT]
v:2675 [binder, in MetaCoq.Translations.MiniHoTT_paths]
v:2681 [binder, in MetaCoq.Translations.MiniHoTT_paths]
v:269 [binder, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
v:27 [binder, in MetaCoq.Template.Normal]
v:27 [binder, in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
v:2701 [binder, in MetaCoq.Translations.MiniHoTT]
v:2706 [binder, in MetaCoq.Translations.MiniHoTT]
v:2709 [binder, in MetaCoq.Translations.MiniHoTT_paths]
v:271 [binder, in MetaCoq.PCUIC.PCUICAlpha]
v:2712 [binder, in MetaCoq.Translations.MiniHoTT]
v:2714 [binder, in MetaCoq.Translations.MiniHoTT_paths]
v:2718 [binder, in MetaCoq.Translations.MiniHoTT]
v:2720 [binder, in MetaCoq.Translations.MiniHoTT_paths]
v:2725 [binder, in MetaCoq.Translations.MiniHoTT]
v:2726 [binder, in MetaCoq.Translations.MiniHoTT_paths]
v:2730 [binder, in MetaCoq.Translations.MiniHoTT]
v:2733 [binder, in MetaCoq.Translations.MiniHoTT_paths]
v:2738 [binder, in MetaCoq.Translations.MiniHoTT]
v:2738 [binder, in MetaCoq.Translations.MiniHoTT_paths]
v:2744 [binder, in MetaCoq.Translations.MiniHoTT]
v:2746 [binder, in MetaCoq.Translations.MiniHoTT_paths]
v:2750 [binder, in MetaCoq.Translations.MiniHoTT]
v:2752 [binder, in MetaCoq.Translations.MiniHoTT_paths]
v:2757 [binder, in MetaCoq.Translations.MiniHoTT]
v:2758 [binder, in MetaCoq.Translations.MiniHoTT_paths]
v:2762 [binder, in MetaCoq.Translations.MiniHoTT]
v:2765 [binder, in MetaCoq.Translations.MiniHoTT_paths]
v:277 [binder, in MetaCoq.PCUIC.PCUICAlpha]
v:2770 [binder, in MetaCoq.Translations.MiniHoTT]
v:2770 [binder, in MetaCoq.Translations.MiniHoTT_paths]
v:2776 [binder, in MetaCoq.Translations.MiniHoTT]
v:2778 [binder, in MetaCoq.Translations.MiniHoTT_paths]
v:2781 [binder, in MetaCoq.Translations.MiniHoTT]
v:2784 [binder, in MetaCoq.Translations.MiniHoTT_paths]
v:2785 [binder, in MetaCoq.Translations.MiniHoTT]
v:2789 [binder, in MetaCoq.Translations.MiniHoTT_paths]
v:279 [binder, in MetaCoq.Template.common.uGraph]
v:2790 [binder, in MetaCoq.Translations.MiniHoTT]
v:2793 [binder, in MetaCoq.Translations.MiniHoTT_paths]
v:2798 [binder, in MetaCoq.Translations.MiniHoTT_paths]
v:28 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
v:28 [binder, in MetaCoq.PCUIC.PCUICSN]
v:28 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
v:281 [binder, in MetaCoq.Template.common.uGraph]
v:282 [binder, in MetaCoq.PCUIC.PCUICAlpha]
v:2822 [binder, in MetaCoq.Translations.MiniHoTT]
v:2829 [binder, in MetaCoq.Translations.MiniHoTT]
v:283 [binder, in MetaCoq.Template.common.uGraph]
v:2830 [binder, in MetaCoq.Translations.MiniHoTT_paths]
v:2837 [binder, in MetaCoq.Translations.MiniHoTT_paths]
v:284 [binder, in MetaCoq.Template.Environment]
v:2861 [binder, in MetaCoq.Translations.MiniHoTT]
v:2869 [binder, in MetaCoq.Translations.MiniHoTT_paths]
v:287 [binder, in MetaCoq.Template.Universes]
v:287 [binder, in MetaCoq.Template.Environment]
v:287 [binder, in MetaCoq.Erasure.EWcbvEval]
v:2870 [binder, in MetaCoq.Translations.MiniHoTT]
v:2878 [binder, in MetaCoq.Translations.MiniHoTT_paths]
v:29 [binder, in MetaCoq.PCUIC.PCUICNormal]
v:29 [binder, in MetaCoq.Template.common.uGraph]
v:29 [binder, in MetaCoq.PCUIC.PCUICEquality]
v:290 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
v:291 [binder, in MetaCoq.Template.Environment]
v:292 [binder, in MetaCoq.Erasure.EWcbvEval]
v:2928 [binder, in MetaCoq.Translations.MiniHoTT]
v:2936 [binder, in MetaCoq.Translations.MiniHoTT_paths]
v:295 [binder, in MetaCoq.PCUIC.PCUICConversion]
v:296 [binder, in MetaCoq.Erasure.EWcbvEval]
v:297 [binder, in MetaCoq.Template.Environment]
v:298 [binder, in MetaCoq.Template.Universes]
v:299 [binder, in MetaCoq.Erasure.EWcbvEval]
v:3 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
v:3 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
v:300 [binder, in MetaCoq.PCUIC.PCUICConversion]
v:301 [binder, in MetaCoq.Template.Universes]
v:303 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
v:305 [binder, in MetaCoq.PCUIC.PCUICConversion]
v:306 [binder, in MetaCoq.Template.Universes]
v:307 [binder, in MetaCoq.PCUIC.PCUICConfluence]
v:307 [binder, in MetaCoq.PCUIC.PCUICConversion]
v:309 [binder, in MetaCoq.Erasure.EWcbvEval]
v:31 [binder, in MetaCoq.SafeChecker.PCUICWfReduction]
v:31 [binder, in MetaCoq.Erasure.ETransform]
v:310 [binder, in MetaCoq.Template.Universes]
v:311 [binder, in MetaCoq.Template.WcbvEval]
v:311 [binder, in MetaCoq.PCUIC.PCUICConversion]
v:312 [binder, in MetaCoq.Template.Universes]
v:312 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
v:314 [binder, in MetaCoq.Template.Universes]
v:315 [binder, in MetaCoq.Template.WcbvEval]
v:315 [binder, in MetaCoq.Erasure.EWcbvEval]
v:316 [binder, in MetaCoq.Template.Universes]
v:318 [binder, in MetaCoq.Template.Universes]
v:32 [binder, in MetaCoq.Template.TermEquality]
v:32 [binder, in MetaCoq.PCUIC.PCUICNormal]
v:320 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
v:321 [binder, in MetaCoq.Template.Universes]
v:326 [binder, in MetaCoq.Template.Universes]
v:33 [binder, in MetaCoq.SafeChecker.PCUICWfReduction]
v:331 [binder, in MetaCoq.Erasure.EArities]
v:331 [binder, in MetaCoq.Erasure.ERemoveParams]
v:334 [binder, in MetaCoq.PCUIC.PCUICEquality]
v:34 [binder, in MetaCoq.Template.Normal]
v:340 [binder, in MetaCoq.Template.common.uGraph]
v:343 [binder, in MetaCoq.PCUIC.PCUICConversion]
v:344 [binder, in MetaCoq.Template.common.uGraph]
v:35 [binder, in MetaCoq.PCUIC.PCUICNormal]
v:35 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
v:354 [binder, in MetaCoq.PCUIC.PCUICConfluence]
v:356 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
v:36 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
v:365 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
v:367 [binder, in MetaCoq.Erasure.EWcbvEval]
v:369 [binder, in MetaCoq.Template.common.uGraph]
v:37 [binder, in MetaCoq.Translations.param_binary]
v:370 [binder, in MetaCoq.Template.common.uGraph]
v:371 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
v:371 [binder, in MetaCoq.Template.common.uGraph]
v:371 [binder, in MetaCoq.Translations.MiniHoTT]
v:372 [binder, in MetaCoq.Template.common.uGraph]
v:374 [binder, in MetaCoq.Erasure.ERemoveParams]
v:378 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
v:378 [binder, in MetaCoq.Translations.MiniHoTT]
v:378 [binder, in MetaCoq.Erasure.EWcbvEval]
v:379 [binder, in MetaCoq.Translations.MiniHoTT_paths]
v:38 [binder, in MetaCoq.PCUIC.PCUICCumulativity]
v:38 [binder, in MetaCoq.Erasure.ErasureCorrectness]
v:38 [binder, in MetaCoq.PCUIC.PCUICNormal]
v:383 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
v:384 [binder, in MetaCoq.PCUIC.PCUICReduction]
v:385 [binder, in MetaCoq.Translations.MiniHoTT]
v:386 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
v:386 [binder, in MetaCoq.Translations.MiniHoTT_paths]
v:386 [binder, in MetaCoq.Erasure.EWcbvEval]
v:389 [binder, in MetaCoq.PCUIC.PCUICReduction]
v:392 [binder, in MetaCoq.Translations.MiniHoTT]
v:393 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
v:393 [binder, in MetaCoq.Translations.MiniHoTT_paths]
v:394 [binder, in MetaCoq.PCUIC.PCUICEquality]
v:397 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
v:398 [binder, in MetaCoq.PCUIC.PCUICEquality]
v:399 [binder, in MetaCoq.Translations.MiniHoTT]
v:4 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
v:4 [binder, in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
v:40 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
v:400 [binder, in MetaCoq.Translations.MiniHoTT_paths]
v:403 [binder, in MetaCoq.Erasure.EWcbvEval]
v:407 [binder, in MetaCoq.Translations.MiniHoTT]
v:407 [binder, in MetaCoq.Translations.MiniHoTT_paths]
v:41 [binder, in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
v:41 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
v:412 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
v:415 [binder, in MetaCoq.Translations.MiniHoTT]
v:415 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
v:415 [binder, in MetaCoq.Translations.MiniHoTT_paths]
v:417 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
v:418 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
v:421 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
v:423 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
v:423 [binder, in MetaCoq.Translations.MiniHoTT]
v:423 [binder, in MetaCoq.Translations.MiniHoTT_paths]
v:425 [binder, in MetaCoq.Erasure.EWcbvEval]
v:429 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
v:43 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
v:431 [binder, in MetaCoq.Translations.MiniHoTT_paths]
v:437 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
v:439 [binder, in MetaCoq.Erasure.EWcbvEval]
v:44 [binder, in MetaCoq.PCUIC.PCUICNormal]
v:44 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
v:44 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
v:442 [binder, in MetaCoq.Template.common.uGraph]
v:444 [binder, in MetaCoq.Template.common.uGraph]
v:446 [binder, in MetaCoq.PCUIC.PCUICEquality]
v:449 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
v:45 [binder, in MetaCoq.PCUIC.PCUICSN]
v:451 [binder, in MetaCoq.PCUIC.PCUICEquality]
v:452 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
v:452 [binder, in MetaCoq.PCUIC.PCUICConversion]
v:46 [binder, in MetaCoq.PCUIC.PCUICSafeLemmata]
v:46 [binder, in MetaCoq.Erasure.ETransform]
v:460 [binder, in MetaCoq.PCUIC.PCUICProgress]
v:460 [binder, in MetaCoq.PCUIC.PCUICEquality]
v:463 [binder, in MetaCoq.PCUIC.PCUICProgress]
v:466 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
v:468 [binder, in MetaCoq.Template.Universes]
v:468 [binder, in MetaCoq.PCUIC.PCUICEquality]
v:47 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
v:47 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
v:470 [binder, in MetaCoq.Template.Typing]
v:473 [binder, in MetaCoq.Template.Typing]
v:476 [binder, in MetaCoq.Template.Universes]
v:477 [binder, in MetaCoq.Template.Universes]
v:479 [binder, in MetaCoq.PCUIC.PCUICProgress]
v:48 [binder, in MetaCoq.PCUIC.PCUICSafeLemmata]
v:482 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
v:484 [binder, in MetaCoq.Template.Universes]
v:487 [binder, in MetaCoq.PCUIC.PCUICProgress]
v:487 [binder, in MetaCoq.Template.Universes]
v:489 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
v:489 [binder, in MetaCoq.Examples.tauto]
v:49 [binder, in MetaCoq.Template.EnvMap]
v:491 [binder, in MetaCoq.Examples.tauto]
v:494 [binder, in MetaCoq.PCUIC.PCUICSpine]
v:499 [binder, in MetaCoq.Template.Universes]
v:5 [binder, in MetaCoq.PCUIC.PCUICTransform]
v:50 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
v:506 [binder, in MetaCoq.Examples.tauto]
v:508 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
v:51 [binder, in MetaCoq.PCUIC.PCUICSN]
v:512 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
v:515 [binder, in MetaCoq.Template.common.uGraph]
v:517 [binder, in MetaCoq.Template.EnvironmentTyping]
V:518 [binder, in MetaCoq.PCUIC.PCUICSR]
v:519 [binder, in MetaCoq.Template.utils.MCList]
v:52 [binder, in MetaCoq.Erasure.ESpineView]
v:52 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
v:521 [binder, in MetaCoq.Template.Universes]
v:523 [binder, in MetaCoq.Template.utils.MCList]
V:525 [binder, in MetaCoq.PCUIC.PCUICSR]
v:526 [binder, in MetaCoq.Template.EnvironmentTyping]
v:527 [binder, in MetaCoq.PCUIC.PCUICInductives]
v:528 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
v:53 [binder, in MetaCoq.Template.EnvMap]
v:53 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
V:532 [binder, in MetaCoq.PCUIC.PCUICSR]
v:538 [binder, in MetaCoq.Template.EnvironmentTyping]
V:539 [binder, in MetaCoq.PCUIC.PCUICSR]
v:540 [binder, in MetaCoq.PCUIC.PCUICConfluence]
v:542 [binder, in MetaCoq.Template.Universes]
v:543 [binder, in MetaCoq.Template.EnvironmentTyping]
v:549 [binder, in MetaCoq.PCUIC.PCUICConfluence]
v:55 [binder, in MetaCoq.PCUIC.PCUICSafeLemmata]
v:56 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
v:561 [binder, in MetaCoq.PCUIC.PCUICEquality]
v:563 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
V:565 [binder, in MetaCoq.PCUIC.PCUICConfluence]
v:566 [binder, in MetaCoq.PCUIC.PCUICEquality]
v:566 [binder, in MetaCoq.PCUIC.PCUICConversion]
v:57 [binder, in MetaCoq.Template.Normal]
v:57 [binder, in MetaCoq.PCUIC.PCUICNormal]
v:57 [binder, in MetaCoq.Template.EnvMap]
v:570 [binder, in MetaCoq.Template.EnvironmentTyping]
v:570 [binder, in MetaCoq.PCUIC.PCUICConfluence]
v:572 [binder, in MetaCoq.PCUIC.PCUICEquality]
v:572 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
v:573 [binder, in MetaCoq.Template.common.uGraph]
v:574 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
v:578 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
v:58 [binder, in MetaCoq.Erasure.EDeps]
v:58 [binder, in MetaCoq.PCUIC.PCUICConvCumInversion]
v:58 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
v:58 [binder, in MetaCoq.Template.Transform]
v:580 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
v:588 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
v:59 [binder, in MetaCoq.Template.utils.ReflectEq]
v:59 [binder, in MetaCoq.PCUIC.PCUICSN]
v:59 [binder, in MetaCoq.Erasure.ETransform]
v:6 [binder, in MetaCoq.Erasure.ErasureCorrectness]
v:6 [binder, in MetaCoq.Template.TermEquality]
v:6 [binder, in MetaCoq.Template.TemplateProgram]
v:6 [binder, in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
v:6 [binder, in MetaCoq.PCUIC.PCUICConvCumInversion]
v:60 [binder, in MetaCoq.Template.Normal]
v:605 [binder, in MetaCoq.Template.common.uGraph]
v:61 [binder, in MetaCoq.PCUIC.PCUICSafeLemmata]
v:61 [binder, in MetaCoq.Template.EnvMap]
v:618 [binder, in MetaCoq.Template.utils.wGraph]
v:62 [binder, in MetaCoq.PCUIC.PCUICCumulativity]
v:62 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
v:62 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
v:620 [binder, in MetaCoq.PCUIC.PCUICEquality]
v:621 [binder, in MetaCoq.Template.utils.wGraph]
v:624 [binder, in MetaCoq.Template.utils.wGraph]
v:626 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
v:627 [binder, in MetaCoq.Template.utils.wGraph]
v:63 [binder, in MetaCoq.Template.Universes]
v:63 [binder, in MetaCoq.PCUIC.PCUICSN]
v:631 [binder, in MetaCoq.Template.utils.wGraph]
v:631 [binder, in MetaCoq.PCUIC.PCUICConversion]
v:633 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
v:633 [binder, in MetaCoq.PCUIC.PCUICConversion]
v:635 [binder, in MetaCoq.Template.utils.wGraph]
v:636 [binder, in MetaCoq.Template.EnvironmentTyping]
v:638 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
v:640 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
v:645 [binder, in MetaCoq.Template.utils.wGraph]
v:648 [binder, in MetaCoq.PCUIC.PCUICConversion]
v:649 [binder, in MetaCoq.Template.utils.wGraph]
v:654 [binder, in MetaCoq.PCUIC.PCUICConversion]
v:66 [binder, in MetaCoq.Template.Normal]
v:664 [binder, in MetaCoq.PCUIC.PCUICEquality]
v:664 [binder, in MetaCoq.Template.utils.wGraph]
v:664 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
v:667 [binder, in MetaCoq.Template.utils.wGraph]
v:670 [binder, in MetaCoq.Template.utils.wGraph]
v:670 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
v:671 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
v:673 [binder, in MetaCoq.Template.utils.wGraph]
v:675 [binder, in MetaCoq.Template.utils.All_Forall]
v:675 [binder, in MetaCoq.PCUIC.PCUICEquality]
v:676 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
v:679 [binder, in MetaCoq.PCUIC.PCUICEquality]
v:679 [binder, in MetaCoq.Template.utils.wGraph]
v:68 [binder, in MetaCoq.PCUIC.PCUICCumulativity]
v:68 [binder, in MetaCoq.Template.common.uGraph]
v:68 [binder, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
v:680 [binder, in MetaCoq.Template.Universes]
v:680 [binder, in MetaCoq.Template.utils.MCList]
v:682 [binder, in MetaCoq.Template.Universes]
v:683 [binder, in MetaCoq.Template.common.uGraph]
v:683 [binder, in MetaCoq.PCUIC.PCUICEquality]
v:683 [binder, in MetaCoq.Template.utils.wGraph]
v:687 [binder, in MetaCoq.PCUIC.PCUICEquality]
v:69 [binder, in MetaCoq.PCUIC.PCUICConvCumInversion]
v:69 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
v:690 [binder, in MetaCoq.PCUIC.PCUICConversion]
v:693 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
v:695 [binder, in MetaCoq.PCUIC.PCUICEquality]
v:697 [binder, in MetaCoq.Template.utils.wGraph]
v:697 [binder, in MetaCoq.PCUIC.PCUICConversion]
v:699 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
v:70 [binder, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
v:70 [binder, in MetaCoq.Erasure.ETransform]
v:701 [binder, in MetaCoq.Template.utils.wGraph]
v:704 [binder, in MetaCoq.PCUIC.PCUICEquality]
v:71 [binder, in MetaCoq.PCUIC.PCUICInversion]
v:711 [binder, in MetaCoq.PCUIC.PCUICConversion]
v:717 [binder, in MetaCoq.PCUIC.PCUICConversion]
v:719 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
v:72 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
v:724 [binder, in MetaCoq.PCUIC.PCUICConversion]
v:73 [binder, in MetaCoq.Template.Normal]
v:730 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
v:733 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
v:733 [binder, in MetaCoq.PCUIC.PCUICConversion]
v:736 [binder, in MetaCoq.PCUIC.PCUICConversion]
v:738 [binder, in MetaCoq.PCUIC.PCUICConversion]
v:74 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
v:741 [binder, in MetaCoq.PCUIC.PCUICConversion]
v:743 [binder, in MetaCoq.PCUIC.PCUICConversion]
v:745 [binder, in MetaCoq.PCUIC.PCUICConversion]
v:747 [binder, in MetaCoq.PCUIC.PCUICConversion]
v:749 [binder, in MetaCoq.PCUIC.PCUICConversion]
v:75 [binder, in MetaCoq.PCUIC.PCUICConvCumInversion]
v:75 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
v:751 [binder, in MetaCoq.PCUIC.PCUICConversion]
v:753 [binder, in MetaCoq.PCUIC.PCUICConversion]
v:755 [binder, in MetaCoq.PCUIC.PCUICConversion]
v:758 [binder, in MetaCoq.PCUIC.PCUICConversion]
v:760 [binder, in MetaCoq.Template.utils.wGraph]
v:760 [binder, in MetaCoq.PCUIC.PCUICConversion]
v:761 [binder, in MetaCoq.Template.utils.wGraph]
v:763 [binder, in MetaCoq.PCUIC.PCUICConversion]
v:764 [binder, in MetaCoq.Translations.MiniHoTT]
v:765 [binder, in MetaCoq.PCUIC.PCUICConversion]
v:77 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
v:771 [binder, in MetaCoq.PCUIC.PCUICConversion]
v:772 [binder, in MetaCoq.Translations.MiniHoTT_paths]
v:777 [binder, in MetaCoq.PCUIC.PCUICConversion]
v:78 [binder, in MetaCoq.PCUIC.PCUICSafeLemmata]
v:78 [binder, in MetaCoq.PCUIC.PCUICInversion]
v:781 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
v:796 [binder, in MetaCoq.PCUIC.PCUICConfluence]
v:80 [binder, in MetaCoq.Erasure.ETransform]
v:800 [binder, in MetaCoq.PCUIC.PCUICConfluence]
v:804 [binder, in MetaCoq.PCUIC.PCUICConfluence]
v:805 [binder, in MetaCoq.PCUIC.PCUICConversion]
v:81 [binder, in MetaCoq.PCUIC.PCUICSafeLemmata]
v:82 [binder, in MetaCoq.Template.common.uGraph]
v:82 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
v:832 [binder, in MetaCoq.PCUIC.PCUICSpine]
v:836 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
v:84 [binder, in MetaCoq.Template.common.uGraph]
v:845 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
v:85 [binder, in MetaCoq.PCUIC.PCUICSafeLemmata]
v:85 [binder, in MetaCoq.Template.common.uGraph]
v:858 [binder, in MetaCoq.Template.utils.All_Forall]
v:88 [binder, in MetaCoq.PCUIC.PCUICSafeLemmata]
v:89 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
v:9 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
v:9 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
v:907 [binder, in MetaCoq.PCUIC.PCUICConfluence]
v:91 [binder, in MetaCoq.PCUIC.PCUICSafeLemmata]
v:91 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
v:91 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
v:92 [binder, in MetaCoq.Erasure.ETransform]
v:929 [binder, in MetaCoq.PCUIC.PCUICConfluence]
v:94 [binder, in MetaCoq.Template.Universes]
v:948 [binder, in MetaCoq.Erasure.ErasureFunction]
v:95 [binder, in MetaCoq.PCUIC.PCUICSafeLemmata]
v:95 [binder, in MetaCoq.PCUIC.PCUICConvCumInversion]
v:955 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
v:96 [binder, in MetaCoq.Template.Universes]
v:97 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
v:976 [binder, in MetaCoq.PCUIC.PCUICReduction]
v:979 [binder, in MetaCoq.PCUIC.PCUICReduction]
v:982 [binder, in MetaCoq.PCUIC.PCUICReduction]
v:985 [binder, in MetaCoq.Erasure.ErasureFunction]
v:985 [binder, in MetaCoq.PCUIC.PCUICReduction]
v:99 [binder, in MetaCoq.Template.common.uGraph]



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)