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)

R

R [definition, in MetaCoq.SafeChecker.PCUICSafeReduce]
R [definition, in MetaCoq.SafeChecker.PCUICSafeConversion]
raise [projection, in MetaCoq.Template.monad_utils]
raise [abbreviation, in MetaCoq.SafeChecker.PCUICTypeChecker]
rangsort:226 [binder, in MetaCoq.Template.Universes]
rangsort:294 [binder, in MetaCoq.Template.Universes]
rarg [projection, in MetaCoq.Template.BasicAst]
rarg [projection, in MetaCoq.Erasure.EAst]
rarg:144 [binder, in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
rarg:156 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
rarg:157 [binder, in MetaCoq.Erasure.EWcbvEval]
rarg:23 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
rarg:246 [binder, in MetaCoq.PCUIC.PCUICNormal]
rarg:257 [binder, in MetaCoq.PCUIC.PCUICNormal]
rarg:257 [binder, in MetaCoq.Template.WcbvEval]
rarg:267 [binder, in MetaCoq.PCUIC.PCUICNormal]
rarg:340 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
rarg:343 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
rarg:61 [binder, in MetaCoq.PCUIC.PCUICNormal]
ra:1001 [binder, in MetaCoq.PCUIC.PCUICReduction]
ra:1022 [binder, in MetaCoq.PCUIC.PCUICReduction]
ra:1027 [binder, in MetaCoq.PCUIC.PCUICReduction]
ra:1067 [binder, in MetaCoq.PCUIC.PCUICReduction]
ra:1072 [binder, in MetaCoq.PCUIC.PCUICReduction]
ra:1093 [binder, in MetaCoq.PCUIC.PCUICReduction]
ra:1098 [binder, in MetaCoq.PCUIC.PCUICReduction]
ra:1765 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
ra:19 [binder, in MetaCoq.PCUIC.Syntax.PCUICReflect]
ra:28 [binder, in MetaCoq.PCUIC.Syntax.PCUICReflect]
ra:39 [binder, in MetaCoq.PCUIC.Syntax.PCUICReflect]
ra:47 [binder, in MetaCoq.PCUIC.Syntax.PCUICReflect]
RA:53 [binder, in MetaCoq.PCUIC.utils.PCUICUtils]
RA:72 [binder, in MetaCoq.Template.utils.ReflectEq]
ra:996 [binder, in MetaCoq.PCUIC.PCUICReduction]
rb:20 [binder, in MetaCoq.PCUIC.Syntax.PCUICReflect]
rb:29 [binder, in MetaCoq.PCUIC.Syntax.PCUICReflect]
RB:54 [binder, in MetaCoq.PCUIC.utils.PCUICUtils]
rctx:1154 [binder, in MetaCoq.PCUIC.PCUICConfluence]
rctx:1159 [binder, in MetaCoq.PCUIC.PCUICConfluence]
rc:30 [binder, in MetaCoq.PCUIC.Syntax.PCUICReflect]
rd:29 [binder, in MetaCoq.Template.TemplateMonad.Extractable]
rd:33 [binder, in MetaCoq.Template.TemplateMonad.Extractable]
rd:38 [binder, in MetaCoq.Template.TemplateMonad.Extractable]
rd:43 [binder, in MetaCoq.Template.TemplateMonad.Core]
rd:43 [binder, in MetaCoq.Template.TemplateMonad.Extractable]
rebuild_case_branch_ctx [definition, in MetaCoq.Template.Checker]
rebuild_case_predicate_ctx [definition, in MetaCoq.Template.Checker]
rebuild_wf_env_transform [definition, in MetaCoq.Erasure.ETransform]
rebuild_wf_env [definition, in MetaCoq.Erasure.ETransform]
rec [abbreviation, in MetaCoq.SafeChecker.PCUICSafeReduce]
recomp_branch' [abbreviation, in MetaCoq.PCUIC.PCUICReduction]
recomp_branch [abbreviation, in MetaCoq.PCUIC.PCUICReduction]
recursivity_kind [inductive, in MetaCoq.Template.BasicAst]
recursivity_kind [inductive, in MetaCoq.Erasure.EAst]
red [inductive, in MetaCoq.Template.Typing]
red [definition, in MetaCoq.PCUIC.PCUICReduction]
RedConfluence [section, in MetaCoq.PCUIC.PCUICConfluence]
RedConv [section, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
redctx:1170 [binder, in MetaCoq.PCUIC.PCUICConfluence]
redctx:1214 [binder, in MetaCoq.PCUIC.PCUICConfluence]
RedEq [section, in MetaCoq.PCUIC.PCUICConfluence]
RedFlags [module, in MetaCoq.PCUIC.PCUICNormal]
RedFlags [module, in MetaCoq.Template.Checker]
RedFlags.beta [projection, in MetaCoq.PCUIC.PCUICNormal]
RedFlags.beta [projection, in MetaCoq.Template.Checker]
RedFlags.cofix_ [projection, in MetaCoq.PCUIC.PCUICNormal]
RedFlags.cofix_ [projection, in MetaCoq.Template.Checker]
RedFlags.default [definition, in MetaCoq.PCUIC.PCUICNormal]
RedFlags.default [definition, in MetaCoq.Template.Checker]
RedFlags.delta [projection, in MetaCoq.PCUIC.PCUICNormal]
RedFlags.delta [projection, in MetaCoq.Template.Checker]
RedFlags.fix_ [projection, in MetaCoq.PCUIC.PCUICNormal]
RedFlags.fix_ [projection, in MetaCoq.Template.Checker]
RedFlags.iota [projection, in MetaCoq.PCUIC.PCUICNormal]
RedFlags.iota [projection, in MetaCoq.Template.Checker]
RedFlags.nodelta [definition, in MetaCoq.PCUIC.PCUICNormal]
RedFlags.t [record, in MetaCoq.PCUIC.PCUICNormal]
RedFlags.t [record, in MetaCoq.Template.Checker]
RedFlags.zeta [projection, in MetaCoq.PCUIC.PCUICNormal]
RedFlags.zeta [projection, in MetaCoq.Template.Checker]
redl [inductive, in MetaCoq.PCUIC.PCUICReduction]
redl_context_trans [lemma, in MetaCoq.PCUIC.PCUICReduction]
redl_context_impl [lemma, in MetaCoq.PCUIC.PCUICReduction]
redl_branch [definition, in MetaCoq.PCUIC.PCUICReduction]
redl_context [definition, in MetaCoq.PCUIC.PCUICReduction]
redl_term [definition, in MetaCoq.PCUIC.PCUICReduction]
redl_preserve [lemma, in MetaCoq.PCUIC.PCUICReduction]
redp [definition, in MetaCoq.SafeChecker.PCUICWfReduction]
RedPred [section, in MetaCoq.PCUIC.PCUICConfluence]
redp_subterm_rel [definition, in MetaCoq.SafeChecker.PCUICWfReduction]
redp_red [instance, in MetaCoq.SafeChecker.PCUICWfReduction]
redp_trans [instance, in MetaCoq.SafeChecker.PCUICWfReduction]
redt:257 [binder, in MetaCoq.Template.Checker]
redt:259 [binder, in MetaCoq.Template.Checker]
redt:272 [binder, in MetaCoq.Template.Checker]
redt:274 [binder, in MetaCoq.Template.Checker]
Reduce [section, in MetaCoq.SafeChecker.PCUICSafeReduce]
reduce [definition, in MetaCoq.Template.Checker]
Reduce [section, in MetaCoq.Template.Checker]
reduced_proj_body_whne [lemma, in MetaCoq.SafeChecker.PCUICSafeConversion]
reduced_case_discriminee_whne [lemma, in MetaCoq.SafeChecker.PCUICSafeConversion]
ReduceFns [section, in MetaCoq.SafeChecker.PCUICSafeReduce]
reduce_to_ind_irrel [lemma, in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
reduce_to_sort_irrel [lemma, in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
reduce_to_prod_irrel [lemma, in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
reduce_stack_eq [definition, in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
reduce_stack_eq [definition, in MetaCoq.Erasure.ErasureFunction]
reduce_to_ind_complete [lemma, in MetaCoq.SafeChecker.PCUICSafeReduce]
reduce_to_ind [definition, in MetaCoq.SafeChecker.PCUICSafeReduce]
reduce_to_prod_complete [lemma, in MetaCoq.SafeChecker.PCUICSafeReduce]
reduce_to_prod [definition, in MetaCoq.SafeChecker.PCUICSafeReduce]
reduce_to_sort_complete [lemma, in MetaCoq.SafeChecker.PCUICSafeReduce]
reduce_to_sort [definition, in MetaCoq.SafeChecker.PCUICSafeReduce]
reduce_term_complete [lemma, in MetaCoq.SafeChecker.PCUICSafeReduce]
reduce_stack_whnf [lemma, in MetaCoq.SafeChecker.PCUICSafeReduce]
reduce_stack_prop [lemma, in MetaCoq.SafeChecker.PCUICSafeReduce]
reduce_term_sound [lemma, in MetaCoq.SafeChecker.PCUICSafeReduce]
reduce_term [definition, in MetaCoq.SafeChecker.PCUICSafeReduce]
reduce_stack_noLamApp [lemma, in MetaCoq.SafeChecker.PCUICSafeReduce]
reduce_stack_noApp [lemma, in MetaCoq.SafeChecker.PCUICSafeReduce]
reduce_stack_isred [lemma, in MetaCoq.SafeChecker.PCUICSafeReduce]
reduce_stack_context [lemma, in MetaCoq.SafeChecker.PCUICSafeReduce]
reduce_stack_decompose [lemma, in MetaCoq.SafeChecker.PCUICSafeReduce]
reduce_stack_sound [lemma, in MetaCoq.SafeChecker.PCUICSafeReduce]
reduce_stack_Req [lemma, in MetaCoq.SafeChecker.PCUICSafeReduce]
reduce_stack [definition, in MetaCoq.SafeChecker.PCUICSafeReduce]
reduce_stack_full [definition, in MetaCoq.SafeChecker.PCUICSafeReduce]
reduce_to_ind [definition, in MetaCoq.Template.Checker]
reduce_to_prod [definition, in MetaCoq.Template.Checker]
reduce_to_sort [definition, in MetaCoq.Template.Checker]
reduce_opt [definition, in MetaCoq.Template.Checker]
reduce_stack_term [definition, in MetaCoq.Template.Checker]
reduce_stack [definition, in MetaCoq.Template.Checker]
Reduce.reducewf [section, in MetaCoq.SafeChecker.PCUICSafeReduce]
reduce:356 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
reducible_head_None [lemma, in MetaCoq.SafeChecker.PCUICSafeConversion]
reducible_head_decompose [lemma, in MetaCoq.SafeChecker.PCUICSafeConversion]
reducible_head_cored [lemma, in MetaCoq.SafeChecker.PCUICSafeConversion]
reducible_head_red_zippx [lemma, in MetaCoq.SafeChecker.PCUICSafeConversion]
reducible_head_red_zipp [lemma, in MetaCoq.SafeChecker.PCUICSafeConversion]
reducible_head [definition, in MetaCoq.SafeChecker.PCUICSafeConversion]
reducible_head [definition, in MetaCoq.Template.Checker]
Reduction [constructor, in MetaCoq.SafeChecker.PCUICSafeConversion]
Reduction [library]
ReductionCongruence [section, in MetaCoq.PCUIC.PCUICReduction]
ReductionCongruence.Congruences [section, in MetaCoq.PCUIC.PCUICReduction]
ReductionCongruence.FillContext [section, in MetaCoq.PCUIC.PCUICReduction]
reductionStrategy [inductive, in MetaCoq.Template.TemplateMonad.Common]
red_conv_conv_inv [lemma, in MetaCoq.PCUIC.PCUICCumulativity]
red_conv_conv [lemma, in MetaCoq.PCUIC.PCUICCumulativity]
red_conv [lemma, in MetaCoq.PCUIC.PCUICCumulativity]
red_cumul_cumul_inv [lemma, in MetaCoq.PCUIC.PCUICCumulativity]
red_cumul_cumul [lemma, in MetaCoq.PCUIC.PCUICCumulativity]
red_cumul_inv [lemma, in MetaCoq.PCUIC.PCUICCumulativity]
red_cumul [lemma, in MetaCoq.PCUIC.PCUICCumulativity]
red_zipc [lemma, in MetaCoq.PCUIC.PCUICSafeLemmata]
red_cored_cored [lemma, in MetaCoq.PCUIC.PCUICSafeLemmata]
red_welltyped [lemma, in MetaCoq.PCUIC.PCUICSafeLemmata]
red_neq_cored [lemma, in MetaCoq.PCUIC.PCUICSafeLemmata]
red_const [lemma, in MetaCoq.PCUIC.PCUICSafeLemmata]
red_cored_or_eq [lemma, in MetaCoq.PCUIC.PCUICSafeLemmata]
red_case_isproof [lemma, in MetaCoq.Erasure.EArities]
red_on_free_vars [lemma, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
red_proj [constructor, in MetaCoq.Template.Typing]
red_delta [constructor, in MetaCoq.Template.Typing]
red_cofix_proj [constructor, in MetaCoq.Template.Typing]
red_cofix_case [constructor, in MetaCoq.Template.Typing]
red_fix [constructor, in MetaCoq.Template.Typing]
red_iota [constructor, in MetaCoq.Template.Typing]
red_rel [constructor, in MetaCoq.Template.Typing]
red_zeta [constructor, in MetaCoq.Template.Typing]
red_beta [constructor, in MetaCoq.Template.Typing]
red_cofix_case [constructor, in MetaCoq.PCUIC.PCUICWcbvEval]
red_cofix_proj [constructor, in MetaCoq.PCUIC.PCUICWcbvEval]
red_fix [constructor, in MetaCoq.PCUIC.PCUICWcbvEval]
red_proj [constructor, in MetaCoq.PCUIC.PCUICWcbvEval]
red_proj_in [constructor, in MetaCoq.PCUIC.PCUICWcbvEval]
red_iota [constructor, in MetaCoq.PCUIC.PCUICWcbvEval]
red_case_in [constructor, in MetaCoq.PCUIC.PCUICWcbvEval]
red_delta [constructor, in MetaCoq.PCUIC.PCUICWcbvEval]
red_zeta [constructor, in MetaCoq.PCUIC.PCUICWcbvEval]
red_let_in [constructor, in MetaCoq.PCUIC.PCUICWcbvEval]
red_beta [constructor, in MetaCoq.PCUIC.PCUICWcbvEval]
red_app_right [constructor, in MetaCoq.PCUIC.PCUICWcbvEval]
red_app_left [constructor, in MetaCoq.PCUIC.PCUICWcbvEval]
red_red [lemma, in MetaCoq.PCUIC.PCUICSubstitution]
red_letin_alt [lemma, in MetaCoq.PCUIC.PCUICSubstitution]
red_abs_alt [lemma, in MetaCoq.PCUIC.PCUICSubstitution]
red_it_mkProd_or_LetIn_mkApps_Ind [lemma, in MetaCoq.PCUIC.PCUICInductives]
red_it_mkProd_or_LetIn_smash [lemma, in MetaCoq.PCUIC.PCUICInductives]
red_destInd [lemma, in MetaCoq.PCUIC.PCUICInductives]
red_subst_instance [lemma, in MetaCoq.PCUIC.PCUICInductiveInversion]
red_cumul_prop [lemma, in MetaCoq.PCUIC.PCUICCumulProp]
red_conv_prop [lemma, in MetaCoq.PCUIC.PCUICCumulProp]
red_upto_conv_ctx_prop [lemma, in MetaCoq.PCUIC.PCUICCumulProp]
red_terms_on_free_vars [lemma, in MetaCoq.PCUIC.PCUICNormal]
red_ctx_rel_subst [lemma, in MetaCoq.PCUIC.PCUICNormal]
red_expand_lets_ctx [lemma, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
red_context_rel_conv_extended_subst [lemma, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
red_terms_lift [lemma, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
red_context_rel_assumptions [lemma, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
red_expand_lets [lemma, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
red_ws_cumul_pb_inv [lemma, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
red_ws_cumul_pb [lemma, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
red_ws_cumul_pb_right [lemma, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
red_ws_cumul_pb_left [lemma, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
red_conv [lemma, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
red_is_open_term [lemma, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
red_ctx_rel_par_conv [lemma, in MetaCoq.PCUIC.PCUICConvCumInversion]
red_viewc [definition, in MetaCoq.SafeChecker.PCUICSafeReduce]
red_view_other [constructor, in MetaCoq.SafeChecker.PCUICSafeReduce]
red_view_Proj [constructor, in MetaCoq.SafeChecker.PCUICSafeReduce]
red_view_Case [constructor, in MetaCoq.SafeChecker.PCUICSafeReduce]
red_view_Fix [constructor, in MetaCoq.SafeChecker.PCUICSafeReduce]
red_view_Lambda [constructor, in MetaCoq.SafeChecker.PCUICSafeReduce]
red_view_App [constructor, in MetaCoq.SafeChecker.PCUICSafeReduce]
red_view_Const [constructor, in MetaCoq.SafeChecker.PCUICSafeReduce]
red_view_LetIn [constructor, in MetaCoq.SafeChecker.PCUICSafeReduce]
red_view_Rel [constructor, in MetaCoq.SafeChecker.PCUICSafeReduce]
red_view [inductive, in MetaCoq.SafeChecker.PCUICSafeReduce]
red_discr [definition, in MetaCoq.SafeChecker.PCUICSafeReduce]
red_welltyped [lemma, in MetaCoq.SafeChecker.PCUICSafeReduce]
red_conv_cum_r [lemma, in MetaCoq.SafeChecker.PCUICSafeConversion]
red_conv_cum_l [lemma, in MetaCoq.SafeChecker.PCUICSafeConversion]
red_brs_refl [instance, in MetaCoq.SafeChecker.PCUICSafeConversion]
red_confluence [lemma, in MetaCoq.PCUIC.PCUICConfluence]
red_ws_red_left [lemma, in MetaCoq.PCUIC.PCUICConfluence]
red_mkApps_tConst_axiom [lemma, in MetaCoq.PCUIC.PCUICConfluence]
red_mkApps_tRel [lemma, in MetaCoq.PCUIC.PCUICConfluence]
red_mkApps_tInd [lemma, in MetaCoq.PCUIC.PCUICConfluence]
red_mkApps_tConstruct [lemma, in MetaCoq.PCUIC.PCUICConfluence]
red_ctx_red_ctx_alpha_trans [lemma, in MetaCoq.PCUIC.PCUICConfluence]
red_ctx_alpha_refl [instance, in MetaCoq.PCUIC.PCUICConfluence]
red_ctx_alpha [definition, in MetaCoq.PCUIC.PCUICConfluence]
red_eq_context_upto_names [lemma, in MetaCoq.PCUIC.PCUICConfluence]
red_context_trans [lemma, in MetaCoq.PCUIC.PCUICConfluence]
red_ctx_red_context [lemma, in MetaCoq.PCUIC.PCUICConfluence]
red_ws_red [lemma, in MetaCoq.PCUIC.PCUICConfluence]
red_ctx_clos_rt_red1_ctx [lemma, in MetaCoq.PCUIC.PCUICConfluence]
red_ctx_refl [instance, in MetaCoq.PCUIC.PCUICConfluence]
red_rel_ctx [definition, in MetaCoq.PCUIC.PCUICConfluence]
red_trans_clos_pred1 [lemma, in MetaCoq.PCUIC.PCUICConfluence]
red_ctx [definition, in MetaCoq.PCUIC.PCUICConfluence]
red_pred [lemma, in MetaCoq.PCUIC.PCUICConfluence]
red_pred' [lemma, in MetaCoq.PCUIC.PCUICConfluence]
red_eq_term_upto_univ_l [lemma, in MetaCoq.PCUIC.PCUICConfluence]
red_eq_term_upto_univ_r [lemma, in MetaCoq.PCUIC.PCUICConfluence]
red_Trans [instance, in MetaCoq.PCUIC.PCUICConfluence]
red_Refl [instance, in MetaCoq.PCUIC.PCUICConfluence]
red_terms_evar [lemma, in MetaCoq.PCUIC.PCUICConversion]
red_rel_all [lemma, in MetaCoq.PCUIC.PCUICConversion]
red_fix_or_cofix_body [lemma, in MetaCoq.PCUIC.PCUICConversion]
red_terms_refl [instance, in MetaCoq.PCUIC.PCUICConversion]
red_brs_refl [instance, in MetaCoq.PCUIC.PCUICConversion]
red_terms_ws_cumul_pb_terms [lemma, in MetaCoq.PCUIC.PCUICConversion]
red_terms [abbreviation, in MetaCoq.PCUIC.PCUICConversion]
red_it_mkProd_or_LetIn_smash [lemma, in MetaCoq.PCUIC.PCUICCanonicity]
red_decl_refl [lemma, in MetaCoq.PCUIC.PCUICContextConversion]
red_eq_context_upto_r [lemma, in MetaCoq.PCUIC.PCUICContextConversion]
red_eq_context_upto_l [lemma, in MetaCoq.PCUIC.PCUICContextConversion]
red_red_ctx_inv' [lemma, in MetaCoq.PCUIC.PCUICContextConversion]
red_red_ctx_inv [lemma, in MetaCoq.PCUIC.PCUICContextConversion]
red_compare_term_r [lemma, in MetaCoq.PCUIC.PCUICContextConversion]
red_compare_term_l [lemma, in MetaCoq.PCUIC.PCUICContextConversion]
red_ctx_closed_right [lemma, in MetaCoq.PCUIC.PCUICContextConversion]
red_ctx_closed_left [lemma, in MetaCoq.PCUIC.PCUICContextConversion]
red_ctx_ws_cumul_ctx_pb [lemma, in MetaCoq.PCUIC.PCUICContextConversion]
red_ctx_on_free_vars_term [lemma, in MetaCoq.PCUIC.PCUICContextConversion]
red_red_ctx [lemma, in MetaCoq.PCUIC.PCUICContextConversion]
red_red_ctx_aux' [lemma, in MetaCoq.PCUIC.PCUICContextConversion]
red_red_ctx' [lemma, in MetaCoq.PCUIC.PCUICContextConversion]
red_ctx_on_free_vars [lemma, in MetaCoq.PCUIC.PCUICContextConversion]
red_ctx_app [lemma, in MetaCoq.PCUIC.PCUICContextConversion]
red_ctx_skip [lemma, in MetaCoq.PCUIC.PCUICContextConversion]
red_ctx_app_context_l [lemma, in MetaCoq.PCUIC.PCUICSR]
red_ctx_clos_rt_red1_ctx [lemma, in MetaCoq.PCUIC.PCUICSR]
red_terms_refl [lemma, in MetaCoq.PCUIC.PCUICSR]
red_one_decl_ws_cumul_ctx_pb [lemma, in MetaCoq.PCUIC.PCUICSR]
red_one_decl_red_context [lemma, in MetaCoq.PCUIC.PCUICSR]
red_one_decl_red_ctx [lemma, in MetaCoq.PCUIC.PCUICSR]
red_rename [lemma, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
red_on_free_vars [lemma, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
red_ctx_rel_red_context_rel [lemma, in MetaCoq.PCUIC.PCUICContextReduction]
red_context_rel_inv [lemma, in MetaCoq.PCUIC.PCUICContextReduction]
red_context_app_right [lemma, in MetaCoq.PCUIC.PCUICContextReduction]
red_context_trans [lemma, in MetaCoq.PCUIC.PCUICContextReduction]
red_context_rel_on_ctx_free_vars [lemma, in MetaCoq.PCUIC.PCUICContextReduction]
red_context_on_ctx_free_vars [lemma, in MetaCoq.PCUIC.PCUICContextReduction]
red_context_app_same_left [lemma, in MetaCoq.PCUIC.PCUICContextReduction]
red_context_app [lemma, in MetaCoq.PCUIC.PCUICContextReduction]
red_red_ctx [lemma, in MetaCoq.PCUIC.PCUICContextReduction]
red_context_app_same [lemma, in MetaCoq.PCUIC.PCUICContextReduction]
red_context_refl [lemma, in MetaCoq.PCUIC.PCUICContextReduction]
red_decls_refl [lemma, in MetaCoq.PCUIC.PCUICContextReduction]
red_prod_alt [lemma, in MetaCoq.PCUIC.PCUICContextReduction]
red_zippx [lemma, in MetaCoq.PCUIC.PCUICReduction]
red_zipp [lemma, in MetaCoq.PCUIC.PCUICReduction]
red_context_zip [lemma, in MetaCoq.PCUIC.PCUICReduction]
red_atom [lemma, in MetaCoq.PCUIC.PCUICReduction]
red_evar [lemma, in MetaCoq.PCUIC.PCUICReduction]
red_one_evar [lemma, in MetaCoq.PCUIC.PCUICReduction]
red_prod [lemma, in MetaCoq.PCUIC.PCUICReduction]
red_prod_r [lemma, in MetaCoq.PCUIC.PCUICReduction]
red_prod_l [lemma, in MetaCoq.PCUIC.PCUICReduction]
red_cofix_congr [lemma, in MetaCoq.PCUIC.PCUICReduction]
red_cofix_body [lemma, in MetaCoq.PCUIC.PCUICReduction]
red_cofix_one_body [lemma, in MetaCoq.PCUIC.PCUICReduction]
red_cofix_ty [lemma, in MetaCoq.PCUIC.PCUICReduction]
red_cofix_one_ty [lemma, in MetaCoq.PCUIC.PCUICReduction]
red_fix_congr [lemma, in MetaCoq.PCUIC.PCUICReduction]
red_fix_body [lemma, in MetaCoq.PCUIC.PCUICReduction]
red_fix_one_body [lemma, in MetaCoq.PCUIC.PCUICReduction]
red_fix_ty [lemma, in MetaCoq.PCUIC.PCUICReduction]
red_fix_one_ty [lemma, in MetaCoq.PCUIC.PCUICReduction]
red_proj_c [lemma, in MetaCoq.PCUIC.PCUICReduction]
red_it_mkProd_or_LetIn [lemma, in MetaCoq.PCUIC.PCUICReduction]
red_it_mkLambda_or_LetIn [lemma, in MetaCoq.PCUIC.PCUICReduction]
red_case [lemma, in MetaCoq.PCUIC.PCUICReduction]
red_case_brs [lemma, in MetaCoq.PCUIC.PCUICReduction]
red_one_brs_red_brs [lemma, in MetaCoq.PCUIC.PCUICReduction]
red_brs [definition, in MetaCoq.PCUIC.PCUICReduction]
red_one_brs [definition, in MetaCoq.PCUIC.PCUICReduction]
red_case_one_brs [lemma, in MetaCoq.PCUIC.PCUICReduction]
red_case_c [lemma, in MetaCoq.PCUIC.PCUICReduction]
red_case_p [lemma, in MetaCoq.PCUIC.PCUICReduction]
red_case_pars [lemma, in MetaCoq.PCUIC.PCUICReduction]
red_one_param [lemma, in MetaCoq.PCUIC.PCUICReduction]
red_letin [lemma, in MetaCoq.PCUIC.PCUICReduction]
red_mkApps [lemma, in MetaCoq.PCUIC.PCUICReduction]
red_mkApps_f [lemma, in MetaCoq.PCUIC.PCUICReduction]
red_app [lemma, in MetaCoq.PCUIC.PCUICReduction]
red_app_r [lemma, in MetaCoq.PCUIC.PCUICReduction]
red_abs [lemma, in MetaCoq.PCUIC.PCUICReduction]
red_one_decl_red_ctx_rel [lemma, in MetaCoq.PCUIC.PCUICReduction]
red_one_context_redl [lemma, in MetaCoq.PCUIC.PCUICReduction]
red_one_branch [abbreviation, in MetaCoq.PCUIC.PCUICReduction]
red_one_context_decl [abbreviation, in MetaCoq.PCUIC.PCUICReduction]
red_one_context_decl_rel [definition, in MetaCoq.PCUIC.PCUICReduction]
red_one_term [abbreviation, in MetaCoq.PCUIC.PCUICReduction]
red_ctx_congr [lemma, in MetaCoq.PCUIC.PCUICReduction]
red_contextual_closure_equiv [lemma, in MetaCoq.PCUIC.PCUICReduction]
red_contextual_closure [lemma, in MetaCoq.PCUIC.PCUICReduction]
red_trans [lemma, in MetaCoq.PCUIC.PCUICReduction]
red_step [lemma, in MetaCoq.PCUIC.PCUICReduction]
red_rect_1n [definition, in MetaCoq.PCUIC.PCUICReduction]
red_rect_n1 [definition, in MetaCoq.PCUIC.PCUICReduction]
red_rect' [definition, in MetaCoq.PCUIC.PCUICReduction]
red_context_rel [definition, in MetaCoq.PCUIC.PCUICReduction]
red_context [definition, in MetaCoq.PCUIC.PCUICReduction]
red_vdef_body [constructor, in MetaCoq.PCUIC.PCUICReduction]
red_vass [constructor, in MetaCoq.PCUIC.PCUICReduction]
red_decls [inductive, in MetaCoq.PCUIC.PCUICReduction]
red_ctx_rel [definition, in MetaCoq.PCUIC.PCUICReduction]
red_one_ctx_rel [definition, in MetaCoq.PCUIC.PCUICReduction]
red_proj [constructor, in MetaCoq.PCUIC.PCUICReduction]
red_delta [constructor, in MetaCoq.PCUIC.PCUICReduction]
red_cofix_proj [constructor, in MetaCoq.PCUIC.PCUICReduction]
red_cofix_case [constructor, in MetaCoq.PCUIC.PCUICReduction]
red_fix [constructor, in MetaCoq.PCUIC.PCUICReduction]
red_iota [constructor, in MetaCoq.PCUIC.PCUICReduction]
red_rel [constructor, in MetaCoq.PCUIC.PCUICReduction]
red_zeta [constructor, in MetaCoq.PCUIC.PCUICReduction]
red_beta [constructor, in MetaCoq.PCUIC.PCUICReduction]
red_expand_let [lemma, in MetaCoq.PCUIC.PCUICSpine]
red_context [abbreviation, in MetaCoq.Erasure.Prelim]
red_decls [inductive, in MetaCoq.Erasure.Prelim]
red1 [inductive, in MetaCoq.Template.Typing]
red1 [inductive, in MetaCoq.PCUIC.PCUICWcbvEval]
red1 [inductive, in MetaCoq.PCUIC.PCUICReduction]
red1P [definition, in MetaCoq.PCUIC.PCUICSubstitution]
red1P_on_free_vars_right [definition, in MetaCoq.PCUIC.PCUICSubstitution]
red1P_on_free_vars_ctx [definition, in MetaCoq.PCUIC.PCUICSubstitution]
red1P_on_free_vars_left [definition, in MetaCoq.PCUIC.PCUICSubstitution]
red1P_red1 [definition, in MetaCoq.PCUIC.PCUICSubstitution]
red1_eval [lemma, in MetaCoq.PCUIC.PCUICProgress]
red1_incl [lemma, in MetaCoq.PCUIC.PCUICProgress]
red1_closed [lemma, in MetaCoq.PCUIC.PCUICProgress]
red1_mkApps_left [lemma, in MetaCoq.PCUIC.PCUICProgress]
red1_alpha_eq [lemma, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
red1_conv [lemma, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
red1_cumul_inv [lemma, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
red1_cumul [lemma, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
red1_on_free_vars [lemma, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
red1_ind_all [lemma, in MetaCoq.Template.Typing]
red1_it_mkProd_or_LetIn_smash [lemma, in MetaCoq.PCUIC.PCUICInductives]
red1_destInd [lemma, in MetaCoq.PCUIC.PCUICInductives]
red1_mkApps_r [lemma, in MetaCoq.Template.Reduction]
red1_mkApps_l [lemma, in MetaCoq.Template.Reduction]
red1_mkApp [lemma, in MetaCoq.Template.Reduction]
red1_tApp_mkApp [lemma, in MetaCoq.Template.Reduction]
red1_tApp_mkApps_l [lemma, in MetaCoq.Template.Reduction]
red1_upto_conv_ctx_prop [lemma, in MetaCoq.PCUIC.PCUICCumulProp]
red1_mkApps_tCoFix_inv [lemma, in MetaCoq.PCUIC.PCUICNormal]
red1_mkApps_tFix_inv [lemma, in MetaCoq.PCUIC.PCUICNormal]
red1_mkApps_tInd_inv [lemma, in MetaCoq.PCUIC.PCUICNormal]
red1_mkApps_tConstruct_inv [lemma, in MetaCoq.PCUIC.PCUICNormal]
red1_conv [lemma, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
red1_cumul_inv [lemma, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
red1_cumul [lemma, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
red1_is_open_term [lemma, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
red1_inst [lemma, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
red1_confluent [lemma, in MetaCoq.PCUIC.PCUICConfluence]
red1_eq_context_upto_names [lemma, in MetaCoq.PCUIC.PCUICConfluence]
red1_rel_alpha_red1_rel_inv [lemma, in MetaCoq.PCUIC.PCUICConfluence]
red1_rel_alpha_red1_rel [lemma, in MetaCoq.PCUIC.PCUICConfluence]
red1_rel_alpha_pred1_rel_alpha [lemma, in MetaCoq.PCUIC.PCUICConfluence]
red1_rel_alpha [definition, in MetaCoq.PCUIC.PCUICConfluence]
red1_ctx_on_free_vars [lemma, in MetaCoq.PCUIC.PCUICConfluence]
red1_ctx_pred1_ctx [lemma, in MetaCoq.PCUIC.PCUICConfluence]
red1_rel [definition, in MetaCoq.PCUIC.PCUICConfluence]
red1_weak_confluence [lemma, in MetaCoq.PCUIC.PCUICConfluence]
red1_pred1 [lemma, in MetaCoq.PCUIC.PCUICConfluence]
red1_eq_term_upto_univ_r [lemma, in MetaCoq.PCUIC.PCUICConfluence]
red1_eq_context_upto_r [lemma, in MetaCoq.PCUIC.PCUICConfluence]
red1_eq_term_upto_univ_l [lemma, in MetaCoq.PCUIC.PCUICConfluence]
red1_eq_context_upto_univ_l [lemma, in MetaCoq.PCUIC.PCUICConfluence]
red1_eq_context_upto_l [lemma, in MetaCoq.PCUIC.PCUICConfluence]
red1_ctx_rel [abbreviation, in MetaCoq.PCUIC.PCUICConfluence]
red1_cumulSpec [lemma, in MetaCoq.PCUIC.PCUICConversion]
red1_red_ctx_aux [lemma, in MetaCoq.PCUIC.PCUICContextConversion]
red1_red_ctxP_app [lemma, in MetaCoq.PCUIC.PCUICContextConversion]
red1_red_ctxP [definition, in MetaCoq.PCUIC.PCUICContextConversion]
red1_red_ctx [lemma, in MetaCoq.PCUIC.PCUICSR]
red1_ctx_app [lemma, in MetaCoq.PCUIC.PCUICSR]
red1_it_mkLambda_or_LetIn_ctx [lemma, in MetaCoq.PCUIC.PCUICSR]
red1_subst_instance [lemma, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
red1_rename [lemma, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
red1_red_ctx [lemma, in MetaCoq.PCUIC.PCUICContextReduction]
red1_isLambda [lemma, in MetaCoq.Template.TypingWf]
red1_zippx [lemma, in MetaCoq.PCUIC.PCUICReduction]
red1_zipp [lemma, in MetaCoq.PCUIC.PCUICReduction]
red1_context [lemma, in MetaCoq.PCUIC.PCUICReduction]
red1_fill_context_hole [lemma, in MetaCoq.PCUIC.PCUICReduction]
red1_it_mkProd_or_LetIn [lemma, in MetaCoq.PCUIC.PCUICReduction]
red1_it_mkLambda_or_LetIn [lemma, in MetaCoq.PCUIC.PCUICReduction]
red1_mkApps_r [lemma, in MetaCoq.PCUIC.PCUICReduction]
red1_mkApps_f [lemma, in MetaCoq.PCUIC.PCUICReduction]
red1_one_branch [abbreviation, in MetaCoq.PCUIC.PCUICReduction]
red1_one_context_decl [abbreviation, in MetaCoq.PCUIC.PCUICReduction]
red1_one_term [abbreviation, in MetaCoq.PCUIC.PCUICReduction]
red1_red [lemma, in MetaCoq.PCUIC.PCUICReduction]
red1_ind_all [lemma, in MetaCoq.PCUIC.PCUICReduction]
red1_ctx_rel [definition, in MetaCoq.PCUIC.PCUICReduction]
red1_ctx [definition, in MetaCoq.PCUIC.PCUICReduction]
red1:244 [binder, in MetaCoq.Template.Checker]
red2:245 [binder, in MetaCoq.Template.Checker]
red:646 [binder, in MetaCoq.PCUIC.PCUICReduction]
red:7 [binder, in MetaCoq.Template.TemplateMonad.Extractable]
referenced_impl_sq_wf [definition, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
referenced_pop [definition, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
referenced_impl_graph_wf [projection, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
referenced_impl_graph [projection, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
referenced_impl_wf [projection, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
referenced_impl_env [projection, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
referenced_impl [record, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
referenced_impl_ext_graph_wf [projection, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
referenced_impl_ext_graph [projection, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
referenced_impl_ext_wf [projection, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
referenced_impl_env_ext [projection, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
referenced_impl_ext [record, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
reference_pop_decls_correct [lemma, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
refine_red1_Γ [lemma, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
refine_red1_r [lemma, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
refine_red1_Γ [lemma, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
refine_red1_r [lemma, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
refine_red1_Γ [lemma, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
refine_red1_r [lemma, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
refine_pred [lemma, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
Reflect [library]
ReflectAst [library]
ReflectEq [record, in MetaCoq.Template.utils.ReflectEq]
ReflectEq [library]
ReflectEq_EqDec [instance, in MetaCoq.Template.utils.ReflectEq]
reflectEq_andb_right [lemma, in MetaCoq.PCUIC.Syntax.PCUICReflect]
reflectEq_andb_left [lemma, in MetaCoq.PCUIC.Syntax.PCUICReflect]
reflectEq_andb_3 [lemma, in MetaCoq.PCUIC.Syntax.PCUICReflect]
reflectEq_andb [lemma, in MetaCoq.PCUIC.Syntax.PCUICReflect]
ReflectEq_term [instance, in MetaCoq.Erasure.EReflect]
ReflectF [constructor, in MetaCoq.Template.utils.MCReflect]
reflectF [constructor, in MetaCoq.Template.utils.ReflectEq]
reflectP [constructor, in MetaCoq.Template.utils.ReflectEq]
reflectProp [inductive, in MetaCoq.Template.utils.ReflectEq]
reflectProp_reflect [lemma, in MetaCoq.Template.utils.ReflectEq]
reflectProp_sigma_simpl [lemma, in MetaCoq.PCUIC.Syntax.PCUICReflect]
reflectProp_noConfusion [lemma, in MetaCoq.PCUIC.Syntax.PCUICReflect]
reflectProp_equiv [lemma, in MetaCoq.PCUIC.Syntax.PCUICReflect]
ReflectT [constructor, in MetaCoq.Template.utils.MCReflect]
reflectT [inductive, in MetaCoq.Template.utils.MCReflect]
reflectT_pred2 [lemma, in MetaCoq.Template.utils.MCReflect]
reflectT_pred [lemma, in MetaCoq.Template.utils.MCReflect]
reflectT_subrelation' [lemma, in MetaCoq.Template.utils.MCReflect]
reflectT_subrelation [lemma, in MetaCoq.Template.utils.MCReflect]
reflectT_reflect [lemma, in MetaCoq.Template.utils.MCReflect]
reflect_reflectT [lemma, in MetaCoq.Template.utils.MCReflect]
reflect_equiv [lemma, in MetaCoq.Template.utils.ByteCompareSpec]
reflect_eq_projection [instance, in MetaCoq.Template.Kernames]
reflect_eq_inductive [instance, in MetaCoq.Template.Kernames]
reflect_stack [instance, in MetaCoq.PCUIC.Syntax.PCUICPosition]
reflect_choice [instance, in MetaCoq.PCUIC.Syntax.PCUICPosition]
reflect_prod [instance, in MetaCoq.Template.utils.ReflectEq]
reflect_sig_true [instance, in MetaCoq.Template.utils.ReflectEq]
reflect_bool [instance, in MetaCoq.Template.utils.ReflectEq]
reflect_nat [instance, in MetaCoq.Template.utils.ReflectEq]
reflect_list [instance, in MetaCoq.Template.utils.ReflectEq]
reflect_option [instance, in MetaCoq.Template.utils.ReflectEq]
reflect_reflectProp_2 [lemma, in MetaCoq.Template.utils.ReflectEq]
reflect_reflectProp_1 [lemma, in MetaCoq.Template.utils.ReflectEq]
reflect_reflectProp [lemma, in MetaCoq.Template.utils.ReflectEq]
reflect_Variance [instance, in MetaCoq.Template.Reflect]
reflect_allowed_eliminations [instance, in MetaCoq.Template.Reflect]
reflect_universes_decl [instance, in MetaCoq.Template.Reflect]
reflect_ConstraintType [instance, in MetaCoq.Template.Reflect]
reflect_recursivity_kind [instance, in MetaCoq.Template.Reflect]
reflect_case_info [instance, in MetaCoq.Template.Reflect]
reflect_cast_kind [instance, in MetaCoq.Template.Reflect]
reflect_def [instance, in MetaCoq.Template.Reflect]
reflect_aname [instance, in MetaCoq.Template.Reflect]
reflect_relevance [instance, in MetaCoq.Template.Reflect]
reflect_name [instance, in MetaCoq.Template.Reflect]
reflect_levels [instance, in MetaCoq.Template.Reflect]
reflect_prop_level [instance, in MetaCoq.Template.Reflect]
reflect_prim_float [instance, in MetaCoq.Template.Reflect]
reflect_prim_int [instance, in MetaCoq.Template.Reflect]
reflect_term [instance, in MetaCoq.Template.ReflectAst]
reflect_option_default [lemma, in MetaCoq.Template.utils.MCOption]
reflect_global_decl [instance, in MetaCoq.PCUIC.Syntax.PCUICReflect]
reflect_mutual_inductive_body [instance, in MetaCoq.PCUIC.Syntax.PCUICReflect]
reflect_one_inductive_body [instance, in MetaCoq.PCUIC.Syntax.PCUICReflect]
reflect_projection_body [instance, in MetaCoq.PCUIC.Syntax.PCUICReflect]
reflect_constructor_body [instance, in MetaCoq.PCUIC.Syntax.PCUICReflect]
reflect_constant_body [instance, in MetaCoq.PCUIC.Syntax.PCUICReflect]
reflect_eq_predicate [instance, in MetaCoq.PCUIC.Syntax.PCUICReflect]
reflect_prop_context_decl [lemma, in MetaCoq.PCUIC.Syntax.PCUICReflect]
reflect_prop_list [lemma, in MetaCoq.PCUIC.Syntax.PCUICReflect]
reflect_eq_float64 [instance, in MetaCoq.PCUIC.utils.PCUICPrimitive]
reflect_eq_spec_float [instance, in MetaCoq.PCUIC.utils.PCUICPrimitive]
reflect_eq_uint63 [instance, in MetaCoq.PCUIC.utils.PCUICPrimitive]
reflect_eq_Z [instance, in MetaCoq.PCUIC.utils.PCUICPrimitive]
reflect_global_decl [instance, in MetaCoq.Erasure.EReflect]
reflect_mutual_inductive_body [instance, in MetaCoq.Erasure.EReflect]
reflect_one_inductive_body [instance, in MetaCoq.Erasure.EReflect]
reflect_projection_body [instance, in MetaCoq.Erasure.EReflect]
reflect_constructor_body [instance, in MetaCoq.Erasure.EReflect]
reflect_constant_body [instance, in MetaCoq.Erasure.EReflect]
reflect_eq_term [lemma, in MetaCoq.SafeChecker.PCUICEqualityDec]
reflect_leq_term [lemma, in MetaCoq.SafeChecker.PCUICEqualityDec]
reflect_eqb_termp_napp [lemma, in MetaCoq.SafeChecker.PCUICEqualityDec]
reflect_eqb_ctx_gen [lemma, in MetaCoq.SafeChecker.PCUICEqualityDec]
reflect_eq_term_upto_univ [lemma, in MetaCoq.SafeChecker.PCUICEqualityDec]
reflect_R_global_instance [lemma, in MetaCoq.SafeChecker.PCUICEqualityDec]
reflect_eq_predicate [definition, in MetaCoq.SafeChecker.PCUICEqualityDec]
reflect_eq_ctx [lemma, in MetaCoq.SafeChecker.PCUICEqualityDec]
reflect_eq_context_IH [lemma, in MetaCoq.SafeChecker.PCUICEqualityDec]
Reflexive [record, in MetaCoq.Translations.MiniHoTT]
Reflexive [inductive, in MetaCoq.Translations.MiniHoTT]
Reflexive [record, in MetaCoq.Translations.MiniHoTT_paths]
Reflexive [inductive, in MetaCoq.Translations.MiniHoTT_paths]
reflexive_equiv [instance, in MetaCoq.Translations.MiniHoTT]
reflexive_paths [instance, in MetaCoq.Translations.MiniHoTT]
reflexive_equiv [instance, in MetaCoq.Translations.MiniHoTT_paths]
reflexive_paths [instance, in MetaCoq.Translations.MiniHoTT_paths]
reflexivity [projection, in MetaCoq.Translations.MiniHoTT]
reflexivity [constructor, in MetaCoq.Translations.MiniHoTT]
reflexivity [projection, in MetaCoq.Translations.MiniHoTT_paths]
reflexivity [constructor, in MetaCoq.Translations.MiniHoTT_paths]
refl_red [constructor, in MetaCoq.Template.Typing]
refl_eq_univ_prop [instance, in MetaCoq.PCUIC.PCUICCumulProp]
refl_redl [constructor, in MetaCoq.PCUIC.PCUICReduction]
refl_red [lemma, in MetaCoq.PCUIC.PCUICReduction]
refl':556 [binder, in MetaCoq.PCUIC.PCUICConfluence]
refl:555 [binder, in MetaCoq.PCUIC.PCUICConfluence]
refresh_universes [definition, in MetaCoq.Translations.times_bool_fun]
refresh_universes [definition, in MetaCoq.Translations.param_cheap_packed]
refresh_universes [definition, in MetaCoq.Translations.param_generous_packed]
ref:100 [binder, in MetaCoq.SafeChecker.PCUICWfEnv]
ref:1111 [binder, in MetaCoq.PCUIC.PCUICConversion]
ref:117 [binder, in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
ref:132 [binder, in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
ref:157 [binder, in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
ref:161 [binder, in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
ref:164 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
ref:167 [binder, in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
ref:178 [binder, in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
ref:217 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
ref:240 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
ref:255 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
ref:274 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
ref:279 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
ref:329 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
ref:355 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
ref:371 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
ref:376 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
ref:381 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
ref:58 [binder, in MetaCoq.PCUIC.PCUICPrincipality]
ref:87 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
ref:92 [binder, in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
ref:94 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
reify [definition, in MetaCoq.Examples.tauto]
reify_correct [definition, in MetaCoq.Examples.tauto]
relation [definition, in MetaCoq.Translations.MiniHoTT]
relation [definition, in MetaCoq.Translations.MiniHoTT_paths]
relation_disjunction_Symmetric [instance, in MetaCoq.Template.utils.MCRelations]
relation_disjunction_refl_r [instance, in MetaCoq.Template.utils.MCRelations]
relation_disjunction_refl_l [instance, in MetaCoq.Template.utils.MCRelations]
relation_equivalence_inclusion [lemma, in MetaCoq.Template.utils.MCRelations]
relevance [inductive, in MetaCoq.Template.BasicAst]
Relevant [constructor, in MetaCoq.Template.BasicAst]
reln_alt_eq [lemma, in MetaCoq.PCUIC.utils.PCUICAstUtils]
reln_alt [definition, in MetaCoq.PCUIC.utils.PCUICAstUtils]
reln_list_lift_above [lemma, in MetaCoq.PCUIC.utils.PCUICAstUtils]
reln_length [lemma, in MetaCoq.PCUIC.utils.PCUICAstUtils]
reln_set_binder_name [lemma, in MetaCoq.PCUIC.PCUICSR]
reln_lift [lemma, in MetaCoq.PCUIC.PCUICContexts]
reln_acc [lemma, in MetaCoq.PCUIC.PCUICContexts]
reln_app [lemma, in MetaCoq.PCUIC.PCUICContexts]
reln_subst [lemma, in MetaCoq.PCUIC.PCUICSpine]
relx:88 [binder, in MetaCoq.PCUIC.Syntax.PCUICReflect]
rely:92 [binder, in MetaCoq.PCUIC.Syntax.PCUICReflect]
rel_none [constructor, in MetaCoq.PCUIC.PCUICEquality]
rel_some [constructor, in MetaCoq.PCUIC.PCUICEquality]
rel_option [inductive, in MetaCoq.PCUIC.PCUICEquality]
rel:11 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
rel:16 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
rel:168 [binder, in MetaCoq.PCUIC.PCUICSafeLemmata]
rel:175 [binder, in MetaCoq.PCUIC.PCUICSafeLemmata]
rel:254 [binder, in MetaCoq.PCUIC.PCUICSafeLemmata]
rel:263 [binder, in MetaCoq.PCUIC.PCUICSafeLemmata]
rel:58 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
rel:69 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
rel:780 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
remaining_subst:10 [binder, in MetaCoq.Template.EtaExpand]
remaining:9 [binder, in MetaCoq.Template.EtaExpand]
removelast_length [lemma, in MetaCoq.PCUIC.utils.PCUICAstUtils]
remove_arity [definition, in MetaCoq.PCUIC.utils.PCUICAstUtils]
remove_last_last [lemma, in MetaCoq.Template.utils.MCList]
remove_last_app [lemma, in MetaCoq.Template.utils.MCList]
remove_last [definition, in MetaCoq.Template.utils.MCList]
remove_params_fast_optimization [definition, in MetaCoq.Erasure.ETransform]
remove_params_optimization [definition, in MetaCoq.Erasure.ETransform]
remove_last_length' [lemma, in MetaCoq.Erasure.EWcbvEval]
remove_last_length [lemma, in MetaCoq.Erasure.EWcbvEval]
remove_arity [definition, in MetaCoq.Template.AstUtils]
remove_last_n [definition, in MetaCoq.Examples.add_constructor]
ren [definition, in MetaCoq.PCUIC.PCUICSigmaCalculus]
rename [definition, in MetaCoq.PCUIC.PCUICSigmaCalculus]
rename_telescope [lemma, in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
rename_context_length [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
rename_subst_compose3 [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
rename_subst_compose2 [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
rename_subst_compose1 [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
rename_idsn_idsn [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
rename_inst_assoc [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
rename_ren_id [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
rename_inst [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
rename_shiftn [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
rename_branches_rename_branches [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
rename_branch_rename_branch [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
rename_predicate_rename_predicate [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
rename_compose [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
rename_branch_proper [instance, in MetaCoq.PCUIC.PCUICSigmaCalculus]
rename_predicate_proper [instance, in MetaCoq.PCUIC.PCUICSigmaCalculus]
rename_proper_pointwise [instance, in MetaCoq.PCUIC.PCUICSigmaCalculus]
rename_proper [instance, in MetaCoq.PCUIC.PCUICSigmaCalculus]
rename_branch [abbreviation, in MetaCoq.PCUIC.PCUICSigmaCalculus]
rename_ext [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
rename_telescope [definition, in MetaCoq.PCUIC.PCUICSigmaCalculus]
rename_decl [definition, in MetaCoq.PCUIC.PCUICSigmaCalculus]
rename_context [definition, in MetaCoq.PCUIC.PCUICSigmaCalculus]
rename_branches [abbreviation, in MetaCoq.PCUIC.PCUICSigmaCalculus]
rename_predicate [abbreviation, in MetaCoq.PCUIC.PCUICSigmaCalculus]
rename_context_on_free_vars [lemma, in MetaCoq.PCUIC.Conversion.PCUICOnFreeVarsConv]
rename_on_free_vars [lemma, in MetaCoq.PCUIC.Conversion.PCUICOnFreeVarsConv]
rename_ext_cond [lemma, in MetaCoq.PCUIC.Conversion.PCUICOnFreeVarsConv]
rename_context_lift_context [lemma, in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
rename_context_inst_context [lemma, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
rename_decl_inst_decl [lemma, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
rename_telescope_cons [lemma, in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
rename_telescope_shiftn0 [lemma, in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
rename_telescope_ext [instance, in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
rename_subst_telescope [lemma, in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
rename_wf_cofixpoint [lemma, in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
rename_wf_fixpoint [lemma, in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
rename_check_one_cofix [lemma, in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
rename_check_one_fix [lemma, in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
rename_smash_context [lemma, in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
rename_app_context [lemma, in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
rename_decompose_prod_assum [lemma, in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
rename_predicate_preturn [lemma, in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
rename_case_branch_type [lemma, in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
rename_case_predicate_context [lemma, in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
rename_ind_predicate_context [lemma, in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
rename_iota_red [lemma, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
rename_extended_subst [lemma, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
rename_predicate_set_preturn [lemma, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
rename_predicate_set_pparams [lemma, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
rename_compose [lemma, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
rename_wf_branches [lemma, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
rename_wf_branch [lemma, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
rename_wf_predicate [lemma, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
rename_it_mkProd_or_LetIn [lemma, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
rename_mkProd_or_LetIn [lemma, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
rename_it_mkLambda_or_LetIn [lemma, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
rename_mkLambda_or_LetIn [lemma, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
rename_closed_constructor_body [lemma, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
rename_case_branch_context_gen [lemma, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
rename_cstr_branch_context [lemma, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
rename_inst_case_context_wf [lemma, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
rename_inst_case_context [lemma, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
rename_context_set_binder_name [lemma, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
rename_to_extended_list [lemma, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
rename_reln [lemma, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
rename_cstr_args [lemma, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
rename_context_subst_k [lemma, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
rename_context_subst_instance [lemma, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
rename_context_ext [instance, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
rename_inds [lemma, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
rename_context_lift [lemma, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
rename_shiftnk [lemma, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
rename_context_subst [lemma, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
rename_subst [lemma, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
rename_constructor_body [definition, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
rename_unfold_cofix [lemma, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
rename_unfold_fix [lemma, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
rename_branch [definition, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
rename_closed_extended_subst [lemma, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
rename_closedn_terms [lemma, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
rename_closedn_ctx [lemma, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
rename_closed_decl [lemma, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
rename_closed [lemma, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
rename_closedn [lemma, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
rename_fix_context [lemma, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
rename_context_decl_body [lemma, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
rename_context_nth_error [lemma, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
rename_subst10 [lemma, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
rename_subst0 [lemma, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
rename_context_telescope [lemma, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
rename_context_alt [lemma, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
rename_context_snoc [lemma, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
rename_context_snoc0 [lemma, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
rename_subst_instance [lemma, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
rename_mkApps [lemma, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
rename_rho_iota_red [lemma, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rename_rho_ctx_over [lemma, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rename_rho_ctx [lemma, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rename_decl [definition, in MetaCoq.Template.Pretty]
rename_decl [definition, in MetaCoq.PCUIC.utils.PCUICPretty]
renaming [definition, in MetaCoq.PCUIC.Syntax.PCUICRenameDef]
Renaming [section, in MetaCoq.PCUIC.Syntax.PCUICRenameDef]
Renaming [section, in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
Renaming [section, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
renaming [definition, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
renaming_vdef [lemma, in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
renaming_vass [lemma, in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
renaming_extP [lemma, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
renaming_shift_rho_fix_context [lemma, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
renaming_ext [instance, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
Renaming2 [section, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
ren_lift_renaming [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
ren_subst_consn_comm [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
ren_rshiftk [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
ren_shiftk [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
ren_shift [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
ren_idsn_consn_lt [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
ren_ids_lt [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
ren_ids_length [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
ren_ids [definition, in MetaCoq.PCUIC.PCUICSigmaCalculus]
ren_consn_lt [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
ren_id_ids [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
ren_id [definition, in MetaCoq.PCUIC.PCUICSigmaCalculus]
ren_shiftn [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
ren_ext [instance, in MetaCoq.PCUIC.PCUICSigmaCalculus]
ren_fn [definition, in MetaCoq.PCUIC.PCUICSigmaCalculus]
repack [abbreviation, in MetaCoq.SafeChecker.PCUICSafeConversion]
repeat_snoc [lemma, in MetaCoq.PCUIC.Syntax.PCUICPosition]
replace [definition, in MetaCoq.Translations.times_bool_fun]
replace [definition, in MetaCoq.Translations.param_cheap_packed]
Req [definition, in MetaCoq.SafeChecker.PCUICSafeReduce]
Req_red [lemma, in MetaCoq.SafeChecker.PCUICSafeReduce]
Req_refl [instance, in MetaCoq.SafeChecker.PCUICSafeReduce]
Req_trans [lemma, in MetaCoq.SafeChecker.PCUICSafeReduce]
Req:1109 [binder, in MetaCoq.PCUIC.PCUICConversion]
result [inductive, in MetaCoq.Examples.tauto]
res:101 [binder, in MetaCoq.Template.WcbvEval]
res:102 [binder, in MetaCoq.Erasure.EWcbvEval]
res:104 [binder, in MetaCoq.Erasure.EWcbvEvalInd]
res:107 [binder, in MetaCoq.Erasure.EWcbvEval]
res:112 [binder, in MetaCoq.Erasure.EWcbvEvalInd]
res:113 [binder, in MetaCoq.Erasure.EWcbvEval]
res:114 [binder, in MetaCoq.Template.Checker]
res:116 [binder, in MetaCoq.Erasure.EWcbvEvalInd]
res:117 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
res:119 [binder, in MetaCoq.Template.WcbvEval]
res:119 [binder, in MetaCoq.Erasure.EWcbvEval]
res:122 [binder, in MetaCoq.Erasure.EWcbvEvalInd]
res:125 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
res:127 [binder, in MetaCoq.Template.WcbvEval]
res:134 [binder, in MetaCoq.Erasure.EWcbvEvalInd]
res:147 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
res:150 [binder, in MetaCoq.Template.WcbvEval]
res:152 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
res:156 [binder, in MetaCoq.Template.WcbvEval]
res:161 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
res:161 [binder, in MetaCoq.Template.WcbvEval]
res:169 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
res:173 [binder, in MetaCoq.Template.WcbvEval]
res:177 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
res:186 [binder, in MetaCoq.Template.WcbvEval]
res:19 [binder, in MetaCoq.Erasure.EWcbvEvalInd]
res:193 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
res:195 [binder, in MetaCoq.Template.WcbvEval]
res:202 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
res:210 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
res:213 [binder, in MetaCoq.Template.WcbvEval]
res:214 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
res:220 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
res:221 [binder, in MetaCoq.Template.WcbvEval]
res:25 [binder, in MetaCoq.Erasure.EWcbvEvalInd]
res:28 [binder, in MetaCoq.Erasure.EWcbvEval]
res:326 [binder, in MetaCoq.Erasure.EArities]
res:33 [binder, in MetaCoq.Erasure.EWcbvEval]
res:34 [binder, in MetaCoq.Erasure.EWcbvEvalInd]
res:42 [binder, in MetaCoq.Erasure.EWcbvEval]
res:50 [binder, in MetaCoq.Erasure.EWcbvEvalInd]
res:51 [binder, in MetaCoq.Erasure.EWcbvEval]
res:535 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
res:541 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
res:546 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
res:57 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
res:57 [binder, in MetaCoq.Template.WcbvEval]
res:58 [binder, in MetaCoq.Erasure.EWcbvEval]
res:6 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
res:61 [binder, in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
res:63 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
res:63 [binder, in MetaCoq.Template.WcbvEval]
res:64 [binder, in MetaCoq.Erasure.EWcbvEvalInd]
res:66 [binder, in MetaCoq.Template.Checker]
res:66 [binder, in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
res:66 [binder, in MetaCoq.Erasure.EWcbvEval]
res:69 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
res:69 [binder, in MetaCoq.Template.WcbvEval]
res:7 [binder, in MetaCoq.PCUIC.PCUICProgress]
res:70 [binder, in MetaCoq.Template.Checker]
res:72 [binder, in MetaCoq.Erasure.EWcbvEvalInd]
res:75 [binder, in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
res:77 [binder, in MetaCoq.Template.Checker]
res:81 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
res:81 [binder, in MetaCoq.Template.WcbvEval]
res:83 [binder, in MetaCoq.Template.Checker]
res:83 [binder, in MetaCoq.Erasure.EWcbvEval]
res:87 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
res:88 [binder, in MetaCoq.Template.WcbvEval]
res:89 [binder, in MetaCoq.Template.Checker]
res:91 [binder, in MetaCoq.Erasure.EWcbvEvalInd]
res:923 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
res:94 [binder, in MetaCoq.Erasure.EWcbvEval]
res:99 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
ret [abbreviation, in MetaCoq.SafeChecker.PCUICSafeRetyping]
Ret [definition, in MetaCoq.SafeChecker.PCUICSafeConversion]
ret [projection, in MetaCoq.Template.monad_utils]
ret [abbreviation, in MetaCoq.SafeChecker.PCUICTypeChecker]
retract [definition, in MetaCoq.Translations.times_bool_fun2]
ret_binders:73 [binder, in MetaCoq.Template.Pretty]
ret_binders:80 [binder, in MetaCoq.PCUIC.utils.PCUICPretty]
ret':643 [binder, in MetaCoq.PCUIC.PCUICSR]
ret:189 [binder, in MetaCoq.PCUIC.PCUICAlpha]
ret:199 [binder, in MetaCoq.PCUIC.PCUICAlpha]
ret:642 [binder, in MetaCoq.PCUIC.PCUICSR]
rev [definition, in MetaCoq.Template.utils.MCList]
Reverse_Induction [section, in MetaCoq.Template.utils.MCList]
Reverse_Induction.rev_involutive [variable, in MetaCoq.PCUIC.Syntax.PCUICInduction]
Reverse_Induction.rev_unit [variable, in MetaCoq.PCUIC.Syntax.PCUICInduction]
Reverse_Induction.rev_app_distr [variable, in MetaCoq.PCUIC.Syntax.PCUICInduction]
Reverse_Induction.app_assoc [variable, in MetaCoq.PCUIC.Syntax.PCUICInduction]
Reverse_Induction.app_nil_r [variable, in MetaCoq.PCUIC.Syntax.PCUICInduction]
Reverse_Induction.A [variable, in MetaCoq.PCUIC.Syntax.PCUICInduction]
Reverse_Induction [section, in MetaCoq.PCUIC.Syntax.PCUICInduction]
rev_Forall [lemma, in MetaCoq.Template.utils.All_Forall]
rev_repeat [lemma, in MetaCoq.Template.utils.MCList]
rev_case [lemma, in MetaCoq.Template.utils.MCList]
rev_invol [lemma, in MetaCoq.Template.utils.MCList]
rev_app [lemma, in MetaCoq.Template.utils.MCList]
rev_map_spec [lemma, in MetaCoq.Template.utils.MCList]
rev_mapi [lemma, in MetaCoq.Template.utils.MCList]
rev_mapi_rec [lemma, in MetaCoq.Template.utils.MCList]
rev_ind [lemma, in MetaCoq.Template.utils.MCList]
rev_list_ind [lemma, in MetaCoq.Template.utils.MCList]
rev_map_app [lemma, in MetaCoq.Template.utils.MCList]
rev_map_length [lemma, in MetaCoq.Template.utils.MCList]
rev_length [lemma, in MetaCoq.Template.utils.MCList]
rev_map_cons [lemma, in MetaCoq.Template.utils.MCList]
rev_cons [lemma, in MetaCoq.Template.utils.MCList]
rev_map [definition, in MetaCoq.Template.utils.MCList]
rev_repeat [lemma, in MetaCoq.PCUIC.Syntax.PCUICPosition]
rev_inj [lemma, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
rev_subst_instance [lemma, in MetaCoq.PCUIC.Syntax.PCUICUnivSubst]
rev_rec [lemma, in MetaCoq.PCUIC.Syntax.PCUICInduction]
rev_list_ind [lemma, in MetaCoq.PCUIC.Syntax.PCUICInduction]
Re':175 [binder, in MetaCoq.Template.TermEquality]
Re':182 [binder, in MetaCoq.Template.TermEquality]
Re':191 [binder, in MetaCoq.Template.TermEquality]
Re':210 [binder, in MetaCoq.Template.TermEquality]
Re':218 [binder, in MetaCoq.Template.TermEquality]
Re':247 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
Re':337 [binder, in MetaCoq.PCUIC.PCUICEquality]
Re':344 [binder, in MetaCoq.PCUIC.PCUICEquality]
Re':355 [binder, in MetaCoq.PCUIC.PCUICEquality]
Re':370 [binder, in MetaCoq.PCUIC.PCUICEquality]
Re':377 [binder, in MetaCoq.PCUIC.PCUICEquality]
Re':45 [binder, in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
Re':53 [binder, in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
Re':637 [binder, in MetaCoq.PCUIC.PCUICEquality]
Re:10 [binder, in MetaCoq.Template.TermEquality]
Re:105 [binder, in MetaCoq.PCUIC.PCUICAlpha]
Re:1115 [binder, in MetaCoq.PCUIC.PCUICConversion]
Re:112 [binder, in MetaCoq.PCUIC.PCUICEquality]
Re:116 [binder, in MetaCoq.PCUIC.PCUICEquality]
Re:120 [binder, in MetaCoq.PCUIC.PCUICConfluence]
Re:122 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
Re:14 [binder, in MetaCoq.PCUIC.PCUICEquality]
Re:142 [binder, in MetaCoq.PCUIC.PCUICConfluence]
Re:151 [binder, in MetaCoq.Template.TermEquality]
Re:152 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
Re:161 [binder, in MetaCoq.Template.TermEquality]
Re:173 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
Re:174 [binder, in MetaCoq.Template.TermEquality]
Re:181 [binder, in MetaCoq.Template.TermEquality]
Re:187 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
Re:19 [binder, in MetaCoq.PCUIC.PCUICAlpha]
Re:190 [binder, in MetaCoq.Template.TermEquality]
Re:190 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
Re:205 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
Re:209 [binder, in MetaCoq.Template.TermEquality]
Re:217 [binder, in MetaCoq.Template.TermEquality]
Re:218 [binder, in MetaCoq.PCUIC.PCUICEquality]
Re:225 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
Re:229 [binder, in MetaCoq.PCUIC.PCUICEquality]
Re:229 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
Re:230 [binder, in MetaCoq.Template.TermEquality]
Re:230 [binder, in MetaCoq.PCUIC.PCUICEquality]
Re:231 [binder, in MetaCoq.PCUIC.PCUICEquality]
Re:233 [binder, in MetaCoq.PCUIC.PCUICAlpha]
Re:237 [binder, in MetaCoq.PCUIC.PCUICEquality]
Re:238 [binder, in MetaCoq.PCUIC.PCUICAlpha]
Re:240 [binder, in MetaCoq.PCUIC.PCUICEquality]
Re:242 [binder, in MetaCoq.Template.TermEquality]
Re:245 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
Re:248 [binder, in MetaCoq.PCUIC.PCUICEquality]
Re:261 [binder, in MetaCoq.PCUIC.PCUICEquality]
Re:264 [binder, in MetaCoq.PCUIC.PCUICEquality]
Re:269 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
Re:27 [binder, in MetaCoq.PCUIC.PCUICEquality]
Re:270 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
Re:270 [binder, in MetaCoq.PCUIC.PCUICEquality]
Re:277 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
Re:282 [binder, in MetaCoq.PCUIC.PCUICEquality]
Re:285 [binder, in MetaCoq.PCUIC.PCUICEquality]
Re:285 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
Re:287 [binder, in MetaCoq.PCUIC.PCUICConfluence]
Re:288 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
Re:29 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
Re:293 [binder, in MetaCoq.PCUIC.PCUICEquality]
Re:293 [binder, in MetaCoq.PCUIC.PCUICConfluence]
Re:294 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
Re:296 [binder, in MetaCoq.PCUIC.PCUICConversion]
Re:299 [binder, in MetaCoq.PCUIC.PCUICConfluence]
Re:3 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
Re:30 [binder, in MetaCoq.Template.TermEquality]
Re:300 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
Re:301 [binder, in MetaCoq.PCUIC.PCUICConversion]
Re:308 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
Re:309 [binder, in MetaCoq.PCUIC.PCUICEquality]
Re:317 [binder, in MetaCoq.PCUIC.PCUICConfluence]
Re:317 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
Re:318 [binder, in MetaCoq.PCUIC.PCUICEquality]
Re:32 [binder, in MetaCoq.PCUIC.PCUICEquality]
Re:322 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
Re:324 [binder, in MetaCoq.PCUIC.PCUICEquality]
Re:327 [binder, in MetaCoq.PCUIC.PCUICConfluence]
Re:327 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
Re:335 [binder, in MetaCoq.PCUIC.PCUICConfluence]
Re:336 [binder, in MetaCoq.PCUIC.PCUICEquality]
Re:34 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
Re:341 [binder, in MetaCoq.PCUIC.PCUICConfluence]
Re:343 [binder, in MetaCoq.PCUIC.PCUICEquality]
Re:347 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
Re:349 [binder, in MetaCoq.PCUIC.PCUICConfluence]
Re:35 [binder, in MetaCoq.Template.TermEquality]
Re:354 [binder, in MetaCoq.PCUIC.PCUICEquality]
Re:36 [binder, in MetaCoq.PCUIC.PCUICSafeLemmata]
Re:369 [binder, in MetaCoq.PCUIC.PCUICEquality]
Re:374 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
Re:376 [binder, in MetaCoq.PCUIC.PCUICEquality]
Re:38 [binder, in MetaCoq.PCUIC.PCUICSafeLemmata]
Re:38 [binder, in MetaCoq.PCUIC.PCUICAlpha]
Re:383 [binder, in MetaCoq.PCUIC.PCUICEquality]
Re:384 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
Re:4 [binder, in MetaCoq.Template.TermEquality]
Re:402 [binder, in MetaCoq.PCUIC.PCUICEquality]
Re:42 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
Re:44 [binder, in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
Re:456 [binder, in MetaCoq.PCUIC.PCUICEquality]
Re:465 [binder, in MetaCoq.PCUIC.PCUICEquality]
Re:47 [binder, in MetaCoq.PCUIC.PCUICSN]
Re:48 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
Re:485 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
Re:487 [binder, in MetaCoq.PCUIC.PCUICEquality]
Re:493 [binder, in MetaCoq.PCUIC.PCUICEquality]
Re:499 [binder, in MetaCoq.PCUIC.PCUICEquality]
Re:507 [binder, in MetaCoq.PCUIC.PCUICEquality]
Re:516 [binder, in MetaCoq.PCUIC.PCUICEquality]
Re:52 [binder, in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
Re:523 [binder, in MetaCoq.PCUIC.PCUICConfluence]
Re:525 [binder, in MetaCoq.PCUIC.PCUICEquality]
Re:527 [binder, in MetaCoq.PCUIC.PCUICNormal]
Re:532 [binder, in MetaCoq.PCUIC.PCUICEquality]
Re:535 [binder, in MetaCoq.PCUIC.PCUICNormal]
Re:535 [binder, in MetaCoq.PCUIC.PCUICConfluence]
Re:540 [binder, in MetaCoq.PCUIC.PCUICEquality]
Re:544 [binder, in MetaCoq.PCUIC.PCUICConfluence]
Re:55 [binder, in MetaCoq.PCUIC.PCUICSN]
Re:552 [binder, in MetaCoq.PCUIC.PCUICEquality]
Re:553 [binder, in MetaCoq.PCUIC.PCUICConfluence]
Re:555 [binder, in MetaCoq.PCUIC.PCUICEquality]
Re:56 [binder, in MetaCoq.PCUIC.PCUICPrincipality]
Re:568 [binder, in MetaCoq.PCUIC.PCUICEquality]
Re:58 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
Re:581 [binder, in MetaCoq.PCUIC.PCUICEquality]
Re:586 [binder, in MetaCoq.PCUIC.PCUICEquality]
Re:589 [binder, in MetaCoq.PCUIC.PCUICEquality]
Re:592 [binder, in MetaCoq.PCUIC.PCUICEquality]
Re:595 [binder, in MetaCoq.PCUIC.PCUICEquality]
Re:602 [binder, in MetaCoq.PCUIC.PCUICEquality]
Re:605 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
Re:609 [binder, in MetaCoq.PCUIC.PCUICEquality]
Re:612 [binder, in MetaCoq.PCUIC.PCUICEquality]
Re:617 [binder, in MetaCoq.PCUIC.PCUICEquality]
Re:630 [binder, in MetaCoq.PCUIC.PCUICEquality]
Re:636 [binder, in MetaCoq.PCUIC.PCUICEquality]
Re:64 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
Re:64 [binder, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
Re:641 [binder, in MetaCoq.PCUIC.PCUICEquality]
Re:644 [binder, in MetaCoq.PCUIC.PCUICEquality]
Re:652 [binder, in MetaCoq.PCUIC.PCUICEquality]
Re:652 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
Re:666 [binder, in MetaCoq.PCUIC.PCUICEquality]
Re:668 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
Re:673 [binder, in MetaCoq.PCUIC.PCUICEquality]
Re:674 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
Re:677 [binder, in MetaCoq.PCUIC.PCUICEquality]
Re:681 [binder, in MetaCoq.PCUIC.PCUICEquality]
Re:683 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
Re:685 [binder, in MetaCoq.PCUIC.PCUICEquality]
Re:69 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
Re:691 [binder, in MetaCoq.PCUIC.PCUICEquality]
Re:699 [binder, in MetaCoq.PCUIC.PCUICEquality]
Re:72 [binder, in MetaCoq.Template.TermEquality]
Re:75 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
Re:77 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
Re:79 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
Re:8 [binder, in MetaCoq.PCUIC.PCUICEquality]
Re:84 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
Re:86 [binder, in MetaCoq.PCUIC.PCUICConvCumInversion]
rho [definition, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
Rho [section, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rhoargs:693 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho_ws_pair [definition, in MetaCoq.PCUIC.PCUICConfluence]
rho_ctx [abbreviation, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho_inst_case_context [lemma, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho_All_All2_fold_inv [lemma, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho_triangle_All_All2_ind_terms [lemma, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho_triangle_All_All2_ind [lemma, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho_fix_subst [lemma, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho_cofix_subst [lemma, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho_ctx_app [lemma, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho_ctx_over_app [lemma, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho_lift0 [lemma, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho_rename [lemma, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho_rename_pred [lemma, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho_ctx_rename [lemma, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho_app_proj [lemma, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho_app_case [lemma, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho_fix_elim [lemma, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho_fix_stuck [constructor, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho_fix_red [constructor, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho_fix_spec [inductive, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho_app_fix [lemma, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho_app_cofix [lemma, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho_app_construct [lemma, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho_app_lambda' [lemma, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho_app_lambda [lemma, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho_fix_context_length [lemma, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho_fix_context [definition, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho_ctx_over_length [lemma, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho_iota_red [abbreviation, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho_ctx [abbreviation, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho_ctx_over [abbreviation, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho_br [abbreviation, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho_predicate [abbreviation, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho_iota_red_wf_gen [lemma, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho_iota_red_gen [definition, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho_iota_red_wf [definition, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho_predicate_map_predicate [lemma, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho_predicate_gen [definition, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho_predicate_wf [definition, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho_ctx_over_wf_eq [lemma, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho_ctx_over_wf [definition, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
Rho.All2_telescope_n [section, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
Rho.All2_telescope [section, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
Rho.rho_ctx [section, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho:1 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho:123 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho:132 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho:151 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho:159 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho:164 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho:171 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho:177 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho:182 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho:193 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho:200 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho:211 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho:217 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho:222 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho:231 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho:243 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho:252 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho:259 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rho:637 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rh1:86 [binder, in MetaCoq.Examples.tauto]
rh2:87 [binder, in MetaCoq.Examples.tauto]
rh:102 [binder, in MetaCoq.Examples.tauto]
rh:59 [binder, in MetaCoq.Examples.tauto]
rh:65 [binder, in MetaCoq.Examples.tauto]
rh:84 [binder, in MetaCoq.Examples.tauto]
rh:91 [binder, in MetaCoq.Examples.tauto]
right_dlexmod [constructor, in MetaCoq.PCUIC.utils.PCUICUtils]
right_lex [constructor, in MetaCoq.PCUIC.utils.PCUICUtils]
rigid_head [definition, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
rk':162 [binder, in MetaCoq.PCUIC.PCUICCanonicity]
rk:161 [binder, in MetaCoq.PCUIC.PCUICCanonicity]
Rle':177 [binder, in MetaCoq.Template.TermEquality]
Rle':193 [binder, in MetaCoq.Template.TermEquality]
Rle':212 [binder, in MetaCoq.Template.TermEquality]
Rle':220 [binder, in MetaCoq.Template.TermEquality]
Rle':248 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
Rle':339 [binder, in MetaCoq.PCUIC.PCUICEquality]
Rle':346 [binder, in MetaCoq.PCUIC.PCUICEquality]
Rle':357 [binder, in MetaCoq.PCUIC.PCUICEquality]
Rle':372 [binder, in MetaCoq.PCUIC.PCUICEquality]
Rle':379 [binder, in MetaCoq.PCUIC.PCUICEquality]
Rle':47 [binder, in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
Rle':55 [binder, in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
Rle':639 [binder, in MetaCoq.PCUIC.PCUICEquality]
Rle':693 [binder, in MetaCoq.PCUIC.PCUICEquality]
Rle':701 [binder, in MetaCoq.PCUIC.PCUICEquality]
Rle:106 [binder, in MetaCoq.PCUIC.PCUICAlpha]
Rle:11 [binder, in MetaCoq.Template.TermEquality]
Rle:1110 [binder, in MetaCoq.PCUIC.PCUICConversion]
Rle:1116 [binder, in MetaCoq.PCUIC.PCUICConversion]
Rle:117 [binder, in MetaCoq.PCUIC.PCUICEquality]
Rle:121 [binder, in MetaCoq.PCUIC.PCUICConfluence]
Rle:123 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
Rle:133 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
Rle:141 [binder, in MetaCoq.PCUIC.PCUICConfluence]
Rle:15 [binder, in MetaCoq.PCUIC.PCUICEquality]
Rle:152 [binder, in MetaCoq.Template.TermEquality]
Rle:153 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
Rle:162 [binder, in MetaCoq.Template.TermEquality]
Rle:172 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
Rle:176 [binder, in MetaCoq.Template.TermEquality]
Rle:179 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
Rle:191 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
Rle:192 [binder, in MetaCoq.Template.TermEquality]
Rle:20 [binder, in MetaCoq.PCUIC.PCUICAlpha]
Rle:206 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
Rle:211 [binder, in MetaCoq.Template.TermEquality]
Rle:219 [binder, in MetaCoq.Template.TermEquality]
Rle:219 [binder, in MetaCoq.PCUIC.PCUICEquality]
Rle:226 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
Rle:230 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
Rle:231 [binder, in MetaCoq.Template.TermEquality]
Rle:239 [binder, in MetaCoq.PCUIC.PCUICAlpha]
Rle:241 [binder, in MetaCoq.PCUIC.PCUICEquality]
Rle:243 [binder, in MetaCoq.Template.TermEquality]
Rle:246 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
Rle:249 [binder, in MetaCoq.PCUIC.PCUICEquality]
Rle:252 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
Rle:256 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
Rle:260 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
Rle:262 [binder, in MetaCoq.PCUIC.PCUICEquality]
Rle:270 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
Rle:271 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
Rle:271 [binder, in MetaCoq.PCUIC.PCUICEquality]
Rle:275 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
Rle:278 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
Rle:278 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
Rle:28 [binder, in MetaCoq.PCUIC.PCUICEquality]
Rle:281 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
Rle:283 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
Rle:286 [binder, in MetaCoq.PCUIC.PCUICEquality]
Rle:286 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
Rle:288 [binder, in MetaCoq.PCUIC.PCUICConfluence]
Rle:289 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
Rle:294 [binder, in MetaCoq.PCUIC.PCUICConfluence]
Rle:295 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
Rle:297 [binder, in MetaCoq.PCUIC.PCUICConversion]
Rle:3 [binder, in MetaCoq.PCUIC.PCUICCumulativity]
Rle:30 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
Rle:300 [binder, in MetaCoq.PCUIC.PCUICConfluence]
Rle:301 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
Rle:302 [binder, in MetaCoq.PCUIC.PCUICConversion]
Rle:308 [binder, in MetaCoq.PCUIC.PCUICConfluence]
Rle:309 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
Rle:31 [binder, in MetaCoq.Template.TermEquality]
Rle:310 [binder, in MetaCoq.PCUIC.PCUICEquality]
Rle:318 [binder, in MetaCoq.PCUIC.PCUICConfluence]
Rle:319 [binder, in MetaCoq.PCUIC.PCUICEquality]
Rle:325 [binder, in MetaCoq.PCUIC.PCUICEquality]
Rle:328 [binder, in MetaCoq.PCUIC.PCUICConfluence]
Rle:328 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
Rle:33 [binder, in MetaCoq.PCUIC.PCUICEquality]
Rle:336 [binder, in MetaCoq.PCUIC.PCUICConfluence]
Rle:338 [binder, in MetaCoq.PCUIC.PCUICEquality]
Rle:342 [binder, in MetaCoq.PCUIC.PCUICConfluence]
Rle:345 [binder, in MetaCoq.PCUIC.PCUICEquality]
Rle:350 [binder, in MetaCoq.PCUIC.PCUICConfluence]
Rle:356 [binder, in MetaCoq.PCUIC.PCUICEquality]
Rle:36 [binder, in MetaCoq.Template.TermEquality]
Rle:371 [binder, in MetaCoq.PCUIC.PCUICEquality]
Rle:375 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
Rle:378 [binder, in MetaCoq.PCUIC.PCUICEquality]
Rle:384 [binder, in MetaCoq.PCUIC.PCUICEquality]
Rle:385 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
Rle:389 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
Rle:39 [binder, in MetaCoq.PCUIC.PCUICAlpha]
Rle:392 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
Rle:393 [binder, in MetaCoq.PCUIC.PCUICEquality]
Rle:394 [binder, in MetaCoq.PCUIC.PCUICConfluence]
Rle:397 [binder, in MetaCoq.PCUIC.PCUICEquality]
Rle:40 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
Rle:403 [binder, in MetaCoq.PCUIC.PCUICEquality]
Rle:415 [binder, in MetaCoq.PCUIC.PCUICConfluence]
Rle:43 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
Rle:445 [binder, in MetaCoq.PCUIC.PCUICEquality]
Rle:450 [binder, in MetaCoq.PCUIC.PCUICEquality]
Rle:457 [binder, in MetaCoq.PCUIC.PCUICEquality]
Rle:46 [binder, in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
Rle:466 [binder, in MetaCoq.PCUIC.PCUICEquality]
Rle:466 [binder, in MetaCoq.PCUIC.PCUICConfluence]
Rle:48 [binder, in MetaCoq.PCUIC.PCUICSN]
Rle:486 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
Rle:487 [binder, in MetaCoq.PCUIC.PCUICConfluence]
Rle:488 [binder, in MetaCoq.PCUIC.PCUICEquality]
Rle:49 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
Rle:494 [binder, in MetaCoq.PCUIC.PCUICEquality]
Rle:5 [binder, in MetaCoq.Template.TermEquality]
Rle:500 [binder, in MetaCoq.PCUIC.PCUICEquality]
Rle:508 [binder, in MetaCoq.PCUIC.PCUICEquality]
Rle:517 [binder, in MetaCoq.PCUIC.PCUICEquality]
Rle:524 [binder, in MetaCoq.PCUIC.PCUICConfluence]
Rle:526 [binder, in MetaCoq.PCUIC.PCUICEquality]
Rle:528 [binder, in MetaCoq.PCUIC.PCUICNormal]
Rle:533 [binder, in MetaCoq.PCUIC.PCUICEquality]
Rle:536 [binder, in MetaCoq.PCUIC.PCUICNormal]
Rle:536 [binder, in MetaCoq.PCUIC.PCUICConfluence]
Rle:54 [binder, in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
Rle:541 [binder, in MetaCoq.PCUIC.PCUICEquality]
Rle:545 [binder, in MetaCoq.PCUIC.PCUICConfluence]
Rle:553 [binder, in MetaCoq.PCUIC.PCUICEquality]
Rle:554 [binder, in MetaCoq.PCUIC.PCUICConfluence]
Rle:556 [binder, in MetaCoq.PCUIC.PCUICEquality]
Rle:569 [binder, in MetaCoq.PCUIC.PCUICEquality]
Rle:57 [binder, in MetaCoq.PCUIC.PCUICPrincipality]
Rle:582 [binder, in MetaCoq.PCUIC.PCUICEquality]
Rle:587 [binder, in MetaCoq.PCUIC.PCUICEquality]
Rle:590 [binder, in MetaCoq.PCUIC.PCUICEquality]
Rle:593 [binder, in MetaCoq.PCUIC.PCUICEquality]
Rle:596 [binder, in MetaCoq.PCUIC.PCUICEquality]
Rle:603 [binder, in MetaCoq.PCUIC.PCUICEquality]
Rle:606 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
Rle:610 [binder, in MetaCoq.PCUIC.PCUICEquality]
Rle:613 [binder, in MetaCoq.PCUIC.PCUICEquality]
Rle:618 [binder, in MetaCoq.PCUIC.PCUICEquality]
Rle:63 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
Rle:631 [binder, in MetaCoq.PCUIC.PCUICEquality]
Rle:638 [binder, in MetaCoq.PCUIC.PCUICEquality]
Rle:642 [binder, in MetaCoq.PCUIC.PCUICEquality]
Rle:645 [binder, in MetaCoq.PCUIC.PCUICEquality]
Rle:65 [binder, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
Rle:653 [binder, in MetaCoq.PCUIC.PCUICEquality]
Rle:653 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
Rle:667 [binder, in MetaCoq.PCUIC.PCUICEquality]
Rle:669 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
Rle:675 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
Rle:684 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
Rle:688 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
Rle:691 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
Rle:692 [binder, in MetaCoq.PCUIC.PCUICEquality]
Rle:70 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
Rle:70 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
Rle:70 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
Rle:700 [binder, in MetaCoq.PCUIC.PCUICEquality]
Rle:73 [binder, in MetaCoq.Template.TermEquality]
Rle:73 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
Rle:76 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
Rle:78 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
Rle:80 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
Rle:85 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
Rle:87 [binder, in MetaCoq.PCUIC.PCUICConvCumInversion]
Rle:9 [binder, in MetaCoq.PCUIC.PCUICEquality]
rshiftk [definition, in MetaCoq.PCUIC.PCUICSigmaCalculus]
rshiftk_S [lemma, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
rshiftk_proper [instance, in MetaCoq.PCUIC.PCUICSigmaCalculus]
rs:2866 [binder, in MetaCoq.Translations.MiniHoTT]
rs:2874 [binder, in MetaCoq.Translations.MiniHoTT_paths]
Rtrans [lemma, in MetaCoq.SafeChecker.PCUICSafeReduce]
rtrans_clos [abbreviation, in MetaCoq.PCUIC.utils.PCUICOnOne]
rtrans_clos_length [lemma, in MetaCoq.PCUIC.PCUICConversion]
rtrans_clos_incl [lemma, in MetaCoq.PCUIC.PCUICReduction]
rt_ctx_t_trans [constructor, in MetaCoq.PCUIC.PCUICConfluence]
rt_ctx_t_refl [constructor, in MetaCoq.PCUIC.PCUICConfluence]
rt_ctx_t_step [constructor, in MetaCoq.PCUIC.PCUICConfluence]
rt_ctx_trans [constructor, in MetaCoq.PCUIC.PCUICConfluence]
rt_ctx_refl [constructor, in MetaCoq.PCUIC.PCUICConfluence]
rt_ctx_step [constructor, in MetaCoq.PCUIC.PCUICConfluence]
rt_ctx_decl_trans [constructor, in MetaCoq.PCUIC.PCUICConfluence]
rt_ctx_decl_refl [constructor, in MetaCoq.PCUIC.PCUICConfluence]
rt_ctx_decl_step [constructor, in MetaCoq.PCUIC.PCUICConfluence]
rt1n_ctx_trans [constructor, in MetaCoq.PCUIC.PCUICConfluence]
rt1n_ctx_eq [constructor, in MetaCoq.PCUIC.PCUICConfluence]
run_erase_program_fast [definition, in MetaCoq.Erasure.Erasure]
run_erase_program [definition, in MetaCoq.Erasure.Erasure]
Ru:238 [binder, in MetaCoq.PCUIC.PCUICEquality]
Ru:265 [binder, in MetaCoq.PCUIC.PCUICEquality]
Ru:283 [binder, in MetaCoq.PCUIC.PCUICEquality]
rx:2536 [binder, in MetaCoq.Template.utils.All_Forall]
R_global_instance_impl [instance, in MetaCoq.Template.TermEquality]
R_global_instance_impl_same_napp [instance, in MetaCoq.Template.TermEquality]
R_global_instance_refl [lemma, in MetaCoq.Template.TermEquality]
R_universe_instance_impl' [lemma, in MetaCoq.Template.TermEquality]
R_universe_instance_impl [lemma, in MetaCoq.Template.TermEquality]
R_global_instance [definition, in MetaCoq.Template.TermEquality]
R_opt_variance [definition, in MetaCoq.Template.TermEquality]
R_universe_instance_variance [definition, in MetaCoq.Template.TermEquality]
R_universe_variance [definition, in MetaCoq.Template.TermEquality]
R_universe_instance [definition, in MetaCoq.Template.TermEquality]
R_global_instance_weaken_env [lemma, in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
R_eq_univ_prop_consistent_instances [lemma, in MetaCoq.PCUIC.PCUICCumulProp]
R_opt_variance_impl [lemma, in MetaCoq.PCUIC.PCUICCumulProp]
R_global_instance_flip [lemma, in MetaCoq.PCUIC.PCUICEquality]
R_universe_instance_eq [lemma, in MetaCoq.PCUIC.PCUICEquality]
R_global_instance_empty_impl [instance, in MetaCoq.PCUIC.PCUICEquality]
R_global_instance_impl [instance, in MetaCoq.PCUIC.PCUICEquality]
R_global_instance_impl_same_napp [instance, in MetaCoq.PCUIC.PCUICEquality]
R_global_instance_antisym [instance, in MetaCoq.PCUIC.PCUICEquality]
R_global_instance_equiv [instance, in MetaCoq.PCUIC.PCUICEquality]
R_universe_instance_antisym [lemma, in MetaCoq.PCUIC.PCUICEquality]
R_universe_instance_equiv [instance, in MetaCoq.PCUIC.PCUICEquality]
R_global_instance_trans [instance, in MetaCoq.PCUIC.PCUICEquality]
R_global_instance_sym [lemma, in MetaCoq.PCUIC.PCUICEquality]
R_universe_instance_trans [instance, in MetaCoq.PCUIC.PCUICEquality]
R_universe_instance_sym [instance, in MetaCoq.PCUIC.PCUICEquality]
R_universe_instance_refl [instance, in MetaCoq.PCUIC.PCUICEquality]
R_global_instance_refl [lemma, in MetaCoq.PCUIC.PCUICEquality]
R_universe_instance_impl' [lemma, in MetaCoq.PCUIC.PCUICEquality]
R_universe_instance_impl [lemma, in MetaCoq.PCUIC.PCUICEquality]
R_ind_universes [definition, in MetaCoq.PCUIC.PCUICEquality]
R_global_instance [definition, in MetaCoq.PCUIC.PCUICEquality]
R_opt_variance [definition, in MetaCoq.PCUIC.PCUICEquality]
R_universe_instance_variance [definition, in MetaCoq.PCUIC.PCUICEquality]
R_universe_variance [definition, in MetaCoq.PCUIC.PCUICEquality]
R_universe_instance [definition, in MetaCoq.PCUIC.PCUICEquality]
R_Acc [lemma, in MetaCoq.SafeChecker.PCUICSafeReduce]
R_Acc_aux [lemma, in MetaCoq.SafeChecker.PCUICSafeReduce]
R_singleton [definition, in MetaCoq.SafeChecker.PCUICSafeReduce]
R_Req_R [lemma, in MetaCoq.SafeChecker.PCUICSafeReduce]
R_to_Req [lemma, in MetaCoq.SafeChecker.PCUICSafeReduce]
R_positionR [lemma, in MetaCoq.SafeChecker.PCUICSafeReduce]
R_aux [definition, in MetaCoq.SafeChecker.PCUICSafeReduce]
R_stateR [lemma, in MetaCoq.SafeChecker.PCUICSafeConversion]
R_aux_stateR [lemma, in MetaCoq.SafeChecker.PCUICSafeConversion]
R_positionR2 [lemma, in MetaCoq.SafeChecker.PCUICSafeConversion]
R_aux_positionR2 [lemma, in MetaCoq.SafeChecker.PCUICSafeConversion]
R_cored2 [lemma, in MetaCoq.SafeChecker.PCUICSafeConversion]
R_aux_cored2 [lemma, in MetaCoq.SafeChecker.PCUICSafeConversion]
R_positionR [lemma, in MetaCoq.SafeChecker.PCUICSafeConversion]
R_aux_positionR [lemma, in MetaCoq.SafeChecker.PCUICSafeConversion]
R_cored [lemma, in MetaCoq.SafeChecker.PCUICSafeConversion]
R_irrelevance [lemma, in MetaCoq.SafeChecker.PCUICSafeConversion]
R_aux_irrelevance [lemma, in MetaCoq.SafeChecker.PCUICSafeConversion]
R_Acc [lemma, in MetaCoq.SafeChecker.PCUICSafeConversion]
R_aux_Acc [lemma, in MetaCoq.SafeChecker.PCUICSafeConversion]
R_aux [definition, in MetaCoq.SafeChecker.PCUICSafeConversion]
R_global_instance_empty_universe_instance [lemma, in MetaCoq.PCUIC.PCUICPrincipality]
R_global_instance_nl [lemma, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
R_opt [definition, in MetaCoq.Template.utils.MCOption]
R_universe_instance_flip [lemma, in MetaCoq.PCUIC.PCUICConfluence]
R_universe_instance_variance_irrelevant [lemma, in MetaCoq.PCUIC.PCUICConversion]
R_global_instance_length [lemma, in MetaCoq.PCUIC.PCUICConversion]
R_global_instance_cstr_irrelevant [lemma, in MetaCoq.PCUIC.PCUICSR]
R_opt [definition, in MetaCoq.SafeChecker.PCUICSafeChecker]
R_global_instance_refl_wf [lemma, in MetaCoq.SafeChecker.PCUICEqualityDec]
R':1270 [binder, in MetaCoq.Template.utils.All_Forall]
r':1297 [binder, in MetaCoq.Translations.MiniHoTT]
r':1305 [binder, in MetaCoq.Translations.MiniHoTT_paths]
R':131 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
r':1427 [binder, in MetaCoq.Template.utils.All_Forall]
r':16 [binder, in MetaCoq.Template.Reflect]
R':1629 [binder, in MetaCoq.Template.utils.All_Forall]
r':2061 [binder, in MetaCoq.Template.utils.All_Forall]
R':2362 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
R':33 [binder, in MetaCoq.PCUIC.PCUICSN]
R':40 [binder, in MetaCoq.Template.TermEquality]
R':42 [binder, in MetaCoq.Template.TermEquality]
R':43 [binder, in MetaCoq.PCUIC.PCUICEquality]
R':45 [binder, in MetaCoq.PCUIC.PCUICEquality]
r':54 [binder, in MetaCoq.Template.Reflect]
r':758 [binder, in MetaCoq.Template.utils.MCList]
r':763 [binder, in MetaCoq.Template.utils.MCList]
R1:1022 [binder, in MetaCoq.Template.utils.All_Forall]
R1:1037 [binder, in MetaCoq.Template.utils.All_Forall]
r1:1336 [binder, in MetaCoq.Translations.MiniHoTT]
r1:1344 [binder, in MetaCoq.Translations.MiniHoTT_paths]
r1:1464 [binder, in MetaCoq.Template.utils.All_Forall]
r1:1470 [binder, in MetaCoq.Template.utils.All_Forall]
r1:1479 [binder, in MetaCoq.Template.utils.All_Forall]
r1:1952 [binder, in MetaCoq.Template.utils.All_Forall]
R1:225 [binder, in MetaCoq.PCUIC.PCUICSR]
R1:238 [binder, in MetaCoq.PCUIC.PCUICSR]
R1:338 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
R1:427 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
R1:648 [binder, in MetaCoq.Template.utils.All_Forall]
R1:660 [binder, in MetaCoq.Template.utils.All_Forall]
R1:708 [binder, in MetaCoq.Template.utils.All_Forall]
R1:719 [binder, in MetaCoq.Template.utils.All_Forall]
R1:826 [binder, in MetaCoq.Template.utils.All_Forall]
R1:840 [binder, in MetaCoq.Template.utils.All_Forall]
r1:868 [binder, in MetaCoq.Translations.MiniHoTT]
r1:876 [binder, in MetaCoq.Translations.MiniHoTT_paths]
R2:1023 [binder, in MetaCoq.Template.utils.All_Forall]
R2:1038 [binder, in MetaCoq.Template.utils.All_Forall]
r2:1337 [binder, in MetaCoq.Translations.MiniHoTT]
r2:1345 [binder, in MetaCoq.Translations.MiniHoTT_paths]
r2:1465 [binder, in MetaCoq.Template.utils.All_Forall]
r2:1471 [binder, in MetaCoq.Template.utils.All_Forall]
r2:1480 [binder, in MetaCoq.Template.utils.All_Forall]
r2:1953 [binder, in MetaCoq.Template.utils.All_Forall]
R2:226 [binder, in MetaCoq.PCUIC.PCUICSR]
R2:239 [binder, in MetaCoq.PCUIC.PCUICSR]
R2:339 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
R2:428 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
R2:649 [binder, in MetaCoq.Template.utils.All_Forall]
R2:661 [binder, in MetaCoq.Template.utils.All_Forall]
R2:709 [binder, in MetaCoq.Template.utils.All_Forall]
R2:720 [binder, in MetaCoq.Template.utils.All_Forall]
R2:827 [binder, in MetaCoq.Template.utils.All_Forall]
R2:841 [binder, in MetaCoq.Template.utils.All_Forall]
r2:869 [binder, in MetaCoq.Translations.MiniHoTT]
r2:877 [binder, in MetaCoq.Translations.MiniHoTT_paths]
R3:1024 [binder, in MetaCoq.Template.utils.All_Forall]
R3:1039 [binder, in MetaCoq.Template.utils.All_Forall]
R3:227 [binder, in MetaCoq.PCUIC.PCUICSR]
R3:240 [binder, in MetaCoq.PCUIC.PCUICSR]
R3:341 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
R3:430 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
R3:650 [binder, in MetaCoq.Template.utils.All_Forall]
R3:662 [binder, in MetaCoq.Template.utils.All_Forall]
R3:710 [binder, in MetaCoq.Template.utils.All_Forall]
R3:721 [binder, in MetaCoq.Template.utils.All_Forall]
R3:828 [binder, in MetaCoq.Template.utils.All_Forall]
R3:842 [binder, in MetaCoq.Template.utils.All_Forall]
R:1 [binder, in MetaCoq.Template.TermEquality]
r:1 [binder, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
r:1003 [binder, in MetaCoq.Template.utils.All_Forall]
R:1007 [binder, in MetaCoq.PCUIC.PCUICConfluence]
R:103 [binder, in MetaCoq.Template.utils.MCRelations]
R:1051 [binder, in MetaCoq.PCUIC.PCUICConfluence]
r:106 [binder, in MetaCoq.PCUIC.PCUICConfluence]
R:107 [binder, in MetaCoq.Template.monad_utils]
R:1075 [binder, in MetaCoq.PCUIC.PCUICConfluence]
r:1081 [binder, in MetaCoq.Translations.MiniHoTT]
r:1087 [binder, in MetaCoq.Translations.MiniHoTT]
r:1089 [binder, in MetaCoq.Translations.MiniHoTT_paths]
r:1094 [binder, in MetaCoq.Translations.MiniHoTT]
r:1095 [binder, in MetaCoq.Translations.MiniHoTT_paths]
r:1102 [binder, in MetaCoq.Translations.MiniHoTT_paths]
r:1103 [binder, in MetaCoq.Translations.MiniHoTT]
r:1110 [binder, in MetaCoq.Translations.MiniHoTT]
r:1111 [binder, in MetaCoq.Translations.MiniHoTT_paths]
r:1118 [binder, in MetaCoq.Translations.MiniHoTT]
r:1118 [binder, in MetaCoq.Translations.MiniHoTT_paths]
R:112 [binder, in MetaCoq.Template.utils.All_Forall]
r:1126 [binder, in MetaCoq.Translations.MiniHoTT_paths]
r:1146 [binder, in MetaCoq.PCUIC.PCUICConfluence]
R:116 [binder, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
R:119 [binder, in MetaCoq.Template.utils.All_Forall]
R:119 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
r:1192 [binder, in MetaCoq.Translations.MiniHoTT]
r:1200 [binder, in MetaCoq.Translations.MiniHoTT_paths]
r:1202 [binder, in MetaCoq.Translations.MiniHoTT]
r:1210 [binder, in MetaCoq.Translations.MiniHoTT_paths]
r:1211 [binder, in MetaCoq.Translations.MiniHoTT]
R:1217 [binder, in MetaCoq.PCUIC.PCUICConfluence]
r:1219 [binder, in MetaCoq.Translations.MiniHoTT]
r:1219 [binder, in MetaCoq.Translations.MiniHoTT_paths]
r:1226 [binder, in MetaCoq.Translations.MiniHoTT]
r:1227 [binder, in MetaCoq.Translations.MiniHoTT_paths]
r:1234 [binder, in MetaCoq.Translations.MiniHoTT]
r:1234 [binder, in MetaCoq.Translations.MiniHoTT_paths]
r:1242 [binder, in MetaCoq.Translations.MiniHoTT_paths]
r:1268 [binder, in MetaCoq.Translations.MiniHoTT]
R:1269 [binder, in MetaCoq.Template.utils.All_Forall]
r:1276 [binder, in MetaCoq.Translations.MiniHoTT_paths]
r:1287 [binder, in MetaCoq.Translations.MiniHoTT]
r:129 [binder, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
r:1295 [binder, in MetaCoq.Translations.MiniHoTT_paths]
r:1296 [binder, in MetaCoq.Translations.MiniHoTT]
r:13 [binder, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
R:130 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
r:1304 [binder, in MetaCoq.Translations.MiniHoTT_paths]
r:1308 [binder, in MetaCoq.Translations.MiniHoTT]
r:1316 [binder, in MetaCoq.Translations.MiniHoTT_paths]
r:1318 [binder, in MetaCoq.Translations.MiniHoTT]
r:1326 [binder, in MetaCoq.Translations.MiniHoTT]
r:1326 [binder, in MetaCoq.Translations.MiniHoTT_paths]
R:133 [binder, in MetaCoq.PCUIC.PCUICSafeLemmata]
r:1334 [binder, in MetaCoq.Translations.MiniHoTT_paths]
R:1337 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
r:1342 [binder, in MetaCoq.Translations.MiniHoTT]
r:135 [binder, in MetaCoq.Translations.MiniHoTT]
r:1350 [binder, in MetaCoq.Translations.MiniHoTT]
r:1350 [binder, in MetaCoq.Translations.MiniHoTT_paths]
r:1358 [binder, in MetaCoq.Translations.MiniHoTT_paths]
r:136 [binder, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
r:1366 [binder, in MetaCoq.Translations.MiniHoTT]
r:1367 [binder, in MetaCoq.Translations.MiniHoTT]
R:1370 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
r:1374 [binder, in MetaCoq.Translations.MiniHoTT_paths]
r:1375 [binder, in MetaCoq.Translations.MiniHoTT_paths]
R:139 [binder, in MetaCoq.PCUIC.PCUICSafeLemmata]
R:14 [binder, in MetaCoq.PCUIC.PCUICConfluence]
r:142 [binder, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
r:1426 [binder, in MetaCoq.Template.utils.All_Forall]
r:143 [binder, in MetaCoq.Translations.MiniHoTT_paths]
R:1432 [binder, in MetaCoq.Template.utils.All_Forall]
r:145 [binder, in MetaCoq.Template.Typing]
R:146 [binder, in MetaCoq.PCUIC.utils.PCUICUtils]
R:1460 [binder, in MetaCoq.Template.utils.All_Forall]
r:1463 [binder, in MetaCoq.Template.utils.All_Forall]
R:1468 [binder, in MetaCoq.Template.utils.All_Forall]
R:1483 [binder, in MetaCoq.Template.utils.All_Forall]
r:149 [binder, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
r:1491 [binder, in MetaCoq.Template.utils.All_Forall]
R:1498 [binder, in MetaCoq.Template.utils.All_Forall]
R:15 [binder, in MetaCoq.Template.utils.MCReflect]
R:15 [binder, in MetaCoq.Template.utils.MCRelations]
r:15 [binder, in MetaCoq.Template.Reflect]
r:150 [binder, in MetaCoq.Template.Typing]
r:1506 [binder, in MetaCoq.Template.utils.All_Forall]
R:1513 [binder, in MetaCoq.Template.utils.All_Forall]
r:155 [binder, in MetaCoq.Template.Typing]
R:1584 [binder, in MetaCoq.Template.utils.All_Forall]
R:1588 [binder, in MetaCoq.Template.utils.All_Forall]
R:1592 [binder, in MetaCoq.Template.utils.All_Forall]
r:16 [binder, in MetaCoq.Template.utils.MCReflect]
R:16 [binder, in MetaCoq.Template.utils.All_Forall]
r:16 [binder, in MetaCoq.PCUIC.PCUICTyping]
R:160 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
R:1601 [binder, in MetaCoq.Template.utils.All_Forall]
R:1610 [binder, in MetaCoq.Template.utils.All_Forall]
R:1628 [binder, in MetaCoq.Template.utils.All_Forall]
R:1636 [binder, in MetaCoq.Template.utils.All_Forall]
R:1644 [binder, in MetaCoq.Template.utils.All_Forall]
R:1684 [binder, in MetaCoq.Template.utils.All_Forall]
R:1691 [binder, in MetaCoq.Template.utils.All_Forall]
R:1706 [binder, in MetaCoq.Template.utils.All_Forall]
R:172 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
R:1726 [binder, in MetaCoq.Template.utils.All_Forall]
R:1736 [binder, in MetaCoq.Template.utils.All_Forall]
R:1776 [binder, in MetaCoq.Template.utils.All_Forall]
R:1783 [binder, in MetaCoq.Template.utils.All_Forall]
r:18 [binder, in MetaCoq.PCUIC.PCUICTyping]
r:18 [binder, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
R:1842 [binder, in MetaCoq.Template.utils.All_Forall]
r:1852 [binder, in MetaCoq.Translations.MiniHoTT]
r:1853 [binder, in MetaCoq.Translations.MiniHoTT]
r:1854 [binder, in MetaCoq.Translations.MiniHoTT]
R:186 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
r:1860 [binder, in MetaCoq.Translations.MiniHoTT_paths]
r:1861 [binder, in MetaCoq.Translations.MiniHoTT_paths]
r:1862 [binder, in MetaCoq.Translations.MiniHoTT]
r:1862 [binder, in MetaCoq.Translations.MiniHoTT_paths]
r:1869 [binder, in MetaCoq.Translations.MiniHoTT]
r:1870 [binder, in MetaCoq.Translations.MiniHoTT_paths]
r:1876 [binder, in MetaCoq.Translations.MiniHoTT]
r:1877 [binder, in MetaCoq.Translations.MiniHoTT_paths]
r:1883 [binder, in MetaCoq.Translations.MiniHoTT]
r:1884 [binder, in MetaCoq.Translations.MiniHoTT_paths]
r:1890 [binder, in MetaCoq.Translations.MiniHoTT]
r:1891 [binder, in MetaCoq.Translations.MiniHoTT_paths]
r:1897 [binder, in MetaCoq.Translations.MiniHoTT]
r:1898 [binder, in MetaCoq.Translations.MiniHoTT_paths]
r:1905 [binder, in MetaCoq.Translations.MiniHoTT]
r:1905 [binder, in MetaCoq.Translations.MiniHoTT_paths]
r:1913 [binder, in MetaCoq.Translations.MiniHoTT]
r:1913 [binder, in MetaCoq.Translations.MiniHoTT_paths]
r:1920 [binder, in MetaCoq.Translations.MiniHoTT]
r:1921 [binder, in MetaCoq.Translations.MiniHoTT_paths]
r:1927 [binder, in MetaCoq.Translations.MiniHoTT]
r:1928 [binder, in MetaCoq.Translations.MiniHoTT_paths]
r:1934 [binder, in MetaCoq.Translations.MiniHoTT]
r:1935 [binder, in MetaCoq.Translations.MiniHoTT_paths]
R:1938 [binder, in MetaCoq.Template.utils.All_Forall]
r:1941 [binder, in MetaCoq.Translations.MiniHoTT]
r:1942 [binder, in MetaCoq.Translations.MiniHoTT_paths]
R:1948 [binder, in MetaCoq.Template.utils.All_Forall]
r:1948 [binder, in MetaCoq.Translations.MiniHoTT]
r:1949 [binder, in MetaCoq.Translations.MiniHoTT_paths]
r:1955 [binder, in MetaCoq.Translations.MiniHoTT]
r:1956 [binder, in MetaCoq.Translations.MiniHoTT_paths]
R:1958 [binder, in MetaCoq.Template.utils.All_Forall]
r:1962 [binder, in MetaCoq.Translations.MiniHoTT]
r:1963 [binder, in MetaCoq.Translations.MiniHoTT_paths]
R:1969 [binder, in MetaCoq.Template.utils.All_Forall]
r:1969 [binder, in MetaCoq.Translations.MiniHoTT]
r:1970 [binder, in MetaCoq.Translations.MiniHoTT_paths]
r:1976 [binder, in MetaCoq.Translations.MiniHoTT]
r:1977 [binder, in MetaCoq.Translations.MiniHoTT_paths]
R:1979 [binder, in MetaCoq.Template.utils.All_Forall]
r:198 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
r:1983 [binder, in MetaCoq.Translations.MiniHoTT]
r:1984 [binder, in MetaCoq.Translations.MiniHoTT_paths]
R:1988 [binder, in MetaCoq.Template.utils.All_Forall]
r:1990 [binder, in MetaCoq.Translations.MiniHoTT]
r:1991 [binder, in MetaCoq.Translations.MiniHoTT_paths]
r:1997 [binder, in MetaCoq.Translations.MiniHoTT]
r:1998 [binder, in MetaCoq.Translations.MiniHoTT_paths]
R:2 [binder, in MetaCoq.PCUIC.utils.PCUICOnOne]
R:2 [binder, in MetaCoq.SafeChecker.PCUICWfReduction]
R:20 [binder, in MetaCoq.Template.utils.MCReflect]
r:200 [binder, in MetaCoq.Translations.MiniHoTT]
r:2004 [binder, in MetaCoq.Translations.MiniHoTT]
r:2005 [binder, in MetaCoq.Translations.MiniHoTT_paths]
r:2011 [binder, in MetaCoq.Translations.MiniHoTT]
r:2012 [binder, in MetaCoq.Translations.MiniHoTT_paths]
r:2018 [binder, in MetaCoq.Translations.MiniHoTT]
r:2019 [binder, in MetaCoq.Translations.MiniHoTT_paths]
R:2025 [binder, in MetaCoq.Template.utils.All_Forall]
r:2025 [binder, in MetaCoq.Translations.MiniHoTT]
r:2026 [binder, in MetaCoq.Translations.MiniHoTT_paths]
R:2031 [binder, in MetaCoq.Template.utils.All_Forall]
r:2032 [binder, in MetaCoq.Translations.MiniHoTT]
r:2033 [binder, in MetaCoq.Translations.MiniHoTT_paths]
R:2038 [binder, in MetaCoq.Template.utils.All_Forall]
r:2040 [binder, in MetaCoq.Translations.MiniHoTT_paths]
R:2047 [binder, in MetaCoq.Template.utils.All_Forall]
R:2053 [binder, in MetaCoq.Template.utils.All_Forall]
r:2060 [binder, in MetaCoq.Template.utils.All_Forall]
R:2069 [binder, in MetaCoq.Template.utils.All_Forall]
r:208 [binder, in MetaCoq.Translations.MiniHoTT]
r:208 [binder, in MetaCoq.Translations.MiniHoTT_paths]
r:21 [binder, in MetaCoq.Template.utils.MCReflect]
R:213 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
R:2135 [binder, in MetaCoq.Template.utils.All_Forall]
R:2147 [binder, in MetaCoq.Template.utils.All_Forall]
R:2157 [binder, in MetaCoq.Template.utils.All_Forall]
R:216 [binder, in MetaCoq.Template.utils.All_Forall]
r:216 [binder, in MetaCoq.Translations.MiniHoTT_paths]
r:216 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
R:2166 [binder, in MetaCoq.Template.utils.All_Forall]
R:2192 [binder, in MetaCoq.Template.utils.All_Forall]
R:22 [binder, in MetaCoq.Template.utils.MCOption]
r:22 [binder, in MetaCoq.PCUIC.PCUICTyping]
R:2201 [binder, in MetaCoq.Template.utils.All_Forall]
R:2210 [binder, in MetaCoq.Template.utils.All_Forall]
R:2216 [binder, in MetaCoq.Template.utils.All_Forall]
R:222 [binder, in MetaCoq.Template.TypingWf]
r:2223 [binder, in MetaCoq.Translations.MiniHoTT]
R:2228 [binder, in MetaCoq.Template.utils.All_Forall]
r:2231 [binder, in MetaCoq.Translations.MiniHoTT]
r:2231 [binder, in MetaCoq.Translations.MiniHoTT_paths]
r:2238 [binder, in MetaCoq.Translations.MiniHoTT]
r:2239 [binder, in MetaCoq.Translations.MiniHoTT_paths]
R:2242 [binder, in MetaCoq.Template.utils.All_Forall]
r:2246 [binder, in MetaCoq.Translations.MiniHoTT_paths]
r:2248 [binder, in MetaCoq.Translations.MiniHoTT]
r:2256 [binder, in MetaCoq.Translations.MiniHoTT_paths]
r:2258 [binder, in MetaCoq.Translations.MiniHoTT]
r:2266 [binder, in MetaCoq.Translations.MiniHoTT_paths]
r:2268 [binder, in MetaCoq.Translations.MiniHoTT]
R:227 [binder, in MetaCoq.Template.utils.All_Forall]
r:2276 [binder, in MetaCoq.Translations.MiniHoTT_paths]
r:2278 [binder, in MetaCoq.Translations.MiniHoTT]
r:228 [binder, in MetaCoq.PCUIC.PCUICReduction]
r:2286 [binder, in MetaCoq.Translations.MiniHoTT_paths]
r:2288 [binder, in MetaCoq.Translations.MiniHoTT]
r:2295 [binder, in MetaCoq.Translations.MiniHoTT]
r:2296 [binder, in MetaCoq.Translations.MiniHoTT_paths]
r:2303 [binder, in MetaCoq.Translations.MiniHoTT_paths]
r:234 [binder, in MetaCoq.PCUIC.PCUICReduction]
R:236 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
R:2361 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
R:238 [binder, in MetaCoq.Template.utils.All_Forall]
R:239 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
r:24 [binder, in MetaCoq.Template.BasicAst]
R:24 [binder, in MetaCoq.Template.utils.MCRelations]
r:240 [binder, in MetaCoq.PCUIC.PCUICReduction]
R:2493 [binder, in MetaCoq.Translations.MiniHoTT]
R:25 [binder, in MetaCoq.Template.utils.All_Forall]
R:25 [binder, in MetaCoq.Translations.MiniHoTT]
R:2501 [binder, in MetaCoq.Translations.MiniHoTT_paths]
R:2528 [binder, in MetaCoq.Template.utils.All_Forall]
R:2569 [binder, in MetaCoq.Template.utils.All_Forall]
R:2584 [binder, in MetaCoq.Translations.MiniHoTT]
R:2592 [binder, in MetaCoq.Translations.MiniHoTT_paths]
R:26 [binder, in MetaCoq.Template.utils.MCRelations]
R:263 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
r:275 [binder, in MetaCoq.Translations.MiniHoTT]
r:2771 [binder, in MetaCoq.Translations.MiniHoTT]
r:2772 [binder, in MetaCoq.Translations.MiniHoTT]
r:2779 [binder, in MetaCoq.Translations.MiniHoTT_paths]
r:2780 [binder, in MetaCoq.Translations.MiniHoTT_paths]
r:28 [binder, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
r:282 [binder, in MetaCoq.Translations.MiniHoTT]
r:283 [binder, in MetaCoq.Translations.MiniHoTT_paths]
r:2864 [binder, in MetaCoq.Translations.MiniHoTT]
r:2872 [binder, in MetaCoq.Translations.MiniHoTT_paths]
r:2873 [binder, in MetaCoq.Translations.MiniHoTT]
r:2881 [binder, in MetaCoq.Translations.MiniHoTT_paths]
r:289 [binder, in MetaCoq.Translations.MiniHoTT]
r:290 [binder, in MetaCoq.Translations.MiniHoTT_paths]
r:296 [binder, in MetaCoq.Translations.MiniHoTT]
r:297 [binder, in MetaCoq.Translations.MiniHoTT_paths]
R:3 [binder, in MetaCoq.Template.utils.MCRelations]
R:30 [binder, in MetaCoq.PCUIC.PCUICConfluence]
R:30 [binder, in MetaCoq.Translations.MiniHoTT]
r:303 [binder, in MetaCoq.Translations.MiniHoTT]
r:304 [binder, in MetaCoq.Translations.MiniHoTT_paths]
R:307 [binder, in MetaCoq.PCUIC.PCUICEquality]
r:31 [binder, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
r:310 [binder, in MetaCoq.Translations.MiniHoTT]
r:311 [binder, in MetaCoq.Translations.MiniHoTT_paths]
R:313 [binder, in MetaCoq.PCUIC.PCUICEquality]
r:317 [binder, in MetaCoq.Translations.MiniHoTT]
r:318 [binder, in MetaCoq.Translations.MiniHoTT_paths]
r:319 [binder, in MetaCoq.Template.Typing]
r:32 [binder, in MetaCoq.Template.utils.All_Forall]
R:32 [binder, in MetaCoq.PCUIC.PCUICSN]
r:324 [binder, in MetaCoq.Translations.MiniHoTT]
r:325 [binder, in MetaCoq.Template.Typing]
r:325 [binder, in MetaCoq.Translations.MiniHoTT_paths]
R:325 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
R:33 [binder, in MetaCoq.Template.utils.MCRelations]
R:33 [binder, in MetaCoq.Translations.MiniHoTT_paths]
r:331 [binder, in MetaCoq.Template.Typing]
r:332 [binder, in MetaCoq.Translations.MiniHoTT_paths]
r:35 [binder, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
R:351 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
r:36 [binder, in MetaCoq.Translations.times_bool_fun]
R:36 [binder, in MetaCoq.Template.utils.All_Forall]
R:36 [binder, in MetaCoq.Translations.MiniHoTT]
r:366 [binder, in MetaCoq.PCUIC.PCUICReduction]
R:369 [binder, in MetaCoq.Template.utils.All_Forall]
R:37 [binder, in MetaCoq.Template.utils.MCRelations]
r:37 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
R:371 [binder, in MetaCoq.Template.utils.All_Forall]
R:38 [binder, in MetaCoq.Translations.MiniHoTT_paths]
R:39 [binder, in MetaCoq.Template.TermEquality]
r:398 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
R:40 [binder, in MetaCoq.Template.utils.MCRelations]
R:40 [binder, in MetaCoq.Template.utils.ReflectEq]
r:401 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
r:404 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
r:408 [binder, in MetaCoq.PCUIC.PCUICSR]
R:41 [binder, in MetaCoq.Template.TermEquality]
r:414 [binder, in MetaCoq.PCUIC.PCUICSR]
R:42 [binder, in MetaCoq.PCUIC.PCUICEquality]
r:420 [binder, in MetaCoq.PCUIC.PCUICSR]
r:43 [binder, in MetaCoq.Translations.times_bool_fun]
R:43 [binder, in MetaCoq.Template.utils.MCRelations]
R:43 [binder, in MetaCoq.Template.utils.ReflectEq]
R:43 [binder, in MetaCoq.Translations.MiniHoTT]
R:44 [binder, in MetaCoq.PCUIC.PCUICEquality]
R:44 [binder, in MetaCoq.Translations.MiniHoTT_paths]
r:449 [binder, in MetaCoq.Translations.MiniHoTT]
r:457 [binder, in MetaCoq.Translations.MiniHoTT_paths]
R:46 [binder, in MetaCoq.Template.utils.MCRelations]
R:46 [binder, in MetaCoq.Erasure.ErasureFunction]
r:461 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
r:461 [binder, in MetaCoq.Translations.MiniHoTT]
r:469 [binder, in MetaCoq.Translations.MiniHoTT_paths]
R:47 [binder, in MetaCoq.Template.utils.ReflectEq]
R:47 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
R:49 [binder, in MetaCoq.Template.utils.MCRelations]
R:5 [binder, in MetaCoq.PCUIC.PCUICEquality]
r:5 [binder, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
R:51 [binder, in MetaCoq.Template.utils.MCRelations]
R:51 [binder, in MetaCoq.Translations.MiniHoTT_paths]
R:516 [binder, in MetaCoq.PCUIC.PCUICConfluence]
R:519 [binder, in MetaCoq.PCUIC.PCUICConfluence]
R:526 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
r:53 [binder, in MetaCoq.Template.Reflect]
r:53 [binder, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
r:535 [binder, in MetaCoq.Translations.MiniHoTT]
R:54 [binder, in MetaCoq.Template.utils.MCRelations]
r:543 [binder, in MetaCoq.Translations.MiniHoTT_paths]
r:546 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
r:547 [binder, in MetaCoq.Translations.MiniHoTT]
R:554 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
r:555 [binder, in MetaCoq.Translations.MiniHoTT_paths]
r:557 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
r:568 [binder, in MetaCoq.Translations.MiniHoTT]
R:569 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
R:575 [binder, in MetaCoq.PCUIC.PCUICEquality]
r:576 [binder, in MetaCoq.Translations.MiniHoTT_paths]
r:577 [binder, in MetaCoq.Template.Typing]
R:577 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
r:579 [binder, in MetaCoq.Template.Typing]
r:579 [binder, in MetaCoq.Translations.MiniHoTT]
R:582 [binder, in MetaCoq.PCUIC.PCUICConversion]
r:583 [binder, in MetaCoq.Template.Typing]
r:587 [binder, in MetaCoq.Translations.MiniHoTT_paths]
r:589 [binder, in MetaCoq.Translations.MiniHoTT]
r:597 [binder, in MetaCoq.Translations.MiniHoTT_paths]
r:6 [binder, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
r:60 [binder, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
r:607 [binder, in MetaCoq.Translations.MiniHoTT]
r:615 [binder, in MetaCoq.Translations.MiniHoTT_paths]
r:62 [binder, in MetaCoq.PCUIC.PCUICReduction]
r:624 [binder, in MetaCoq.Template.utils.All_Forall]
R:624 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
R:626 [binder, in MetaCoq.Template.utils.All_Forall]
R:630 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
r:635 [binder, in MetaCoq.Template.utils.All_Forall]
R:64 [binder, in MetaCoq.Template.utils.MCRelations]
R:661 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
r:67 [binder, in MetaCoq.PCUIC.PCUICReduction]
R:72 [binder, in MetaCoq.Template.utils.MCRelations]
r:72 [binder, in MetaCoq.PCUIC.PCUICReduction]
r:727 [binder, in MetaCoq.Translations.MiniHoTT]
r:73 [binder, in MetaCoq.Template.utils.bytestring]
R:732 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
r:734 [binder, in MetaCoq.Translations.MiniHoTT]
r:735 [binder, in MetaCoq.Translations.MiniHoTT_paths]
r:742 [binder, in MetaCoq.Translations.MiniHoTT_paths]
r:743 [binder, in MetaCoq.Translations.MiniHoTT]
R:75 [binder, in MetaCoq.Template.utils.MCRelations]
r:751 [binder, in MetaCoq.Translations.MiniHoTT_paths]
r:757 [binder, in MetaCoq.Template.utils.MCList]
R:76 [binder, in MetaCoq.PCUIC.utils.PCUICOnOne]
R:76 [binder, in MetaCoq.Translations.times_bool_fun2]
r:762 [binder, in MetaCoq.Template.utils.MCList]
R:764 [binder, in MetaCoq.PCUIC.PCUICReduction]
R:774 [binder, in MetaCoq.PCUIC.PCUICConfluence]
R:778 [binder, in MetaCoq.PCUIC.PCUICConfluence]
R:78 [binder, in MetaCoq.Template.utils.MCRelations]
R:782 [binder, in MetaCoq.PCUIC.PCUICConfluence]
R:788 [binder, in MetaCoq.PCUIC.PCUICConfluence]
R:791 [binder, in MetaCoq.PCUIC.PCUICConfluence]
r:797 [binder, in MetaCoq.Template.utils.All_Forall]
R:799 [binder, in MetaCoq.Template.utils.All_Forall]
r:8 [binder, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
R:8 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
R:81 [binder, in MetaCoq.Template.utils.MCRelations]
r:810 [binder, in MetaCoq.Template.utils.All_Forall]
R:810 [binder, in MetaCoq.PCUIC.PCUICConfluence]
r:811 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
R:813 [binder, in MetaCoq.PCUIC.PCUICConfluence]
R:82 [binder, in MetaCoq.PCUIC.utils.PCUICOnOne]
r:820 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
r:826 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
r:834 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
r:838 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
R:84 [binder, in MetaCoq.Template.utils.MCRelations]
R:84 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
r:843 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
r:85 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
r:850 [binder, in MetaCoq.Translations.MiniHoTT]
r:850 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
r:854 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
r:858 [binder, in MetaCoq.Translations.MiniHoTT_paths]
r:859 [binder, in MetaCoq.Translations.MiniHoTT]
r:867 [binder, in MetaCoq.Translations.MiniHoTT_paths]
R:87 [binder, in MetaCoq.Template.utils.MCRelations]
r:87 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
r:877 [binder, in MetaCoq.Translations.MiniHoTT]
R:88 [binder, in MetaCoq.PCUIC.utils.PCUICOnOne]
r:885 [binder, in MetaCoq.Translations.MiniHoTT_paths]
r:887 [binder, in MetaCoq.Translations.MiniHoTT]
R:89 [binder, in MetaCoq.Template.utils.MCRelations]
r:890 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
r:893 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
r:895 [binder, in MetaCoq.Translations.MiniHoTT_paths]
r:898 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
R:9 [binder, in MetaCoq.Template.utils.MCRelations]
R:90 [binder, in MetaCoq.PCUIC.PCUICConfluence]
r:906 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
R:91 [binder, in MetaCoq.Template.utils.MCRelations]
R:91 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
r:913 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
r:917 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
r:920 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
R:920 [binder, in MetaCoq.PCUIC.PCUICReduction]
R:926 [binder, in MetaCoq.PCUIC.PCUICReduction]
r:928 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
R:93 [binder, in MetaCoq.Template.utils.MCRelations]
R:93 [binder, in MetaCoq.PCUIC.utils.PCUICOnOne]
R:934 [binder, in MetaCoq.PCUIC.PCUICConfluence]
r:936 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
R:942 [binder, in MetaCoq.PCUIC.PCUICConfluence]
r:945 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
R:945 [binder, in MetaCoq.PCUIC.PCUICReduction]
R:949 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
R:95 [binder, in MetaCoq.Template.utils.MCRelations]
R:950 [binder, in MetaCoq.PCUIC.PCUICConfluence]
R:951 [binder, in MetaCoq.PCUIC.PCUICConfluence]
r:951 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
r:955 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
r:96 [binder, in MetaCoq.PCUIC.PCUICConfluence]
R:964 [binder, in MetaCoq.PCUIC.PCUICConfluence]
r:967 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
R:97 [binder, in MetaCoq.Template.utils.MCRelations]
r:971 [binder, in MetaCoq.Translations.MiniHoTT]
r:972 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
R:975 [binder, in MetaCoq.PCUIC.PCUICConfluence]
R:976 [binder, in MetaCoq.PCUIC.PCUICConfluence]
r:977 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
r:979 [binder, in MetaCoq.Translations.MiniHoTT_paths]
R:98 [binder, in MetaCoq.SafeChecker.PCUICWfEnv]
r:981 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
R:984 [binder, in MetaCoq.PCUIC.PCUICConfluence]
r:984 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
R:985 [binder, in MetaCoq.PCUIC.PCUICConfluence]
R:986 [binder, in MetaCoq.PCUIC.PCUICConfluence]
r:988 [binder, in MetaCoq.Template.utils.All_Forall]
R:988 [binder, in MetaCoq.PCUIC.PCUICConfluence]
R:99 [binder, in MetaCoq.Template.utils.MCRelations]
R:99 [binder, in MetaCoq.PCUIC.PCUICConfluence]
R:990 [binder, in MetaCoq.PCUIC.PCUICConfluence]
R:991 [binder, in MetaCoq.Template.utils.All_Forall]
R:992 [binder, in MetaCoq.PCUIC.PCUICConfluence]
rΓ:1139 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rΓ:1150 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rΓ:1361 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
rΓ:1368 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]



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)