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)

A (binder)

AA:384 [in MetaCoq.SafeChecker.PCUICSafeChecker]
aa:392 [in MetaCoq.SafeChecker.PCUICSafeChecker]
aa:395 [in MetaCoq.SafeChecker.PCUICSafeChecker]
AA:741 [in MetaCoq.SafeChecker.PCUICSafeChecker]
aa:746 [in MetaCoq.SafeChecker.PCUICSafeChecker]
aa:748 [in MetaCoq.SafeChecker.PCUICSafeChecker]
aa:751 [in MetaCoq.SafeChecker.PCUICSafeChecker]
aa:753 [in MetaCoq.SafeChecker.PCUICSafeChecker]
aa:757 [in MetaCoq.SafeChecker.PCUICSafeChecker]
aa:759 [in MetaCoq.SafeChecker.PCUICSafeChecker]
aa:763 [in MetaCoq.SafeChecker.PCUICSafeChecker]
aa:765 [in MetaCoq.SafeChecker.PCUICSafeChecker]
aa:767 [in MetaCoq.SafeChecker.PCUICSafeChecker]
aa:772 [in MetaCoq.SafeChecker.PCUICSafeChecker]
AA:848 [in MetaCoq.SafeChecker.PCUICSafeChecker]
aa:853 [in MetaCoq.SafeChecker.PCUICSafeChecker]
aa:859 [in MetaCoq.SafeChecker.PCUICSafeChecker]
aa:862 [in MetaCoq.SafeChecker.PCUICSafeChecker]
aa:875 [in MetaCoq.SafeChecker.PCUICSafeChecker]
aa:878 [in MetaCoq.SafeChecker.PCUICSafeChecker]
abstract_structure:250 [in MetaCoq.SafeChecker.PCUICErrors]
abstract_structure:180 [in MetaCoq.SafeChecker.PCUICErrors]
abstract_structure:171 [in MetaCoq.SafeChecker.PCUICErrors]
abstract_env_impl:195 [in MetaCoq.SafeChecker.PCUICWfEnv]
abstract_env_struct0:133 [in MetaCoq.SafeChecker.PCUICWfEnv]
abstract_env_ext_struct0:132 [in MetaCoq.SafeChecker.PCUICWfEnv]
abstract_env_ext_impl:131 [in MetaCoq.SafeChecker.PCUICWfEnv]
abstract_env_impl:130 [in MetaCoq.SafeChecker.PCUICWfEnv]
abstract_env_ext_struct0:72 [in MetaCoq.SafeChecker.PCUICWfEnv]
abstract_env_impl:71 [in MetaCoq.SafeChecker.PCUICWfEnv]
abstract_env_ext_struct0:65 [in MetaCoq.SafeChecker.PCUICWfEnv]
abstract_env_impl:64 [in MetaCoq.SafeChecker.PCUICWfEnv]
abstract_env_ext_struct0:61 [in MetaCoq.SafeChecker.PCUICWfEnv]
abstract_env_impl:60 [in MetaCoq.SafeChecker.PCUICWfEnv]
abstract_env_ext_struct0:57 [in MetaCoq.SafeChecker.PCUICWfEnv]
abstract_env_impl:56 [in MetaCoq.SafeChecker.PCUICWfEnv]
abstract_env_ext_impl:30 [in MetaCoq.SafeChecker.PCUICWfEnv]
abstract_env_impl:29 [in MetaCoq.SafeChecker.PCUICWfEnv]
abstract_env_impl:14 [in MetaCoq.SafeChecker.PCUICWfEnv]
abs:1059 [in MetaCoq.Erasure.ErasureFunction]
abs:1063 [in MetaCoq.Erasure.ErasureFunction]
abs:1065 [in MetaCoq.Erasure.ErasureFunction]
abs:1067 [in MetaCoq.Erasure.ErasureFunction]
Abs:117 [in MetaCoq.SafeChecker.PCUICSafeReduce]
acc':754 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
acc:101 [in MetaCoq.Template.utils.MCList]
acc:103 [in MetaCoq.Template.utils.MCList]
acc:105 [in MetaCoq.PCUIC.utils.PCUICPretty]
acc:1074 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
acc:1083 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
acc:109 [in MetaCoq.Template.utils.MCList]
acc:111 [in MetaCoq.Template.utils.MCList]
acc:1155 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
acc:116 [in MetaCoq.Template.Checker]
acc:1167 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
acc:1172 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
acc:122 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
acc:126 [in MetaCoq.Template.Checker]
acc:130 [in MetaCoq.Template.utils.bytestring]
acc:130 [in MetaCoq.Erasure.EAstUtils]
acc:1317 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
acc:132 [in MetaCoq.Erasure.EAstUtils]
acc:133 [in MetaCoq.Template.utils.bytestring]
acc:134 [in MetaCoq.Erasure.EAstUtils]
acc:134 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
acc:136 [in MetaCoq.Erasure.EAstUtils]
acc:137 [in MetaCoq.Template.Pretty]
acc:138 [in MetaCoq.Template.TypingWf]
acc:179 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
acc:187 [in MetaCoq.Template.Environment]
acc:193 [in MetaCoq.Template.Environment]
acc:209 [in MetaCoq.Template.Environment]
acc:22 [in MetaCoq.Template.utils.bytestring]
acc:252 [in MetaCoq.PCUIC.PCUICWfUniverses]
acc:3 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
acc:305 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
acc:310 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
acc:311 [in MetaCoq.PCUIC.PCUICSpine]
acc:32 [in MetaCoq.Template.EnvMap]
acc:345 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
acc:415 [in MetaCoq.Template.Checker]
acc:430 [in MetaCoq.SafeChecker.PCUICSafeChecker]
acc:458 [in MetaCoq.Template.utils.wGraph]
acc:460 [in MetaCoq.Template.utils.wGraph]
acc:464 [in MetaCoq.Template.utils.MCList]
acc:474 [in MetaCoq.Template.utils.MCList]
acc:507 [in MetaCoq.PCUIC.PCUICSpine]
acc:513 [in MetaCoq.Template.EnvironmentTyping]
acc:54 [in MetaCoq.SafeChecker.PCUICSafeReduce]
acc:582 [in MetaCoq.Template.common.uGraph]
acc:587 [in MetaCoq.Template.common.uGraph]
acc:61 [in MetaCoq.Template.utils.MCList]
acc:64 [in MetaCoq.Template.Kernames]
acc:65 [in MetaCoq.Template.Kernames]
acc:70 [in MetaCoq.Template.utils.MCList]
acc:73 [in MetaCoq.PCUIC.PCUICSR]
acc:753 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
acc:82 [in MetaCoq.Template.utils.MCList]
acc:84 [in MetaCoq.Template.utils.MCList]
acc:846 [in MetaCoq.Erasure.ErasureFunction]
acc:89 [in MetaCoq.PCUIC.PCUICSR]
acc:89 [in MetaCoq.PCUIC.PCUICContexts]
acc:93 [in MetaCoq.PCUIC.PCUICContexts]
acc:95 [in MetaCoq.Template.utils.MCList]
acc:97 [in MetaCoq.Template.utils.MCList]
acc:97 [in MetaCoq.PCUIC.PCUICSR]
acc:999 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
acG2:1157 [in MetaCoq.Template.utils.wGraph]
acG:1162 [in MetaCoq.Template.utils.wGraph]
Aeq:1660 [in MetaCoq.Translations.MiniHoTT]
Aeq:1668 [in MetaCoq.Translations.MiniHoTT_paths]
aftr:1423 [in MetaCoq.SafeChecker.PCUICSafeReduce]
af:477 [in MetaCoq.Examples.tauto]
af:479 [in MetaCoq.Examples.tauto]
af:481 [in MetaCoq.Examples.tauto]
allowed_elim:125 [in MetaCoq.PCUIC.PCUICInversion]
allowed_elim:58 [in MetaCoq.PCUIC.PCUICTyping]
allowed:250 [in MetaCoq.Template.Universes]
allowed:5 [in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
allowed:63 [in MetaCoq.PCUIC.PCUICWeakeningEnv]
allowed:640 [in MetaCoq.Template.Universes]
allq:173 [in MetaCoq.Template.monad_utils]
allq:207 [in MetaCoq.Template.monad_utils]
allq:769 [in MetaCoq.SafeChecker.PCUICSafeChecker]
all_levels:81 [in MetaCoq.PCUIC.PCUICWeakeningEnv]
all_levels:470 [in MetaCoq.Template.EnvironmentTyping]
all_levels:82 [in MetaCoq.SafeChecker.PCUICSafeChecker]
all:119 [in MetaCoq.PCUIC.utils.PCUICPretty]
all:269 [in MetaCoq.Template.EnvironmentTyping]
all:276 [in MetaCoq.Template.EnvironmentTyping]
all:59 [in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
all:68 [in MetaCoq.PCUIC.utils.PCUICPretty]
all:71 [in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
al:496 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
al:652 [in MetaCoq.SafeChecker.PCUICTypeChecker]
app':236 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
app':239 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
app':79 [in MetaCoq.Erasure.EAstUtils]
app':82 [in MetaCoq.Erasure.EAstUtils]
app:16 [in MetaCoq.Translations.param_binary]
app:180 [in MetaCoq.Erasure.ERemoveParams]
app:20 [in MetaCoq.Translations.param_binary]
app:6 [in MetaCoq.Translations.param_original]
apq:2997 [in MetaCoq.Translations.MiniHoTT]
apq:2998 [in MetaCoq.Translations.MiniHoTT]
apq:3005 [in MetaCoq.Translations.MiniHoTT_paths]
apq:3006 [in MetaCoq.Translations.MiniHoTT_paths]
argctx':134 [in MetaCoq.PCUIC.PCUICInductiveInversion]
argctx':161 [in MetaCoq.PCUIC.PCUICInductiveInversion]
argctx':710 [in MetaCoq.PCUIC.PCUICInductiveInversion]
argctx2:133 [in MetaCoq.PCUIC.PCUICInductiveInversion]
argctx2:160 [in MetaCoq.PCUIC.PCUICInductiveInversion]
argctx:132 [in MetaCoq.PCUIC.PCUICInductiveInversion]
argctx:159 [in MetaCoq.PCUIC.PCUICInductiveInversion]
argctx:260 [in MetaCoq.PCUIC.PCUICInductiveInversion]
argctx:331 [in MetaCoq.SafeChecker.PCUICSafeChecker]
argctx:412 [in MetaCoq.PCUIC.PCUICInductives]
argctx:428 [in MetaCoq.PCUIC.PCUICInductives]
argctx:709 [in MetaCoq.PCUIC.PCUICInductiveInversion]
argd:594 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
argsi:569 [in MetaCoq.PCUIC.PCUICSpine]
argsort:613 [in MetaCoq.Template.EnvironmentTyping]
argsort:916 [in MetaCoq.SafeChecker.PCUICSafeChecker]
argsr':1144 [in MetaCoq.PCUIC.PCUICConversion]
argsr:1143 [in MetaCoq.PCUIC.PCUICConversion]
argsubst':129 [in MetaCoq.PCUIC.PCUICInductiveInversion]
argsubst':156 [in MetaCoq.PCUIC.PCUICInductiveInversion]
argsubst:127 [in MetaCoq.PCUIC.PCUICInductiveInversion]
argsubst:154 [in MetaCoq.PCUIC.PCUICInductiveInversion]
argsubst:410 [in MetaCoq.PCUIC.PCUICInductives]
argsubst:426 [in MetaCoq.PCUIC.PCUICInductives]
argsub:560 [in MetaCoq.PCUIC.PCUICSpine]
argsv':73 [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
argsv:103 [in MetaCoq.PCUIC.PCUICWcbvEval]
argsv:107 [in MetaCoq.Template.WcbvEval]
argsv:173 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
argsv:181 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
argsv:192 [in MetaCoq.Template.WcbvEval]
argsv:201 [in MetaCoq.Template.WcbvEval]
argsv:233 [in MetaCoq.PCUIC.PCUICWcbvEval]
argsv:241 [in MetaCoq.Erasure.EWcbvEval]
argsv:247 [in MetaCoq.Erasure.EWcbvEval]
argsv:252 [in MetaCoq.Erasure.EWcbvEval]
argsv:289 [in MetaCoq.PCUIC.PCUICWcbvEval]
argsv:292 [in MetaCoq.PCUIC.PCUICWcbvEval]
argsv:297 [in MetaCoq.PCUIC.PCUICWcbvEval]
argsv:391 [in MetaCoq.Erasure.EWcbvEval]
argsv:62 [in MetaCoq.Erasure.EWcbvEval]
argsv:68 [in MetaCoq.Erasure.EWcbvEvalInd]
argsv:71 [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
argsv:71 [in MetaCoq.Erasure.EWcbvEval]
argsv:78 [in MetaCoq.Erasure.EWcbvEvalInd]
argsv:95 [in MetaCoq.PCUIC.PCUICWcbvEval]
argsv:98 [in MetaCoq.Template.WcbvEval]
args_sub:557 [in MetaCoq.PCUIC.PCUICSpine]
args'':129 [in MetaCoq.PCUIC.Bidirectional.BDUnique]
args'':31 [in MetaCoq.PCUIC.Bidirectional.BDUnique]
args':104 [in MetaCoq.Erasure.EArities]
args':111 [in MetaCoq.PCUIC.PCUICInductiveInversion]
args':112 [in MetaCoq.PCUIC.PCUICConvCumInversion]
args':114 [in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
args':1142 [in MetaCoq.PCUIC.PCUICConversion]
args':1168 [in MetaCoq.PCUIC.PCUICConversion]
args':1176 [in MetaCoq.PCUIC.PCUICConversion]
args':121 [in MetaCoq.PCUIC.PCUICInductiveInversion]
args':1230 [in MetaCoq.PCUIC.PCUICConversion]
args':124 [in MetaCoq.PCUIC.PCUICEquality]
args':1268 [in MetaCoq.PCUIC.PCUICConfluence]
args':127 [in MetaCoq.PCUIC.PCUICElimination]
args':1274 [in MetaCoq.PCUIC.PCUICConfluence]
args':128 [in MetaCoq.PCUIC.Bidirectional.BDUnique]
args':1280 [in MetaCoq.PCUIC.PCUICConfluence]
args':1287 [in MetaCoq.PCUIC.PCUICConfluence]
args':136 [in MetaCoq.Template.WcbvEval]
args':137 [in MetaCoq.Erasure.EWcbvEval]
args':141 [in MetaCoq.PCUIC.Bidirectional.BDUnique]
args':148 [in MetaCoq.PCUIC.PCUICInductiveInversion]
args':152 [in MetaCoq.PCUIC.Bidirectional.BDUnique]
args':163 [in MetaCoq.Erasure.EWcbvEvalInd]
args':17 [in MetaCoq.SafeChecker.PCUICSafeConversion]
args':172 [in MetaCoq.PCUIC.PCUICCanonicity]
args':179 [in MetaCoq.PCUIC.PCUICCanonicity]
args':18 [in MetaCoq.Erasure.Prelim]
args':188 [in MetaCoq.PCUIC.PCUICCanonicity]
args':188 [in MetaCoq.PCUIC.PCUICSpine]
args':195 [in MetaCoq.PCUIC.PCUICSpine]
args':202 [in MetaCoq.PCUIC.PCUICSpine]
args':208 [in MetaCoq.Erasure.EWcbvEval]
args':21 [in MetaCoq.PCUIC.PCUICExpandLets]
args':228 [in MetaCoq.Erasure.EConstructorsAsBlocks]
args':230 [in MetaCoq.Template.WcbvEval]
args':231 [in MetaCoq.Erasure.EWcbvEval]
args':236 [in MetaCoq.Erasure.EWcbvEval]
args':237 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
args':245 [in MetaCoq.PCUIC.PCUICCumulProp]
args':246 [in MetaCoq.Erasure.EWcbvEval]
args':252 [in MetaCoq.PCUIC.Syntax.PCUICCases]
args':264 [in MetaCoq.Erasure.EArities]
args':264 [in MetaCoq.PCUIC.PCUICWcbvEval]
args':264 [in MetaCoq.Erasure.EWcbvEval]
args':269 [in MetaCoq.PCUIC.PCUICWcbvEval]
args':272 [in MetaCoq.Erasure.EWcbvEval]
args':274 [in MetaCoq.PCUIC.PCUICWcbvEval]
args':275 [in MetaCoq.Erasure.EArities]
args':277 [in MetaCoq.Erasure.EWcbvEval]
args':279 [in MetaCoq.PCUIC.PCUICWcbvEval]
args':279 [in MetaCoq.Erasure.ERemoveParams]
args':28 [in MetaCoq.PCUIC.PCUICPrincipality]
args':280 [in MetaCoq.Erasure.EWcbvEval]
args':283 [in MetaCoq.Erasure.ERemoveParams]
args':30 [in MetaCoq.PCUIC.Bidirectional.BDUnique]
args':315 [in MetaCoq.Template.EtaExpand]
args':32 [in MetaCoq.PCUIC.PCUICContextSubst]
args':320 [in MetaCoq.Template.EtaExpand]
args':321 [in MetaCoq.PCUIC.PCUICSpine]
args':33 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
args':334 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
args':342 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
args':343 [in MetaCoq.PCUIC.PCUICCumulProp]
args':345 [in MetaCoq.PCUIC.PCUICSpine]
args':35 [in MetaCoq.Erasure.EArities]
args':352 [in MetaCoq.PCUIC.PCUICConversion]
args':354 [in MetaCoq.PCUIC.PCUICCumulProp]
args':355 [in MetaCoq.PCUIC.PCUICInductiveInversion]
args':357 [in MetaCoq.PCUIC.PCUICWcbvEval]
args':357 [in MetaCoq.PCUIC.PCUICSpine]
args':364 [in MetaCoq.PCUIC.PCUICCumulProp]
args':369 [in MetaCoq.Erasure.EWcbvEval]
args':377 [in MetaCoq.PCUIC.PCUICProgress]
args':390 [in MetaCoq.Erasure.EWcbvEval]
args':405 [in MetaCoq.Erasure.EWcbvEval]
args':41 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
args':412 [in MetaCoq.Erasure.EWcbvEval]
args':42 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
args':420 [in MetaCoq.Erasure.EWcbvEval]
args':428 [in MetaCoq.Erasure.EWcbvEval]
args':433 [in MetaCoq.PCUIC.PCUICNormal]
args':440 [in MetaCoq.PCUIC.PCUICNormal]
args':441 [in MetaCoq.Erasure.EWcbvEval]
args':445 [in MetaCoq.PCUIC.PCUICNormal]
args':453 [in MetaCoq.PCUIC.PCUICNormal]
args':453 [in MetaCoq.Erasure.EWcbvEval]
args':458 [in MetaCoq.PCUIC.PCUICConversion]
args':468 [in MetaCoq.Erasure.EEtaExpandedFix]
args':483 [in MetaCoq.PCUIC.PCUICConversion]
args':489 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
args':496 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
args':51 [in MetaCoq.PCUIC.PCUICConversion]
args':51 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
args':5231 [in MetaCoq.SafeChecker.PCUICSafeConversion]
args':529 [in MetaCoq.PCUIC.PCUICInductives]
args':540 [in MetaCoq.Erasure.EEtaExpandedFix]
args':548 [in MetaCoq.Erasure.EEtaExpandedFix]
args':555 [in MetaCoq.PCUIC.PCUICSpine]
args':56 [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
args':567 [in MetaCoq.PCUIC.PCUICSpine]
args':57 [in MetaCoq.PCUIC.PCUICConversion]
args':58 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
args':59 [in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
args':592 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
args':597 [in MetaCoq.PCUIC.PCUICSpine]
args':603 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
args':613 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
args':615 [in MetaCoq.PCUIC.PCUICSpine]
args':65 [in MetaCoq.PCUIC.PCUICContextSubst]
args':66 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
args':716 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
args':72 [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
args':720 [in MetaCoq.PCUIC.PCUICSpine]
args':75 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
args':76 [in MetaCoq.PCUIC.PCUICContextSubst]
args':80 [in MetaCoq.Template.TermEquality]
args':82 [in MetaCoq.Erasure.EArities]
args':827 [in MetaCoq.PCUIC.PCUICSpine]
args':85 [in MetaCoq.Erasure.EArities]
args':93 [in MetaCoq.Erasure.EArities]
args':94 [in MetaCoq.PCUIC.PCUICCanonicity]
args':98 [in MetaCoq.PCUIC.PCUICInductiveInversion]
args':98 [in MetaCoq.PCUIC.PCUICConvCumInversion]
args0:103 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
args0:1038 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
args0:114 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
args0:1224 [in MetaCoq.PCUIC.PCUICConversion]
args0:1315 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
args0:195 [in MetaCoq.PCUIC.PCUICParallelReduction]
args0:207 [in MetaCoq.PCUIC.PCUICParallelReduction]
args0:218 [in MetaCoq.PCUIC.PCUICParallelReduction]
args0:231 [in MetaCoq.PCUIC.PCUICParallelReduction]
args0:245 [in MetaCoq.PCUIC.PCUICParallelReduction]
args0:371 [in MetaCoq.PCUIC.PCUICParallelReduction]
args0:385 [in MetaCoq.PCUIC.PCUICParallelReduction]
args0:398 [in MetaCoq.PCUIC.PCUICParallelReduction]
args0:413 [in MetaCoq.PCUIC.PCUICParallelReduction]
args0:432 [in MetaCoq.PCUIC.PCUICParallelReduction]
args0:81 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
args0:94 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
args1:1039 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
args1:106 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
args1:115 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
args1:131 [in MetaCoq.SafeChecker.PCUICErrors]
args1:1316 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
args1:142 [in MetaCoq.SafeChecker.PCUICErrors]
args1:152 [in MetaCoq.SafeChecker.PCUICErrors]
args1:196 [in MetaCoq.PCUIC.PCUICParallelReduction]
args1:208 [in MetaCoq.PCUIC.PCUICParallelReduction]
args1:219 [in MetaCoq.PCUIC.PCUICParallelReduction]
args1:232 [in MetaCoq.PCUIC.PCUICParallelReduction]
args1:246 [in MetaCoq.PCUIC.PCUICParallelReduction]
args1:372 [in MetaCoq.PCUIC.PCUICParallelReduction]
args1:386 [in MetaCoq.PCUIC.PCUICParallelReduction]
args1:399 [in MetaCoq.PCUIC.PCUICParallelReduction]
args1:414 [in MetaCoq.PCUIC.PCUICParallelReduction]
args1:433 [in MetaCoq.PCUIC.PCUICParallelReduction]
args1:4399 [in MetaCoq.SafeChecker.PCUICSafeConversion]
args1:4417 [in MetaCoq.SafeChecker.PCUICSafeConversion]
args1:85 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
args1:95 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
args:1 [in MetaCoq.Erasure.Prelim]
args:10 [in MetaCoq.PCUIC.PCUICContextSubst]
args:100 [in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
args:100 [in MetaCoq.Template.Typing]
args:100 [in MetaCoq.PCUIC.PCUICFirstorder]
args:100 [in MetaCoq.PCUIC.Syntax.PCUICCases]
args:1006 [in MetaCoq.Erasure.ErasureFunction]
args:101 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
args:1013 [in MetaCoq.PCUIC.PCUICInductiveInversion]
args:1020 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
args:103 [in MetaCoq.Erasure.EWellformed]
args:103 [in MetaCoq.PCUIC.PCUICCanonicity]
args:104 [in MetaCoq.Erasure.EEtaExpandedFix]
args:104 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
args:105 [in MetaCoq.PCUIC.PCUICSpine]
args:106 [in MetaCoq.Template.WcbvEval]
args:107 [in MetaCoq.Template.Typing]
args:1077 [in MetaCoq.SafeChecker.PCUICTypeChecker]
args:108 [in MetaCoq.Erasure.EWcbvEvalInd]
args:1082 [in MetaCoq.Template.Typing]
args:109 [in MetaCoq.Erasure.EWellformed]
args:11 [in MetaCoq.PCUIC.PCUICProgress]
args:110 [in MetaCoq.PCUIC.PCUICInductiveInversion]
args:110 [in MetaCoq.PCUIC.PCUICConvCumInversion]
args:110 [in MetaCoq.PCUIC.PCUICCanonicity]
args:1102 [in MetaCoq.SafeChecker.PCUICTypeChecker]
args:111 [in MetaCoq.Erasure.EAstUtils]
args:111 [in MetaCoq.Erasure.EWcbvEval]
args:112 [in MetaCoq.Template.EtaExpand]
args:112 [in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
args:113 [in MetaCoq.PCUIC.PCUICArities]
args:113 [in MetaCoq.PCUIC.PCUICWcbvEval]
args:113 [in MetaCoq.Erasure.EAstUtils]
args:114 [in MetaCoq.Template.Typing]
args:1141 [in MetaCoq.PCUIC.PCUICConversion]
args:115 [in MetaCoq.Erasure.EInduction]
args:115 [in MetaCoq.Template.WcbvEval]
args:115 [in MetaCoq.Erasure.EAstUtils]
args:116 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
args:1167 [in MetaCoq.PCUIC.PCUICConversion]
args:117 [in MetaCoq.Erasure.EWcbvEval]
args:1175 [in MetaCoq.PCUIC.PCUICConversion]
args:118 [in MetaCoq.PCUIC.PCUICEtaExpand]
args:118 [in MetaCoq.PCUIC.PCUICInductiveInversion]
args:118 [in MetaCoq.Erasure.EEtaExpanded]
args:12 [in MetaCoq.Erasure.EEtaExpandedFix]
args:12 [in MetaCoq.Erasure.Prelim]
args:120 [in MetaCoq.PCUIC.PCUICArities]
args:120 [in MetaCoq.Erasure.EInlineProjections]
args:120 [in MetaCoq.Erasure.EWcbvEvalInd]
args:121 [in MetaCoq.Template.Typing]
args:121 [in MetaCoq.PCUIC.PCUICCanonicity]
args:122 [in MetaCoq.PCUIC.PCUICWcbvEval]
args:122 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
args:1223 [in MetaCoq.PCUIC.PCUICConversion]
args:1229 [in MetaCoq.PCUIC.PCUICConversion]
args:123 [in MetaCoq.PCUIC.PCUICEquality]
args:124 [in MetaCoq.PCUIC.PCUICArities]
args:124 [in MetaCoq.Template.WcbvEval]
args:124 [in MetaCoq.Erasure.EEtaExpanded]
args:124 [in MetaCoq.Erasure.EOptimizePropDiscr]
args:1259 [in MetaCoq.SafeChecker.PCUICSafeReduce]
args:126 [in MetaCoq.Erasure.ERemoveParams]
args:1263 [in MetaCoq.SafeChecker.PCUICSafeReduce]
args:1266 [in MetaCoq.PCUIC.PCUICConfluence]
args:127 [in MetaCoq.PCUIC.Bidirectional.BDUnique]
args:1272 [in MetaCoq.PCUIC.PCUICConfluence]
args:1278 [in MetaCoq.PCUIC.PCUICConfluence]
args:128 [in MetaCoq.PCUIC.PCUICElimination]
args:128 [in MetaCoq.Erasure.EConstructorsAsBlocks]
args:128 [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
args:128 [in MetaCoq.Erasure.EWcbvEval]
args:1284 [in MetaCoq.PCUIC.PCUICConfluence]
args:129 [in MetaCoq.Erasure.EConstructorsAsBlocks]
args:129 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
args:13 [in MetaCoq.PCUIC.PCUICElimination]
args:13 [in MetaCoq.PCUIC.PCUICExpandLets]
args:13 [in MetaCoq.PCUIC.PCUICEtaExpand]
args:130 [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
args:131 [in MetaCoq.Template.Typing]
args:131 [in MetaCoq.PCUIC.PCUICContexts]
args:132 [in MetaCoq.Template.EtaExpand]
args:132 [in MetaCoq.PCUIC.PCUICArities]
args:132 [in MetaCoq.PCUIC.PCUICWfUniverses]
args:132 [in MetaCoq.Erasure.EConstructorsAsBlocks]
args:132 [in MetaCoq.Erasure.EWcbvEvalInd]
args:132 [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
args:132 [in MetaCoq.PCUIC.PCUICSpine]
args:133 [in MetaCoq.PCUIC.PCUICWcbvEval]
args:133 [in MetaCoq.Erasure.EConstructorsAsBlocks]
args:133 [in MetaCoq.PCUIC.PCUICCanonicity]
args:133 [in MetaCoq.Erasure.ERemoveParams]
args:134 [in MetaCoq.Erasure.EConstructorsAsBlocks]
args:135 [in MetaCoq.PCUIC.PCUICSubstitution]
args:135 [in MetaCoq.Template.WcbvEval]
args:135 [in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
args:1352 [in MetaCoq.Erasure.ErasureFunction]
args:136 [in MetaCoq.PCUIC.PCUICArities]
args:136 [in MetaCoq.PCUIC.PCUICFirstorder]
args:136 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
args:136 [in MetaCoq.Erasure.EWcbvEval]
args:1361 [in MetaCoq.Erasure.ErasureFunction]
args:137 [in MetaCoq.Erasure.EConstructorsAsBlocks]
args:1379 [in MetaCoq.Erasure.ErasureFunction]
args:138 [in MetaCoq.PCUIC.PCUICEtaExpand]
args:138 [in MetaCoq.Erasure.EEtaExpanded]
args:138 [in MetaCoq.Template.AstUtils]
args:1398 [in MetaCoq.SafeChecker.PCUICSafeReduce]
args:14 [in MetaCoq.SafeChecker.PCUICSafeConversion]
args:140 [in MetaCoq.PCUIC.PCUICArities]
args:140 [in MetaCoq.PCUIC.Bidirectional.BDUnique]
args:1400 [in MetaCoq.SafeChecker.PCUICSafeReduce]
args:1401 [in MetaCoq.Erasure.ErasureFunction]
args:1407 [in MetaCoq.SafeChecker.PCUICSafeReduce]
args:1414 [in MetaCoq.SafeChecker.PCUICSafeReduce]
args:142 [in MetaCoq.Erasure.EConstructorsAsBlocks]
args:142 [in MetaCoq.PCUIC.PCUICFirstorder]
args:1422 [in MetaCoq.SafeChecker.PCUICSafeReduce]
args:1429 [in MetaCoq.SafeChecker.PCUICSafeReduce]
args:143 [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
args:1438 [in MetaCoq.SafeChecker.PCUICSafeReduce]
args:145 [in MetaCoq.PCUIC.PCUICInductiveInversion]
args:145 [in MetaCoq.PCUIC.PCUICTyping]
args:145 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
args:146 [in MetaCoq.PCUIC.PCUICWfUniverses]
args:147 [in MetaCoq.Template.EtaExpand]
args:148 [in MetaCoq.PCUIC.PCUICSpine]
args:149 [in MetaCoq.Erasure.EWcbvEvalInd]
args:150 [in MetaCoq.PCUIC.Bidirectional.BDUnique]
args:151 [in MetaCoq.Erasure.EConstructorsAsBlocks]
args:151 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
args:151 [in MetaCoq.Examples.tauto]
args:151 [in MetaCoq.Erasure.EGlobalEnv]
args:153 [in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
args:154 [in MetaCoq.Template.EtaExpand]
args:155 [in MetaCoq.Examples.tauto]
args:155 [in MetaCoq.Template.AstUtils]
args:156 [in MetaCoq.PCUIC.PCUICCanonicity]
args:156 [in MetaCoq.PCUIC.PCUICContexts]
args:157 [in MetaCoq.PCUIC.PCUICInversion]
args:158 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
args:159 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
args:159 [in MetaCoq.PCUIC.PCUICContexts]
args:16 [in MetaCoq.Template.EtaExpand]
args:16 [in MetaCoq.Erasure.EInduction]
args:16 [in MetaCoq.PCUIC.PCUICExpandLets]
args:16 [in MetaCoq.PCUIC.PCUICCanonicity]
args:16 [in MetaCoq.PCUIC.PCUICContextSubst]
args:160 [in MetaCoq.Template.WfAst]
args:160 [in MetaCoq.PCUIC.PCUICSubstitution]
args:161 [in MetaCoq.Template.EtaExpand]
args:161 [in MetaCoq.PCUIC.PCUICSafeLemmata]
args:162 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
args:162 [in MetaCoq.PCUIC.PCUICWcbvEval]
args:162 [in MetaCoq.Erasure.EWcbvEvalInd]
args:162 [in MetaCoq.PCUIC.PCUICContexts]
args:164 [in MetaCoq.PCUIC.PCUICWcbvEval]
args:164 [in MetaCoq.PCUIC.PCUICFirstorder]
args:165 [in MetaCoq.Template.LiftSubst]
args:166 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
args:167 [in MetaCoq.PCUIC.PCUICElimination]
args:167 [in MetaCoq.Erasure.EWcbvEval]
args:168 [in MetaCoq.PCUIC.PCUICWcbvEval]
args:169 [in MetaCoq.Template.WcbvEval]
args:169 [in MetaCoq.PCUIC.PCUICCanonicity]
args:169 [in MetaCoq.Erasure.EWcbvEval]
args:17 [in MetaCoq.Erasure.EEtaExpandedFix]
args:17 [in MetaCoq.PCUIC.PCUICEtaExpand]
args:17 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
args:17 [in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
args:17 [in MetaCoq.Erasure.Prelim]
args:170 [in MetaCoq.PCUIC.PCUICContexts]
args:171 [in MetaCoq.Erasure.ERemoveParams]
args:172 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
args:1724 [in MetaCoq.SafeChecker.PCUICSafeReduce]
args:1725 [in MetaCoq.SafeChecker.PCUICSafeReduce]
args:173 [in MetaCoq.PCUIC.PCUICWcbvEval]
args:173 [in MetaCoq.Erasure.EWcbvEval]
args:173 [in MetaCoq.PCUIC.PCUICSpine]
args:1735 [in MetaCoq.SafeChecker.PCUICSafeReduce]
args:174 [in MetaCoq.PCUIC.PCUICInductives]
args:175 [in MetaCoq.Erasure.ERemoveParams]
args:176 [in MetaCoq.PCUIC.PCUICCanonicity]
args:177 [in MetaCoq.PCUIC.PCUICEtaExpand]
args:177 [in MetaCoq.PCUIC.PCUICNormal]
args:177 [in MetaCoq.PCUIC.PCUICReduction]
args:178 [in MetaCoq.Examples.tauto]
args:179 [in MetaCoq.Template.WcbvEval]
args:18 [in MetaCoq.PCUIC.PCUICReduction]
args:181 [in MetaCoq.PCUIC.PCUICFirstorder]
args:181 [in MetaCoq.PCUIC.PCUICCanonicity]
args:181 [in MetaCoq.Erasure.EWcbvEval]
args:182 [in MetaCoq.Template.Ast]
args:183 [in MetaCoq.Template.EtaExpand]
args:183 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
args:184 [in MetaCoq.PCUIC.PCUICNormal]
args:184 [in MetaCoq.PCUIC.PCUICReduction]
args:185 [in MetaCoq.PCUIC.PCUICSpine]
args:186 [in MetaCoq.PCUIC.PCUICFirstorder]
args:186 [in MetaCoq.PCUIC.PCUICCanonicity]
args:187 [in MetaCoq.PCUIC.PCUICProgress]
args:187 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
args:187 [in MetaCoq.Erasure.EWcbvEval]
args:188 [in MetaCoq.Erasure.EEtaExpanded]
args:19 [in MetaCoq.Erasure.ESpineView]
args:191 [in MetaCoq.PCUIC.PCUICNormal]
args:191 [in MetaCoq.Template.WcbvEval]
args:192 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
args:192 [in MetaCoq.Erasure.EWcbvEval]
args:192 [in MetaCoq.PCUIC.PCUICReduction]
args:193 [in MetaCoq.PCUIC.PCUICSpine]
args:195 [in MetaCoq.Erasure.EEtaExpanded]
args:197 [in MetaCoq.Erasure.EConstructorsAsBlocks]
args:197 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
args:198 [in MetaCoq.Template.Ast]
args:198 [in MetaCoq.PCUIC.PCUICCanonicity]
args:200 [in MetaCoq.PCUIC.PCUICWfUniverses]
args:200 [in MetaCoq.Template.WcbvEval]
args:200 [in MetaCoq.PCUIC.PCUICReduction]
args:200 [in MetaCoq.PCUIC.PCUICSpine]
args:201 [in MetaCoq.Erasure.EWcbvEval]
args:203 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
args:2045 [in MetaCoq.SafeChecker.PCUICSafeConversion]
args:205 [in MetaCoq.PCUIC.PCUICCanonicity]
args:206 [in MetaCoq.PCUIC.PCUICSafeLemmata]
args:206 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
args:206 [in MetaCoq.Erasure.EWcbvEval]
args:207 [in MetaCoq.PCUIC.PCUICSpine]
args:209 [in MetaCoq.Template.WcbvEval]
args:21 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
args:210 [in MetaCoq.PCUIC.PCUICReduction]
args:211 [in MetaCoq.Template.EtaExpand]
args:211 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
args:212 [in MetaCoq.Erasure.EInduction]
args:212 [in MetaCoq.PCUIC.PCUICSpine]
args:215 [in MetaCoq.Erasure.EEtaExpanded]
args:216 [in MetaCoq.PCUIC.PCUICWcbvEval]
args:216 [in MetaCoq.Erasure.EConstructorsAsBlocks]
args:218 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
args:218 [in MetaCoq.Template.WcbvEval]
args:219 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
args:22 [in MetaCoq.Template.EtaExpand]
args:22 [in MetaCoq.PCUIC.PCUICExpandLets]
args:220 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
args:221 [in MetaCoq.Erasure.EEtaExpanded]
args:222 [in MetaCoq.Erasure.EConstructorsAsBlocks]
args:223 [in MetaCoq.PCUIC.PCUICCanonicity]
args:224 [in MetaCoq.PCUIC.PCUICWcbvEval]
args:225 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
args:226 [in MetaCoq.PCUIC.PCUICInductiveInversion]
args:227 [in MetaCoq.PCUIC.PCUICCanonicity]
args:228 [in MetaCoq.Erasure.EEtaExpanded]
args:229 [in MetaCoq.Template.WcbvEval]
args:229 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
args:229 [in MetaCoq.Erasure.EWcbvEval]
args:23 [in MetaCoq.PCUIC.PCUICElimination]
args:230 [in MetaCoq.SafeChecker.PCUICSafeReduce]
args:231 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
args:231 [in MetaCoq.PCUIC.PCUICNormal]
args:232 [in MetaCoq.Template.EtaExpand]
args:234 [in MetaCoq.PCUIC.PCUICSubstitution]
args:234 [in MetaCoq.Erasure.EWcbvEval]
args:236 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
args:239 [in MetaCoq.PCUIC.PCUICWcbvEval]
args:239 [in MetaCoq.PCUIC.PCUICSubstitution]
args:24 [in MetaCoq.Erasure.EEtaExpandedFix]
args:24 [in MetaCoq.PCUIC.PCUICReduction]
args:241 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
args:244 [in MetaCoq.PCUIC.PCUICCumulProp]
args:245 [in MetaCoq.PCUIC.PCUICNormal]
args:245 [in MetaCoq.Erasure.EWcbvEval]
args:246 [in MetaCoq.PCUIC.PCUICWcbvEval]
args:247 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
args:248 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
args:249 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
args:251 [in MetaCoq.PCUIC.Syntax.PCUICCases]
args:251 [in MetaCoq.Erasure.EEtaExpanded]
args:253 [in MetaCoq.PCUIC.PCUICTyping]
args:2530 [in MetaCoq.Template.utils.All_Forall]
args:255 [in MetaCoq.PCUIC.PCUICInductiveInversion]
args:256 [in MetaCoq.PCUIC.PCUICNormal]
args:256 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
args:256 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
args:26 [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
args:26 [in MetaCoq.PCUIC.PCUICTyping]
args:263 [in MetaCoq.Erasure.EArities]
args:263 [in MetaCoq.PCUIC.PCUICWcbvEval]
args:263 [in MetaCoq.Template.WcbvEval]
args:263 [in MetaCoq.Erasure.EWcbvEval]
args:264 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
args:266 [in MetaCoq.PCUIC.PCUICNormal]
args:267 [in MetaCoq.Template.Typing]
args:267 [in MetaCoq.Template.WcbvEval]
args:267 [in MetaCoq.PCUIC.PCUICSpine]
args:268 [in MetaCoq.PCUIC.PCUICWcbvEval]
args:269 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
args:27 [in MetaCoq.PCUIC.PCUICSafeLemmata]
args:27 [in MetaCoq.PCUIC.PCUICPrincipality]
args:27 [in MetaCoq.PCUIC.Bidirectional.BDUnique]
args:271 [in MetaCoq.Erasure.EWcbvEval]
args:272 [in MetaCoq.Template.WcbvEval]
args:273 [in MetaCoq.PCUIC.PCUICWcbvEval]
args:274 [in MetaCoq.Erasure.EArities]
args:275 [in MetaCoq.Template.Typing]
args:275 [in MetaCoq.Erasure.ERemoveParams]
args:276 [in MetaCoq.Erasure.ERemoveParams]
args:276 [in MetaCoq.Erasure.EWcbvEval]
args:277 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
args:278 [in MetaCoq.PCUIC.PCUICWcbvEval]
args:278 [in MetaCoq.Erasure.ERemoveParams]
args:279 [in MetaCoq.Template.WcbvEval]
args:279 [in MetaCoq.Erasure.EWcbvEval]
args:28 [in MetaCoq.PCUIC.PCUICCanonicity]
args:281 [in MetaCoq.Template.WcbvEval]
args:282 [in MetaCoq.Erasure.ERemoveParams]
args:283 [in MetaCoq.Template.Typing]
args:285 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
args:286 [in MetaCoq.PCUIC.PCUICSafeLemmata]
args:286 [in MetaCoq.Erasure.ERemoveParams]
args:288 [in MetaCoq.Erasure.EArities]
args:288 [in MetaCoq.PCUIC.PCUICWcbvEval]
args:288 [in MetaCoq.Erasure.EEtaExpanded]
args:288 [in MetaCoq.PCUIC.PCUICSpine]
args:289 [in MetaCoq.Template.EtaExpand]
args:29 [in MetaCoq.PCUIC.PCUICContextSubst]
args:291 [in MetaCoq.Template.Typing]
args:291 [in MetaCoq.Erasure.EEtaExpanded]
args:294 [in MetaCoq.PCUIC.PCUICSpine]
args:295 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
args:295 [in MetaCoq.Template.EtaExpand]
args:296 [in MetaCoq.Erasure.EArities]
args:3 [in MetaCoq.Template.EtaExpand]
args:3 [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
args:30 [in MetaCoq.PCUIC.PCUICEtaExpand]
args:301 [in MetaCoq.Template.Typing]
args:303 [in MetaCoq.Template.EtaExpand]
args:306 [in MetaCoq.Template.WcbvEval]
args:308 [in MetaCoq.Erasure.EWcbvEval]
args:31 [in MetaCoq.Erasure.EWcbvEvalInd]
args:31 [in MetaCoq.PCUIC.PCUICReduction]
args:310 [in MetaCoq.Template.EtaExpand]
args:310 [in MetaCoq.PCUIC.PCUICSpine]
args:311 [in MetaCoq.PCUIC.PCUICInductiveInversion]
args:314 [in MetaCoq.Template.EtaExpand]
args:314 [in MetaCoq.Template.TypingWf]
args:316 [in MetaCoq.PCUIC.PCUICWcbvEval]
args:319 [in MetaCoq.Template.EtaExpand]
args:319 [in MetaCoq.PCUIC.PCUICSpine]
args:32 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
args:32 [in MetaCoq.PCUIC.PCUICArities]
args:32 [in MetaCoq.PCUIC.PCUICWcbvEval]
args:32 [in MetaCoq.Erasure.EInlineProjections]
args:32 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
args:32 [in MetaCoq.PCUIC.PCUICCanonicity]
args:320 [in MetaCoq.PCUIC.PCUICWcbvEval]
args:324 [in MetaCoq.Template.EtaExpand]
args:324 [in MetaCoq.PCUIC.PCUICSpine]
args:326 [in MetaCoq.PCUIC.PCUICNormal]
args:327 [in MetaCoq.Template.TypingWf]
args:328 [in MetaCoq.PCUIC.PCUICSpine]
args:329 [in MetaCoq.Erasure.EWcbvEval]
args:33 [in MetaCoq.PCUIC.PCUICElimination]
args:330 [in MetaCoq.Erasure.EArities]
args:331 [in MetaCoq.PCUIC.PCUICNormal]
args:333 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
args:333 [in MetaCoq.SafeChecker.PCUICSafeChecker]
args:333 [in MetaCoq.Template.TypingWf]
args:335 [in MetaCoq.PCUIC.PCUICSpine]
args:337 [in MetaCoq.PCUIC.PCUICProgress]
args:339 [in MetaCoq.PCUIC.PCUICSpine]
args:34 [in MetaCoq.Erasure.EArities]
args:34 [in MetaCoq.Template.Typing]
args:34 [in MetaCoq.PCUIC.PCUICTyping]
args:341 [in MetaCoq.Erasure.EArities]
args:341 [in MetaCoq.PCUIC.PCUICCumulProp]
args:341 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
args:343 [in MetaCoq.Template.TypingWf]
args:344 [in MetaCoq.PCUIC.PCUICSpine]
args:35 [in MetaCoq.Erasure.EEtaExpandedFix]
args:35 [in MetaCoq.PCUIC.PCUICContextSubst]
args:350 [in MetaCoq.PCUIC.PCUICConversion]
args:350 [in MetaCoq.PCUIC.PCUICSpine]
args:351 [in MetaCoq.PCUIC.PCUICCumulProp]
args:353 [in MetaCoq.PCUIC.PCUICInductiveInversion]
args:354 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
args:355 [in MetaCoq.Erasure.EEtaExpandedFix]
args:355 [in MetaCoq.PCUIC.PCUICWcbvEval]
args:356 [in MetaCoq.PCUIC.PCUICSpine]
args:357 [in MetaCoq.PCUIC.PCUICConfluence]
args:357 [in MetaCoq.PCUIC.PCUICSR]
args:358 [in MetaCoq.PCUIC.PCUICConfluence]
args:361 [in MetaCoq.PCUIC.PCUICCumulProp]
args:363 [in MetaCoq.PCUIC.PCUICSpine]
args:364 [in MetaCoq.PCUIC.PCUICSR]
args:364 [in MetaCoq.Erasure.ERemoveParams]
args:366 [in MetaCoq.Erasure.EWcbvEval]
args:368 [in MetaCoq.PCUIC.PCUICProgress]
args:369 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
args:369 [in MetaCoq.PCUIC.PCUICConfluence]
args:369 [in MetaCoq.PCUIC.PCUICSpine]
args:37 [in MetaCoq.PCUIC.Syntax.PCUICCases]
args:370 [in MetaCoq.PCUIC.PCUICConfluence]
args:372 [in MetaCoq.PCUIC.PCUICSR]
args:374 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
args:375 [in MetaCoq.PCUIC.PCUICSpine]
args:376 [in MetaCoq.PCUIC.PCUICProgress]
args:376 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
args:38 [in MetaCoq.PCUIC.PCUICCanonicity]
args:38 [in MetaCoq.Template.AstUtils]
args:38 [in MetaCoq.PCUIC.PCUICReduction]
args:380 [in MetaCoq.PCUIC.PCUICSR]
args:382 [in MetaCoq.PCUIC.PCUICSpine]
args:383 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
args:384 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
args:385 [in MetaCoq.Erasure.EWcbvEval]
args:386 [in MetaCoq.PCUIC.PCUICSpine]
args:39 [in MetaCoq.PCUIC.PCUICProgress]
args:39 [in MetaCoq.PCUIC.PCUICWcbvEval]
args:39 [in MetaCoq.Erasure.EWcbvEval]
args:390 [in MetaCoq.PCUIC.PCUICSR]
args:391 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
args:392 [in MetaCoq.Template.Ast]
args:392 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
args:394 [in MetaCoq.PCUIC.PCUICProgress]
args:395 [in MetaCoq.PCUIC.PCUICInductives]
args:398 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
args:399 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
args:4 [in MetaCoq.Erasure.EDeps]
args:4 [in MetaCoq.PCUIC.PCUICContextSubst]
args:40 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
args:40 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
args:402 [in MetaCoq.Erasure.EWcbvEval]
args:404 [in MetaCoq.PCUIC.PCUICInductives]
args:405 [in MetaCoq.PCUIC.PCUICProgress]
args:409 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
args:41 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
args:41 [in MetaCoq.PCUIC.PCUICWcbvEval]
args:41 [in MetaCoq.PCUIC.PCUICFirstorder]
args:41 [in MetaCoq.Template.WcbvEval]
args:410 [in MetaCoq.Erasure.EEtaExpandedFix]
args:410 [in MetaCoq.Erasure.EWcbvEval]
args:411 [in MetaCoq.Template.EtaExpand]
args:412 [in MetaCoq.PCUIC.PCUICProgress]
args:416 [in MetaCoq.PCUIC.PCUICProgress]
args:416 [in MetaCoq.Erasure.EEtaExpandedFix]
args:417 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
args:417 [in MetaCoq.Erasure.EWcbvEval]
args:418 [in MetaCoq.PCUIC.PCUICInductives]
args:42 [in MetaCoq.Erasure.EOptimizePropDiscr]
args:422 [in MetaCoq.PCUIC.PCUICProgress]
args:424 [in MetaCoq.Erasure.EEtaExpandedFix]
args:424 [in MetaCoq.Erasure.EWcbvEval]
args:424 [in MetaCoq.SafeChecker.PCUICSafeChecker]
args:428 [in MetaCoq.PCUIC.PCUICProgress]
args:43 [in MetaCoq.PCUIC.PCUICWcbvEval]
args:432 [in MetaCoq.PCUIC.PCUICNormal]
args:436 [in MetaCoq.PCUIC.PCUICProgress]
args:436 [in MetaCoq.SafeChecker.PCUICSafeChecker]
args:437 [in MetaCoq.PCUIC.PCUICNormal]
args:438 [in MetaCoq.Erasure.EWcbvEval]
args:439 [in MetaCoq.PCUIC.PCUICInductives]
args:44 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
args:44 [in MetaCoq.SafeChecker.PCUICTypeChecker]
args:442 [in MetaCoq.SafeChecker.PCUICSafeChecker]
args:447 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
args:447 [in MetaCoq.PCUIC.PCUICNormal]
args:45 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
args:45 [in MetaCoq.PCUIC.PCUICWcbvEval]
args:450 [in MetaCoq.Erasure.EWcbvEval]
args:451 [in MetaCoq.PCUIC.PCUICNormal]
args:452 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
args:452 [in MetaCoq.SafeChecker.PCUICSafeChecker]
args:456 [in MetaCoq.PCUIC.PCUICConversion]
args:459 [in MetaCoq.Erasure.EEtaExpandedFix]
args:46 [in MetaCoq.Erasure.EAstUtils]
args:462 [in MetaCoq.SafeChecker.PCUICSafeChecker]
args:465 [in MetaCoq.Erasure.EEtaExpandedFix]
args:469 [in MetaCoq.PCUIC.PCUICConversion]
args:47 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
args:47 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
args:47 [in MetaCoq.PCUIC.PCUICWcbvEval]
args:47 [in MetaCoq.PCUIC.PCUICEtaExpand]
args:47 [in MetaCoq.Erasure.EWcbvEvalInd]
args:47 [in MetaCoq.PCUIC.PCUICReduction]
args:472 [in MetaCoq.SafeChecker.PCUICSafeChecker]
args:476 [in MetaCoq.PCUIC.PCUICProgress]
args:476 [in MetaCoq.PCUIC.PCUICConversion]
args:479 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
args:48 [in MetaCoq.Erasure.EEtaExpandedFix]
args:48 [in MetaCoq.Erasure.EWcbvEval]
args:481 [in MetaCoq.SafeChecker.PCUICSafeChecker]
args:482 [in MetaCoq.PCUIC.PCUICConversion]
args:484 [in MetaCoq.PCUIC.PCUICProgress]
args:488 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
args:488 [in MetaCoq.PCUIC.PCUICConversion]
args:488 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
args:49 [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
args:49 [in MetaCoq.PCUIC.PCUICCanonicity]
args:493 [in MetaCoq.PCUIC.PCUICConversion]
args:495 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
args:498 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
args:5 [in MetaCoq.Erasure.EEtaExpandedFix]
args:5 [in MetaCoq.Erasure.EWcbvEval]
args:50 [in MetaCoq.PCUIC.PCUICFirstorder]
args:50 [in MetaCoq.PCUIC.PCUICConversion]
args:50 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
args:50 [in MetaCoq.SafeChecker.PCUICTypeChecker]
args:502 [in MetaCoq.PCUIC.PCUICSpine]
args:503 [in MetaCoq.Erasure.EEtaExpandedFix]
args:503 [in MetaCoq.Template.utils.MCList]
args:51 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
args:51 [in MetaCoq.PCUIC.PCUICInductiveInversion]
args:51 [in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
args:511 [in MetaCoq.Erasure.EEtaExpandedFix]
args:515 [in MetaCoq.Erasure.EEtaExpandedFix]
args:515 [in MetaCoq.PCUIC.PCUICSpine]
args:517 [in MetaCoq.Erasure.EEtaExpandedFix]
args:519 [in MetaCoq.PCUIC.PCUICSpine]
args:52 [in MetaCoq.PCUIC.PCUICInductives]
args:523 [in MetaCoq.PCUIC.PCUICSpine]
args:526 [in MetaCoq.PCUIC.PCUICInductives]
args:528 [in MetaCoq.Erasure.EEtaExpandedFix]
args:53 [in MetaCoq.Erasure.EEtaExpandedFix]
args:532 [in MetaCoq.SafeChecker.PCUICSafeConversion]
args:532 [in MetaCoq.PCUIC.PCUICSpine]
args:538 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
args:539 [in MetaCoq.Erasure.EEtaExpandedFix]
args:541 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
args:547 [in MetaCoq.Erasure.EEtaExpandedFix]
args:548 [in MetaCoq.PCUIC.PCUICInductives]
args:55 [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
args:552 [in MetaCoq.PCUIC.PCUICInductives]
args:554 [in MetaCoq.PCUIC.PCUICSpine]
args:556 [in MetaCoq.Erasure.EEtaExpandedFix]
args:559 [in MetaCoq.PCUIC.PCUICSpine]
args:56 [in MetaCoq.PCUIC.PCUICConversion]
args:56 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
args:56 [in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
args:564 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
args:566 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
args:566 [in MetaCoq.PCUIC.PCUICInductives]
args:566 [in MetaCoq.PCUIC.PCUICSpine]
args:57 [in MetaCoq.PCUIC.PCUICContextSubst]
args:572 [in MetaCoq.PCUIC.PCUICSpine]
args:574 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
args:579 [in MetaCoq.PCUIC.PCUICTyping]
args:58 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
args:58 [in MetaCoq.Erasure.EEtaExpandedFix]
args:58 [in MetaCoq.Erasure.EOptimizePropDiscr]
args:580 [in MetaCoq.PCUIC.PCUICSpine]
args:586 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
args:587 [in MetaCoq.Template.Typing]
args:590 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
args:591 [in MetaCoq.PCUIC.PCUICSpine]
args:594 [in MetaCoq.Template.Typing]
args:596 [in MetaCoq.PCUIC.PCUICSpine]
args:6 [in MetaCoq.Examples.constructor_tac]
args:60 [in MetaCoq.PCUIC.PCUICNormal]
args:60 [in MetaCoq.PCUIC.PCUICContextSubst]
args:601 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
args:61 [in MetaCoq.PCUIC.PCUICEtaExpand]
args:610 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
args:613 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
args:614 [in MetaCoq.PCUIC.PCUICSpine]
args:617 [in MetaCoq.PCUIC.PCUICParallelReduction]
args:619 [in MetaCoq.PCUIC.PCUICSpine]
args:623 [in MetaCoq.PCUIC.PCUICSpine]
args:64 [in MetaCoq.PCUIC.PCUICContextSubst]
args:64 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
args:65 [in MetaCoq.Erasure.EGenericMapEnv]
args:671 [in MetaCoq.Template.Typing]
args:680 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
args:684 [in MetaCoq.Template.utils.MCList]
args:69 [in MetaCoq.Erasure.EEtaExpandedFix]
args:69 [in MetaCoq.PCUIC.PCUICFirstorder]
args:692 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
args:70 [in MetaCoq.PCUIC.PCUICContextSubst]
args:70 [in MetaCoq.PCUIC.PCUICSpine]
args:713 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
args:719 [in MetaCoq.PCUIC.PCUICSpine]
args:719 [in MetaCoq.SafeChecker.PCUICTypeChecker]
args:72 [in MetaCoq.PCUIC.PCUICEtaExpand]
args:72 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
args:728 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
args:73 [in MetaCoq.PCUIC.PCUICCanonicity]
args:73 [in MetaCoq.PCUIC.PCUICContextSubst]
args:731 [in MetaCoq.Template.Typing]
args:74 [in MetaCoq.Translations.times_bool_fun]
args:74 [in MetaCoq.Erasure.EAstUtils]
args:74 [in MetaCoq.Erasure.Prelim]
args:76 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
args:76 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
args:77 [in MetaCoq.Translations.times_bool_fun]
args:77 [in MetaCoq.PCUIC.PCUICWcbvEval]
args:77 [in MetaCoq.PCUIC.PCUICEtaExpand]
args:77 [in MetaCoq.Template.WcbvEval]
args:779 [in MetaCoq.PCUIC.PCUICInductiveInversion]
args:79 [in MetaCoq.Template.TermEquality]
args:79 [in MetaCoq.PCUIC.PCUICCanonicity]
args:79 [in MetaCoq.PCUIC.PCUICContextSubst]
args:8 [in MetaCoq.Erasure.EDeps]
args:8 [in MetaCoq.Examples.constructor_tac]
args:80 [in MetaCoq.PCUIC.PCUICNormal]
args:80 [in MetaCoq.PCUIC.PCUICFirstorder]
args:80 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
args:805 [in MetaCoq.PCUIC.PCUICInductiveInversion]
args:81 [in MetaCoq.Erasure.EArities]
args:819 [in MetaCoq.PCUIC.PCUICSpine]
args:826 [in MetaCoq.PCUIC.PCUICSpine]
args:83 [in MetaCoq.PCUIC.PCUICElimination]
args:83 [in MetaCoq.PCUIC.PCUICNormal]
args:84 [in MetaCoq.PCUIC.PCUICWcbvEval]
args:84 [in MetaCoq.Erasure.EAstUtils]
args:85 [in MetaCoq.Erasure.EEtaExpandedFix]
args:85 [in MetaCoq.PCUIC.PCUICConvCumInversion]
args:85 [in MetaCoq.Template.WcbvEval]
args:87 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
args:87 [in MetaCoq.PCUIC.PCUICCanonicity]
args:88 [in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
args:89 [in MetaCoq.Erasure.EConstructorsAsBlocks]
args:89 [in MetaCoq.PCUIC.PCUICFirstorder]
args:89 [in MetaCoq.Erasure.EWcbvEval]
args:9 [in MetaCoq.PCUIC.PCUICArities]
args:9 [in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
args:902 [in MetaCoq.PCUIC.PCUICTyping]
args:906 [in MetaCoq.Template.utils.MCList]
args:91 [in MetaCoq.Erasure.EInlineProjections]
args:911 [in MetaCoq.PCUIC.PCUICInductiveInversion]
args:92 [in MetaCoq.Template.EtaExpand]
args:92 [in MetaCoq.Erasure.EArities]
args:92 [in MetaCoq.Erasure.EConstructorsAsBlocks]
args:93 [in MetaCoq.PCUIC.PCUICCanonicity]
args:937 [in MetaCoq.PCUIC.PCUICParallelReduction]
args:94 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
args:95 [in MetaCoq.PCUIC.PCUICEtaExpand]
args:959 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
args:96 [in MetaCoq.Template.EtaExpand]
args:96 [in MetaCoq.PCUIC.PCUICConvCumInversion]
args:962 [in MetaCoq.PCUIC.PCUICInductiveInversion]
args:97 [in MetaCoq.PCUIC.PCUICInductiveInversion]
args:97 [in MetaCoq.Template.WcbvEval]
args:98 [in MetaCoq.Erasure.EWellformed]
args:98 [in MetaCoq.Erasure.EWcbvEval]
args:980 [in MetaCoq.PCUIC.PCUICInductiveInversion]
args:99 [in MetaCoq.Erasure.EWcbvEvalInd]
args:996 [in MetaCoq.PCUIC.PCUICInductiveInversion]
arg':372 [in MetaCoq.PCUIC.PCUICNormal]
arg':534 [in MetaCoq.Erasure.EEtaExpandedFix]
arg1:247 [in MetaCoq.PCUIC.PCUICParallelReduction]
arg1:434 [in MetaCoq.PCUIC.PCUICParallelReduction]
arg:132 [in MetaCoq.Template.Typing]
arg:1397 [in MetaCoq.SafeChecker.PCUICSafeReduce]
arg:1401 [in MetaCoq.SafeChecker.PCUICSafeReduce]
arg:147 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
arg:198 [in MetaCoq.Erasure.Extract]
arg:2 [in MetaCoq.Erasure.Prelim]
arg:212 [in MetaCoq.PCUIC.PCUICReduction]
arg:243 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
arg:247 [in MetaCoq.PCUIC.PCUICNormal]
arg:258 [in MetaCoq.PCUIC.PCUICNormal]
arg:268 [in MetaCoq.PCUIC.PCUICNormal]
arg:303 [in MetaCoq.Template.Typing]
arg:333 [in MetaCoq.PCUIC.PCUICNormal]
arg:371 [in MetaCoq.PCUIC.PCUICNormal]
arg:392 [in MetaCoq.PCUIC.PCUICSR]
arg:411 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
arg:49 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
arg:49 [in MetaCoq.PCUIC.PCUICReduction]
arg:533 [in MetaCoq.Erasure.EEtaExpandedFix]
arg:576 [in MetaCoq.PCUIC.PCUICSpine]
arg:582 [in MetaCoq.PCUIC.PCUICSpine]
arg:590 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
arg:605 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
arg:62 [in MetaCoq.PCUIC.PCUICNormal]
arg:68 [in MetaCoq.PCUIC.PCUICInductives]
arg:72 [in MetaCoq.PCUIC.PCUICInductives]
arg:79 [in MetaCoq.Erasure.EDeps]
arg:82 [in MetaCoq.PCUIC.PCUICCanonicity]
arities2:94 [in MetaCoq.Translations.param_cheap_packed]
arities2:97 [in MetaCoq.Translations.param_cheap_packed]
arities:118 [in MetaCoq.Template.Environment]
arities:135 [in MetaCoq.Template.Environment]
arities:167 [in MetaCoq.Erasure.Extract]
arities:255 [in MetaCoq.Template.Environment]
arities:259 [in MetaCoq.Template.Environment]
arities:263 [in MetaCoq.Template.Environment]
arities:269 [in MetaCoq.Template.Environment]
arities:678 [in MetaCoq.Erasure.ErasureFunction]
arities:93 [in MetaCoq.Translations.param_cheap_packed]
arities:96 [in MetaCoq.Translations.param_cheap_packed]
arity:21 [in MetaCoq.PCUIC.PCUICInductives]
arity:233 [in MetaCoq.PCUIC.PCUICSubstitution]
arity:410 [in MetaCoq.Template.EtaExpand]
ar:6 [in MetaCoq.Erasure.Extract]
ar:63 [in MetaCoq.Translations.param_original]
ar:64 [in MetaCoq.Translations.param_original]
ar:67 [in MetaCoq.Translations.param_binary]
ar:68 [in MetaCoq.Translations.param_binary]
as_name:74 [in MetaCoq.Template.Pretty]
as_name:81 [in MetaCoq.PCUIC.utils.PCUICPretty]
As:10 [in MetaCoq.Template.Pretty]
As:13 [in MetaCoq.PCUIC.utils.PCUICPretty]
As:59 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
As:60 [in MetaCoq.Template.AstUtils]
auctx':534 [in MetaCoq.Template.EnvironmentTyping]
auxt:81 [in MetaCoq.Erasure.EInduction]
aux:120 [in MetaCoq.Template.Checker]
aux:127 [in MetaCoq.Erasure.EGlobalEnv]
aux:1299 [in MetaCoq.SafeChecker.PCUICSafeConversion]
aux:134 [in MetaCoq.Erasure.EGlobalEnv]
aux:1378 [in MetaCoq.SafeChecker.PCUICSafeReduce]
aux:1389 [in MetaCoq.SafeChecker.PCUICSafeReduce]
aux:146 [in MetaCoq.Template.utils.bytestring]
aux:1478 [in MetaCoq.SafeChecker.PCUICSafeConversion]
aux:15 [in MetaCoq.Template.Typing]
aux:1527 [in MetaCoq.SafeChecker.PCUICSafeConversion]
aux:1791 [in MetaCoq.SafeChecker.PCUICSafeConversion]
aux:1951 [in MetaCoq.SafeChecker.PCUICSafeConversion]
aux:2159 [in MetaCoq.SafeChecker.PCUICSafeConversion]
aux:22 [in MetaCoq.Template.Typing]
aux:232 [in MetaCoq.PCUIC.Syntax.PCUICCases]
aux:2381 [in MetaCoq.SafeChecker.PCUICSafeConversion]
aux:239 [in MetaCoq.PCUIC.Syntax.PCUICCases]
aux:2397 [in MetaCoq.SafeChecker.PCUICSafeConversion]
aux:24 [in MetaCoq.Erasure.EPretty]
aux:245 [in MetaCoq.PCUIC.PCUICAst]
aux:2569 [in MetaCoq.SafeChecker.PCUICSafeConversion]
aux:26 [in MetaCoq.Template.Pretty]
aux:261 [in MetaCoq.SafeChecker.PCUICSafeConversion]
aux:27 [in MetaCoq.PCUIC.utils.PCUICPretty]
aux:291 [in MetaCoq.Template.Ast]
aux:299 [in MetaCoq.PCUIC.PCUICParallelReduction]
aux:310 [in MetaCoq.PCUIC.PCUICParallelReduction]
aux:42 [in MetaCoq.PCUIC.utils.PCUICPretty]
aux:4428 [in MetaCoq.SafeChecker.PCUICSafeConversion]
aux:4575 [in MetaCoq.SafeChecker.PCUICSafeConversion]
aux:51 [in MetaCoq.Template.Pretty]
aux:5244 [in MetaCoq.SafeChecker.PCUICSafeConversion]
aux:5490 [in MetaCoq.SafeChecker.PCUICSafeConversion]
aux:64 [in MetaCoq.Template.utils.MCList]
aux:719 [in MetaCoq.SafeChecker.PCUICSafeConversion]
aux:73 [in MetaCoq.Template.utils.MCList]
aux:8 [in MetaCoq.Template.utils.MCString]
au:338 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
au:434 [in MetaCoq.Template.Universes]
av:105 [in MetaCoq.PCUIC.PCUICWcbvEval]
av:175 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
av:183 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
av:190 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
av:389 [in MetaCoq.Erasure.EWcbvEval]
av:435 [in MetaCoq.Template.Universes]
av:64 [in MetaCoq.Erasure.EWcbvEval]
av:70 [in MetaCoq.Erasure.EWcbvEvalInd]
av:73 [in MetaCoq.Erasure.EWcbvEval]
av:80 [in MetaCoq.Erasure.EWcbvEvalInd]
av:81 [in MetaCoq.Erasure.EWcbvEval]
av:89 [in MetaCoq.Erasure.EWcbvEvalInd]
av:97 [in MetaCoq.PCUIC.PCUICWcbvEval]
awt:1087 [in MetaCoq.Erasure.ErasureFunction]
awt:1092 [in MetaCoq.Erasure.ErasureFunction]
awt:1096 [in MetaCoq.Erasure.ErasureFunction]
awt:1100 [in MetaCoq.Erasure.ErasureFunction]
awt:1108 [in MetaCoq.Erasure.ErasureFunction]
awt:1113 [in MetaCoq.Erasure.ErasureFunction]
awt:1117 [in MetaCoq.Erasure.ErasureFunction]
awt:1121 [in MetaCoq.Erasure.ErasureFunction]
awt:496 [in MetaCoq.Erasure.ErasureFunction]
awt:502 [in MetaCoq.Erasure.ErasureFunction]
awt:507 [in MetaCoq.Erasure.ErasureFunction]
awt:512 [in MetaCoq.Erasure.ErasureFunction]
awt:523 [in MetaCoq.Erasure.ErasureFunction]
awt:529 [in MetaCoq.Erasure.ErasureFunction]
awt:534 [in MetaCoq.Erasure.ErasureFunction]
awt:539 [in MetaCoq.Erasure.ErasureFunction]
awt:561 [in MetaCoq.Erasure.ErasureFunction]
awt:566 [in MetaCoq.Erasure.ErasureFunction]
awt:570 [in MetaCoq.Erasure.ErasureFunction]
awt:574 [in MetaCoq.Erasure.ErasureFunction]
awt:582 [in MetaCoq.Erasure.ErasureFunction]
awt:587 [in MetaCoq.Erasure.ErasureFunction]
awt:591 [in MetaCoq.Erasure.ErasureFunction]
awt:595 [in MetaCoq.Erasure.ErasureFunction]
awt:610 [in MetaCoq.Erasure.ErasureFunction]
awt:615 [in MetaCoq.Erasure.ErasureFunction]
awt:621 [in MetaCoq.Erasure.ErasureFunction]
awt:627 [in MetaCoq.Erasure.ErasureFunction]
awt:637 [in MetaCoq.Erasure.ErasureFunction]
awt:642 [in MetaCoq.Erasure.ErasureFunction]
awt:648 [in MetaCoq.Erasure.ErasureFunction]
awt:654 [in MetaCoq.Erasure.ErasureFunction]
awt:723 [in MetaCoq.Erasure.ErasureFunction]
awt:729 [in MetaCoq.Erasure.ErasureFunction]
awt:734 [in MetaCoq.Erasure.ErasureFunction]
awt:739 [in MetaCoq.Erasure.ErasureFunction]
awt:750 [in MetaCoq.Erasure.ErasureFunction]
awt:756 [in MetaCoq.Erasure.ErasureFunction]
awt:761 [in MetaCoq.Erasure.ErasureFunction]
awt:766 [in MetaCoq.Erasure.ErasureFunction]
A'':21 [in MetaCoq.PCUIC.Bidirectional.BDUnique]
A'':91 [in MetaCoq.PCUIC.Bidirectional.BDUnique]
A':102 [in MetaCoq.PCUIC.Bidirectional.BDUnique]
A':103 [in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
A':1036 [in MetaCoq.PCUIC.PCUICParallelReduction]
A':1047 [in MetaCoq.PCUIC.PCUICParallelReduction]
a':107 [in MetaCoq.Template.TermEquality]
A':109 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
A':110 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
A':112 [in MetaCoq.Translations.translation_utils]
A':1134 [in MetaCoq.PCUIC.PCUICReduction]
A':1142 [in MetaCoq.PCUIC.PCUICReduction]
A':115 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
A':115 [in MetaCoq.PCUIC.Bidirectional.BDUnique]
A':121 [in MetaCoq.Translations.translation_utils]
a':127 [in MetaCoq.SafeChecker.PCUICSafeReduce]
A':130 [in MetaCoq.Translations.translation_utils]
a':130 [in MetaCoq.Erasure.EWcbvEval]
a':133 [in MetaCoq.SafeChecker.PCUICSafeReduce]
a':135 [in MetaCoq.PCUIC.PCUICWcbvEval]
a':139 [in MetaCoq.PCUIC.PCUICWcbvEval]
a':139 [in MetaCoq.Erasure.EWcbvEval]
a':140 [in MetaCoq.Template.WcbvEval]
a':143 [in MetaCoq.Erasure.EWcbvEval]
A':1430 [in MetaCoq.Template.utils.All_Forall]
a':146 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
a':148 [in MetaCoq.Template.WcbvEval]
a':149 [in MetaCoq.SafeChecker.PCUICSafeReduce]
A':149 [in MetaCoq.Template.Checker]
a':151 [in MetaCoq.PCUIC.PCUICEquality]
a':151 [in MetaCoq.Erasure.EWcbvEvalInd]
a':152 [in MetaCoq.SafeChecker.PCUICSafeReduce]
A':1608 [in MetaCoq.Template.utils.All_Forall]
a':165 [in MetaCoq.Erasure.EWcbvEvalInd]
A':1689 [in MetaCoq.Template.utils.All_Forall]
A':1724 [in MetaCoq.Template.utils.All_Forall]
a':174 [in MetaCoq.Erasure.EWcbvEvalInd]
a':18 [in MetaCoq.Erasure.EWcbvEvalInd]
A':181 [in MetaCoq.PCUIC.PCUICTyping]
a':182 [in MetaCoq.PCUIC.PCUICWcbvEval]
A':19 [in MetaCoq.Translations.standard_model]
A':19 [in MetaCoq.PCUIC.Bidirectional.BDUnique]
A':195 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
A':2067 [in MetaCoq.Template.utils.All_Forall]
A':21 [in MetaCoq.Translations.standard_model]
A':215 [in MetaCoq.PCUIC.PCUICCumulProp]
A':219 [in MetaCoq.SafeChecker.PCUICTypeChecker]
A':22 [in MetaCoq.Translations.times_bool_fun]
a':226 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
A':23 [in MetaCoq.Translations.times_bool_fun]
a':234 [in MetaCoq.Template.WcbvEval]
A':24 [in MetaCoq.Translations.standard_model]
A':2479 [in MetaCoq.Template.utils.All_Forall]
A':25 [in MetaCoq.Translations.times_bool_fun]
a':251 [in MetaCoq.PCUIC.PCUICNormal]
A':266 [in MetaCoq.PCUIC.PCUICConversion]
a':27 [in MetaCoq.Erasure.EWcbvEval]
A':28 [in MetaCoq.Translations.standard_model]
a':280 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
A':29 [in MetaCoq.Translations.times_bool_fun]
a':313 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
A':37 [in MetaCoq.Translations.param_cheap_packed]
a':371 [in MetaCoq.Erasure.EWcbvEval]
a':374 [in MetaCoq.PCUIC.PCUICConversion]
A':39 [in MetaCoq.Translations.param_cheap_packed]
A':39 [in MetaCoq.Translations.standard_model]
a':393 [in MetaCoq.Erasure.EWcbvEval]
A':394 [in MetaCoq.PCUIC.PCUICNormal]
A':399 [in MetaCoq.PCUIC.PCUICNormal]
A':411 [in MetaCoq.PCUIC.PCUICConversion]
A':42 [in MetaCoq.Translations.param_cheap_packed]
A':421 [in MetaCoq.PCUIC.PCUICConversion]
A':424 [in MetaCoq.PCUIC.PCUICInductiveInversion]
A':43 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
A':43 [in MetaCoq.Translations.param_generous_packed]
a':431 [in MetaCoq.Erasure.EWcbvEval]
a':441 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
a':444 [in MetaCoq.Erasure.EWcbvEval]
a':453 [in MetaCoq.Erasure.EEtaExpandedFix]
A':46 [in MetaCoq.Translations.param_generous_packed]
A':47 [in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
a':470 [in MetaCoq.Erasure.EEtaExpandedFix]
A':48 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
A':48 [in MetaCoq.Translations.param_generous_packed]
A':51 [in MetaCoq.Translations.param_generous_packed]
A':52 [in MetaCoq.Translations.param_cheap_packed]
A':53 [in MetaCoq.PCUIC.PCUICArities]
a':55 [in MetaCoq.Template.WcbvEval]
a':56 [in MetaCoq.PCUIC.PCUICWcbvEval]
a':565 [in MetaCoq.Erasure.EEtaExpandedFix]
a':567 [in MetaCoq.Erasure.EEtaExpandedFix]
A':57 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
A':61 [in MetaCoq.Translations.param_generous_packed]
A':62 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
a':645 [in MetaCoq.Template.Universes]
a':650 [in MetaCoq.Template.Universes]
a':67 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
A':732 [in MetaCoq.Template.utils.MCList]
A':787 [in MetaCoq.PCUIC.PCUICConversion]
A':81 [in MetaCoq.Translations.times_bool_fun2]
A':88 [in MetaCoq.PCUIC.Bidirectional.BDUnique]
A':9 [in MetaCoq.Erasure.ErasureProperties]
A':94 [in MetaCoq.Translations.translation_utils]
a':965 [in MetaCoq.PCUIC.PCUICReduction]
A':983 [in MetaCoq.Translations.MiniHoTT]
A':991 [in MetaCoq.Translations.MiniHoTT_paths]
a0:106 [in MetaCoq.Template.utils.MCRelations]
a0:108 [in MetaCoq.Template.utils.MCRelations]
a0:12 [in MetaCoq.Template.utils.MCList]
A0:15 [in MetaCoq.Translations.param_original]
A0:18 [in MetaCoq.Translations.param_original]
a0:180 [in MetaCoq.PCUIC.PCUICParallelReduction]
A0:27 [in MetaCoq.Translations.param_original]
A0:29 [in MetaCoq.Translations.param_binary]
A0:32 [in MetaCoq.Translations.param_binary]
A0:33 [in MetaCoq.Translations.param_original]
a0:348 [in MetaCoq.PCUIC.PCUICParallelReduction]
A0:41 [in MetaCoq.Translations.param_binary]
A0:46 [in MetaCoq.Translations.param_binary]
A0:50 [in MetaCoq.Translations.standard_model]
A1:16 [in MetaCoq.Translations.param_original]
A1:17 [in MetaCoq.SafeChecker.PCUICErrors]
a1:181 [in MetaCoq.PCUIC.PCUICParallelReduction]
A1:19 [in MetaCoq.Translations.param_original]
A1:25 [in MetaCoq.SafeChecker.PCUICErrors]
A1:28 [in MetaCoq.Translations.param_original]
a1:281 [in MetaCoq.SafeChecker.PCUICErrors]
a1:288 [in MetaCoq.SafeChecker.PCUICErrors]
A1:30 [in MetaCoq.Translations.param_binary]
a1:301 [in MetaCoq.SafeChecker.PCUICErrors]
a1:309 [in MetaCoq.SafeChecker.PCUICErrors]
A1:34 [in MetaCoq.Translations.param_binary]
A1:34 [in MetaCoq.SafeChecker.PCUICErrors]
A1:34 [in MetaCoq.Translations.param_original]
a1:349 [in MetaCoq.PCUIC.PCUICParallelReduction]
A1:42 [in MetaCoq.Translations.param_binary]
A1:42 [in MetaCoq.Translations.param_generous_packed]
a1:4408 [in MetaCoq.SafeChecker.PCUICSafeConversion]
A1:48 [in MetaCoq.Translations.param_binary]
A1:513 [in MetaCoq.PCUIC.PCUICConversion]
A1:546 [in MetaCoq.SafeChecker.PCUICSafeConversion]
A1:552 [in MetaCoq.SafeChecker.PCUICSafeConversion]
A1:8 [in MetaCoq.SafeChecker.PCUICErrors]
A1:820 [in MetaCoq.PCUIC.PCUICConversion]
A1:828 [in MetaCoq.PCUIC.PCUICConversion]
A1:852 [in MetaCoq.PCUIC.PCUICConversion]
A1:864 [in MetaCoq.PCUIC.PCUICConversion]
A1:873 [in MetaCoq.PCUIC.PCUICConversion]
A1:881 [in MetaCoq.PCUIC.PCUICConversion]
a2:104 [in MetaCoq.Translations.param_cheap_packed]
a2:110 [in MetaCoq.Translations.param_cheap_packed]
A2:12 [in MetaCoq.SafeChecker.PCUICErrors]
a2:136 [in MetaCoq.Translations.param_cheap_packed]
a2:142 [in MetaCoq.Translations.param_cheap_packed]
A2:21 [in MetaCoq.SafeChecker.PCUICErrors]
A2:29 [in MetaCoq.SafeChecker.PCUICErrors]
a2:302 [in MetaCoq.SafeChecker.PCUICErrors]
a2:310 [in MetaCoq.SafeChecker.PCUICErrors]
A2:34 [in MetaCoq.Translations.param_cheap_packed]
A2:38 [in MetaCoq.SafeChecker.PCUICErrors]
A2:40 [in MetaCoq.Translations.param_generous_packed]
A2:514 [in MetaCoq.PCUIC.PCUICConversion]
A2:549 [in MetaCoq.SafeChecker.PCUICSafeConversion]
A2:555 [in MetaCoq.SafeChecker.PCUICSafeConversion]
A2:821 [in MetaCoq.PCUIC.PCUICConversion]
A2:829 [in MetaCoq.PCUIC.PCUICConversion]
A2:853 [in MetaCoq.PCUIC.PCUICConversion]
A2:867 [in MetaCoq.PCUIC.PCUICConversion]
A2:874 [in MetaCoq.PCUIC.PCUICConversion]
A2:882 [in MetaCoq.PCUIC.PCUICConversion]
A:1 [in MetaCoq.Template.utils.MCSquash]
A:1 [in MetaCoq.Template.utils.MCReflect]
A:1 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
A:1 [in MetaCoq.Translations.times_bool_fun]
A:1 [in MetaCoq.Template.utils.All_Forall]
A:1 [in MetaCoq.Template.utils.MCList]
A:1 [in MetaCoq.PCUIC.utils.PCUICUtils]
A:1 [in MetaCoq.PCUIC.utils.PCUICOnOne]
A:1 [in MetaCoq.PCUIC.PCUICInductives]
A:1 [in MetaCoq.Template.utils.MCString]
A:1 [in MetaCoq.Template.utils.MCEquality]
A:1 [in MetaCoq.PCUIC.PCUICEquality]
A:1 [in MetaCoq.Translations.sigma]
A:1 [in MetaCoq.Template.utils.MCPred]
A:1 [in MetaCoq.PCUIC.PCUICAst]
A:1 [in MetaCoq.Erasure.EWellformed]
A:1 [in MetaCoq.Template.EnvMap]
A:1 [in MetaCoq.PCUIC.Syntax.PCUICUnivSubst]
A:1 [in MetaCoq.Template.utils.MCOption]
A:1 [in MetaCoq.Translations.MiniHoTT]
A:1 [in MetaCoq.Template.utils.MCProd]
A:1 [in MetaCoq.Translations.MiniHoTT_paths]
A:1 [in MetaCoq.Template.UnivSubst]
A:1 [in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
A:1 [in MetaCoq.Template.Transform]
A:1 [in MetaCoq.SafeChecker.PCUICTypeChecker]
A:10 [in MetaCoq.Template.utils.MCCompare]
A:10 [in MetaCoq.Translations.times_bool_fun]
A:10 [in MetaCoq.Template.Normal]
A:10 [in MetaCoq.SafeChecker.PCUICWfReduction]
A:10 [in MetaCoq.Template.utils.MCUtils]
a:10 [in MetaCoq.Erasure.EWcbvEvalInd]
A:10 [in MetaCoq.PCUIC.Syntax.PCUICUnivSubst]
A:10 [in MetaCoq.Translations.MiniHoTT]
A:10 [in MetaCoq.Template.utils.MCProd]
A:10 [in MetaCoq.Examples.add_constructor]
A:100 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
A:100 [in MetaCoq.PCUIC.PCUICAst]
A:100 [in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
A:1001 [in MetaCoq.Translations.MiniHoTT_paths]
A:1004 [in MetaCoq.Translations.MiniHoTT]
A:1006 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
a:1006 [in MetaCoq.PCUIC.PCUICConfluence]
A:101 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
A:101 [in MetaCoq.PCUIC.PCUICCumulProp]
A:101 [in MetaCoq.PCUIC.Bidirectional.BDUnique]
A:101 [in MetaCoq.Translations.times_bool_fun2]
A:101 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
A:101 [in MetaCoq.Translations.param_generous_packed]
A:1012 [in MetaCoq.Translations.MiniHoTT_paths]
A:1013 [in MetaCoq.Translations.MiniHoTT]
A:1016 [in MetaCoq.Template.utils.All_Forall]
A:1019 [in MetaCoq.Translations.MiniHoTT]
A:102 [in MetaCoq.PCUIC.PCUICValidity]
A:102 [in MetaCoq.Template.utils.MCOption]
A:102 [in MetaCoq.Translations.MiniHoTT]
A:1021 [in MetaCoq.Translations.MiniHoTT_paths]
A:1026 [in MetaCoq.PCUIC.PCUICTyping]
A:1027 [in MetaCoq.Translations.MiniHoTT_paths]
A:103 [in MetaCoq.Template.utils.All_Forall]
A:1031 [in MetaCoq.Template.utils.All_Forall]
A:1031 [in MetaCoq.Translations.MiniHoTT]
A:1032 [in MetaCoq.PCUIC.PCUICConversion]
A:1035 [in MetaCoq.PCUIC.PCUICParallelReduction]
A:1037 [in MetaCoq.Translations.MiniHoTT]
A:1039 [in MetaCoq.Translations.MiniHoTT_paths]
A:104 [in MetaCoq.Template.BasicAst]
A:104 [in MetaCoq.Template.utils.MCList]
a:104 [in MetaCoq.PCUIC.PCUICWcbvEval]
A:104 [in MetaCoq.Template.Ast]
A:104 [in MetaCoq.PCUIC.PCUICTyping]
A:104 [in MetaCoq.Translations.MiniHoTT_paths]
A:104 [in MetaCoq.SafeChecker.PCUICEqualityDec]
A:1045 [in MetaCoq.Translations.MiniHoTT_paths]
a:1045 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
A:1046 [in MetaCoq.Template.utils.All_Forall]
A:1046 [in MetaCoq.PCUIC.PCUICParallelReduction]
A:1047 [in MetaCoq.Translations.MiniHoTT]
A:1048 [in MetaCoq.PCUIC.PCUICConfluence]
A:105 [in MetaCoq.Translations.param_binary]
a:105 [in MetaCoq.Template.utils.MCRelations]
A:105 [in MetaCoq.PCUIC.PCUICArities]
A:105 [in MetaCoq.PCUIC.PCUICCumulProp]
A:105 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
a:105 [in MetaCoq.Translations.param_cheap_packed]
A:105 [in MetaCoq.Template.utils.MCOption]
A:105 [in MetaCoq.Template.monad_utils]
A:1055 [in MetaCoq.Translations.MiniHoTT_paths]
A:1057 [in MetaCoq.Template.utils.All_Forall]
A:1058 [in MetaCoq.Translations.MiniHoTT]
a:106 [in MetaCoq.Template.TermEquality]
a:106 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
A:1064 [in MetaCoq.Translations.MiniHoTT]
A:1066 [in MetaCoq.Translations.MiniHoTT_paths]
A:1067 [in MetaCoq.Template.utils.All_Forall]
a:107 [in MetaCoq.Template.utils.MCRelations]
A:107 [in MetaCoq.PCUIC.PCUICTyping]
a:107 [in MetaCoq.Erasure.EAstUtils]
A:107 [in MetaCoq.SafeChecker.PCUICEqualityDec]
A:1070 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
A:1070 [in MetaCoq.Translations.MiniHoTT]
A:1072 [in MetaCoq.PCUIC.PCUICConfluence]
A:1072 [in MetaCoq.Translations.MiniHoTT_paths]
a:1074 [in MetaCoq.PCUIC.PCUICConfluence]
A:1076 [in MetaCoq.Translations.MiniHoTT]
A:1077 [in MetaCoq.Template.utils.All_Forall]
a:1078 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
A:1078 [in MetaCoq.Translations.MiniHoTT_paths]
A:1078 [in MetaCoq.SafeChecker.PCUICSafeChecker]
A:1079 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
a:1079 [in MetaCoq.Template.utils.wGraph]
A:108 [in MetaCoq.Template.BasicAst]
A:108 [in MetaCoq.Translations.translation_utils]
A:108 [in MetaCoq.Erasure.ERemoveParams]
a:1082 [in MetaCoq.Template.utils.wGraph]
A:1082 [in MetaCoq.Translations.MiniHoTT]
A:1084 [in MetaCoq.Translations.MiniHoTT_paths]
A:1087 [in MetaCoq.Template.utils.All_Forall]
A:1088 [in MetaCoq.Translations.MiniHoTT]
A:109 [in MetaCoq.PCUIC.PCUICValidity]
a:109 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
a:109 [in MetaCoq.Erasure.EAstUtils]
A:1090 [in MetaCoq.Translations.MiniHoTT_paths]
A:1096 [in MetaCoq.Translations.MiniHoTT]
A:1096 [in MetaCoq.Translations.MiniHoTT_paths]
A:1097 [in MetaCoq.Template.utils.All_Forall]
A:11 [in MetaCoq.Template.BasicAst]
A:11 [in MetaCoq.Template.TemplateMonad.Core]
A:11 [in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
A:11 [in MetaCoq.PCUIC.PCUICGeneration]
a:11 [in MetaCoq.Translations.MiniHoTT]
a:11 [in MetaCoq.Examples.demo]
A:11 [in MetaCoq.Template.utils.MCPrelude]
A:11 [in MetaCoq.Erasure.EOptimizePropDiscr]
A:110 [in MetaCoq.Translations.param_binary]
a:110 [in MetaCoq.Template.utils.MCRelations]
A:110 [in MetaCoq.Template.Ast]
A:110 [in MetaCoq.Translations.MiniHoTT]
A:110 [in MetaCoq.Translations.MiniHoTT_paths]
A:110 [in MetaCoq.SafeChecker.PCUICEqualityDec]
A:1104 [in MetaCoq.Template.Typing]
A:1104 [in MetaCoq.Translations.MiniHoTT]
A:1104 [in MetaCoq.Translations.MiniHoTT_paths]
A:1107 [in MetaCoq.Template.utils.All_Forall]
A:111 [in MetaCoq.Translations.times_bool_fun]
A:111 [in MetaCoq.Template.utils.All_Forall]
a:111 [in MetaCoq.Translations.param_cheap_packed]
A:111 [in MetaCoq.Template.utils.MCOption]
A:1112 [in MetaCoq.Template.utils.All_Forall]
A:1112 [in MetaCoq.Translations.MiniHoTT]
A:1112 [in MetaCoq.Translations.MiniHoTT_paths]
a:1113 [in MetaCoq.SafeChecker.PCUICTypeChecker]
A:1114 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
A:1117 [in MetaCoq.Template.utils.All_Forall]
a:112 [in MetaCoq.Template.utils.MCRelations]
A:112 [in MetaCoq.Template.utils.MCList]
A:112 [in MetaCoq.Template.utils.MCOption]
A:112 [in MetaCoq.PCUIC.Bidirectional.BDUnique]
a:112 [in MetaCoq.Erasure.EWcbvEval]
A:1120 [in MetaCoq.Translations.MiniHoTT]
A:1120 [in MetaCoq.Translations.MiniHoTT_paths]
A:1126 [in MetaCoq.Template.utils.All_Forall]
A:1126 [in MetaCoq.Translations.MiniHoTT]
A:1127 [in MetaCoq.SafeChecker.PCUICTypeChecker]
A:1128 [in MetaCoq.Translations.MiniHoTT_paths]
A:113 [in MetaCoq.Translations.param_binary]
A:113 [in MetaCoq.Translations.times_bool_fun]
A:113 [in MetaCoq.Translations.param_cheap_packed]
A:113 [in MetaCoq.Template.utils.MCOption]
A:1132 [in MetaCoq.Translations.MiniHoTT]
A:1132 [in MetaCoq.PCUIC.PCUICReduction]
A:1134 [in MetaCoq.Translations.MiniHoTT_paths]
A:1135 [in MetaCoq.Template.utils.All_Forall]
A:1136 [in MetaCoq.PCUIC.PCUICReduction]
A:1138 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
A:1138 [in MetaCoq.Translations.MiniHoTT]
A:1139 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
A:114 [in MetaCoq.Erasure.ErasureFunction]
A:1140 [in MetaCoq.Translations.MiniHoTT_paths]
A:1140 [in MetaCoq.PCUIC.PCUICReduction]
A:1144 [in MetaCoq.Template.utils.All_Forall]
A:1144 [in MetaCoq.Translations.MiniHoTT]
A:1145 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
A:1146 [in MetaCoq.Translations.MiniHoTT_paths]
A:1147 [in MetaCoq.Translations.MiniHoTT]
A:115 [in MetaCoq.Template.BasicAst]
A:115 [in MetaCoq.Template.utils.All_Forall]
A:115 [in MetaCoq.Translations.param_cheap_packed]
A:115 [in MetaCoq.Translations.MiniHoTT]
A:1150 [in MetaCoq.Translations.MiniHoTT]
A:1152 [in MetaCoq.Translations.MiniHoTT_paths]
A:1153 [in MetaCoq.Template.utils.All_Forall]
A:1155 [in MetaCoq.Translations.MiniHoTT_paths]
A:1156 [in MetaCoq.Translations.MiniHoTT]
A:1158 [in MetaCoq.Translations.MiniHoTT_paths]
A:116 [in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
A:116 [in MetaCoq.Erasure.EConstructorsAsBlocks]
a:116 [in MetaCoq.Erasure.ErasureProperties]
A:116 [in MetaCoq.Erasure.EAstUtils]
A:1161 [in MetaCoq.PCUIC.PCUICReduction]
A:1162 [in MetaCoq.Template.utils.All_Forall]
A:1162 [in MetaCoq.Translations.MiniHoTT]
A:1164 [in MetaCoq.Translations.MiniHoTT_paths]
A:1169 [in MetaCoq.PCUIC.PCUICReduction]
A:117 [in MetaCoq.Translations.param_binary]
A:117 [in MetaCoq.Template.utils.MCList]
A:117 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
A:1170 [in MetaCoq.Translations.MiniHoTT_paths]
A:1171 [in MetaCoq.Template.utils.All_Forall]
A:1173 [in MetaCoq.Translations.MiniHoTT]
A:1173 [in MetaCoq.PCUIC.PCUICReduction]
A:1177 [in MetaCoq.Template.utils.All_Forall]
A:1179 [in MetaCoq.PCUIC.PCUICReduction]
A:118 [in MetaCoq.SafeChecker.PCUICSafeReduce]
A:118 [in MetaCoq.Translations.MiniHoTT_paths]
a:118 [in MetaCoq.Erasure.EWcbvEval]
A:118 [in MetaCoq.PCUIC.PCUICSpine]
A:1181 [in MetaCoq.Template.utils.All_Forall]
A:1181 [in MetaCoq.Translations.MiniHoTT_paths]
A:1184 [in MetaCoq.Translations.MiniHoTT]
A:1189 [in MetaCoq.Template.utils.All_Forall]
A:119 [in MetaCoq.Template.BasicAst]
A:119 [in MetaCoq.Erasure.EConstructorsAsBlocks]
A:119 [in MetaCoq.Erasure.EAstUtils]
a:119 [in MetaCoq.PCUIC.PCUICSpine]
A:1192 [in MetaCoq.Translations.MiniHoTT_paths]
A:1194 [in MetaCoq.Translations.MiniHoTT]
A:1195 [in MetaCoq.Template.utils.All_Forall]
A:12 [in MetaCoq.Erasure.EArities]
A:12 [in MetaCoq.Template.TemplateMonad.Core]
A:12 [in MetaCoq.Template.utils.MCString]
A:12 [in MetaCoq.Template.utils.ReflectEq]
A:12 [in MetaCoq.PCUIC.PCUICPrincipality]
A:12 [in MetaCoq.Template.TemplateMonad.Common]
a:12 [in MetaCoq.Template.UnivSubst]
A:120 [in MetaCoq.Template.monad_utils]
A:1201 [in MetaCoq.Template.utils.All_Forall]
A:1202 [in MetaCoq.Translations.MiniHoTT_paths]
A:1204 [in MetaCoq.Translations.MiniHoTT]
A:1207 [in MetaCoq.Template.utils.All_Forall]
a:121 [in MetaCoq.Erasure.EWcbvEvalInd]
A:1212 [in MetaCoq.Template.utils.All_Forall]
A:1212 [in MetaCoq.Translations.MiniHoTT]
A:1212 [in MetaCoq.Translations.MiniHoTT_paths]
A:1216 [in MetaCoq.Template.utils.All_Forall]
a:1218 [in MetaCoq.Template.utils.All_Forall]
A:122 [in MetaCoq.PCUIC.Syntax.PCUICCases]
A:1220 [in MetaCoq.Template.utils.All_Forall]
A:1220 [in MetaCoq.Translations.MiniHoTT]
A:1220 [in MetaCoq.Translations.MiniHoTT_paths]
A:1225 [in MetaCoq.Template.utils.All_Forall]
A:1228 [in MetaCoq.Translations.MiniHoTT]
A:1228 [in MetaCoq.Translations.MiniHoTT_paths]
A:123 [in MetaCoq.Translations.param_binary]
a:123 [in MetaCoq.Template.WfAst]
A:123 [in MetaCoq.Translations.MiniHoTT]
A:123 [in MetaCoq.Translations.MiniHoTT_paths]
A:1233 [in MetaCoq.Template.utils.All_Forall]
A:1236 [in MetaCoq.Translations.MiniHoTT]
A:1236 [in MetaCoq.Translations.MiniHoTT_paths]
a:124 [in MetaCoq.Erasure.EEtaExpandedFix]
A:124 [in MetaCoq.Template.utils.MCList]
A:124 [in MetaCoq.Template.Ast]
a:124 [in MetaCoq.Template.LiftSubst]
A:1243 [in MetaCoq.Template.utils.All_Forall]
A:1244 [in MetaCoq.Translations.MiniHoTT_paths]
a:1246 [in MetaCoq.Translations.MiniHoTT]
a:125 [in MetaCoq.Erasure.EInlineProjections]
a:125 [in MetaCoq.Translations.MiniHoTT]
A:125 [in MetaCoq.PCUIC.PCUICSpine]
A:1250 [in MetaCoq.Translations.MiniHoTT]
A:1254 [in MetaCoq.Template.utils.All_Forall]
a:1254 [in MetaCoq.Translations.MiniHoTT_paths]
a:1258 [in MetaCoq.Translations.MiniHoTT]
A:1258 [in MetaCoq.Translations.MiniHoTT_paths]
A:126 [in MetaCoq.Translations.translation_utils]
A:126 [in MetaCoq.Template.utils.All_Forall]
a:126 [in MetaCoq.Template.WfAst]
a:126 [in MetaCoq.SafeChecker.PCUICSafeReduce]
A:126 [in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
A:1260 [in MetaCoq.Translations.MiniHoTT]
a:1266 [in MetaCoq.Translations.MiniHoTT_paths]
A:1267 [in MetaCoq.Template.utils.All_Forall]
A:1268 [in MetaCoq.Translations.MiniHoTT_paths]
a:127 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
A:127 [in MetaCoq.PCUIC.PCUICConfluence]
a:127 [in MetaCoq.Erasure.ERemoveParams]
A:1270 [in MetaCoq.Translations.MiniHoTT]
A:1271 [in MetaCoq.PCUIC.PCUICConversion]
A:1276 [in MetaCoq.Translations.MiniHoTT]
A:1277 [in MetaCoq.Template.utils.All_Forall]
A:1278 [in MetaCoq.Translations.MiniHoTT_paths]
A:128 [in MetaCoq.Template.utils.MCList]
A:1280 [in MetaCoq.Translations.MiniHoTT]
A:1282 [in MetaCoq.Template.utils.All_Forall]
A:1284 [in MetaCoq.Translations.MiniHoTT_paths]
A:1287 [in MetaCoq.Template.utils.All_Forall]
A:1288 [in MetaCoq.Translations.MiniHoTT]
A:1288 [in MetaCoq.Translations.MiniHoTT_paths]
A:129 [in MetaCoq.Translations.times_bool_fun]
A:129 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
A:129 [in MetaCoq.SafeChecker.PCUICSafeReduce]
a:129 [in MetaCoq.Erasure.EWcbvEval]
A:1292 [in MetaCoq.Template.utils.All_Forall]
A:1296 [in MetaCoq.Translations.MiniHoTT_paths]
A:1298 [in MetaCoq.Template.utils.All_Forall]
A:1298 [in MetaCoq.Translations.MiniHoTT]
A:13 [in MetaCoq.PCUIC.PCUICRedTypeIrrelevance]
A:13 [in MetaCoq.Template.utils.MCRelations]
A:13 [in MetaCoq.Template.TemplateMonad.Core]
A:13 [in MetaCoq.Template.Normal]
A:13 [in MetaCoq.SafeChecker.PCUICWfReduction]
A:13 [in MetaCoq.SafeChecker.SafeTemplateChecker]
A:13 [in MetaCoq.Template.utils.MCOption]
A:13 [in MetaCoq.Translations.times_bool_fun2]
A:13 [in MetaCoq.PCUIC.Syntax.PCUICNamelessDef]
a:130 [in MetaCoq.Template.utils.MCList]
a:130 [in MetaCoq.Erasure.ErasureProperties]
A:1300 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
A:1303 [in MetaCoq.Template.utils.All_Forall]
a:1303 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
A:1306 [in MetaCoq.Translations.MiniHoTT_paths]
a:1307 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
A:131 [in MetaCoq.Translations.times_bool_fun]
A:131 [in MetaCoq.Erasure.ErasureProperties]
A:131 [in MetaCoq.Translations.MiniHoTT_paths]
A:1310 [in MetaCoq.Translations.MiniHoTT]
A:1312 [in MetaCoq.Template.utils.All_Forall]
A:1318 [in MetaCoq.Translations.MiniHoTT_paths]
A:1319 [in MetaCoq.Template.utils.All_Forall]
A:1319 [in MetaCoq.Translations.MiniHoTT]
A:132 [in MetaCoq.Template.utils.All_Forall]
A:132 [in MetaCoq.PCUIC.PCUICSafeLemmata]
a:132 [in MetaCoq.SafeChecker.PCUICSafeReduce]
A:132 [in MetaCoq.Examples.tauto]
A:132 [in MetaCoq.Translations.MiniHoTT]
a:132 [in MetaCoq.Erasure.EEtaExpanded]
A:1326 [in MetaCoq.Template.utils.All_Forall]
A:1327 [in MetaCoq.Translations.MiniHoTT]
A:1327 [in MetaCoq.Translations.MiniHoTT_paths]
A:133 [in MetaCoq.Erasure.EInduction]
a:133 [in MetaCoq.PCUIC.PCUICFirstorder]
a:133 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
a:133 [in MetaCoq.Erasure.EWcbvEvalInd]
a:133 [in MetaCoq.Translations.MiniHoTT_paths]
A:133 [in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
A:1332 [in MetaCoq.Template.utils.All_Forall]
A:1335 [in MetaCoq.Translations.MiniHoTT_paths]
A:1337 [in MetaCoq.Template.utils.All_Forall]
A:1338 [in MetaCoq.Translations.MiniHoTT]
a:134 [in MetaCoq.PCUIC.PCUICWcbvEval]
A:134 [in MetaCoq.PCUIC.PCUICFirstorder]
A:134 [in MetaCoq.Examples.tauto]
A:1342 [in MetaCoq.Template.utils.All_Forall]
A:1346 [in MetaCoq.Template.utils.All_Forall]
A:1346 [in MetaCoq.Translations.MiniHoTT]
A:1346 [in MetaCoq.Translations.MiniHoTT_paths]
A:135 [in MetaCoq.Translations.translation_utils]
a:135 [in MetaCoq.Erasure.ErasureProperties]
a:135 [in MetaCoq.SafeChecker.PCUICSafeReduce]
A:1352 [in MetaCoq.Template.utils.All_Forall]
A:1354 [in MetaCoq.Translations.MiniHoTT_paths]
A:1356 [in MetaCoq.Translations.MiniHoTT]
A:136 [in MetaCoq.Template.utils.All_Forall]
A:136 [in MetaCoq.Examples.tauto]
a:1360 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
A:1360 [in MetaCoq.Translations.MiniHoTT]
A:1362 [in MetaCoq.Template.utils.All_Forall]
A:1364 [in MetaCoq.Translations.MiniHoTT_paths]
A:1368 [in MetaCoq.Translations.MiniHoTT]
A:1368 [in MetaCoq.Translations.MiniHoTT_paths]
A:1369 [in MetaCoq.SafeChecker.PCUICSafeReduce]
A:137 [in MetaCoq.Template.utils.MCList]
A:137 [in MetaCoq.Translations.MiniHoTT]
A:1372 [in MetaCoq.Template.utils.All_Forall]
A:1376 [in MetaCoq.Translations.MiniHoTT_paths]
A:138 [in MetaCoq.PCUIC.PCUICSafeLemmata]
A:138 [in MetaCoq.PCUIC.utils.PCUICUtils]
a:138 [in MetaCoq.PCUIC.PCUICWcbvEval]
a:138 [in MetaCoq.Erasure.EWcbvEval]
A:1380 [in MetaCoq.Template.utils.All_Forall]
A:1387 [in MetaCoq.Template.utils.All_Forall]
A:139 [in MetaCoq.Template.utils.All_Forall]
A:139 [in MetaCoq.Erasure.EArities]
A:139 [in MetaCoq.Template.utils.MCList]
A:139 [in MetaCoq.Template.utils.bytestring]
a:139 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
a:139 [in MetaCoq.Template.WcbvEval]
A:1395 [in MetaCoq.Template.utils.All_Forall]
A:1399 [in MetaCoq.Template.utils.All_Forall]
A:14 [in MetaCoq.Template.utils.MCReflect]
A:14 [in MetaCoq.Translations.translation_utils]
A:14 [in MetaCoq.Template.utils.All_Forall]
A:14 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
A:14 [in MetaCoq.Template.TemplateMonad.Core]
a:14 [in MetaCoq.PCUIC.Syntax.PCUICViews]
A:14 [in MetaCoq.PCUIC.PCUICCumulProp]
A:14 [in MetaCoq.Translations.MiniHoTT_paths]
A:14 [in MetaCoq.Template.TemplateMonad.Common]
A:140 [in MetaCoq.Template.BasicAst]
A:140 [in MetaCoq.Translations.times_bool_fun]
a:140 [in MetaCoq.Template.utils.MCList]
A:140 [in MetaCoq.Template.Ast]
A:140 [in MetaCoq.Template.utils.MCProd]
A:140 [in MetaCoq.Translations.MiniHoTT_paths]
A:140 [in MetaCoq.SafeChecker.PCUICEqualityDec]
A:1404 [in MetaCoq.Template.utils.All_Forall]
a:141 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
A:1412 [in MetaCoq.Template.utils.All_Forall]
A:1413 [in MetaCoq.Translations.MiniHoTT]
A:1417 [in MetaCoq.Template.utils.All_Forall]
A:142 [in MetaCoq.Translations.times_bool_fun]
a:142 [in MetaCoq.Erasure.EWcbvEval]
A:1421 [in MetaCoq.Translations.MiniHoTT]
A:1421 [in MetaCoq.Translations.MiniHoTT_paths]
A:1422 [in MetaCoq.Template.utils.All_Forall]
A:1422 [in MetaCoq.Translations.MiniHoTT]
A:1423 [in MetaCoq.Translations.MiniHoTT]
A:1428 [in MetaCoq.Template.utils.All_Forall]
A:1429 [in MetaCoq.Translations.MiniHoTT_paths]
A:143 [in MetaCoq.Erasure.EArities]
A:143 [in MetaCoq.Template.utils.MCList]
a:143 [in MetaCoq.Erasure.EConstructorsAsBlocks]
A:143 [in MetaCoq.Examples.tauto]
A:143 [in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
A:1430 [in MetaCoq.Translations.MiniHoTT_paths]
a:1431 [in MetaCoq.Translations.MiniHoTT]
A:1431 [in MetaCoq.Translations.MiniHoTT_paths]
a:1432 [in MetaCoq.Translations.MiniHoTT]
A:1433 [in MetaCoq.Translations.MiniHoTT]
A:1438 [in MetaCoq.Translations.MiniHoTT]
A:1439 [in MetaCoq.Template.utils.All_Forall]
a:1439 [in MetaCoq.Translations.MiniHoTT_paths]
A:144 [in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
A:144 [in MetaCoq.Template.utils.All_Forall]
A:144 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
A:144 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
a:144 [in MetaCoq.Erasure.EGlobalEnv]
A:144 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
a:1440 [in MetaCoq.Translations.MiniHoTT_paths]
A:1441 [in MetaCoq.Translations.MiniHoTT_paths]
A:1444 [in MetaCoq.Template.utils.All_Forall]
A:1445 [in MetaCoq.Translations.MiniHoTT]
A:1446 [in MetaCoq.Translations.MiniHoTT_paths]
a:145 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
A:145 [in MetaCoq.Examples.tauto]
A:145 [in MetaCoq.Translations.MiniHoTT_paths]
A:145 [in MetaCoq.SafeChecker.PCUICEqualityDec]
A:1450 [in MetaCoq.Template.utils.All_Forall]
A:1452 [in MetaCoq.Translations.MiniHoTT]
A:1453 [in MetaCoq.Translations.MiniHoTT_paths]
A:1458 [in MetaCoq.Template.utils.All_Forall]
a:1459 [in MetaCoq.Translations.MiniHoTT]
A:146 [in MetaCoq.Translations.MiniHoTT]
a:1460 [in MetaCoq.Translations.MiniHoTT]
A:1460 [in MetaCoq.Translations.MiniHoTT_paths]
A:1461 [in MetaCoq.Translations.MiniHoTT]
A:1466 [in MetaCoq.Template.utils.All_Forall]
a:1466 [in MetaCoq.Translations.MiniHoTT]
a:1467 [in MetaCoq.Translations.MiniHoTT]
a:1467 [in MetaCoq.Translations.MiniHoTT_paths]
a:1468 [in MetaCoq.Translations.MiniHoTT]
a:1468 [in MetaCoq.Translations.MiniHoTT_paths]
A:1469 [in MetaCoq.Translations.MiniHoTT_paths]
A:147 [in MetaCoq.Template.utils.All_Forall]
A:147 [in MetaCoq.Erasure.EArities]
A:147 [in MetaCoq.Template.utils.bytestring]
A:147 [in MetaCoq.Template.Ast]
A:147 [in MetaCoq.Examples.tauto]
a:147 [in MetaCoq.Template.WcbvEval]
A:1472 [in MetaCoq.Translations.MiniHoTT]
A:1474 [in MetaCoq.Template.utils.All_Forall]
A:1474 [in MetaCoq.Translations.MiniHoTT]
a:1474 [in MetaCoq.Translations.MiniHoTT_paths]
a:1475 [in MetaCoq.Translations.MiniHoTT_paths]
a:1476 [in MetaCoq.Translations.MiniHoTT_paths]
A:148 [in MetaCoq.Template.utils.All_Forall]
A:148 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
a:148 [in MetaCoq.SafeChecker.PCUICSafeReduce]
A:1480 [in MetaCoq.Translations.MiniHoTT_paths]
A:1481 [in MetaCoq.Template.utils.All_Forall]
A:1482 [in MetaCoq.Translations.MiniHoTT]
A:1482 [in MetaCoq.Translations.MiniHoTT_paths]
A:1489 [in MetaCoq.Translations.MiniHoTT]
A:149 [in MetaCoq.Template.EnvironmentTyping]
A:1490 [in MetaCoq.Translations.MiniHoTT_paths]
a:1492 [in MetaCoq.Template.utils.All_Forall]
a:1495 [in MetaCoq.Template.utils.All_Forall]
A:1496 [in MetaCoq.Template.utils.All_Forall]
a:1496 [in MetaCoq.Translations.MiniHoTT]
A:1497 [in MetaCoq.Translations.MiniHoTT]
A:1497 [in MetaCoq.Translations.MiniHoTT_paths]
A:15 [in MetaCoq.Template.BasicAst]
A:15 [in MetaCoq.Template.TemplateMonad.Core]
A:15 [in MetaCoq.Template.utils.MCList]
A:15 [in MetaCoq.PCUIC.utils.PCUICUtils]
a:15 [in MetaCoq.Examples.demo]
a:15 [in MetaCoq.Translations.MiniHoTT_paths]
A:150 [in MetaCoq.Template.utils.bytestring]
a:150 [in MetaCoq.PCUIC.PCUICEquality]
a:150 [in MetaCoq.Erasure.EWcbvEvalInd]
A:150 [in MetaCoq.Template.monad_utils]
A:150 [in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
A:1504 [in MetaCoq.Translations.MiniHoTT]
a:1504 [in MetaCoq.Translations.MiniHoTT_paths]
A:1505 [in MetaCoq.Translations.MiniHoTT_paths]
a:1507 [in MetaCoq.Template.utils.All_Forall]
A:151 [in MetaCoq.Erasure.EArities]
A:151 [in MetaCoq.Template.utils.MCList]
a:151 [in MetaCoq.SafeChecker.PCUICSafeReduce]
A:151 [in MetaCoq.Translations.MiniHoTT]
a:1510 [in MetaCoq.Template.utils.All_Forall]
A:1511 [in MetaCoq.Template.utils.All_Forall]
A:1512 [in MetaCoq.Translations.MiniHoTT_paths]
A:1516 [in MetaCoq.Translations.MiniHoTT]
A:1518 [in MetaCoq.Template.utils.All_Forall]
A:152 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
a:152 [in MetaCoq.Erasure.ErasureProperties]
A:152 [in MetaCoq.SafeChecker.PCUICSafeChecker]
A:1523 [in MetaCoq.Template.utils.All_Forall]
A:1524 [in MetaCoq.Translations.MiniHoTT_paths]
A:1528 [in MetaCoq.Translations.MiniHoTT]
A:153 [in MetaCoq.PCUIC.PCUICElimination]
a:153 [in MetaCoq.Erasure.ELiftSubst]
A:153 [in MetaCoq.Translations.param_cheap_packed]
A:1531 [in MetaCoq.Template.utils.All_Forall]
A:1533 [in MetaCoq.Translations.MiniHoTT]
A:1536 [in MetaCoq.Translations.MiniHoTT_paths]
A:1538 [in MetaCoq.Template.utils.All_Forall]
A:154 [in MetaCoq.Translations.times_bool_fun]
A:154 [in MetaCoq.Template.utils.All_Forall]
a:154 [in MetaCoq.PCUIC.PCUICSubstitution]
A:154 [in MetaCoq.Translations.param_cheap_packed]
A:154 [in MetaCoq.Translations.MiniHoTT_paths]
a:1540 [in MetaCoq.Translations.MiniHoTT]
A:1541 [in MetaCoq.Translations.MiniHoTT_paths]
A:1546 [in MetaCoq.Template.utils.All_Forall]
a:1548 [in MetaCoq.Translations.MiniHoTT_paths]
A:155 [in MetaCoq.Template.EnvironmentTyping]
A:155 [in MetaCoq.Translations.param_cheap_packed]
A:1552 [in MetaCoq.Template.utils.All_Forall]
A:1553 [in MetaCoq.Translations.MiniHoTT]
a:1554 [in MetaCoq.SafeChecker.PCUICSafeReduce]
A:156 [in MetaCoq.Erasure.EArities]
A:156 [in MetaCoq.Template.TermEquality]
A:156 [in MetaCoq.Template.Ast]
A:156 [in MetaCoq.PCUIC.PCUICCumulProp]
A:156 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
A:156 [in MetaCoq.Translations.param_cheap_packed]
A:156 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
A:156 [in MetaCoq.Translations.MiniHoTT]
A:1560 [in MetaCoq.Template.utils.All_Forall]
A:1560 [in MetaCoq.Translations.MiniHoTT]
A:1561 [in MetaCoq.Translations.MiniHoTT_paths]
A:1567 [in MetaCoq.Translations.MiniHoTT]
A:1568 [in MetaCoq.Template.utils.All_Forall]
A:1568 [in MetaCoq.Translations.MiniHoTT_paths]
A:157 [in MetaCoq.Template.TermEquality]
A:157 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
A:157 [in MetaCoq.PCUIC.PCUICSpine]
A:1572 [in MetaCoq.Template.utils.All_Forall]
A:1574 [in MetaCoq.Translations.MiniHoTT]
A:1575 [in MetaCoq.Template.utils.All_Forall]
A:1575 [in MetaCoq.Translations.MiniHoTT_paths]
A:158 [in MetaCoq.Template.utils.MCList]
A:1581 [in MetaCoq.Translations.MiniHoTT]
A:1582 [in MetaCoq.Translations.MiniHoTT_paths]
A:1583 [in MetaCoq.Template.utils.All_Forall]
A:1586 [in MetaCoq.Translations.MiniHoTT]
A:1587 [in MetaCoq.Template.utils.All_Forall]
A:1589 [in MetaCoq.Translations.MiniHoTT_paths]
A:159 [in MetaCoq.Template.utils.All_Forall]
a:159 [in MetaCoq.PCUIC.PCUICSubstitution]
A:159 [in MetaCoq.Template.TermEquality]
A:159 [in MetaCoq.PCUIC.PCUICTyping]
A:159 [in MetaCoq.Translations.MiniHoTT_paths]
A:1590 [in MetaCoq.Translations.MiniHoTT]
A:1591 [in MetaCoq.Template.utils.All_Forall]
A:1594 [in MetaCoq.Translations.MiniHoTT_paths]
A:1595 [in MetaCoq.Template.utils.All_Forall]
A:1598 [in MetaCoq.Translations.MiniHoTT]
A:1598 [in MetaCoq.Translations.MiniHoTT_paths]
A:1599 [in MetaCoq.Template.utils.All_Forall]
A:16 [in MetaCoq.Template.TemplateMonad.Core]
a:16 [in MetaCoq.PCUIC.Syntax.PCUICViews]
A:16 [in MetaCoq.SafeChecker.PCUICWfReduction]
A:16 [in MetaCoq.Template.Environment]
a:16 [in MetaCoq.Template.utils.MCOption]
A:16 [in MetaCoq.PCUIC.PCUICConfluence]
A:16 [in MetaCoq.Translations.MiniHoTT]
A:16 [in MetaCoq.PCUIC.Bidirectional.BDUnique]
A:160 [in MetaCoq.Erasure.EDeps]
A:160 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
A:1603 [in MetaCoq.Translations.MiniHoTT]
A:1606 [in MetaCoq.Template.utils.All_Forall]
A:1606 [in MetaCoq.Translations.MiniHoTT_paths]
A:161 [in MetaCoq.SafeChecker.PCUICSafeReduce]
A:1611 [in MetaCoq.Translations.MiniHoTT_paths]
a:1612 [in MetaCoq.SafeChecker.PCUICSafeReduce]
A:1616 [in MetaCoq.Translations.MiniHoTT]
A:1617 [in MetaCoq.Template.utils.All_Forall]
A:162 [in MetaCoq.PCUIC.PCUICCumulProp]
A:162 [in MetaCoq.Translations.MiniHoTT]
A:162 [in MetaCoq.Template.AstUtils]
A:1623 [in MetaCoq.Translations.MiniHoTT]
A:1624 [in MetaCoq.Translations.MiniHoTT_paths]
A:1626 [in MetaCoq.Template.utils.All_Forall]
A:1629 [in MetaCoq.Translations.MiniHoTT]
A:163 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
A:163 [in MetaCoq.Template.utils.All_Forall]
A:163 [in MetaCoq.Template.utils.MCList]
A:163 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
A:163 [in MetaCoq.Template.monad_utils]
A:163 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
A:163 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
A:1631 [in MetaCoq.Translations.MiniHoTT_paths]
A:1634 [in MetaCoq.Template.utils.All_Forall]
A:1637 [in MetaCoq.Translations.MiniHoTT_paths]
A:164 [in MetaCoq.Template.Ast]
A:164 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
a:164 [in MetaCoq.Erasure.EWcbvEvalInd]
A:164 [in MetaCoq.Translations.MiniHoTT_paths]
a:164 [in MetaCoq.PCUIC.PCUICReduction]
A:1642 [in MetaCoq.Template.utils.All_Forall]
A:1642 [in MetaCoq.Translations.MiniHoTT]
A:1649 [in MetaCoq.Translations.MiniHoTT]
A:1650 [in MetaCoq.Template.utils.All_Forall]
A:1650 [in MetaCoq.Translations.MiniHoTT_paths]
A:1654 [in MetaCoq.Translations.MiniHoTT]
A:1657 [in MetaCoq.Translations.MiniHoTT_paths]
A:1658 [in MetaCoq.Template.utils.All_Forall]
A:166 [in MetaCoq.Translations.times_bool_fun]
A:166 [in MetaCoq.PCUIC.PCUICTyping]
A:166 [in MetaCoq.Template.LiftSubst]
A:166 [in MetaCoq.Template.AstUtils]
A:1662 [in MetaCoq.Translations.MiniHoTT_paths]
A:1666 [in MetaCoq.Template.utils.All_Forall]
A:1674 [in MetaCoq.Template.utils.All_Forall]
A:1674 [in MetaCoq.Translations.MiniHoTT]
A:168 [in MetaCoq.PCUIC.PCUICCumulProp]
A:168 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
A:168 [in MetaCoq.Translations.MiniHoTT]
A:1680 [in MetaCoq.Template.utils.All_Forall]
A:1682 [in MetaCoq.Template.utils.All_Forall]
A:1682 [in MetaCoq.Translations.MiniHoTT_paths]
A:1683 [in MetaCoq.Translations.MiniHoTT]
A:1687 [in MetaCoq.Template.utils.All_Forall]
A:169 [in MetaCoq.Template.utils.All_Forall]
A:1691 [in MetaCoq.Translations.MiniHoTT_paths]
A:1692 [in MetaCoq.Translations.MiniHoTT]
A:1699 [in MetaCoq.Template.utils.All_Forall]
A:17 [in MetaCoq.Translations.translation_utils]
A:17 [in MetaCoq.Template.TemplateMonad.Core]
A:17 [in MetaCoq.Template.utils.ReflectEq]
a:17 [in MetaCoq.Erasure.EWcbvEvalInd]
A:17 [in MetaCoq.PCUIC.PCUICPrincipality]
A:17 [in MetaCoq.Template.utils.MCOption]
A:17 [in MetaCoq.PCUIC.Syntax.PCUICReflect]
a:17 [in MetaCoq.Translations.MiniHoTT]
A:17 [in MetaCoq.Template.utils.MCProd]
A:17 [in MetaCoq.Template.TemplateMonad.Common]
a:17 [in MetaCoq.Erasure.EOptimizePropDiscr]
A:170 [in MetaCoq.Translations.MiniHoTT_paths]
A:170 [in MetaCoq.SafeChecker.PCUICTypeChecker]
A:1700 [in MetaCoq.Translations.MiniHoTT_paths]
A:1701 [in MetaCoq.Template.utils.All_Forall]
A:1702 [in MetaCoq.Translations.MiniHoTT]
A:1707 [in MetaCoq.Translations.MiniHoTT]
A:171 [in MetaCoq.Erasure.EEtaExpandedFix]
A:171 [in MetaCoq.PCUIC.PCUICEtaExpand]
A:1710 [in MetaCoq.Translations.MiniHoTT_paths]
A:1714 [in MetaCoq.Template.utils.All_Forall]
A:1714 [in MetaCoq.Translations.MiniHoTT]
A:1715 [in MetaCoq.Translations.MiniHoTT_paths]
A:172 [in MetaCoq.Translations.times_bool_fun]
A:172 [in MetaCoq.Template.utils.MCList]
A:172 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
A:1721 [in MetaCoq.Translations.MiniHoTT]
A:1722 [in MetaCoq.Template.utils.All_Forall]
A:1722 [in MetaCoq.Translations.MiniHoTT_paths]
A:1727 [in MetaCoq.Translations.MiniHoTT]
A:1729 [in MetaCoq.Translations.MiniHoTT_paths]
A:173 [in MetaCoq.Erasure.EArities]
a:173 [in MetaCoq.PCUIC.PCUICEtaExpand]
a:173 [in MetaCoq.Erasure.EWcbvEvalInd]
A:173 [in MetaCoq.PCUIC.PCUICTyping]
a:173 [in MetaCoq.Erasure.ERemoveParams]
A:1734 [in MetaCoq.Template.utils.All_Forall]
A:1735 [in MetaCoq.Translations.MiniHoTT_paths]
A:1736 [in MetaCoq.Translations.MiniHoTT]
A:174 [in MetaCoq.Template.utils.All_Forall]
a:174 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
A:174 [in MetaCoq.PCUIC.PCUICCumulProp]
A:174 [in MetaCoq.Translations.MiniHoTT]
A:1740 [in MetaCoq.Template.utils.All_Forall]
A:1740 [in MetaCoq.SafeChecker.PCUICSafeReduce]
A:1744 [in MetaCoq.Translations.MiniHoTT_paths]
A:1745 [in MetaCoq.Translations.MiniHoTT]
A:1746 [in MetaCoq.Template.utils.All_Forall]
A:1750 [in MetaCoq.Template.utils.All_Forall]
A:1753 [in MetaCoq.Translations.MiniHoTT_paths]
A:1754 [in MetaCoq.Translations.MiniHoTT]
a:1756 [in MetaCoq.Translations.MiniHoTT]
A:1758 [in MetaCoq.Template.utils.All_Forall]
A:176 [in MetaCoq.Translations.MiniHoTT_paths]
A:1762 [in MetaCoq.Translations.MiniHoTT_paths]
A:1764 [in MetaCoq.Translations.MiniHoTT]
a:1764 [in MetaCoq.Translations.MiniHoTT_paths]
A:1766 [in MetaCoq.Template.utils.All_Forall]
A:1772 [in MetaCoq.Translations.MiniHoTT_paths]
A:1773 [in MetaCoq.Translations.MiniHoTT]
A:1774 [in MetaCoq.Template.utils.All_Forall]
A:178 [in MetaCoq.Translations.times_bool_fun]
A:178 [in MetaCoq.Template.utils.All_Forall]
A:178 [in MetaCoq.Erasure.EArities]
A:178 [in MetaCoq.PCUIC.PCUICInversion]
A:178 [in MetaCoq.PCUIC.PCUICTyping]
A:178 [in MetaCoq.Template.monad_utils]
a:178 [in MetaCoq.Erasure.ERemoveParams]
A:1781 [in MetaCoq.Template.utils.All_Forall]
A:1781 [in MetaCoq.Translations.MiniHoTT_paths]
A:1782 [in MetaCoq.Translations.MiniHoTT]
A:1787 [in MetaCoq.Template.utils.All_Forall]
a:1787 [in MetaCoq.Translations.MiniHoTT]
A:1790 [in MetaCoq.Translations.MiniHoTT_paths]
A:1792 [in MetaCoq.Translations.MiniHoTT]
A:1795 [in MetaCoq.Template.utils.All_Forall]
a:1795 [in MetaCoq.Translations.MiniHoTT_paths]
A:1798 [in MetaCoq.Translations.MiniHoTT]
A:18 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
a:18 [in MetaCoq.Translations.translation_utils]
A:18 [in MetaCoq.Template.TemplateMonad.Core]
A:18 [in MetaCoq.Template.utils.MCList]
A:18 [in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
A:18 [in MetaCoq.Translations.MiniHoTT_paths]
A:18 [in MetaCoq.PCUIC.utils.PCUICSize]
A:180 [in MetaCoq.Template.utils.MCList]
A:1800 [in MetaCoq.Template.utils.All_Forall]
A:1800 [in MetaCoq.Translations.MiniHoTT_paths]
A:1803 [in MetaCoq.Translations.MiniHoTT]
A:1806 [in MetaCoq.Translations.MiniHoTT_paths]
A:1808 [in MetaCoq.Template.utils.All_Forall]
A:1809 [in MetaCoq.Translations.MiniHoTT]
A:181 [in MetaCoq.Translations.times_bool_fun]
a:181 [in MetaCoq.PCUIC.PCUICWcbvEval]
a:181 [in MetaCoq.Template.WcbvEval]
A:1811 [in MetaCoq.Translations.MiniHoTT_paths]
A:1812 [in MetaCoq.Translations.MiniHoTT]
A:1815 [in MetaCoq.Translations.MiniHoTT]
A:1816 [in MetaCoq.Template.utils.All_Forall]
A:1817 [in MetaCoq.Translations.MiniHoTT_paths]
A:182 [in MetaCoq.Template.utils.All_Forall]
a:182 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
A:182 [in MetaCoq.PCUIC.PCUICNormal]
A:182 [in MetaCoq.Translations.MiniHoTT_paths]
A:1820 [in MetaCoq.Template.utils.All_Forall]
A:1820 [in MetaCoq.Translations.MiniHoTT]
A:1820 [in MetaCoq.Translations.MiniHoTT_paths]
A:1823 [in MetaCoq.Translations.MiniHoTT_paths]
A:1825 [in MetaCoq.Template.utils.All_Forall]
A:1825 [in MetaCoq.Translations.MiniHoTT]
A:1828 [in MetaCoq.Translations.MiniHoTT_paths]
A:1830 [in MetaCoq.Template.utils.All_Forall]
A:1833 [in MetaCoq.Translations.MiniHoTT_paths]
A:1836 [in MetaCoq.Template.utils.All_Forall]
A:1838 [in MetaCoq.Template.utils.All_Forall]
A:1839 [in MetaCoq.Translations.MiniHoTT]
A:184 [in MetaCoq.Template.BasicAst]
A:184 [in MetaCoq.Translations.times_bool_fun]
a:184 [in MetaCoq.PCUIC.PCUICWcbvEval]
A:184 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
A:1845 [in MetaCoq.Translations.MiniHoTT]
A:1847 [in MetaCoq.Translations.MiniHoTT_paths]
A:185 [in MetaCoq.Translations.MiniHoTT]
a:185 [in MetaCoq.Erasure.EWcbvEval]
A:1851 [in MetaCoq.Template.utils.All_Forall]
A:1853 [in MetaCoq.Translations.MiniHoTT_paths]
A:1855 [in MetaCoq.Translations.MiniHoTT]
A:1858 [in MetaCoq.Template.utils.All_Forall]
A:186 [in MetaCoq.Template.utils.MCList]
A:1863 [in MetaCoq.Translations.MiniHoTT]
A:1863 [in MetaCoq.Translations.MiniHoTT_paths]
A:1865 [in MetaCoq.Template.utils.All_Forall]
A:187 [in MetaCoq.Template.BasicAst]
A:187 [in MetaCoq.Translations.times_bool_fun]
a:187 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
A:1870 [in MetaCoq.Translations.MiniHoTT]
A:1871 [in MetaCoq.Translations.MiniHoTT_paths]
A:1872 [in MetaCoq.Template.utils.All_Forall]
A:1877 [in MetaCoq.Translations.MiniHoTT]
A:1878 [in MetaCoq.Translations.MiniHoTT_paths]
a:188 [in MetaCoq.PCUIC.PCUICEtaExpand]
A:1880 [in MetaCoq.Template.utils.All_Forall]
A:1884 [in MetaCoq.Translations.MiniHoTT]
A:1885 [in MetaCoq.Translations.MiniHoTT_paths]
A:1886 [in MetaCoq.Template.utils.All_Forall]
A:189 [in MetaCoq.Template.utils.All_Forall]
a:189 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
A:189 [in MetaCoq.PCUIC.PCUICNormal]
A:189 [in MetaCoq.Translations.MiniHoTT]
A:1891 [in MetaCoq.Translations.MiniHoTT]
A:1892 [in MetaCoq.Template.utils.All_Forall]
A:1892 [in MetaCoq.Translations.MiniHoTT_paths]
A:1898 [in MetaCoq.Template.utils.All_Forall]
A:1899 [in MetaCoq.Translations.MiniHoTT]
A:1899 [in MetaCoq.Translations.MiniHoTT_paths]
A:19 [in MetaCoq.Template.utils.MCReflect]
A:19 [in MetaCoq.Template.BasicAst]
A:19 [in MetaCoq.Translations.translation_utils]
A:19 [in MetaCoq.Template.TemplateMonad.Core]
A:19 [in MetaCoq.PCUIC.Syntax.PCUICViews]
A:19 [in MetaCoq.Template.Environment]
A:19 [in MetaCoq.PCUIC.PCUICConfluence]
a:19 [in MetaCoq.Examples.demo]
a:19 [in MetaCoq.Translations.MiniHoTT_paths]
a:190 [in MetaCoq.PCUIC.PCUICWcbvEval]
A:1904 [in MetaCoq.Template.utils.All_Forall]
A:1907 [in MetaCoq.Translations.MiniHoTT]
A:1907 [in MetaCoq.Translations.MiniHoTT_paths]
A:1909 [in MetaCoq.Template.utils.All_Forall]
A:191 [in MetaCoq.Template.utils.MCList]
A:1914 [in MetaCoq.Translations.MiniHoTT]
A:1915 [in MetaCoq.Translations.MiniHoTT_paths]
A:1916 [in MetaCoq.Template.utils.All_Forall]
A:1919 [in MetaCoq.Template.utils.All_Forall]
A:1921 [in MetaCoq.Translations.MiniHoTT]
A:1922 [in MetaCoq.Translations.MiniHoTT_paths]
A:1924 [in MetaCoq.Template.utils.All_Forall]
A:1928 [in MetaCoq.Translations.MiniHoTT]
A:1929 [in MetaCoq.Template.utils.All_Forall]
A:1929 [in MetaCoq.Translations.MiniHoTT_paths]
A:193 [in MetaCoq.PCUIC.PCUICSafeLemmata]
A:193 [in MetaCoq.SafeChecker.PCUICSafeConversion]
A:193 [in MetaCoq.Examples.tauto]
A:193 [in MetaCoq.Translations.MiniHoTT]
A:193 [in MetaCoq.Translations.MiniHoTT_paths]
A:1934 [in MetaCoq.Template.utils.All_Forall]
A:1935 [in MetaCoq.Translations.MiniHoTT]
A:1936 [in MetaCoq.Translations.MiniHoTT_paths]
A:194 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
A:1942 [in MetaCoq.Translations.MiniHoTT]
A:1943 [in MetaCoq.Translations.MiniHoTT_paths]
A:1946 [in MetaCoq.Template.utils.All_Forall]
A:1949 [in MetaCoq.Translations.MiniHoTT]
A:195 [in MetaCoq.PCUIC.PCUICEtaExpand]
A:195 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
A:195 [in MetaCoq.PCUIC.PCUICTyping]
A:1950 [in MetaCoq.Translations.MiniHoTT_paths]
A:1954 [in MetaCoq.Template.utils.All_Forall]
A:1956 [in MetaCoq.Translations.MiniHoTT]
A:1957 [in MetaCoq.Translations.MiniHoTT_paths]
A:196 [in MetaCoq.Template.utils.All_Forall]
A:196 [in MetaCoq.Template.utils.MCList]
A:1963 [in MetaCoq.Translations.MiniHoTT]
A:1964 [in MetaCoq.Translations.MiniHoTT_paths]
A:1967 [in MetaCoq.Template.utils.All_Forall]
A:197 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
A:197 [in MetaCoq.Translations.MiniHoTT_paths]
A:1970 [in MetaCoq.Translations.MiniHoTT]
A:1971 [in MetaCoq.Translations.MiniHoTT_paths]
A:1977 [in MetaCoq.Template.utils.All_Forall]
A:1977 [in MetaCoq.Translations.MiniHoTT]
A:1978 [in MetaCoq.Translations.MiniHoTT_paths]
A:1984 [in MetaCoq.Translations.MiniHoTT]
A:1985 [in MetaCoq.Translations.MiniHoTT_paths]
A:1986 [in MetaCoq.Template.utils.All_Forall]
A:199 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
A:199 [in MetaCoq.Template.monad_utils]
A:1991 [in MetaCoq.Translations.MiniHoTT]
A:1992 [in MetaCoq.Translations.MiniHoTT_paths]
A:1995 [in MetaCoq.Template.utils.All_Forall]
A:1998 [in MetaCoq.Translations.MiniHoTT]
A:1999 [in MetaCoq.Translations.MiniHoTT_paths]
A:20 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
a:20 [in MetaCoq.Examples.demo]
A:20 [in MetaCoq.Translations.times_bool_fun2]
a:20 [in MetaCoq.Erasure.EWcbvEval]
a:20 [in MetaCoq.Template.AstUtils]
A:200 [in MetaCoq.Translations.times_bool_fun]
A:200 [in MetaCoq.Template.utils.MCList]
A:200 [in MetaCoq.PCUIC.PCUICNormal]
A:2003 [in MetaCoq.Template.utils.All_Forall]
A:2005 [in MetaCoq.Translations.MiniHoTT]
A:2006 [in MetaCoq.Translations.MiniHoTT_paths]
A:2008 [in MetaCoq.Template.utils.All_Forall]
A:201 [in MetaCoq.Template.utils.All_Forall]
A:201 [in MetaCoq.Translations.MiniHoTT]
A:201 [in MetaCoq.Translations.MiniHoTT_paths]
A:2012 [in MetaCoq.Translations.MiniHoTT]
A:2013 [in MetaCoq.Translations.MiniHoTT_paths]
A:2017 [in MetaCoq.Template.utils.All_Forall]
A:2019 [in MetaCoq.Translations.MiniHoTT]
A:202 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
A:2020 [in MetaCoq.Translations.MiniHoTT_paths]
A:2023 [in MetaCoq.Template.utils.All_Forall]
A:2026 [in MetaCoq.Translations.MiniHoTT]
A:2027 [in MetaCoq.Translations.MiniHoTT_paths]
A:2029 [in MetaCoq.Template.utils.All_Forall]
A:2033 [in MetaCoq.Translations.MiniHoTT]
A:2034 [in MetaCoq.Translations.MiniHoTT_paths]
A:2036 [in MetaCoq.Template.utils.All_Forall]
A:2038 [in MetaCoq.Translations.MiniHoTT]
A:2041 [in MetaCoq.Template.utils.All_Forall]
A:2041 [in MetaCoq.Translations.MiniHoTT_paths]
A:2043 [in MetaCoq.SafeChecker.PCUICSafeConversion]
A:2043 [in MetaCoq.Translations.MiniHoTT]
A:2045 [in MetaCoq.Template.utils.All_Forall]
A:2046 [in MetaCoq.Translations.MiniHoTT_paths]
A:2048 [in MetaCoq.Translations.MiniHoTT]
A:205 [in MetaCoq.Translations.times_bool_fun]
A:205 [in MetaCoq.Template.utils.All_Forall]
A:205 [in MetaCoq.Erasure.EConstructorsAsBlocks]
A:205 [in MetaCoq.PCUIC.PCUICNormal]
A:2051 [in MetaCoq.SafeChecker.PCUICSafeConversion]
A:2051 [in MetaCoq.Translations.MiniHoTT_paths]
A:2052 [in MetaCoq.Template.utils.All_Forall]
A:2053 [in MetaCoq.Translations.MiniHoTT]
A:2056 [in MetaCoq.Template.utils.All_Forall]
A:2056 [in MetaCoq.Translations.MiniHoTT_paths]
A:2058 [in MetaCoq.Translations.MiniHoTT]
A:206 [in MetaCoq.Template.utils.MCList]
A:206 [in MetaCoq.SafeChecker.PCUICTypeChecker]
A:2061 [in MetaCoq.Translations.MiniHoTT_paths]
A:2062 [in MetaCoq.Template.utils.All_Forall]
A:2063 [in MetaCoq.Translations.MiniHoTT]
A:2065 [in MetaCoq.Template.utils.All_Forall]
A:2066 [in MetaCoq.Translations.MiniHoTT_paths]
A:2068 [in MetaCoq.Translations.MiniHoTT]
a:207 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
A:207 [in MetaCoq.Erasure.EConstructorsAsBlocks]
A:207 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
A:2071 [in MetaCoq.Translations.MiniHoTT_paths]
A:2073 [in MetaCoq.Translations.MiniHoTT]
A:2076 [in MetaCoq.Template.utils.All_Forall]
A:2076 [in MetaCoq.Translations.MiniHoTT_paths]
A:208 [in MetaCoq.Translations.times_bool_fun]
A:2080 [in MetaCoq.Template.utils.All_Forall]
A:2081 [in MetaCoq.Translations.MiniHoTT]
A:2081 [in MetaCoq.Translations.MiniHoTT_paths]
A:2086 [in MetaCoq.Template.utils.All_Forall]
A:2089 [in MetaCoq.Translations.MiniHoTT]
A:2089 [in MetaCoq.Translations.MiniHoTT_paths]
A:209 [in MetaCoq.PCUIC.PCUICProgress]
A:209 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
A:209 [in MetaCoq.Translations.MiniHoTT]
A:209 [in MetaCoq.Translations.MiniHoTT_paths]
A:2093 [in MetaCoq.Template.utils.All_Forall]
A:2096 [in MetaCoq.Translations.MiniHoTT]
A:2097 [in MetaCoq.Translations.MiniHoTT_paths]
A:21 [in MetaCoq.Template.TemplateMonad.Core]
A:21 [in MetaCoq.PCUIC.PCUICNormal]
a:21 [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
a:21 [in MetaCoq.PCUIC.Syntax.PCUICUnivSubst]
A:21 [in MetaCoq.Template.Reflect]
A:21 [in MetaCoq.Template.utils.MCOption]
A:21 [in MetaCoq.Template.monad_utils]
a:210 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
a:210 [in MetaCoq.Template.utils.MCList]
A:210 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
A:2101 [in MetaCoq.Template.utils.All_Forall]
A:2103 [in MetaCoq.Translations.MiniHoTT]
A:2104 [in MetaCoq.Translations.MiniHoTT_paths]
A:2108 [in MetaCoq.Template.utils.All_Forall]
A:211 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
A:211 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
A:2111 [in MetaCoq.Translations.MiniHoTT]
A:2111 [in MetaCoq.Translations.MiniHoTT_paths]
A:2115 [in MetaCoq.Template.utils.All_Forall]
A:2119 [in MetaCoq.Template.utils.All_Forall]
A:2119 [in MetaCoq.Translations.MiniHoTT]
A:2119 [in MetaCoq.Translations.MiniHoTT_paths]
A:212 [in MetaCoq.Template.utils.All_Forall]
A:212 [in MetaCoq.Template.utils.MCList]
a:212 [in MetaCoq.Erasure.EConstructorsAsBlocks]
A:212 [in MetaCoq.PCUIC.PCUICCumulProp]
A:2126 [in MetaCoq.Translations.MiniHoTT]
a:2127 [in MetaCoq.Template.utils.All_Forall]
A:2127 [in MetaCoq.Translations.MiniHoTT_paths]
A:213 [in MetaCoq.Translations.MiniHoTT]
a:2130 [in MetaCoq.Template.utils.All_Forall]
A:2131 [in MetaCoq.Template.utils.All_Forall]
A:2133 [in MetaCoq.Translations.MiniHoTT]
A:2134 [in MetaCoq.Translations.MiniHoTT_paths]
A:2140 [in MetaCoq.Translations.MiniHoTT]
A:2141 [in MetaCoq.Translations.MiniHoTT_paths]
A:2147 [in MetaCoq.Translations.MiniHoTT]
A:2148 [in MetaCoq.Translations.MiniHoTT_paths]
A:215 [in MetaCoq.SafeChecker.PCUICSafeReduce]
A:215 [in MetaCoq.Template.TypingWf]
A:2154 [in MetaCoq.Translations.MiniHoTT]
A:2155 [in MetaCoq.Template.utils.All_Forall]
A:2155 [in MetaCoq.Translations.MiniHoTT_paths]
A:216 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
A:216 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
A:2161 [in MetaCoq.Translations.MiniHoTT]
A:2162 [in MetaCoq.Translations.MiniHoTT_paths]
A:2164 [in MetaCoq.Template.utils.All_Forall]
A:2169 [in MetaCoq.Translations.MiniHoTT]
A:2169 [in MetaCoq.Translations.MiniHoTT_paths]
A:217 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
A:217 [in MetaCoq.Translations.MiniHoTT]
A:217 [in MetaCoq.Translations.MiniHoTT_paths]
A:2172 [in MetaCoq.Template.utils.All_Forall]
A:2175 [in MetaCoq.Translations.MiniHoTT]
A:2177 [in MetaCoq.Translations.MiniHoTT_paths]
A:218 [in MetaCoq.Template.utils.MCList]
A:218 [in MetaCoq.SafeChecker.PCUICErrors]
A:2181 [in MetaCoq.Template.utils.All_Forall]
A:2183 [in MetaCoq.Translations.MiniHoTT]
A:2183 [in MetaCoq.Translations.MiniHoTT_paths]
A:2189 [in MetaCoq.Translations.MiniHoTT]
a:219 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
A:2191 [in MetaCoq.Translations.MiniHoTT_paths]
A:2197 [in MetaCoq.Translations.MiniHoTT]
A:2197 [in MetaCoq.Translations.MiniHoTT_paths]
A:22 [in MetaCoq.Template.utils.MCUtils]
a:22 [in MetaCoq.Template.monad_utils]
a:22 [in MetaCoq.Template.TypingWf]
A:220 [in MetaCoq.PCUIC.PCUICAlpha]
A:220 [in MetaCoq.PCUIC.PCUICSR]
A:2203 [in MetaCoq.Translations.MiniHoTT]
A:2205 [in MetaCoq.Translations.MiniHoTT_paths]
a:221 [in MetaCoq.SafeChecker.PCUICErrors]
A:221 [in MetaCoq.Translations.MiniHoTT_paths]
A:2211 [in MetaCoq.Translations.MiniHoTT]
A:2211 [in MetaCoq.Translations.MiniHoTT_paths]
A:2217 [in MetaCoq.Translations.MiniHoTT]
A:2219 [in MetaCoq.Translations.MiniHoTT_paths]
A:222 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
A:2222 [in MetaCoq.Template.utils.All_Forall]
A:2225 [in MetaCoq.Translations.MiniHoTT]
A:2225 [in MetaCoq.Translations.MiniHoTT_paths]
A:223 [in MetaCoq.Template.utils.All_Forall]
A:223 [in MetaCoq.Template.utils.MCList]
A:223 [in MetaCoq.PCUIC.PCUICEquality]
A:223 [in MetaCoq.SafeChecker.PCUICErrors]
A:223 [in MetaCoq.Translations.MiniHoTT]
A:2233 [in MetaCoq.Translations.MiniHoTT]
A:2233 [in MetaCoq.Translations.MiniHoTT_paths]
A:2237 [in MetaCoq.Template.utils.All_Forall]
A:224 [in MetaCoq.PCUIC.PCUICEquality]
a:224 [in MetaCoq.SafeChecker.PCUICSafeReduce]
A:2240 [in MetaCoq.Translations.MiniHoTT]
A:2241 [in MetaCoq.Translations.MiniHoTT_paths]
A:2248 [in MetaCoq.Translations.MiniHoTT_paths]
a:225 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
A:225 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
A:225 [in MetaCoq.Translations.MiniHoTT_paths]
A:2250 [in MetaCoq.Translations.MiniHoTT]
A:2251 [in MetaCoq.Template.utils.All_Forall]
A:2257 [in MetaCoq.Template.utils.All_Forall]
A:2258 [in MetaCoq.Translations.MiniHoTT_paths]
a:226 [in MetaCoq.PCUIC.PCUICWcbvEval]
A:226 [in MetaCoq.PCUIC.PCUICEquality]
a:226 [in MetaCoq.SafeChecker.PCUICErrors]
A:2260 [in MetaCoq.Translations.MiniHoTT]
A:2265 [in MetaCoq.Template.utils.All_Forall]
A:2268 [in MetaCoq.Translations.MiniHoTT_paths]
A:227 [in MetaCoq.Template.utils.MCList]
A:227 [in MetaCoq.PCUIC.PCUICAlpha]
A:227 [in MetaCoq.SafeChecker.PCUICSafeReduce]
a:227 [in MetaCoq.Template.TypingWf]
A:2270 [in MetaCoq.Translations.MiniHoTT]
A:2272 [in MetaCoq.Template.utils.All_Forall]
A:2278 [in MetaCoq.Template.utils.All_Forall]
A:2278 [in MetaCoq.Translations.MiniHoTT_paths]
a:228 [in MetaCoq.SafeChecker.PCUICErrors]
A:2280 [in MetaCoq.Translations.MiniHoTT]
A:2282 [in MetaCoq.Template.utils.All_Forall]
A:2288 [in MetaCoq.Translations.MiniHoTT_paths]
A:229 [in MetaCoq.SafeChecker.PCUICErrors]
a:229 [in MetaCoq.SafeChecker.PCUICSafeReduce]
A:229 [in MetaCoq.Translations.MiniHoTT]
A:2290 [in MetaCoq.Translations.MiniHoTT]
A:2291 [in MetaCoq.Template.utils.All_Forall]
A:2296 [in MetaCoq.Template.utils.All_Forall]
a:2296 [in MetaCoq.Translations.MiniHoTT]
A:2298 [in MetaCoq.Translations.MiniHoTT]
A:2298 [in MetaCoq.Translations.MiniHoTT_paths]
a:2299 [in MetaCoq.Translations.MiniHoTT]
A:23 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
A:23 [in MetaCoq.Template.utils.MCRelations]
A:23 [in MetaCoq.Template.utils.All_Forall]
A:23 [in MetaCoq.PCUIC.PCUICAst]
A:23 [in MetaCoq.Translations.MiniHoTT]
A:23 [in MetaCoq.Template.monad_utils]
a:23 [in MetaCoq.PCUIC.PCUICContextSubst]
a:2304 [in MetaCoq.Translations.MiniHoTT_paths]
A:2305 [in MetaCoq.Template.utils.All_Forall]
A:2305 [in MetaCoq.Translations.MiniHoTT]
a:2306 [in MetaCoq.Translations.MiniHoTT]
A:2306 [in MetaCoq.Translations.MiniHoTT_paths]
a:2307 [in MetaCoq.Translations.MiniHoTT_paths]
A:231 [in MetaCoq.Template.utils.MCList]
A:231 [in MetaCoq.Translations.MiniHoTT_paths]
A:2312 [in MetaCoq.Translations.MiniHoTT]
A:2313 [in MetaCoq.Translations.MiniHoTT_paths]
A:2314 [in MetaCoq.Template.utils.All_Forall]
a:2314 [in MetaCoq.Translations.MiniHoTT_paths]
A:2318 [in MetaCoq.Translations.MiniHoTT]
A:232 [in MetaCoq.SafeChecker.PCUICErrors]
A:2320 [in MetaCoq.Translations.MiniHoTT_paths]
A:2323 [in MetaCoq.Template.utils.All_Forall]
A:2324 [in MetaCoq.Translations.MiniHoTT]
A:2326 [in MetaCoq.Translations.MiniHoTT_paths]
A:2329 [in MetaCoq.Template.utils.All_Forall]
a:233 [in MetaCoq.SafeChecker.PCUICErrors]
a:233 [in MetaCoq.Template.WcbvEval]
A:233 [in MetaCoq.PCUIC.PCUICSR]
A:2330 [in MetaCoq.Translations.MiniHoTT]
A:2332 [in MetaCoq.Translations.MiniHoTT_paths]
A:2334 [in MetaCoq.Translations.MiniHoTT]
A:2335 [in MetaCoq.Template.utils.All_Forall]
A:2338 [in MetaCoq.Translations.MiniHoTT_paths]
A:2339 [in MetaCoq.Translations.MiniHoTT]
A:234 [in MetaCoq.Template.utils.All_Forall]
A:234 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
a:234 [in MetaCoq.PCUIC.PCUICWcbvEval]
A:234 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
A:234 [in MetaCoq.SafeChecker.PCUICErrors]
A:234 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
A:2342 [in MetaCoq.Translations.MiniHoTT_paths]
A:2344 [in MetaCoq.Template.utils.All_Forall]
A:2344 [in MetaCoq.Translations.MiniHoTT]
A:2347 [in MetaCoq.Translations.MiniHoTT_paths]
A:235 [in MetaCoq.Template.utils.MCList]
A:235 [in MetaCoq.Erasure.Extract]
A:235 [in MetaCoq.Translations.MiniHoTT]
A:2352 [in MetaCoq.Translations.MiniHoTT_paths]
A:2353 [in MetaCoq.Translations.MiniHoTT]
A:2359 [in MetaCoq.SafeChecker.PCUICSafeConversion]
A:236 [in MetaCoq.PCUIC.PCUICEquality]
A:2360 [in MetaCoq.Template.utils.All_Forall]
A:2361 [in MetaCoq.Translations.MiniHoTT_paths]
a:2365 [in MetaCoq.SafeChecker.PCUICSafeConversion]
A:2366 [in MetaCoq.Translations.MiniHoTT]
A:237 [in MetaCoq.Translations.MiniHoTT_paths]
A:237 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
A:2374 [in MetaCoq.Translations.MiniHoTT_paths]
A:2378 [in MetaCoq.Translations.MiniHoTT]
a:238 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
A:238 [in MetaCoq.Template.utils.MCList]
A:238 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
A:238 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
A:2386 [in MetaCoq.Translations.MiniHoTT_paths]
A:239 [in MetaCoq.SafeChecker.PCUICErrors]
a:239 [in MetaCoq.PCUIC.PCUICTyping]
A:239 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
A:2390 [in MetaCoq.Translations.MiniHoTT]
A:2398 [in MetaCoq.Translations.MiniHoTT_paths]
A:24 [in MetaCoq.Template.utils.MCReflect]
A:24 [in MetaCoq.Translations.translation_utils]
A:24 [in MetaCoq.PCUIC.PCUICArities]
A:24 [in MetaCoq.PCUIC.PCUICNormal]
A:24 [in MetaCoq.Translations.MiniHoTT]
A:24 [in MetaCoq.Translations.MiniHoTT_paths]
A:24 [in MetaCoq.Translations.times_bool_fun2]
a:24 [in MetaCoq.Erasure.EAstUtils]
a:240 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
A:2404 [in MetaCoq.Translations.MiniHoTT]
A:241 [in MetaCoq.PCUIC.PCUICSubstitution]
A:241 [in MetaCoq.SafeChecker.PCUICErrors]
A:241 [in MetaCoq.Translations.MiniHoTT]
A:2412 [in MetaCoq.Translations.MiniHoTT]
A:2412 [in MetaCoq.Translations.MiniHoTT_paths]
a:242 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
a:242 [in MetaCoq.SafeChecker.PCUICSafeConversion]
A:242 [in MetaCoq.Template.TypingWf]
A:2420 [in MetaCoq.Translations.MiniHoTT_paths]
A:2424 [in MetaCoq.Translations.MiniHoTT]
A:243 [in MetaCoq.Template.utils.MCList]
A:243 [in MetaCoq.Template.Environment]
A:243 [in MetaCoq.Translations.MiniHoTT_paths]
a:2430 [in MetaCoq.Translations.MiniHoTT]
A:2432 [in MetaCoq.Translations.MiniHoTT_paths]
a:2433 [in MetaCoq.Translations.MiniHoTT]
A:2435 [in MetaCoq.Template.utils.All_Forall]
a:2436 [in MetaCoq.Translations.MiniHoTT]
A:2437 [in MetaCoq.Translations.MiniHoTT]
a:2438 [in MetaCoq.Translations.MiniHoTT_paths]
a:2439 [in MetaCoq.Translations.MiniHoTT]
a:244 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
a:2441 [in MetaCoq.Translations.MiniHoTT_paths]
A:2444 [in MetaCoq.Template.utils.All_Forall]
a:2444 [in MetaCoq.Translations.MiniHoTT_paths]
A:2445 [in MetaCoq.Translations.MiniHoTT_paths]
a:2447 [in MetaCoq.Translations.MiniHoTT_paths]
A:245 [in MetaCoq.Template.utils.All_Forall]
A:245 [in MetaCoq.Template.utils.MCList]
A:245 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
A:2451 [in MetaCoq.Translations.MiniHoTT]
A:2453 [in MetaCoq.Template.utils.All_Forall]
A:2459 [in MetaCoq.Translations.MiniHoTT_paths]
a:246 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
a:246 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
A:246 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
A:246 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
A:2462 [in MetaCoq.Template.utils.All_Forall]
A:2465 [in MetaCoq.Translations.MiniHoTT]
A:2468 [in MetaCoq.Template.utils.All_Forall]
A:247 [in MetaCoq.Translations.MiniHoTT]
a:2472 [in MetaCoq.Translations.MiniHoTT]
A:2473 [in MetaCoq.Template.utils.All_Forall]
A:2473 [in MetaCoq.Translations.MiniHoTT_paths]
A:2476 [in MetaCoq.Template.utils.All_Forall]
A:2476 [in MetaCoq.Translations.MiniHoTT]
a:248 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
A:248 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
a:2480 [in MetaCoq.Translations.MiniHoTT_paths]
a:2483 [in MetaCoq.Translations.MiniHoTT]
A:2484 [in MetaCoq.Translations.MiniHoTT_paths]
A:2488 [in MetaCoq.Translations.MiniHoTT]
A:249 [in MetaCoq.PCUIC.PCUICElimination]
A:249 [in MetaCoq.Translations.MiniHoTT_paths]
a:2491 [in MetaCoq.Translations.MiniHoTT_paths]
A:2492 [in MetaCoq.Template.utils.All_Forall]
A:2496 [in MetaCoq.Translations.MiniHoTT_paths]
a:25 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
A:25 [in MetaCoq.Template.utils.MCRelations]
A:25 [in MetaCoq.Template.utils.MCList]
a:25 [in MetaCoq.Erasure.EInlineProjections]
A:25 [in MetaCoq.Template.utils.ReflectEq]
A:25 [in MetaCoq.PCUIC.PCUICGeneration]
A:25 [in MetaCoq.PCUIC.Syntax.PCUICReflect]
A:25 [in MetaCoq.Examples.demo]
A:25 [in MetaCoq.Template.utils.MCProd]
a:25 [in MetaCoq.Translations.MiniHoTT_paths]
A:25 [in MetaCoq.SafeChecker.PCUICSafeChecker]
a:250 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
a:250 [in MetaCoq.Template.Typing]
a:250 [in MetaCoq.PCUIC.PCUICNormal]
A:250 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
a:2500 [in MetaCoq.Translations.MiniHoTT]
a:2503 [in MetaCoq.Translations.MiniHoTT]
A:2504 [in MetaCoq.Template.utils.All_Forall]
A:2504 [in MetaCoq.Translations.MiniHoTT]
a:2508 [in MetaCoq.Translations.MiniHoTT_paths]
A:251 [in MetaCoq.Template.utils.MCList]
A:251 [in MetaCoq.SafeChecker.PCUICErrors]
a:2511 [in MetaCoq.Translations.MiniHoTT_paths]
A:2512 [in MetaCoq.Translations.MiniHoTT_paths]
A:2517 [in MetaCoq.Translations.MiniHoTT]
a:252 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
A:2522 [in MetaCoq.Template.utils.All_Forall]
A:2525 [in MetaCoq.Translations.MiniHoTT_paths]
a:2527 [in MetaCoq.Translations.MiniHoTT]
A:2529 [in MetaCoq.Translations.MiniHoTT]
A:253 [in MetaCoq.Template.utils.All_Forall]
A:253 [in MetaCoq.Translations.MiniHoTT]
a:2535 [in MetaCoq.Translations.MiniHoTT_paths]
a:2536 [in MetaCoq.Translations.MiniHoTT]
A:2537 [in MetaCoq.Translations.MiniHoTT_paths]
A:2538 [in MetaCoq.Template.utils.All_Forall]
A:2538 [in MetaCoq.Translations.MiniHoTT]
a:254 [in MetaCoq.SafeChecker.PCUICErrors]
a:2541 [in MetaCoq.Translations.MiniHoTT]
a:2543 [in MetaCoq.Translations.MiniHoTT]
a:2544 [in MetaCoq.Translations.MiniHoTT]
a:2544 [in MetaCoq.Translations.MiniHoTT_paths]
A:2545 [in MetaCoq.Translations.MiniHoTT]
A:2546 [in MetaCoq.Translations.MiniHoTT_paths]
A:2549 [in MetaCoq.Template.utils.All_Forall]
a:2549 [in MetaCoq.Translations.MiniHoTT]
a:2549 [in MetaCoq.Translations.MiniHoTT_paths]
A:255 [in MetaCoq.PCUIC.PCUICElimination]
A:255 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
A:255 [in MetaCoq.Translations.MiniHoTT_paths]
a:2551 [in MetaCoq.Translations.MiniHoTT_paths]
A:2552 [in MetaCoq.Translations.MiniHoTT]
a:2552 [in MetaCoq.Translations.MiniHoTT_paths]
A:2553 [in MetaCoq.Translations.MiniHoTT_paths]
a:2556 [in MetaCoq.Translations.MiniHoTT]
a:2557 [in MetaCoq.Translations.MiniHoTT_paths]
A:2558 [in MetaCoq.Translations.MiniHoTT]
A:256 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
A:2560 [in MetaCoq.Translations.MiniHoTT_paths]
A:2563 [in MetaCoq.Template.utils.All_Forall]
a:2563 [in MetaCoq.Translations.MiniHoTT]
a:2564 [in MetaCoq.Translations.MiniHoTT_paths]
a:2565 [in MetaCoq.Translations.MiniHoTT]
A:2566 [in MetaCoq.Translations.MiniHoTT_paths]
a:2568 [in MetaCoq.Translations.MiniHoTT]
a:2569 [in MetaCoq.Translations.MiniHoTT]
A:257 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
A:257 [in MetaCoq.SafeChecker.PCUICErrors]
a:2571 [in MetaCoq.Translations.MiniHoTT_paths]
a:2573 [in MetaCoq.Translations.MiniHoTT]
a:2573 [in MetaCoq.Translations.MiniHoTT_paths]
a:2574 [in MetaCoq.Translations.MiniHoTT]
a:2576 [in MetaCoq.Translations.MiniHoTT_paths]
a:2577 [in MetaCoq.Translations.MiniHoTT_paths]
A:2579 [in MetaCoq.Template.utils.All_Forall]
A:2579 [in MetaCoq.Translations.MiniHoTT]
A:258 [in MetaCoq.Template.utils.MCList]
a:258 [in MetaCoq.SafeChecker.PCUICErrors]
a:2581 [in MetaCoq.Translations.MiniHoTT_paths]
a:2582 [in MetaCoq.Translations.MiniHoTT_paths]
a:2586 [in MetaCoq.Translations.MiniHoTT]
A:2587 [in MetaCoq.Translations.MiniHoTT_paths]
A:259 [in MetaCoq.SafeChecker.PCUICErrors]
A:259 [in MetaCoq.Translations.MiniHoTT]
A:2590 [in MetaCoq.Template.utils.All_Forall]
a:2591 [in MetaCoq.Translations.MiniHoTT]
a:2594 [in MetaCoq.Translations.MiniHoTT]
a:2594 [in MetaCoq.Translations.MiniHoTT_paths]
A:2595 [in MetaCoq.Translations.MiniHoTT]
a:2597 [in MetaCoq.Translations.MiniHoTT]
a:2599 [in MetaCoq.Translations.MiniHoTT]
a:2599 [in MetaCoq.Translations.MiniHoTT_paths]
A:26 [in MetaCoq.Translations.translation_utils]
A:26 [in MetaCoq.Template.TemplateMonad.Core]
a:26 [in MetaCoq.Erasure.EAstUtils]
a:26 [in MetaCoq.PCUIC.PCUICContextSubst]
a:26 [in MetaCoq.Erasure.EWcbvEval]
A:260 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
A:260 [in MetaCoq.Template.TypingWf]
a:2600 [in MetaCoq.Translations.MiniHoTT]
A:2601 [in MetaCoq.Template.utils.All_Forall]
a:2601 [in MetaCoq.Translations.MiniHoTT]
A:2602 [in MetaCoq.Translations.MiniHoTT]
a:2602 [in MetaCoq.Translations.MiniHoTT_paths]
A:2603 [in MetaCoq.Translations.MiniHoTT_paths]
a:2605 [in MetaCoq.Translations.MiniHoTT]
a:2605 [in MetaCoq.Translations.MiniHoTT_paths]
a:2606 [in MetaCoq.Translations.MiniHoTT]
a:2607 [in MetaCoq.Translations.MiniHoTT_paths]
a:2608 [in MetaCoq.Translations.MiniHoTT]
a:2608 [in MetaCoq.Translations.MiniHoTT_paths]
a:2609 [in MetaCoq.Translations.MiniHoTT_paths]
A:261 [in MetaCoq.Template.utils.All_Forall]
A:261 [in MetaCoq.Translations.MiniHoTT_paths]
A:2610 [in MetaCoq.Translations.MiniHoTT]
A:2610 [in MetaCoq.Translations.MiniHoTT_paths]
a:2613 [in MetaCoq.Translations.MiniHoTT]
a:2613 [in MetaCoq.Translations.MiniHoTT_paths]
a:2614 [in MetaCoq.Translations.MiniHoTT_paths]
a:2616 [in MetaCoq.Translations.MiniHoTT]
a:2616 [in MetaCoq.Translations.MiniHoTT_paths]
A:2618 [in MetaCoq.Translations.MiniHoTT_paths]
a:2619 [in MetaCoq.Translations.MiniHoTT]
A:2620 [in MetaCoq.Translations.MiniHoTT]
a:2621 [in MetaCoq.Translations.MiniHoTT_paths]
a:2624 [in MetaCoq.Translations.MiniHoTT_paths]
A:2627 [in MetaCoq.Translations.MiniHoTT]
a:2627 [in MetaCoq.Translations.MiniHoTT_paths]
A:2628 [in MetaCoq.Translations.MiniHoTT_paths]
A:263 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
A:263 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
a:2630 [in MetaCoq.Translations.MiniHoTT]
a:2633 [in MetaCoq.Translations.MiniHoTT]
A:2634 [in MetaCoq.Translations.MiniHoTT]
A:2635 [in MetaCoq.Translations.MiniHoTT_paths]
A:2638 [in MetaCoq.Translations.MiniHoTT]
a:2638 [in MetaCoq.Translations.MiniHoTT_paths]
A:264 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
A:264 [in MetaCoq.SafeChecker.PCUICErrors]
A:264 [in MetaCoq.PCUIC.PCUICConversion]
a:2641 [in MetaCoq.Translations.MiniHoTT]
a:2641 [in MetaCoq.Translations.MiniHoTT_paths]
A:2642 [in MetaCoq.Translations.MiniHoTT_paths]
A:2643 [in MetaCoq.Translations.MiniHoTT]
a:2646 [in MetaCoq.Translations.MiniHoTT]
A:2646 [in MetaCoq.Translations.MiniHoTT_paths]
a:2648 [in MetaCoq.Translations.MiniHoTT]
a:2649 [in MetaCoq.Translations.MiniHoTT_paths]
A:265 [in MetaCoq.Translations.MiniHoTT]
A:2651 [in MetaCoq.Translations.MiniHoTT]
A:2651 [in MetaCoq.Translations.MiniHoTT_paths]
a:2654 [in MetaCoq.Translations.MiniHoTT_paths]
a:2655 [in MetaCoq.Translations.MiniHoTT]
a:2656 [in MetaCoq.Translations.MiniHoTT_paths]
A:2658 [in MetaCoq.Translations.MiniHoTT]
A:2659 [in MetaCoq.Translations.MiniHoTT_paths]
A:266 [in MetaCoq.Template.utils.MCList]
a:2663 [in MetaCoq.Translations.MiniHoTT_paths]
A:2664 [in MetaCoq.Translations.MiniHoTT]
A:2666 [in MetaCoq.Translations.MiniHoTT_paths]
A:267 [in MetaCoq.Template.common.uGraph]
A:267 [in MetaCoq.Translations.MiniHoTT_paths]
A:2670 [in MetaCoq.Translations.MiniHoTT]
A:2672 [in MetaCoq.Translations.MiniHoTT_paths]
A:2676 [in MetaCoq.Translations.MiniHoTT]
A:2678 [in MetaCoq.Translations.MiniHoTT_paths]
A:268 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
A:268 [in MetaCoq.SafeChecker.PCUICErrors]
A:2684 [in MetaCoq.Translations.MiniHoTT_paths]
A:269 [in MetaCoq.Translations.MiniHoTT]
A:2690 [in MetaCoq.Translations.MiniHoTT]
A:2698 [in MetaCoq.Translations.MiniHoTT]
A:2698 [in MetaCoq.Translations.MiniHoTT_paths]
A:27 [in MetaCoq.Template.utils.MCReflect]
A:27 [in MetaCoq.PCUIC.PCUICProgress]
A:27 [in MetaCoq.Template.Reflect]
A:27 [in MetaCoq.Template.utils.MCOption]
A:27 [in MetaCoq.PCUIC.PCUICConfluence]
A:27 [in MetaCoq.Translations.times_bool_fun2]
a:27 [in MetaCoq.Erasure.ECSubst]
A:2703 [in MetaCoq.Translations.MiniHoTT]
A:2706 [in MetaCoq.Translations.MiniHoTT_paths]
A:2709 [in MetaCoq.Translations.MiniHoTT]
A:271 [in MetaCoq.Template.utils.All_Forall]
A:271 [in MetaCoq.PCUIC.PCUICConversion]
A:2711 [in MetaCoq.Translations.MiniHoTT_paths]
A:2715 [in MetaCoq.Translations.MiniHoTT]
A:2717 [in MetaCoq.Translations.MiniHoTT_paths]
A:272 [in MetaCoq.SafeChecker.PCUICErrors]
A:2722 [in MetaCoq.Translations.MiniHoTT]
A:2723 [in MetaCoq.Translations.MiniHoTT_paths]
A:2727 [in MetaCoq.Translations.MiniHoTT]
A:273 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
A:273 [in MetaCoq.Translations.MiniHoTT_paths]
A:2730 [in MetaCoq.Translations.MiniHoTT_paths]
A:2735 [in MetaCoq.Translations.MiniHoTT]
A:2735 [in MetaCoq.Translations.MiniHoTT_paths]
A:274 [in MetaCoq.Template.utils.MCList]
A:274 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
A:2741 [in MetaCoq.Translations.MiniHoTT]
A:2743 [in MetaCoq.Translations.MiniHoTT_paths]
A:2747 [in MetaCoq.Translations.MiniHoTT]
A:2749 [in MetaCoq.Translations.MiniHoTT_paths]
A:2754 [in MetaCoq.Translations.MiniHoTT]
A:2755 [in MetaCoq.Translations.MiniHoTT_paths]
A:2759 [in MetaCoq.Translations.MiniHoTT]
A:276 [in MetaCoq.Translations.MiniHoTT]
A:276 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
A:2762 [in MetaCoq.Translations.MiniHoTT_paths]
A:2767 [in MetaCoq.Translations.MiniHoTT]
A:2767 [in MetaCoq.Translations.MiniHoTT_paths]
A:277 [in MetaCoq.Translations.MiniHoTT_paths]
A:2773 [in MetaCoq.Translations.MiniHoTT]
A:2775 [in MetaCoq.Translations.MiniHoTT_paths]
A:2778 [in MetaCoq.Translations.MiniHoTT]
A:2781 [in MetaCoq.Translations.MiniHoTT_paths]
A:2782 [in MetaCoq.Translations.MiniHoTT]
A:2786 [in MetaCoq.Translations.MiniHoTT_paths]
A:2787 [in MetaCoq.Translations.MiniHoTT]
A:279 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
a:279 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
A:2790 [in MetaCoq.Translations.MiniHoTT_paths]
A:2795 [in MetaCoq.Translations.MiniHoTT_paths]
A:2796 [in MetaCoq.Translations.MiniHoTT]
A:28 [in MetaCoq.PCUIC.Typing.PCUICInstTyp]
a:28 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
A:28 [in MetaCoq.Template.TemplateMonad.Core]
a:28 [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
A:28 [in MetaCoq.Erasure.EEtaExpanded]
A:28 [in MetaCoq.PCUIC.utils.PCUICPrimitive]
A:280 [in MetaCoq.PCUIC.PCUICAst]
A:2804 [in MetaCoq.Translations.MiniHoTT_paths]
A:2808 [in MetaCoq.Translations.MiniHoTT]
A:281 [in MetaCoq.Template.utils.All_Forall]
A:281 [in MetaCoq.Template.utils.MCList]
A:2816 [in MetaCoq.Translations.MiniHoTT]
A:2816 [in MetaCoq.Translations.MiniHoTT_paths]
A:2819 [in MetaCoq.Translations.MiniHoTT]
a:282 [in MetaCoq.SafeChecker.PCUICErrors]
A:282 [in MetaCoq.Template.WcbvEval]
A:2824 [in MetaCoq.Translations.MiniHoTT_paths]
A:2826 [in MetaCoq.Translations.MiniHoTT]
A:2827 [in MetaCoq.Translations.MiniHoTT_paths]
A:283 [in MetaCoq.Translations.MiniHoTT]
A:283 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
A:2831 [in MetaCoq.Translations.MiniHoTT]
A:2834 [in MetaCoq.Translations.MiniHoTT_paths]
A:2837 [in MetaCoq.Translations.MiniHoTT]
A:2839 [in MetaCoq.Translations.MiniHoTT_paths]
A:284 [in MetaCoq.Template.WcbvEval]
A:284 [in MetaCoq.PCUIC.PCUICConversion]
A:284 [in MetaCoq.Translations.MiniHoTT_paths]
a:2845 [in MetaCoq.Translations.MiniHoTT]
A:2845 [in MetaCoq.Translations.MiniHoTT_paths]
A:2847 [in MetaCoq.Translations.MiniHoTT]
A:285 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
A:285 [in MetaCoq.Template.utils.MCList]
a:2850 [in MetaCoq.Translations.MiniHoTT]
a:2852 [in MetaCoq.Translations.MiniHoTT]
a:2853 [in MetaCoq.Translations.MiniHoTT_paths]
A:2855 [in MetaCoq.Translations.MiniHoTT_paths]
A:2858 [in MetaCoq.Translations.MiniHoTT]
a:2858 [in MetaCoq.Translations.MiniHoTT_paths]
a:2860 [in MetaCoq.Translations.MiniHoTT_paths]
A:2866 [in MetaCoq.Translations.MiniHoTT_paths]
A:2867 [in MetaCoq.Translations.MiniHoTT]
A:287 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
A:2875 [in MetaCoq.Translations.MiniHoTT_paths]
A:2876 [in MetaCoq.Translations.MiniHoTT]
a:2878 [in MetaCoq.Translations.MiniHoTT]
A:288 [in MetaCoq.Template.WcbvEval]
A:2884 [in MetaCoq.Translations.MiniHoTT_paths]
a:2886 [in MetaCoq.Translations.MiniHoTT_paths]
A:2887 [in MetaCoq.Translations.MiniHoTT]
A:289 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
a:289 [in MetaCoq.SafeChecker.PCUICErrors]
A:2895 [in MetaCoq.Translations.MiniHoTT_paths]
A:2898 [in MetaCoq.Translations.MiniHoTT]
A:29 [in MetaCoq.Erasure.EArities]
a:29 [in MetaCoq.Template.TemplateMonad.Core]
A:29 [in MetaCoq.Template.utils.MCList]
A:29 [in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
A:29 [in MetaCoq.Translations.MiniHoTT]
A:290 [in MetaCoq.PCUIC.PCUICConversion]
A:290 [in MetaCoq.Translations.MiniHoTT]
a:2901 [in MetaCoq.Translations.MiniHoTT]
A:2906 [in MetaCoq.Translations.MiniHoTT_paths]
a:2909 [in MetaCoq.Translations.MiniHoTT_paths]
A:291 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
A:291 [in MetaCoq.Template.utils.All_Forall]
A:291 [in MetaCoq.PCUIC.PCUICAst]
A:291 [in MetaCoq.Translations.MiniHoTT_paths]
A:291 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
A:291 [in MetaCoq.SafeChecker.PCUICEqualityDec]
A:2912 [in MetaCoq.Translations.MiniHoTT]
a:2917 [in MetaCoq.Translations.MiniHoTT]
A:292 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
A:2920 [in MetaCoq.Translations.MiniHoTT]
A:2920 [in MetaCoq.Translations.MiniHoTT_paths]
a:2925 [in MetaCoq.Translations.MiniHoTT]
a:2925 [in MetaCoq.Translations.MiniHoTT_paths]
A:2928 [in MetaCoq.Translations.MiniHoTT_paths]
A:293 [in MetaCoq.Template.utils.MCList]
A:293 [in MetaCoq.PCUIC.PCUICSubstitution]
A:2932 [in MetaCoq.Translations.MiniHoTT]
a:2933 [in MetaCoq.Translations.MiniHoTT_paths]
a:2938 [in MetaCoq.Translations.MiniHoTT]
A:294 [in MetaCoq.Template.utils.All_Forall]
A:2940 [in MetaCoq.Translations.MiniHoTT_paths]
a:2946 [in MetaCoq.Translations.MiniHoTT_paths]
A:2947 [in MetaCoq.Translations.MiniHoTT]
a:295 [in MetaCoq.SafeChecker.PCUICErrors]
A:295 [in MetaCoq.SafeChecker.PCUICEqualityDec]
a:2953 [in MetaCoq.Translations.MiniHoTT]
a:2955 [in MetaCoq.Translations.MiniHoTT]
A:2955 [in MetaCoq.Translations.MiniHoTT_paths]
A:2957 [in MetaCoq.Translations.MiniHoTT]
a:2961 [in MetaCoq.Translations.MiniHoTT_paths]
a:2962 [in MetaCoq.Translations.MiniHoTT]
a:2963 [in MetaCoq.Translations.MiniHoTT_paths]
A:2964 [in MetaCoq.Translations.MiniHoTT]
A:2965 [in MetaCoq.Translations.MiniHoTT_paths]
a:2967 [in MetaCoq.Translations.MiniHoTT]
A:2969 [in MetaCoq.Translations.MiniHoTT]
A:297 [in MetaCoq.Template.utils.All_Forall]
A:297 [in MetaCoq.Template.utils.MCList]
A:297 [in MetaCoq.Translations.MiniHoTT]
a:2970 [in MetaCoq.Translations.MiniHoTT_paths]
a:2971 [in MetaCoq.Translations.MiniHoTT]
A:2972 [in MetaCoq.Translations.MiniHoTT_paths]
a:2973 [in MetaCoq.Translations.MiniHoTT]
a:2974 [in MetaCoq.Translations.MiniHoTT]
A:2975 [in MetaCoq.Translations.MiniHoTT]
a:2975 [in MetaCoq.Translations.MiniHoTT_paths]
a:2977 [in MetaCoq.Translations.MiniHoTT]
A:2977 [in MetaCoq.Translations.MiniHoTT_paths]
A:2979 [in MetaCoq.Translations.MiniHoTT]
a:2979 [in MetaCoq.Translations.MiniHoTT_paths]
A:298 [in MetaCoq.Translations.MiniHoTT_paths]
a:2981 [in MetaCoq.Translations.MiniHoTT_paths]
a:2982 [in MetaCoq.Translations.MiniHoTT_paths]
A:2983 [in MetaCoq.Translations.MiniHoTT_paths]
a:2985 [in MetaCoq.Translations.MiniHoTT_paths]
A:2987 [in MetaCoq.Translations.MiniHoTT_paths]
A:2989 [in MetaCoq.Translations.MiniHoTT]
A:299 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
a:2991 [in MetaCoq.Translations.MiniHoTT]
a:2993 [in MetaCoq.Translations.MiniHoTT]
a:2995 [in MetaCoq.Translations.MiniHoTT]
A:2997 [in MetaCoq.Translations.MiniHoTT_paths]
a:2999 [in MetaCoq.Translations.MiniHoTT_paths]
A:3 [in MetaCoq.Template.utils.MCSquash]
A:3 [in MetaCoq.Template.TemplateMonad.Core]
A:3 [in MetaCoq.Template.utils.MCList]
A:3 [in MetaCoq.Template.TemplateCheckWf]
A:3 [in MetaCoq.PCUIC.PCUICParallelReduction]
A:3 [in MetaCoq.PCUIC.PCUICFirstorder]
A:3 [in MetaCoq.Template.utils.MCUtils]
A:3 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
A:3 [in MetaCoq.Template.Transform]
A:3 [in MetaCoq.Template.TemplateMonad.Extractable]
a:3 [in MetaCoq.Erasure.Prelim]
a:30 [in MetaCoq.PCUIC.Syntax.PCUICViews]
a:30 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
A:30 [in MetaCoq.Erasure.EWellformed]
A:30 [in MetaCoq.Template.utils.MCProd]
A:30 [in MetaCoq.Translations.times_bool_fun2]
A:300 [in MetaCoq.Template.utils.All_Forall]
a:3001 [in MetaCoq.Translations.MiniHoTT_paths]
A:3002 [in MetaCoq.Translations.MiniHoTT]
a:3003 [in MetaCoq.Translations.MiniHoTT_paths]
A:303 [in MetaCoq.Template.utils.All_Forall]
A:303 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
A:304 [in MetaCoq.Translations.MiniHoTT]
A:305 [in MetaCoq.Template.utils.MCList]
A:305 [in MetaCoq.Translations.MiniHoTT_paths]
A:307 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
A:307 [in MetaCoq.Erasure.EEtaExpandedFix]
A:307 [in MetaCoq.Template.utils.All_Forall]
a:308 [in MetaCoq.SafeChecker.PCUICErrors]
A:31 [in MetaCoq.Erasure.EPretty]
A:31 [in MetaCoq.Template.utils.ReflectEq]
A:31 [in MetaCoq.PCUIC.PCUICSN]
A:31 [in MetaCoq.Examples.demo]
A:31 [in MetaCoq.Translations.MiniHoTT_paths]
A:31 [in MetaCoq.Template.AstUtils]
A:310 [in MetaCoq.PCUIC.PCUICElimination]
A:310 [in MetaCoq.PCUIC.PCUICSR]
A:311 [in MetaCoq.Template.utils.All_Forall]
A:311 [in MetaCoq.Translations.MiniHoTT]
A:311 [in MetaCoq.SafeChecker.PCUICSafeChecker]
A:312 [in MetaCoq.Template.utils.MCList]
a:312 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
A:312 [in MetaCoq.Translations.MiniHoTT_paths]
A:315 [in MetaCoq.PCUIC.PCUICElimination]
A:315 [in MetaCoq.Template.utils.All_Forall]
A:317 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
A:317 [in MetaCoq.PCUIC.PCUICAst]
A:318 [in MetaCoq.Translations.MiniHoTT]
A:319 [in MetaCoq.Template.utils.All_Forall]
A:319 [in MetaCoq.Template.utils.MCList]
A:319 [in MetaCoq.Translations.MiniHoTT_paths]
A:32 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
A:32 [in MetaCoq.Template.utils.MCRelations]
A:32 [in MetaCoq.Translations.MiniHoTT_paths]
A:320 [in MetaCoq.PCUIC.PCUICElimination]
A:320 [in MetaCoq.PCUIC.PCUICSR]
A:322 [in MetaCoq.Template.utils.All_Forall]
a:322 [in MetaCoq.PCUIC.PCUICWcbvEval]
A:323 [in MetaCoq.PCUIC.PCUICAst]
a:324 [in MetaCoq.Template.utils.All_Forall]
A:325 [in MetaCoq.PCUIC.PCUICElimination]
A:325 [in MetaCoq.Template.utils.All_Forall]
A:325 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
A:325 [in MetaCoq.Translations.MiniHoTT]
A:326 [in MetaCoq.Translations.MiniHoTT_paths]
a:327 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
A:327 [in MetaCoq.Template.utils.MCList]
A:329 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
a:329 [in MetaCoq.Erasure.EEtaExpandedFix]
A:33 [in MetaCoq.Template.utils.All_Forall]
A:33 [in MetaCoq.Template.TemplateMonad.Core]
A:33 [in MetaCoq.PCUIC.PCUICParallelReduction]
a:33 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
A:33 [in MetaCoq.Template.utils.MCOption]
A:33 [in MetaCoq.Template.monad_utils]
A:33 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
A:33 [in MetaCoq.Erasure.Prelim]
A:330 [in MetaCoq.Template.utils.All_Forall]
A:330 [in MetaCoq.Translations.MiniHoTT]
A:331 [in MetaCoq.PCUIC.PCUICAst]
A:333 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
A:333 [in MetaCoq.Template.utils.MCList]
A:333 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
A:333 [in MetaCoq.Translations.MiniHoTT_paths]
a:335 [in MetaCoq.Erasure.EEtaExpandedFix]
A:335 [in MetaCoq.Translations.MiniHoTT]
A:337 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
A:337 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
A:338 [in MetaCoq.Template.utils.All_Forall]
A:338 [in MetaCoq.Translations.MiniHoTT_paths]
a:34 [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
A:34 [in MetaCoq.Template.AstUtils]
A:340 [in MetaCoq.Template.utils.MCList]
A:340 [in MetaCoq.Translations.MiniHoTT]
A:340 [in MetaCoq.SafeChecker.PCUICEqualityDec]
A:343 [in MetaCoq.Translations.MiniHoTT_paths]
a:344 [in MetaCoq.PCUIC.PCUICSR]
A:345 [in MetaCoq.Translations.MiniHoTT]
A:345 [in MetaCoq.Template.TypingWf]
A:346 [in MetaCoq.Template.utils.All_Forall]
A:347 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
A:348 [in MetaCoq.Template.utils.MCList]
A:348 [in MetaCoq.Translations.MiniHoTT_paths]
A:35 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
A:35 [in MetaCoq.Template.utils.ReflectEq]
A:35 [in MetaCoq.Template.Checker]
A:35 [in MetaCoq.Translations.MiniHoTT]
a:35 [in MetaCoq.Erasure.Prelim]
A:350 [in MetaCoq.Translations.MiniHoTT]
A:351 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
A:353 [in MetaCoq.Template.utils.All_Forall]
A:353 [in MetaCoq.Translations.MiniHoTT_paths]
A:354 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
A:354 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
A:354 [in MetaCoq.Template.utils.MCList]
A:355 [in MetaCoq.Translations.MiniHoTT]
A:358 [in MetaCoq.Translations.MiniHoTT_paths]
A:359 [in MetaCoq.PCUIC.PCUICProgress]
A:359 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
A:36 [in MetaCoq.PCUIC.Typing.PCUICInstTyp]
A:36 [in MetaCoq.Template.utils.MCRelations]
A:36 [in MetaCoq.Template.utils.MCList]
a:36 [in MetaCoq.PCUIC.Syntax.PCUICViews]
a:36 [in MetaCoq.Erasure.EOptimizePropDiscr]
A:360 [in MetaCoq.Translations.MiniHoTT]
A:361 [in MetaCoq.Template.utils.All_Forall]
A:361 [in MetaCoq.Template.utils.MCList]
A:362 [in MetaCoq.PCUIC.PCUICWcbvEval]
a:363 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
A:363 [in MetaCoq.Translations.MiniHoTT_paths]
A:365 [in MetaCoq.Translations.MiniHoTT]
A:366 [in MetaCoq.Template.utils.All_Forall]
A:367 [in MetaCoq.Template.utils.MCList]
A:368 [in MetaCoq.Template.utils.All_Forall]
A:368 [in MetaCoq.Translations.MiniHoTT_paths]
A:37 [in MetaCoq.PCUIC.utils.PCUICUtils]
A:37 [in MetaCoq.Examples.tauto]
A:37 [in MetaCoq.PCUIC.PCUICConfluence]
A:37 [in MetaCoq.PCUIC.Syntax.PCUICReflect]
A:37 [in MetaCoq.Translations.MiniHoTT_paths]
A:370 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
A:370 [in MetaCoq.Template.utils.All_Forall]
a:370 [in MetaCoq.Erasure.EWcbvEval]
A:372 [in MetaCoq.Template.utils.All_Forall]
A:372 [in MetaCoq.Template.utils.MCList]
A:372 [in MetaCoq.Translations.MiniHoTT]
A:372 [in MetaCoq.SafeChecker.PCUICSafeChecker]
a:373 [in MetaCoq.PCUIC.PCUICConversion]
A:373 [in MetaCoq.Translations.MiniHoTT_paths]
A:374 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
A:374 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
A:376 [in MetaCoq.Template.utils.MCList]
A:378 [in MetaCoq.Template.EtaExpand]
a:378 [in MetaCoq.Template.utils.All_Forall]
a:378 [in MetaCoq.SafeChecker.PCUICSafeChecker]
a:379 [in MetaCoq.Template.utils.MCList]
A:379 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
A:379 [in MetaCoq.Translations.MiniHoTT]
a:38 [in MetaCoq.Template.Checker]
A:38 [in MetaCoq.Template.utils.MCProd]
a:38 [in MetaCoq.Erasure.EAstUtils]
A:38 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
A:38 [in MetaCoq.Examples.add_constructor]
a:38 [in MetaCoq.Erasure.Prelim]
A:380 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
A:380 [in MetaCoq.Translations.MiniHoTT_paths]
a:381 [in MetaCoq.Template.utils.All_Forall]
A:382 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
A:382 [in MetaCoq.Template.utils.MCList]
A:382 [in MetaCoq.Template.Checker]
A:382 [in MetaCoq.SafeChecker.PCUICSafeChecker]
A:384 [in MetaCoq.Template.utils.All_Forall]
a:385 [in MetaCoq.Template.Checker]
A:386 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
A:386 [in MetaCoq.Translations.MiniHoTT]
a:386 [in MetaCoq.SafeChecker.PCUICSafeChecker]
A:387 [in MetaCoq.Template.Checker]
A:387 [in MetaCoq.Translations.MiniHoTT_paths]
A:388 [in MetaCoq.Template.utils.MCList]
a:388 [in MetaCoq.Template.Checker]
a:388 [in MetaCoq.Erasure.EWcbvEval]
A:389 [in MetaCoq.PCUIC.PCUICAst]
A:389 [in MetaCoq.Template.Checker]
A:39 [in MetaCoq.Template.utils.MCRelations]
A:39 [in MetaCoq.PCUIC.PCUICInversion]
A:39 [in MetaCoq.Template.utils.ReflectEq]
A:39 [in MetaCoq.Template.utils.MCOption]
A:39 [in MetaCoq.PCUIC.PCUICCanonicity]
A:391 [in MetaCoq.Template.utils.MCList]
A:392 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
A:392 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
a:392 [in MetaCoq.Erasure.EWcbvEval]
A:393 [in MetaCoq.PCUIC.PCUICNormal]
A:393 [in MetaCoq.Translations.MiniHoTT]
A:394 [in MetaCoq.Template.utils.MCList]
A:394 [in MetaCoq.Template.Checker]
A:394 [in MetaCoq.Translations.MiniHoTT_paths]
a:394 [in MetaCoq.SafeChecker.PCUICSafeChecker]
A:395 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
A:396 [in MetaCoq.Template.utils.All_Forall]
A:396 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
A:396 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
A:396 [in MetaCoq.PCUIC.PCUICAst]
A:398 [in MetaCoq.PCUIC.PCUICNormal]
A:398 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
A:399 [in MetaCoq.Template.utils.MCList]
A:4 [in MetaCoq.Template.utils.MCReflect]
A:4 [in MetaCoq.Template.Universes]
A:4 [in MetaCoq.Template.TemplateMonad.Core]
A:4 [in MetaCoq.PCUIC.TemplateToPCUIC]
A:4 [in MetaCoq.Template.TemplateMonad.Extractable]
A:40 [in MetaCoq.Template.TemplateMonad.Core]
a:40 [in MetaCoq.Template.common.uGraph]
A:40 [in MetaCoq.Template.Checker]
a:40 [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
A:40 [in MetaCoq.Translations.times_bool_fun2]
a:40 [in MetaCoq.Erasure.EAstUtils]
A:40 [in MetaCoq.Examples.add_constructor]
A:401 [in MetaCoq.Translations.MiniHoTT]
A:401 [in MetaCoq.Translations.MiniHoTT_paths]
A:402 [in MetaCoq.Template.utils.MCList]
a:403 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
A:403 [in MetaCoq.PCUIC.PCUICAst]
A:404 [in MetaCoq.Template.utils.All_Forall]
A:405 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
A:406 [in MetaCoq.Template.utils.MCList]
A:406 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
A:407 [in MetaCoq.Template.common.uGraph]
A:409 [in MetaCoq.PCUIC.PCUICConversion]
A:409 [in MetaCoq.Translations.MiniHoTT]
A:409 [in MetaCoq.Translations.MiniHoTT_paths]
a:41 [in MetaCoq.PCUIC.Syntax.PCUICViews]
A:41 [in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
A:41 [in MetaCoq.Erasure.ErasureFunction]
a:41 [in MetaCoq.Template.Checker]
A:410 [in MetaCoq.Template.utils.All_Forall]
a:410 [in MetaCoq.Template.utils.MCList]
A:410 [in MetaCoq.PCUIC.PCUICAst]
A:411 [in MetaCoq.Template.utils.MCList]
A:412 [in MetaCoq.PCUIC.PCUICNormal]
A:414 [in MetaCoq.Template.utils.MCList]
A:417 [in MetaCoq.Translations.MiniHoTT]
A:417 [in MetaCoq.Translations.MiniHoTT_paths]
A:418 [in MetaCoq.Template.utils.MCList]
A:419 [in MetaCoq.PCUIC.PCUICConversion]
A:42 [in MetaCoq.Template.utils.MCRelations]
A:42 [in MetaCoq.PCUIC.PCUICNormal]
A:42 [in MetaCoq.Template.utils.ReflectEq]
A:42 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
A:42 [in MetaCoq.Template.Checker]
A:42 [in MetaCoq.Template.utils.MCOption]
A:42 [in MetaCoq.Translations.MiniHoTT]
A:42 [in MetaCoq.Template.monad_utils]
a:42 [in MetaCoq.Erasure.ECSubst]
a:42 [in MetaCoq.Erasure.Prelim]
A:420 [in MetaCoq.Template.utils.All_Forall]
A:420 [in MetaCoq.Template.utils.MCList]
a:420 [in MetaCoq.PCUIC.PCUICNormal]
A:420 [in MetaCoq.PCUIC.PCUICAst]
a:422 [in MetaCoq.Erasure.EEtaExpandedFix]
A:422 [in MetaCoq.PCUIC.PCUICInductiveInversion]
A:422 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
A:423 [in MetaCoq.Template.utils.MCList]
A:424 [in MetaCoq.PCUIC.PCUICConversion]
A:425 [in MetaCoq.Translations.MiniHoTT]
A:425 [in MetaCoq.Translations.MiniHoTT_paths]
A:427 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
A:428 [in MetaCoq.Template.utils.MCList]
A:429 [in MetaCoq.Translations.MiniHoTT]
A:43 [in MetaCoq.Template.BasicAst]
A:43 [in MetaCoq.Translations.translation_utils]
A:43 [in MetaCoq.Examples.tauto]
A:43 [in MetaCoq.Translations.MiniHoTT_paths]
A:43 [in MetaCoq.Template.TypingWf]
A:43 [in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
A:430 [in MetaCoq.Template.utils.All_Forall]
A:430 [in MetaCoq.Template.utils.MCList]
a:430 [in MetaCoq.Erasure.EWcbvEval]
A:433 [in MetaCoq.Translations.MiniHoTT_paths]
A:434 [in MetaCoq.Template.utils.All_Forall]
A:434 [in MetaCoq.Template.utils.MCList]
A:434 [in MetaCoq.Translations.MiniHoTT]
A:436 [in MetaCoq.Template.common.uGraph]
A:436 [in MetaCoq.PCUIC.PCUICAst]
A:437 [in MetaCoq.Translations.MiniHoTT_paths]
A:44 [in MetaCoq.Template.BasicAst]
A:44 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
A:44 [in MetaCoq.Template.TemplateMonad.Core]
A:44 [in MetaCoq.PCUIC.utils.PCUICUtils]
A:44 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
a:44 [in MetaCoq.PCUIC.PCUICConfluence]
A:44 [in MetaCoq.Translations.standard_model]
A:44 [in MetaCoq.Template.utils.MCProd]
A:440 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
A:440 [in MetaCoq.Template.utils.All_Forall]
A:440 [in MetaCoq.Template.utils.MCList]
a:440 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
A:442 [in MetaCoq.Translations.MiniHoTT]
A:442 [in MetaCoq.Translations.MiniHoTT_paths]
A:443 [in MetaCoq.Template.utils.All_Forall]
a:443 [in MetaCoq.Erasure.EWcbvEval]
A:445 [in MetaCoq.Template.utils.MCList]
A:446 [in MetaCoq.Template.utils.All_Forall]
A:446 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
A:448 [in MetaCoq.Template.utils.MCList]
A:448 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
A:45 [in MetaCoq.Template.utils.MCRelations]
A:45 [in MetaCoq.Template.utils.All_Forall]
A:45 [in MetaCoq.Template.utils.MCList]
A:45 [in MetaCoq.Erasure.ErasureFunction]
a:45 [in MetaCoq.PCUIC.PCUICConfluence]
A:45 [in MetaCoq.PCUIC.Syntax.PCUICReflect]
a:45 [in MetaCoq.Erasure.ECSubst]
A:45 [in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
A:45 [in MetaCoq.Template.LiftSubst]
A:45 [in MetaCoq.PCUIC.utils.PCUICPretty]
A:450 [in MetaCoq.Translations.MiniHoTT_paths]
A:451 [in MetaCoq.Template.utils.All_Forall]
A:451 [in MetaCoq.Template.utils.MCList]
A:451 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
a:452 [in MetaCoq.Erasure.EEtaExpandedFix]
A:452 [in MetaCoq.Translations.MiniHoTT]
A:454 [in MetaCoq.Template.utils.MCList]
A:456 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
A:457 [in MetaCoq.Template.utils.MCList]
A:458 [in MetaCoq.Template.utils.All_Forall]
A:458 [in MetaCoq.PCUIC.PCUICAst]
A:46 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
a:46 [in MetaCoq.PCUIC.Syntax.PCUICViews]
A:46 [in MetaCoq.Template.Ast]
A:46 [in MetaCoq.PCUIC.PCUICInversion]
A:46 [in MetaCoq.Template.utils.ReflectEq]
A:46 [in MetaCoq.SafeChecker.PCUICSafeReduce]
A:46 [in MetaCoq.PCUIC.PCUICConfluence]
A:46 [in MetaCoq.Translations.standard_model]
A:460 [in MetaCoq.Translations.MiniHoTT_paths]
a:461 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
A:462 [in MetaCoq.Template.utils.MCList]
A:462 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
A:462 [in MetaCoq.Translations.MiniHoTT]
A:464 [in MetaCoq.Template.utils.All_Forall]
a:464 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
A:464 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
a:467 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
A:467 [in MetaCoq.PCUIC.PCUICAst]
A:468 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
A:468 [in MetaCoq.Translations.MiniHoTT]
a:469 [in MetaCoq.Erasure.EEtaExpandedFix]
A:469 [in MetaCoq.Template.utils.MCList]
A:47 [in MetaCoq.Template.BasicAst]
A:47 [in MetaCoq.Template.TemplateMonad.Core]
A:47 [in MetaCoq.PCUIC.PCUICWfUniverses]
A:47 [in MetaCoq.Template.Checker]
A:47 [in MetaCoq.Template.utils.MCOption]
A:47 [in MetaCoq.PCUIC.PCUICSR]
A:470 [in MetaCoq.Template.utils.All_Forall]
a:470 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
A:470 [in MetaCoq.Translations.MiniHoTT_paths]
A:472 [in MetaCoq.Template.utils.MCList]
a:473 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
A:474 [in MetaCoq.Template.utils.All_Forall]
A:474 [in MetaCoq.Translations.MiniHoTT]
A:475 [in MetaCoq.PCUIC.PCUICAst]
A:476 [in MetaCoq.Template.utils.MCList]
a:476 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
A:476 [in MetaCoq.Translations.MiniHoTT_paths]
A:477 [in MetaCoq.Erasure.EEtaExpandedFix]
A:478 [in MetaCoq.Translations.MiniHoTT]
A:479 [in MetaCoq.Template.utils.All_Forall]
A:479 [in MetaCoq.Template.utils.MCList]
A:48 [in MetaCoq.Template.utils.MCRelations]
A:48 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
a:48 [in MetaCoq.Template.AstUtils]
A:481 [in MetaCoq.Erasure.EEtaExpandedFix]
A:481 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
A:482 [in MetaCoq.Template.utils.MCList]
A:482 [in MetaCoq.Translations.MiniHoTT_paths]
A:483 [in MetaCoq.PCUIC.PCUICAst]
A:483 [in MetaCoq.SafeChecker.PCUICSafeChecker]
A:484 [in MetaCoq.Erasure.EEtaExpandedFix]
A:484 [in MetaCoq.Template.utils.MCList]
A:486 [in MetaCoq.Template.utils.All_Forall]
a:486 [in MetaCoq.Template.utils.MCList]
A:486 [in MetaCoq.Translations.MiniHoTT]
A:486 [in MetaCoq.Translations.MiniHoTT_paths]
A:488 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
A:489 [in MetaCoq.Template.utils.MCList]
A:49 [in MetaCoq.Template.Normal]
A:49 [in MetaCoq.PCUIC.PCUICParallelReduction]
A:49 [in MetaCoq.Template.Checker]
A:49 [in MetaCoq.Translations.standard_model]
A:49 [in MetaCoq.Translations.MiniHoTT]
A:49 [in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
a:491 [in MetaCoq.Template.utils.MCList]
A:491 [in MetaCoq.PCUIC.PCUICAst]
A:493 [in MetaCoq.Template.utils.All_Forall]
A:494 [in MetaCoq.Template.utils.MCList]
a:494 [in MetaCoq.Translations.MiniHoTT]
A:494 [in MetaCoq.Translations.MiniHoTT_paths]
A:495 [in MetaCoq.Translations.MiniHoTT]
A:496 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
A:497 [in MetaCoq.PCUIC.PCUICAst]
A:498 [in MetaCoq.Template.utils.All_Forall]
A:498 [in MetaCoq.Template.utils.MCList]
A:499 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
A:5 [in MetaCoq.Template.BasicAst]
A:5 [in MetaCoq.Template.utils.MCPred]
A:5 [in MetaCoq.Template.utils.MCOption]
A:50 [in MetaCoq.PCUIC.Typing.PCUICInstTyp]
A:50 [in MetaCoq.Template.utils.MCRelations]
A:50 [in MetaCoq.Template.utils.ReflectEq]
A:50 [in MetaCoq.Template.utils.MCOption]
A:50 [in MetaCoq.Translations.MiniHoTT_paths]
A:50 [in MetaCoq.Translations.times_bool_fun2]
A:50 [in MetaCoq.Template.TypingWf]
A:501 [in MetaCoq.Translations.MiniHoTT]
A:502 [in MetaCoq.Template.utils.MCList]
A:502 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
a:502 [in MetaCoq.Translations.MiniHoTT_paths]
A:503 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
A:503 [in MetaCoq.Translations.MiniHoTT_paths]
A:504 [in MetaCoq.Template.utils.All_Forall]
A:504 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
A:505 [in MetaCoq.Template.utils.MCList]
A:505 [in MetaCoq.PCUIC.PCUICAst]
A:509 [in MetaCoq.Template.utils.All_Forall]
A:509 [in MetaCoq.Template.utils.MCList]
A:509 [in MetaCoq.Translations.MiniHoTT_paths]
A:51 [in MetaCoq.Template.BasicAst]
A:51 [in MetaCoq.Translations.times_bool_fun]
A:51 [in MetaCoq.Template.utils.All_Forall]
A:51 [in MetaCoq.PCUIC.utils.PCUICUtils]
A:510 [in MetaCoq.Translations.MiniHoTT]
A:511 [in MetaCoq.PCUIC.PCUICTyping]
A:513 [in MetaCoq.Template.utils.MCList]
A:513 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
A:514 [in MetaCoq.PCUIC.PCUICAst]
A:515 [in MetaCoq.Template.utils.All_Forall]
A:515 [in MetaCoq.PCUIC.PCUICConfluence]
A:516 [in MetaCoq.Template.utils.MCList]
A:517 [in MetaCoq.Translations.MiniHoTT]
A:518 [in MetaCoq.Translations.MiniHoTT_paths]
A:52 [in MetaCoq.PCUIC.PCUICProgress]
A:52 [in MetaCoq.Template.utils.MCRelations]
A:52 [in MetaCoq.PCUIC.PCUICArities]
A:52 [in MetaCoq.Template.Normal]
A:52 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
A:52 [in MetaCoq.Translations.standard_model]
A:52 [in MetaCoq.Examples.demo]
A:520 [in MetaCoq.Template.utils.MCList]
a:522 [in MetaCoq.Template.utils.All_Forall]
A:523 [in MetaCoq.Template.utils.All_Forall]
A:524 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
A:524 [in MetaCoq.Examples.tauto]
A:524 [in MetaCoq.Translations.MiniHoTT]
A:525 [in MetaCoq.Translations.MiniHoTT_paths]
A:527 [in MetaCoq.Examples.tauto]
A:528 [in MetaCoq.Template.utils.All_Forall]
A:529 [in MetaCoq.Template.utils.MCList]
A:53 [in MetaCoq.Examples.tauto]
A:53 [in MetaCoq.PCUIC.PCUICConfluence]
A:53 [in MetaCoq.Translations.standard_model]
A:53 [in MetaCoq.PCUIC.Syntax.PCUICReflect]
A:53 [in MetaCoq.Template.utils.MCProd]
A:53 [in MetaCoq.Translations.times_bool_fun2]
A:532 [in MetaCoq.Template.utils.MCList]
A:532 [in MetaCoq.Translations.MiniHoTT_paths]
A:533 [in MetaCoq.Template.utils.All_Forall]
A:534 [in MetaCoq.PCUIC.PCUICAst]
A:535 [in MetaCoq.Template.utils.MCList]
a:536 [in MetaCoq.PCUIC.PCUICSpine]
a:537 [in MetaCoq.Template.utils.MCList]
a:537 [in MetaCoq.PCUIC.PCUICSubstitution]
A:537 [in MetaCoq.Translations.MiniHoTT]
A:538 [in MetaCoq.Template.utils.All_Forall]
A:54 [in MetaCoq.Template.utils.MCList]
a:54 [in MetaCoq.Template.utils.bytestring]
A:54 [in MetaCoq.Template.utils.ReflectEq]
A:54 [in MetaCoq.Erasure.ELiftSubst]
a:54 [in MetaCoq.Template.WcbvEval]
A:54 [in MetaCoq.Template.Pretty]
A:540 [in MetaCoq.Template.utils.MCList]
A:543 [in MetaCoq.Template.utils.All_Forall]
a:543 [in MetaCoq.PCUIC.PCUICSpine]
A:545 [in MetaCoq.PCUIC.PCUICAst]
A:545 [in MetaCoq.Translations.MiniHoTT_paths]
A:547 [in MetaCoq.Template.utils.MCList]
A:548 [in MetaCoq.Template.utils.All_Forall]
A:548 [in MetaCoq.Translations.MiniHoTT]
A:549 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
a:55 [in MetaCoq.PCUIC.PCUICWcbvEval]
A:55 [in MetaCoq.Template.Ast]
a:55 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
A:550 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
A:553 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
A:554 [in MetaCoq.Template.utils.All_Forall]
A:556 [in MetaCoq.Template.utils.MCList]
A:556 [in MetaCoq.Template.common.uGraph]
A:556 [in MetaCoq.PCUIC.PCUICAst]
A:556 [in MetaCoq.Translations.MiniHoTT_paths]
A:558 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
a:559 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
A:559 [in MetaCoq.Translations.MiniHoTT]
A:56 [in MetaCoq.Template.BasicAst]
A:56 [in MetaCoq.PCUIC.utils.PCUICUtils]
A:56 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
A:56 [in MetaCoq.PCUIC.PCUICInversion]
A:56 [in MetaCoq.Template.utils.ReflectEq]
A:56 [in MetaCoq.Translations.MiniHoTT]
A:560 [in MetaCoq.Template.utils.All_Forall]
A:561 [in MetaCoq.Template.common.uGraph]
A:561 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
a:562 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
a:564 [in MetaCoq.Erasure.EEtaExpandedFix]
a:566 [in MetaCoq.Erasure.EEtaExpandedFix]
A:566 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
A:567 [in MetaCoq.Template.utils.All_Forall]
A:567 [in MetaCoq.Translations.MiniHoTT_paths]
A:57 [in MetaCoq.Template.utils.All_Forall]
A:57 [in MetaCoq.Template.utils.MCOption]
A:57 [in MetaCoq.Examples.demo]
A:57 [in MetaCoq.Translations.MiniHoTT_paths]
A:57 [in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
A:57 [in MetaCoq.Template.TypingWf]
A:570 [in MetaCoq.Translations.MiniHoTT]
A:573 [in MetaCoq.PCUIC.PCUICEquality]
A:574 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
A:574 [in MetaCoq.PCUIC.PCUICSpine]
A:577 [in MetaCoq.Template.utils.All_Forall]
a:578 [in MetaCoq.PCUIC.PCUICEquality]
A:578 [in MetaCoq.Translations.MiniHoTT_paths]
A:58 [in MetaCoq.Template.utils.All_Forall]
A:58 [in MetaCoq.Template.utils.MCList]
A:58 [in MetaCoq.PCUIC.Syntax.PCUICReflect]
A:581 [in MetaCoq.PCUIC.PCUICConversion]
A:581 [in MetaCoq.Translations.MiniHoTT]
a:582 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
A:582 [in MetaCoq.Template.utils.wGraph]
A:583 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
A:584 [in MetaCoq.Template.utils.All_Forall]
A:587 [in MetaCoq.Template.utils.MCList]
a:587 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
A:588 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
A:589 [in MetaCoq.Template.utils.All_Forall]
A:589 [in MetaCoq.Translations.MiniHoTT_paths]
A:589 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
A:59 [in MetaCoq.Erasure.EAst]
A:59 [in MetaCoq.Examples.demo]
A:59 [in MetaCoq.Template.utils.MCProd]
A:59 [in MetaCoq.Translations.times_bool_fun2]
A:590 [in MetaCoq.PCUIC.PCUICConversion]
A:590 [in MetaCoq.Translations.MiniHoTT]
A:592 [in MetaCoq.Template.utils.MCList]
A:593 [in MetaCoq.PCUIC.PCUICSR]
A:594 [in MetaCoq.Template.utils.All_Forall]
A:594 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
A:595 [in MetaCoq.Template.utils.MCList]
A:598 [in MetaCoq.Template.utils.All_Forall]
A:598 [in MetaCoq.Template.utils.MCList]
A:598 [in MetaCoq.Translations.MiniHoTT_paths]
A:599 [in MetaCoq.Translations.MiniHoTT]
A:6 [in MetaCoq.Template.utils.MCReflect]
A:6 [in MetaCoq.Template.TemplateMonad.Core]
A:6 [in MetaCoq.Template.utils.MCPred]
A:6 [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
A:6 [in MetaCoq.PCUIC.Syntax.PCUICUnivSubst]
A:6 [in MetaCoq.Template.utils.MCProd]
A:6 [in MetaCoq.Translations.MiniHoTT_paths]
A:6 [in MetaCoq.Template.utils.MCPrelude]
A:6 [in MetaCoq.Template.TemplateMonad.Extractable]
A:60 [in MetaCoq.Template.Kernames]
a:60 [in MetaCoq.PCUIC.PCUICConfluence]
A:601 [in MetaCoq.PCUIC.PCUICTyping]
A:603 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
A:603 [in MetaCoq.Template.utils.MCList]
A:604 [in MetaCoq.Template.utils.All_Forall]
A:607 [in MetaCoq.Translations.MiniHoTT_paths]
A:608 [in MetaCoq.Translations.MiniHoTT]
A:61 [in MetaCoq.Template.BasicAst]
a:61 [in MetaCoq.PCUIC.PCUICConfluence]
A:61 [in MetaCoq.Examples.demo]
A:610 [in MetaCoq.Template.utils.All_Forall]
A:612 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
A:615 [in MetaCoq.Template.utils.MCList]
A:616 [in MetaCoq.Template.utils.All_Forall]
A:616 [in MetaCoq.Translations.MiniHoTT_paths]
A:617 [in MetaCoq.Translations.MiniHoTT]
A:62 [in MetaCoq.Template.utils.MCRelations]
A:62 [in MetaCoq.Template.utils.ReflectEq]
A:62 [in MetaCoq.Translations.times_bool_fun2]
A:622 [in MetaCoq.Translations.MiniHoTT]
A:625 [in MetaCoq.Template.utils.All_Forall]
A:625 [in MetaCoq.Translations.MiniHoTT_paths]
A:627 [in MetaCoq.Translations.MiniHoTT]
a:629 [in MetaCoq.Template.common.uGraph]
A:63 [in MetaCoq.PCUIC.PCUICParallelReduction]
A:63 [in MetaCoq.Translations.MiniHoTT]
a:63 [in MetaCoq.Erasure.EWcbvEval]
A:63 [in MetaCoq.Template.TypingWf]
A:630 [in MetaCoq.Translations.MiniHoTT_paths]
A:632 [in MetaCoq.Translations.MiniHoTT]
A:635 [in MetaCoq.Template.utils.MCList]
a:635 [in MetaCoq.Template.common.uGraph]
A:635 [in MetaCoq.Translations.MiniHoTT_paths]
A:638 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
A:638 [in MetaCoq.Template.utils.MCList]
A:64 [in MetaCoq.Template.utils.ReflectEq]
A:64 [in MetaCoq.Template.utils.MCOption]
A:64 [in MetaCoq.Translations.MiniHoTT]
A:64 [in MetaCoq.Translations.MiniHoTT_paths]
A:640 [in MetaCoq.Translations.MiniHoTT_paths]
A:641 [in MetaCoq.Translations.MiniHoTT]
A:642 [in MetaCoq.Template.utils.MCList]
a:644 [in MetaCoq.Template.Universes]
A:644 [in MetaCoq.Template.utils.All_Forall]
A:647 [in MetaCoq.Template.utils.MCList]
A:648 [in MetaCoq.Translations.MiniHoTT]
a:649 [in MetaCoq.Template.Universes]
A:649 [in MetaCoq.Translations.MiniHoTT_paths]
A:65 [in MetaCoq.Template.utils.All_Forall]
A:65 [in MetaCoq.Template.utils.MCList]
A:65 [in MetaCoq.PCUIC.Syntax.PCUICReflect]
A:65 [in MetaCoq.Template.utils.MCProd]
a:65 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
A:650 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
A:652 [in MetaCoq.Translations.MiniHoTT]
A:653 [in MetaCoq.Template.utils.MCList]
A:656 [in MetaCoq.Template.utils.All_Forall]
A:656 [in MetaCoq.Translations.MiniHoTT_paths]
A:658 [in MetaCoq.Template.utils.MCList]
a:658 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
a:66 [in MetaCoq.Template.utils.MCRelations]
A:66 [in MetaCoq.Template.utils.MCOption]
a:66 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
A:660 [in MetaCoq.Translations.MiniHoTT]
A:660 [in MetaCoq.Translations.MiniHoTT_paths]
A:661 [in MetaCoq.PCUIC.PCUICSR]
A:666 [in MetaCoq.Template.utils.MCList]
A:666 [in MetaCoq.Translations.MiniHoTT]
A:668 [in MetaCoq.Template.utils.All_Forall]
A:668 [in MetaCoq.Translations.MiniHoTT_paths]
A:67 [in MetaCoq.Template.BasicAst]
a:67 [in MetaCoq.Template.Kernames]
A:67 [in MetaCoq.Template.utils.MCOption]
A:67 [in MetaCoq.Erasure.EOptimizePropDiscr]
A:672 [in MetaCoq.Template.utils.MCList]
a:674 [in MetaCoq.Translations.MiniHoTT]
A:674 [in MetaCoq.Translations.MiniHoTT_paths]
A:676 [in MetaCoq.Template.utils.All_Forall]
A:676 [in MetaCoq.Template.utils.MCList]
A:677 [in MetaCoq.Translations.MiniHoTT]
A:68 [in MetaCoq.PCUIC.PCUICArities]
A:68 [in MetaCoq.PCUIC.PCUICInversion]
A:68 [in MetaCoq.Template.utils.MCProd]
a:68 [in MetaCoq.Template.LiftSubst]
A:681 [in MetaCoq.Template.utils.MCList]
a:682 [in MetaCoq.Translations.MiniHoTT_paths]
A:683 [in MetaCoq.Template.utils.All_Forall]
a:684 [in MetaCoq.Translations.MiniHoTT]
A:685 [in MetaCoq.Template.utils.MCList]
A:685 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
A:685 [in MetaCoq.Template.Typing]
A:685 [in MetaCoq.Translations.MiniHoTT_paths]
A:686 [in MetaCoq.Translations.MiniHoTT]
A:69 [in MetaCoq.Translations.times_bool_fun]
a:69 [in MetaCoq.Erasure.EWcbvEvalInd]
A:690 [in MetaCoq.Template.utils.All_Forall]
A:690 [in MetaCoq.Template.utils.MCList]
A:692 [in MetaCoq.Template.Typing]
a:692 [in MetaCoq.Translations.MiniHoTT_paths]
A:694 [in MetaCoq.Template.utils.MCList]
A:694 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
A:694 [in MetaCoq.PCUIC.PCUICConfluence]
A:694 [in MetaCoq.Translations.MiniHoTT_paths]
a:695 [in MetaCoq.Translations.MiniHoTT]
A:697 [in MetaCoq.Template.utils.All_Forall]
A:698 [in MetaCoq.Template.utils.MCList]
A:699 [in MetaCoq.Translations.MiniHoTT]
A:7 [in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
A:7 [in MetaCoq.Template.utils.MCRelations]
A:7 [in MetaCoq.Template.utils.All_Forall]
A:7 [in MetaCoq.Template.TemplateMonad.Core]
A:7 [in MetaCoq.Template.utils.MCList]
A:7 [in MetaCoq.PCUIC.PCUICCumulProp]
A:7 [in MetaCoq.Template.utils.MCEquality]
A:7 [in MetaCoq.Template.utils.MCPred]
A:7 [in MetaCoq.SafeChecker.PCUICWfReduction]
A:7 [in MetaCoq.Erasure.ErasureProperties]
A:7 [in MetaCoq.Translations.MiniHoTT]
A:7 [in MetaCoq.Template.TemplateMonad.Common]
A:7 [in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
A:7 [in MetaCoq.SafeChecker.PCUICSafeChecker]
A:70 [in MetaCoq.PCUIC.Syntax.PCUICViews]
A:70 [in MetaCoq.PCUIC.PCUICAlpha]
a:70 [in MetaCoq.PCUIC.PCUICConfluence]
A:70 [in MetaCoq.Translations.times_bool_fun2]
A:703 [in MetaCoq.Template.utils.MCList]
a:703 [in MetaCoq.Translations.MiniHoTT_paths]
A:704 [in MetaCoq.Template.utils.All_Forall]
A:706 [in MetaCoq.Template.utils.MCList]
a:706 [in MetaCoq.Translations.MiniHoTT]
A:706 [in MetaCoq.SafeChecker.PCUICTypeChecker]
A:707 [in MetaCoq.Translations.MiniHoTT_paths]
A:708 [in MetaCoq.Template.Universes]
a:708 [in MetaCoq.Translations.MiniHoTT]
A:709 [in MetaCoq.Translations.MiniHoTT]
A:71 [in MetaCoq.Template.BasicAst]
A:71 [in MetaCoq.Translations.times_bool_fun]
A:71 [in MetaCoq.Template.utils.MCRelations]
A:71 [in MetaCoq.Template.utils.ReflectEq]
A:71 [in MetaCoq.Translations.MiniHoTT]
A:71 [in MetaCoq.Translations.MiniHoTT_paths]
A:713 [in MetaCoq.PCUIC.PCUICInductiveInversion]
A:713 [in MetaCoq.Translations.MiniHoTT]
a:714 [in MetaCoq.Translations.MiniHoTT_paths]
A:716 [in MetaCoq.Template.utils.All_Forall]
A:716 [in MetaCoq.Template.utils.MCList]
a:716 [in MetaCoq.Translations.MiniHoTT_paths]
A:716 [in MetaCoq.PCUIC.PCUICReduction]
A:717 [in MetaCoq.Translations.MiniHoTT_paths]
A:72 [in MetaCoq.Template.utils.All_Forall]
A:72 [in MetaCoq.PCUIC.PCUICArities]
A:72 [in MetaCoq.PCUIC.PCUICParallelReduction]
A:72 [in MetaCoq.Translations.MiniHoTT_paths]
A:72 [in MetaCoq.Template.monad_utils]
a:72 [in MetaCoq.Erasure.EWcbvEval]
A:720 [in MetaCoq.Template.utils.MCList]
A:721 [in MetaCoq.Translations.MiniHoTT]
A:721 [in MetaCoq.Translations.MiniHoTT_paths]
A:724 [in MetaCoq.PCUIC.PCUICEquality]
A:724 [in MetaCoq.PCUIC.PCUICReduction]
A:725 [in MetaCoq.Template.utils.All_Forall]
A:728 [in MetaCoq.Translations.MiniHoTT]
A:729 [in MetaCoq.Translations.MiniHoTT_paths]
A:73 [in MetaCoq.SafeChecker.PCUICSafeReduce]
A:73 [in MetaCoq.Translations.param_original]
A:730 [in MetaCoq.PCUIC.PCUICReduction]
A:731 [in MetaCoq.Template.utils.MCList]
A:732 [in MetaCoq.PCUIC.PCUICReduction]
A:735 [in MetaCoq.Translations.MiniHoTT]
A:736 [in MetaCoq.Translations.MiniHoTT_paths]
A:737 [in MetaCoq.Template.utils.All_Forall]
A:737 [in MetaCoq.PCUIC.PCUICReduction]
A:74 [in MetaCoq.Template.utils.MCRelations]
A:74 [in MetaCoq.Template.utils.MCList]
A:74 [in MetaCoq.PCUIC.PCUICInversion]
A:74 [in MetaCoq.Translations.times_bool_fun2]
A:740 [in MetaCoq.PCUIC.PCUICReduction]
A:743 [in MetaCoq.Translations.MiniHoTT_paths]
A:744 [in MetaCoq.Template.utils.MCList]
A:744 [in MetaCoq.PCUIC.PCUICReduction]
A:745 [in MetaCoq.SafeChecker.PCUICSafeChecker]
A:746 [in MetaCoq.Template.utils.All_Forall]
A:746 [in MetaCoq.Translations.MiniHoTT]
A:749 [in MetaCoq.PCUIC.PCUICReduction]
A:75 [in MetaCoq.Translations.translation_utils]
A:75 [in MetaCoq.Template.EnvironmentTyping]
A:75 [in MetaCoq.Template.utils.ReflectEq]
A:75 [in MetaCoq.Template.utils.MCOption]
A:75 [in MetaCoq.Erasure.EOptimizePropDiscr]
A:752 [in MetaCoq.Template.utils.All_Forall]
A:752 [in MetaCoq.Translations.MiniHoTT]
A:754 [in MetaCoq.Template.utils.MCList]
A:754 [in MetaCoq.Translations.MiniHoTT_paths]
A:755 [in MetaCoq.PCUIC.PCUICReduction]
A:758 [in MetaCoq.Template.utils.All_Forall]
A:758 [in MetaCoq.Translations.MiniHoTT]
A:759 [in MetaCoq.Template.utils.MCList]
A:76 [in MetaCoq.Erasure.EInduction]
A:76 [in MetaCoq.Template.BasicAst]
A:76 [in MetaCoq.Template.utils.All_Forall]
a:76 [in MetaCoq.Template.utils.MCList]
A:76 [in MetaCoq.Translations.MiniHoTT]
A:76 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
A:76 [in MetaCoq.Translations.param_original]
A:76 [in MetaCoq.Translations.param_generous_packed]
A:760 [in MetaCoq.Translations.MiniHoTT_paths]
A:763 [in MetaCoq.Template.utils.All_Forall]
A:763 [in MetaCoq.PCUIC.PCUICReduction]
A:764 [in MetaCoq.Template.utils.MCList]
A:766 [in MetaCoq.Translations.MiniHoTT]
A:766 [in MetaCoq.Translations.MiniHoTT_paths]
a:77 [in MetaCoq.Erasure.ESubstitution]
A:77 [in MetaCoq.Template.utils.MCRelations]
A:77 [in MetaCoq.PCUIC.PCUICArities]
a:77 [in MetaCoq.Template.Pretty]
A:771 [in MetaCoq.Template.utils.All_Forall]
A:772 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
A:772 [in MetaCoq.Translations.MiniHoTT]
A:772 [in MetaCoq.PCUIC.PCUICReduction]
A:773 [in MetaCoq.PCUIC.PCUICConfluence]
A:774 [in MetaCoq.Translations.MiniHoTT_paths]
A:775 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
A:777 [in MetaCoq.Template.utils.MCList]
A:779 [in MetaCoq.Template.utils.All_Forall]
a:78 [in MetaCoq.Template.utils.MCList]
A:78 [in MetaCoq.Template.utils.MCOption]
A:78 [in MetaCoq.Translations.times_bool_fun2]
A:780 [in MetaCoq.Translations.MiniHoTT]
A:780 [in MetaCoq.Translations.MiniHoTT_paths]
A:781 [in MetaCoq.PCUIC.PCUICReduction]
A:781 [in MetaCoq.SafeChecker.PCUICTypeChecker]
a:782 [in MetaCoq.Translations.MiniHoTT]
A:783 [in MetaCoq.PCUIC.PCUICConfluence]
A:784 [in MetaCoq.Template.utils.MCList]
A:784 [in MetaCoq.PCUIC.PCUICConfluence]
A:784 [in MetaCoq.PCUIC.PCUICConversion]
A:785 [in MetaCoq.PCUIC.PCUICConfluence]
a:786 [in MetaCoq.Template.utils.MCList]
A:786 [in MetaCoq.PCUIC.PCUICInductiveInversion]
A:786 [in MetaCoq.PCUIC.PCUICConfluence]
A:787 [in MetaCoq.Template.utils.All_Forall]
A:787 [in MetaCoq.Template.utils.MCList]
A:787 [in MetaCoq.PCUIC.PCUICConfluence]
A:788 [in MetaCoq.Translations.MiniHoTT_paths]
A:789 [in MetaCoq.Translations.MiniHoTT]
A:79 [in MetaCoq.PCUIC.PCUICAlpha]
a:79 [in MetaCoq.Erasure.EWcbvEvalInd]
A:79 [in MetaCoq.Translations.MiniHoTT_paths]
A:790 [in MetaCoq.PCUIC.PCUICConfluence]
a:790 [in MetaCoq.Translations.MiniHoTT_paths]
A:792 [in MetaCoq.PCUIC.PCUICConversion]
a:792 [in MetaCoq.Translations.MiniHoTT]
A:793 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
A:797 [in MetaCoq.Translations.MiniHoTT_paths]
A:798 [in MetaCoq.Template.utils.All_Forall]
A:798 [in MetaCoq.PCUIC.PCUICReduction]
A:8 [in MetaCoq.Template.TemplateMonad.Core]
a:8 [in MetaCoq.PCUIC.PCUICNormal]
A:8 [in MetaCoq.Translations.MiniHoTT]
a:8 [in MetaCoq.PCUIC.PCUICContextSubst]
A:8 [in MetaCoq.Template.utils.MCPrelude]
A:8 [in MetaCoq.Template.AstUtils]
a:8 [in MetaCoq.PCUIC.PCUICReduction]
A:80 [in MetaCoq.Template.utils.MCRelations]
a:80 [in MetaCoq.Template.utils.MCList]
A:80 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
a:80 [in MetaCoq.Erasure.EWcbvEval]
A:800 [in MetaCoq.Translations.MiniHoTT]
a:800 [in MetaCoq.Translations.MiniHoTT_paths]
A:803 [in MetaCoq.PCUIC.PCUICSR]
A:803 [in MetaCoq.PCUIC.PCUICReduction]
A:808 [in MetaCoq.Translations.MiniHoTT_paths]
A:809 [in MetaCoq.PCUIC.PCUICConfluence]
A:81 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
A:81 [in MetaCoq.Template.utils.ReflectEq]
A:81 [in MetaCoq.Translations.MiniHoTT]
A:810 [in MetaCoq.Translations.MiniHoTT]
A:810 [in MetaCoq.PCUIC.PCUICSR]
A:810 [in MetaCoq.PCUIC.PCUICReduction]
A:811 [in MetaCoq.PCUIC.PCUICParallelReduction]
A:812 [in MetaCoq.PCUIC.PCUICConfluence]
a:813 [in MetaCoq.Translations.MiniHoTT]
A:813 [in MetaCoq.PCUIC.PCUICReduction]
A:816 [in MetaCoq.PCUIC.PCUICInductiveInversion]
A:816 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
A:818 [in MetaCoq.Translations.MiniHoTT_paths]
A:82 [in MetaCoq.Translations.times_bool_fun]
A:82 [in MetaCoq.Template.utils.All_Forall]
a:82 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
A:82 [in MetaCoq.PCUIC.PCUICInversion]
A:82 [in MetaCoq.Examples.tauto]
A:82 [in MetaCoq.Translations.MiniHoTT]
A:820 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
A:821 [in MetaCoq.Template.utils.All_Forall]
A:821 [in MetaCoq.Translations.MiniHoTT]
a:821 [in MetaCoq.Translations.MiniHoTT_paths]
A:821 [in MetaCoq.SafeChecker.PCUICTypeChecker]
A:824 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
a:824 [in MetaCoq.Translations.MiniHoTT]
A:829 [in MetaCoq.Translations.MiniHoTT_paths]
A:829 [in MetaCoq.PCUIC.PCUICReduction]
A:83 [in MetaCoq.Translations.param_binary]
A:83 [in MetaCoq.Template.utils.MCRelations]
A:83 [in MetaCoq.Translations.times_bool_fun2]
A:831 [in MetaCoq.PCUIC.PCUICSpine]
A:832 [in MetaCoq.Translations.MiniHoTT]
a:832 [in MetaCoq.Translations.MiniHoTT_paths]
A:835 [in MetaCoq.Template.utils.All_Forall]
a:835 [in MetaCoq.Translations.MiniHoTT]
A:835 [in MetaCoq.SafeChecker.PCUICTypeChecker]
A:839 [in MetaCoq.PCUIC.PCUICInductiveInversion]
A:839 [in MetaCoq.PCUIC.PCUICTyping]
A:84 [in MetaCoq.Template.BasicAst]
A:84 [in MetaCoq.Translations.MiniHoTT_paths]
A:84 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
a:84 [in MetaCoq.PCUIC.utils.PCUICPretty]
A:840 [in MetaCoq.Erasure.ErasureFunction]
A:840 [in MetaCoq.Translations.MiniHoTT_paths]
A:841 [in MetaCoq.Template.utils.MCList]
a:843 [in MetaCoq.Translations.MiniHoTT_paths]
A:844 [in MetaCoq.Translations.MiniHoTT]
A:849 [in MetaCoq.Template.utils.All_Forall]
A:85 [in MetaCoq.Template.utils.MCList]
A:85 [in MetaCoq.Template.utils.ReflectEq]
A:85 [in MetaCoq.Erasure.ELiftSubst]
a:85 [in MetaCoq.Erasure.EAstUtils]
A:85 [in MetaCoq.Translations.param_generous_packed]
A:852 [in MetaCoq.Translations.MiniHoTT_paths]
A:852 [in MetaCoq.SafeChecker.PCUICSafeChecker]
A:853 [in MetaCoq.Translations.MiniHoTT]
A:857 [in MetaCoq.Template.utils.MCList]
A:857 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
A:859 [in MetaCoq.Template.utils.All_Forall]
A:86 [in MetaCoq.Translations.param_binary]
A:86 [in MetaCoq.Template.utils.MCRelations]
a:86 [in MetaCoq.Template.Typing]
a:86 [in MetaCoq.PCUIC.PCUICWcbvEval]
A:86 [in MetaCoq.Template.utils.MCOption]
A:86 [in MetaCoq.Template.monad_utils]
A:86 [in MetaCoq.Translations.times_bool_fun2]
A:86 [in MetaCoq.Translations.param_original]
A:861 [in MetaCoq.Translations.MiniHoTT]
A:861 [in MetaCoq.Translations.MiniHoTT_paths]
A:863 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
A:867 [in MetaCoq.PCUIC.PCUICSR]
A:868 [in MetaCoq.Template.utils.All_Forall]
A:869 [in MetaCoq.Translations.MiniHoTT_paths]
A:87 [in MetaCoq.Translations.times_bool_fun]
a:87 [in MetaCoq.Template.WcbvEval]
A:87 [in MetaCoq.PCUIC.PCUICConfluence]
A:87 [in MetaCoq.PCUIC.Bidirectional.BDUnique]
A:87 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
A:87 [in MetaCoq.Translations.param_original]
A:870 [in MetaCoq.Template.utils.MCList]
A:870 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
A:871 [in MetaCoq.Translations.MiniHoTT]
A:872 [in MetaCoq.PCUIC.PCUICSR]
A:876 [in MetaCoq.Template.utils.All_Forall]
A:876 [in MetaCoq.Template.utils.MCList]
A:877 [in MetaCoq.PCUIC.PCUICSR]
A:879 [in MetaCoq.Translations.MiniHoTT]
A:879 [in MetaCoq.Translations.MiniHoTT_paths]
A:88 [in MetaCoq.Template.utils.MCRelations]
a:88 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
A:88 [in MetaCoq.PCUIC.PCUICArities]
a:88 [in MetaCoq.Erasure.EWcbvEvalInd]
A:88 [in MetaCoq.Translations.MiniHoTT]
A:880 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
A:882 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
A:884 [in MetaCoq.Template.utils.All_Forall]
A:887 [in MetaCoq.Translations.MiniHoTT_paths]
A:889 [in MetaCoq.Template.utils.MCList]
A:889 [in MetaCoq.Translations.MiniHoTT]
A:89 [in MetaCoq.Translations.translation_utils]
a:89 [in MetaCoq.Template.utils.MCList]
A:89 [in MetaCoq.Translations.MiniHoTT]
A:89 [in MetaCoq.Translations.MiniHoTT_paths]
A:890 [in MetaCoq.PCUIC.PCUICSR]
A:896 [in MetaCoq.Template.utils.MCList]
A:897 [in MetaCoq.Translations.MiniHoTT_paths]
A:898 [in MetaCoq.Translations.MiniHoTT]
A:899 [in MetaCoq.Template.utils.All_Forall]
A:9 [in MetaCoq.Template.BasicAst]
A:9 [in MetaCoq.Template.TemplateMonad.Core]
a:9 [in MetaCoq.PCUIC.Syntax.PCUICViews]
A:9 [in MetaCoq.Template.utils.MCString]
A:9 [in MetaCoq.Template.utils.MCOption]
a:9 [in MetaCoq.Translations.MiniHoTT]
A:9 [in MetaCoq.Template.utils.MCPrelude]
A:90 [in MetaCoq.Translations.param_binary]
A:90 [in MetaCoq.Template.utils.MCRelations]
A:90 [in MetaCoq.PCUIC.PCUICTyping]
A:90 [in MetaCoq.Translations.MiniHoTT_paths]
a:900 [in MetaCoq.Translations.MiniHoTT]
A:902 [in MetaCoq.Template.utils.MCList]
a:903 [in MetaCoq.Translations.MiniHoTT]
A:905 [in MetaCoq.Template.utils.MCList]
A:906 [in MetaCoq.Translations.MiniHoTT_paths]
A:907 [in MetaCoq.Template.utils.MCList]
a:908 [in MetaCoq.Translations.MiniHoTT_paths]
A:909 [in MetaCoq.Template.utils.All_Forall]
a:91 [in MetaCoq.Template.utils.MCList]
a:91 [in MetaCoq.PCUIC.PCUICNormal]
A:91 [in MetaCoq.Template.monad_utils]
A:91 [in MetaCoq.Translations.times_bool_fun2]
A:91 [in MetaCoq.Translations.param_generous_packed]
A:910 [in MetaCoq.Template.utils.MCList]
A:911 [in MetaCoq.Translations.MiniHoTT]
a:911 [in MetaCoq.Translations.MiniHoTT_paths]
a:912 [in MetaCoq.Template.utils.MCList]
A:913 [in MetaCoq.Template.utils.MCList]
a:914 [in MetaCoq.Translations.MiniHoTT]
a:915 [in MetaCoq.Template.utils.MCList]
A:917 [in MetaCoq.Template.utils.MCList]
a:917 [in MetaCoq.Translations.MiniHoTT]
A:917 [in MetaCoq.PCUIC.PCUICReduction]
A:919 [in MetaCoq.Template.utils.All_Forall]
A:919 [in MetaCoq.Translations.MiniHoTT_paths]
A:92 [in MetaCoq.Template.utils.MCRelations]
A:92 [in MetaCoq.Template.utils.MCOption]
a:920 [in MetaCoq.Template.utils.MCList]
A:922 [in MetaCoq.Template.utils.MCList]
a:922 [in MetaCoq.Translations.MiniHoTT_paths]
A:924 [in MetaCoq.PCUIC.PCUICTyping]
a:925 [in MetaCoq.Translations.MiniHoTT_paths]
A:925 [in MetaCoq.PCUIC.PCUICReduction]
A:927 [in MetaCoq.Template.utils.All_Forall]
A:93 [in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
A:93 [in MetaCoq.Template.BasicAst]
a:93 [in MetaCoq.Template.utils.MCList]
A:93 [in MetaCoq.Template.utils.ReflectEq]
A:933 [in MetaCoq.Template.utils.All_Forall]
A:939 [in MetaCoq.Template.utils.All_Forall]
A:94 [in MetaCoq.Translations.param_binary]
A:94 [in MetaCoq.Template.utils.MCRelations]
A:94 [in MetaCoq.PCUIC.PCUICArities]
A:94 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
A:94 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
A:940 [in MetaCoq.Template.Typing]
A:942 [in MetaCoq.Translations.MiniHoTT]
A:944 [in MetaCoq.PCUIC.PCUICReduction]
A:948 [in MetaCoq.Template.utils.All_Forall]
A:95 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
A:95 [in MetaCoq.Template.utils.All_Forall]
a:95 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
A:95 [in MetaCoq.Template.utils.ReflectEq]
A:95 [in MetaCoq.PCUIC.PCUICTyping]
A:950 [in MetaCoq.Translations.MiniHoTT_paths]
A:951 [in MetaCoq.Translations.MiniHoTT]
A:957 [in MetaCoq.Template.utils.All_Forall]
A:958 [in MetaCoq.Translations.MiniHoTT]
A:959 [in MetaCoq.Translations.MiniHoTT_paths]
A:959 [in MetaCoq.PCUIC.PCUICReduction]
A:96 [in MetaCoq.Template.utils.MCRelations]
a:96 [in MetaCoq.PCUIC.PCUICWcbvEval]
A:96 [in MetaCoq.SafeChecker.PCUICSafeReduce]
A:96 [in MetaCoq.Translations.MiniHoTT]
A:96 [in MetaCoq.Translations.MiniHoTT_paths]
A:96 [in MetaCoq.Translations.times_bool_fun2]
A:96 [in MetaCoq.Translations.param_generous_packed]
a:964 [in MetaCoq.PCUIC.PCUICReduction]
A:965 [in MetaCoq.Translations.MiniHoTT]
A:966 [in MetaCoq.Translations.MiniHoTT_paths]
A:968 [in MetaCoq.Template.utils.All_Forall]
A:97 [in MetaCoq.PCUIC.PCUICAst]
A:97 [in MetaCoq.Template.utils.MCOption]
A:97 [in MetaCoq.Translations.MiniHoTT_paths]
A:97 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
A:973 [in MetaCoq.Translations.MiniHoTT]
A:973 [in MetaCoq.Translations.MiniHoTT_paths]
A:977 [in MetaCoq.Template.utils.All_Forall]
A:98 [in MetaCoq.Template.utils.MCRelations]
A:98 [in MetaCoq.Template.utils.MCList]
A:98 [in MetaCoq.PCUIC.PCUICArities]
A:98 [in MetaCoq.PCUIC.utils.PCUICUtils]
A:98 [in MetaCoq.SafeChecker.PCUICEqualityDec]
A:981 [in MetaCoq.Translations.MiniHoTT_paths]
A:982 [in MetaCoq.Translations.MiniHoTT]
A:989 [in MetaCoq.Template.utils.All_Forall]
a:99 [in MetaCoq.Template.utils.ReflectEq]
A:990 [in MetaCoq.Translations.MiniHoTT_paths]
A:993 [in MetaCoq.Translations.MiniHoTT]



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)