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)

N

name [inductive, in MetaCoq.Template.BasicAst]
nameless [definition, in MetaCoq.PCUIC.Syntax.PCUICNamelessDef]
nameless_eq_term_spec [lemma, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nameless_eqctx_IH [lemma, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nameless_ctx [abbreviation, in MetaCoq.PCUIC.Syntax.PCUICNamelessDef]
nameless_decl [definition, in MetaCoq.PCUIC.Syntax.PCUICNamelessDef]
nameless:4 [binder, in MetaCoq.PCUIC.Syntax.PCUICNamelessDef]
names:110 [binder, in MetaCoq.PCUIC.utils.PCUICPretty]
names:124 [binder, in MetaCoq.Template.Pretty]
names:132 [binder, in MetaCoq.Template.Pretty]
names:80 [binder, in MetaCoq.Template.Pretty]
name_from_term [definition, in MetaCoq.Erasure.EPretty]
name_from_term [definition, in MetaCoq.Template.Pretty]
name_from_term [definition, in MetaCoq.PCUIC.utils.PCUICPretty]
name:47 [binder, in MetaCoq.Examples.demo]
nAnon [constructor, in MetaCoq.Template.BasicAst]
nAnon [definition, in MetaCoq.Translations.translation_utils]
nAnon [definition, in MetaCoq.Translations.param_binary]
nApp [definition, in MetaCoq.PCUIC.utils.PCUICAstUtils]
nApp_mkApps [lemma, in MetaCoq.PCUIC.utils.PCUICAstUtils]
nApp_isApp_false [lemma, in MetaCoq.PCUIC.PCUICWcbvEval]
nApp_decompose_app [lemma, in MetaCoq.Erasure.EAstUtils]
nApp_mkApps [lemma, in MetaCoq.Template.AstUtils]
napp':206 [binder, in MetaCoq.Template.TermEquality]
napp':215 [binder, in MetaCoq.Template.TermEquality]
napp':222 [binder, in MetaCoq.Template.TermEquality]
napp':333 [binder, in MetaCoq.PCUIC.PCUICEquality]
napp':349 [binder, in MetaCoq.PCUIC.PCUICEquality]
napp':360 [binder, in MetaCoq.PCUIC.PCUICEquality]
napp':374 [binder, in MetaCoq.PCUIC.PCUICEquality]
napp':381 [binder, in MetaCoq.PCUIC.PCUICEquality]
napp':386 [binder, in MetaCoq.PCUIC.PCUICEquality]
napp:10 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
napp:103 [binder, in MetaCoq.PCUIC.PCUICCumulativity]
napp:103 [binder, in MetaCoq.PCUIC.PCUICConvCumInversion]
napp:1112 [binder, in MetaCoq.PCUIC.PCUICConversion]
napp:118 [binder, in MetaCoq.PCUIC.PCUICEquality]
napp:1237 [binder, in MetaCoq.PCUIC.PCUICConfluence]
napp:129 [binder, in MetaCoq.Erasure.Prelim]
napp:134 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
napp:14 [binder, in MetaCoq.Erasure.ESpineView]
napp:14 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
napp:150 [binder, in MetaCoq.PCUIC.PCUICCumulativity]
napp:154 [binder, in MetaCoq.Template.TermEquality]
napp:16 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
napp:163 [binder, in MetaCoq.Template.TermEquality]
napp:172 [binder, in MetaCoq.Erasure.EInduction]
napp:173 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
napp:179 [binder, in MetaCoq.Template.TermEquality]
napp:180 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
napp:188 [binder, in MetaCoq.Template.TermEquality]
napp:188 [binder, in MetaCoq.PCUIC.PCUICEquality]
napp:193 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
napp:2 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
napp:202 [binder, in MetaCoq.Template.TermEquality]
napp:205 [binder, in MetaCoq.Template.TermEquality]
napp:208 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
napp:214 [binder, in MetaCoq.Template.TermEquality]
napp:221 [binder, in MetaCoq.Template.TermEquality]
napp:221 [binder, in MetaCoq.PCUIC.PCUICEquality]
napp:228 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
napp:231 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
napp:232 [binder, in MetaCoq.Template.TermEquality]
napp:240 [binder, in MetaCoq.PCUIC.PCUICAlpha]
napp:242 [binder, in MetaCoq.PCUIC.PCUICEquality]
napp:244 [binder, in MetaCoq.Template.TermEquality]
napp:25 [binder, in MetaCoq.PCUIC.PCUICEquality]
napp:251 [binder, in MetaCoq.PCUIC.PCUICEquality]
napp:260 [binder, in MetaCoq.Erasure.EInduction]
napp:263 [binder, in MetaCoq.PCUIC.PCUICEquality]
napp:266 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
napp:27 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
napp:272 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
napp:273 [binder, in MetaCoq.PCUIC.PCUICEquality]
napp:274 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
napp:277 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
napp:28 [binder, in MetaCoq.Template.TermEquality]
napp:280 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
napp:280 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
napp:287 [binder, in MetaCoq.PCUIC.PCUICEquality]
napp:287 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
napp:288 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
napp:296 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
napp:303 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
napp:309 [binder, in MetaCoq.PCUIC.PCUICConfluence]
napp:310 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
napp:316 [binder, in MetaCoq.PCUIC.PCUICEquality]
napp:319 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
napp:32 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
napp:322 [binder, in MetaCoq.PCUIC.PCUICEquality]
napp:33 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
napp:331 [binder, in MetaCoq.PCUIC.PCUICConfluence]
napp:332 [binder, in MetaCoq.PCUIC.PCUICEquality]
napp:341 [binder, in MetaCoq.PCUIC.PCUICEquality]
napp:348 [binder, in MetaCoq.PCUIC.PCUICEquality]
napp:35 [binder, in MetaCoq.PCUIC.PCUICEquality]
napp:351 [binder, in MetaCoq.PCUIC.PCUICEquality]
napp:351 [binder, in MetaCoq.PCUIC.PCUICConfluence]
napp:359 [binder, in MetaCoq.PCUIC.PCUICEquality]
napp:37 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
napp:373 [binder, in MetaCoq.PCUIC.PCUICEquality]
napp:377 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
napp:38 [binder, in MetaCoq.Template.TermEquality]
napp:380 [binder, in MetaCoq.PCUIC.PCUICEquality]
napp:385 [binder, in MetaCoq.PCUIC.PCUICEquality]
napp:388 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
napp:39 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
napp:391 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
napp:394 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
napp:395 [binder, in MetaCoq.PCUIC.PCUICConfluence]
napp:399 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
napp:4 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
napp:40 [binder, in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
napp:403 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
napp:41 [binder, in MetaCoq.Erasure.ESpineView]
napp:416 [binder, in MetaCoq.PCUIC.PCUICConfluence]
napp:44 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
napp:45 [binder, in MetaCoq.SafeChecker.PCUICSafeRetyping]
napp:458 [binder, in MetaCoq.PCUIC.PCUICEquality]
napp:467 [binder, in MetaCoq.PCUIC.PCUICConfluence]
napp:487 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
napp:488 [binder, in MetaCoq.PCUIC.PCUICConfluence]
napp:489 [binder, in MetaCoq.PCUIC.PCUICEquality]
napp:49 [binder, in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
napp:495 [binder, in MetaCoq.PCUIC.PCUICEquality]
napp:505 [binder, in MetaCoq.PCUIC.PCUICEquality]
napp:509 [binder, in MetaCoq.PCUIC.PCUICEquality]
napp:518 [binder, in MetaCoq.PCUIC.PCUICEquality]
napp:529 [binder, in MetaCoq.PCUIC.PCUICNormal]
napp:537 [binder, in MetaCoq.PCUIC.PCUICNormal]
napp:546 [binder, in MetaCoq.PCUIC.PCUICConfluence]
napp:56 [binder, in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
napp:570 [binder, in MetaCoq.PCUIC.PCUICEquality]
napp:59 [binder, in MetaCoq.PCUIC.PCUICPrincipality]
napp:61 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
napp:64 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
napp:64 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
napp:653 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
napp:655 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
napp:66 [binder, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
napp:679 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
napp:680 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
napp:687 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
napp:690 [binder, in MetaCoq.PCUIC.PCUICEquality]
napp:690 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
napp:693 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
napp:702 [binder, in MetaCoq.PCUIC.PCUICEquality]
napp:703 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
napp:71 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
napp:71 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
napp:72 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
napp:74 [binder, in MetaCoq.Template.TermEquality]
napp:74 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
napp:79 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
napp:86 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
napp:88 [binder, in MetaCoq.PCUIC.PCUICConvCumInversion]
napp:97 [binder, in MetaCoq.PCUIC.PCUICCumulativity]
nargs:139 [binder, in MetaCoq.Erasure.EConstructorsAsBlocks]
nargs:141 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
nargs:145 [binder, in MetaCoq.Erasure.EWcbvEval]
nargs:170 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
nargs:189 [binder, in MetaCoq.Erasure.EWcbvEval]
nargs:242 [binder, in MetaCoq.Template.WcbvEval]
nargs:269 [binder, in MetaCoq.Template.WcbvEval]
narg:100 [binder, in MetaCoq.Erasure.EWcbvEvalInd]
narg:100 [binder, in MetaCoq.Erasure.EWcbvEval]
narg:102 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
narg:105 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
narg:105 [binder, in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
narg:106 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
narg:107 [binder, in MetaCoq.PCUIC.PCUICNormal]
narg:108 [binder, in MetaCoq.Template.Typing]
narg:108 [binder, in MetaCoq.Template.WcbvEval]
narg:109 [binder, in MetaCoq.Erasure.EWcbvEvalInd]
narg:112 [binder, in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
narg:114 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
narg:115 [binder, in MetaCoq.Template.Typing]
narg:116 [binder, in MetaCoq.Template.WcbvEval]
narg:119 [binder, in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
narg:122 [binder, in MetaCoq.Template.Typing]
narg:123 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
narg:123 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
narg:125 [binder, in MetaCoq.Template.WcbvEval]
narg:130 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
narg:131 [binder, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
narg:136 [binder, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
narg:137 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
narg:141 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
narg:144 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
narg:147 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
narg:149 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
narg:152 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
narg:161 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
narg:184 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
narg:185 [binder, in MetaCoq.PCUIC.PCUICReduction]
narg:191 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
narg:193 [binder, in MetaCoq.Template.WcbvEval]
narg:193 [binder, in MetaCoq.PCUIC.PCUICReduction]
narg:198 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
narg:201 [binder, in MetaCoq.PCUIC.PCUICReduction]
narg:202 [binder, in MetaCoq.Template.WcbvEval]
narg:207 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
narg:207 [binder, in MetaCoq.PCUIC.PCUICCanonicity]
narg:209 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
narg:210 [binder, in MetaCoq.Template.WcbvEval]
narg:212 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
narg:219 [binder, in MetaCoq.Template.WcbvEval]
narg:220 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
narg:221 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
narg:230 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
narg:232 [binder, in MetaCoq.PCUIC.PCUICNormal]
narg:233 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
narg:240 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
narg:247 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
narg:25 [binder, in MetaCoq.PCUIC.PCUICReduction]
narg:250 [binder, in MetaCoq.Erasure.EWcbvEval]
narg:252 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
narg:255 [binder, in MetaCoq.Erasure.EWcbvEval]
narg:260 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
narg:276 [binder, in MetaCoq.Template.Typing]
narg:28 [binder, in MetaCoq.Template.TypingWf]
narg:284 [binder, in MetaCoq.Template.Typing]
narg:289 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
narg:292 [binder, in MetaCoq.Template.Typing]
narg:294 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
narg:295 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
narg:300 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
narg:303 [binder, in MetaCoq.Template.WcbvEval]
narg:32 [binder, in MetaCoq.PCUIC.PCUICReduction]
narg:325 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
narg:327 [binder, in MetaCoq.PCUIC.PCUICNormal]
narg:339 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
narg:35 [binder, in MetaCoq.Template.TypingWf]
narg:365 [binder, in MetaCoq.PCUIC.PCUICSR]
narg:373 [binder, in MetaCoq.PCUIC.PCUICSR]
narg:374 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
narg:379 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
narg:381 [binder, in MetaCoq.PCUIC.PCUICSR]
narg:384 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
narg:385 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
narg:387 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
narg:39 [binder, in MetaCoq.PCUIC.PCUICReduction]
narg:392 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
narg:400 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
narg:400 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
narg:415 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
narg:44 [binder, in MetaCoq.Erasure.EDeps]
narg:46 [binder, in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
narg:51 [binder, in MetaCoq.Erasure.EDeps]
narg:53 [binder, in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
narg:74 [binder, in MetaCoq.Erasure.EWcbvEval]
narg:75 [binder, in MetaCoq.Erasure.Prelim]
narg:76 [binder, in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
narg:81 [binder, in MetaCoq.Erasure.EWcbvEvalInd]
narg:84 [binder, in MetaCoq.Erasure.EWcbvEval]
narg:89 [binder, in MetaCoq.PCUIC.PCUICNormal]
narg:91 [binder, in MetaCoq.Erasure.EWcbvEval]
narg:92 [binder, in MetaCoq.Erasure.EWcbvEvalInd]
narg:938 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
narg:98 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
narg:98 [binder, in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
narg:99 [binder, in MetaCoq.Template.WcbvEval]
nas':113 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
nas':115 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
nas:1 [binder, in MetaCoq.PCUIC.PCUICCasesContexts]
nAs:10 [binder, in MetaCoq.PCUIC.utils.PCUICPretty]
nas:112 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
nas:114 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
nas:12 [binder, in MetaCoq.PCUIC.PCUICCasesContexts]
nas:144 [binder, in MetaCoq.PCUIC.PCUICAlpha]
nas:196 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
nas:201 [binder, in MetaCoq.PCUIC.PCUICSR]
nas:203 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
nas:206 [binder, in MetaCoq.PCUIC.PCUICSR]
nas:207 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
nas:210 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
nas:215 [binder, in MetaCoq.PCUIC.PCUICSR]
nas:218 [binder, in MetaCoq.PCUIC.PCUICContexts]
nas:221 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
nas:225 [binder, in MetaCoq.PCUIC.PCUICContexts]
nas:229 [binder, in MetaCoq.PCUIC.PCUICContexts]
nas:232 [binder, in MetaCoq.PCUIC.PCUICContexts]
nas:288 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
nas:291 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
nas:297 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
nas:314 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
nas:362 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
nas:365 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
nas:371 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
nas:388 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
nas:45 [binder, in MetaCoq.PCUIC.PCUICValidity]
nas:45 [binder, in MetaCoq.PCUIC.PCUICCasesContexts]
nas:49 [binder, in MetaCoq.Erasure.EPretty]
nas:52 [binder, in MetaCoq.PCUIC.PCUICValidity]
nas:55 [binder, in MetaCoq.Erasure.EPretty]
nAs:56 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
nAs:57 [binder, in MetaCoq.Template.AstUtils]
nas:597 [binder, in MetaCoq.PCUIC.PCUICSR]
nas:659 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
nas:663 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
nAs:7 [binder, in MetaCoq.Template.Pretty]
nas:79 [binder, in MetaCoq.Erasure.Prelim]
nas:797 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
nas:8 [binder, in MetaCoq.PCUIC.PCUICCasesContexts]
nas:891 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
nas:895 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
nas:905 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
nas:907 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
nas:910 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
NativeCast [constructor, in MetaCoq.Template.BasicAst]
nat_rev_ind [lemma, in MetaCoq.Template.utils.MCArith]
nat_recursion_ext [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
nat_le_irrel [lemma, in MetaCoq.Template.Reflect]
Nat_module [abbreviation, in MetaCoq.Examples.demo]
na':100 [binder, in MetaCoq.PCUIC.Bidirectional.BDUnique]
na':102 [binder, in MetaCoq.PCUIC.PCUICConversion]
na':102 [binder, in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
na':1034 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
na':1043 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
na':105 [binder, in MetaCoq.Template.TermEquality]
na':106 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
na':108 [binder, in MetaCoq.SafeChecker.PCUICSafeRetyping]
na':109 [binder, in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
na':109 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
na':11 [binder, in MetaCoq.SafeChecker.PCUICErrors]
na':111 [binder, in MetaCoq.Template.TermEquality]
na':114 [binder, in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
na':138 [binder, in MetaCoq.Erasure.Prelim]
na':142 [binder, in MetaCoq.Erasure.Prelim]
na':143 [binder, in MetaCoq.PCUIC.PCUICEquality]
na':147 [binder, in MetaCoq.Erasure.Prelim]
na':149 [binder, in MetaCoq.PCUIC.PCUICEquality]
na':155 [binder, in MetaCoq.PCUIC.PCUICEquality]
na':18 [binder, in MetaCoq.PCUIC.Bidirectional.BDUnique]
na':20 [binder, in MetaCoq.SafeChecker.PCUICErrors]
na':204 [binder, in MetaCoq.PCUIC.PCUICConversion]
na':213 [binder, in MetaCoq.PCUIC.PCUICConversion]
na':214 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
na':219 [binder, in MetaCoq.PCUIC.PCUICConversion]
na':266 [binder, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
na':270 [binder, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
na':270 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
na':278 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
na':28 [binder, in MetaCoq.SafeChecker.PCUICErrors]
na':286 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
na':3 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
na':323 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
na':330 [binder, in MetaCoq.Template.Environment]
na':333 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
na':334 [binder, in MetaCoq.Template.Environment]
na':342 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
na':37 [binder, in MetaCoq.SafeChecker.PCUICErrors]
na':396 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
na':408 [binder, in MetaCoq.PCUIC.PCUICConversion]
na':409 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
na':411 [binder, in MetaCoq.Template.EnvironmentTyping]
na':417 [binder, in MetaCoq.Template.EnvironmentTyping]
na':418 [binder, in MetaCoq.PCUIC.PCUICConversion]
na':42 [binder, in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
na':421 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
na':432 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
na':439 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
na':446 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
na':46 [binder, in MetaCoq.Erasure.EPretty]
na':46 [binder, in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
na':47 [binder, in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
na':47 [binder, in MetaCoq.Erasure.EPretty]
na':47 [binder, in MetaCoq.Template.Typing]
na':48 [binder, in MetaCoq.Template.Reflect]
na':51 [binder, in MetaCoq.PCUIC.PCUICArities]
na':51 [binder, in MetaCoq.Template.TermEquality]
na':54 [binder, in MetaCoq.PCUIC.PCUICEquality]
na':55 [binder, in MetaCoq.PCUIC.utils.PCUICPretty]
na':56 [binder, in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
na':56 [binder, in MetaCoq.Template.TermEquality]
na':56 [binder, in MetaCoq.PCUIC.utils.PCUICPretty]
na':58 [binder, in MetaCoq.Template.Typing]
na':59 [binder, in MetaCoq.PCUIC.PCUICEquality]
na':59 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
na':60 [binder, in MetaCoq.PCUIC.utils.PCUICOnOne]
na':61 [binder, in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
na':65 [binder, in MetaCoq.PCUIC.utils.PCUICOnOne]
na':65 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
na':69 [binder, in MetaCoq.Template.Pretty]
na':7 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
na':70 [binder, in MetaCoq.Template.Pretty]
na':71 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
na':71 [binder, in MetaCoq.Template.Pretty]
na':744 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
na':75 [binder, in MetaCoq.PCUIC.utils.PCUICPretty]
na':754 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
na':76 [binder, in MetaCoq.PCUIC.utils.PCUICPretty]
na':77 [binder, in MetaCoq.PCUIC.utils.PCUICPretty]
na':786 [binder, in MetaCoq.PCUIC.PCUICConversion]
na':834 [binder, in MetaCoq.PCUIC.PCUICConversion]
na':84 [binder, in MetaCoq.Template.Pretty]
na':841 [binder, in MetaCoq.PCUIC.PCUICConversion]
na':86 [binder, in MetaCoq.PCUIC.Bidirectional.BDUnique]
na':95 [binder, in MetaCoq.PCUIC.PCUICConversion]
na':96 [binder, in MetaCoq.Template.Pretty]
na':97 [binder, in MetaCoq.Template.Pretty]
na':99 [binder, in MetaCoq.Template.TermEquality]
na1:511 [binder, in MetaCoq.PCUIC.PCUICConversion]
na1:545 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
na1:551 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
na1:818 [binder, in MetaCoq.PCUIC.PCUICConversion]
na1:826 [binder, in MetaCoq.PCUIC.PCUICConversion]
na1:848 [binder, in MetaCoq.PCUIC.PCUICConversion]
na1:871 [binder, in MetaCoq.PCUIC.PCUICConversion]
na1:879 [binder, in MetaCoq.PCUIC.PCUICConversion]
na2:512 [binder, in MetaCoq.PCUIC.PCUICConversion]
na2:548 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
na2:554 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
na2:819 [binder, in MetaCoq.PCUIC.PCUICConversion]
na2:827 [binder, in MetaCoq.PCUIC.PCUICConversion]
na2:849 [binder, in MetaCoq.PCUIC.PCUICConversion]
na2:872 [binder, in MetaCoq.PCUIC.PCUICConversion]
na2:880 [binder, in MetaCoq.PCUIC.PCUICConversion]
na:1 [binder, in MetaCoq.PCUIC.Syntax.PCUICNamelessDef]
na:10 [binder, in MetaCoq.PCUIC.Syntax.PCUICViews]
na:10 [binder, in MetaCoq.PCUIC.PCUICGeneration]
na:100 [binder, in MetaCoq.PCUIC.PCUICArities]
na:100 [binder, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
na:1003 [binder, in MetaCoq.PCUIC.PCUICReduction]
na:101 [binder, in MetaCoq.Template.EtaExpand]
na:101 [binder, in MetaCoq.PCUIC.PCUICConversion]
na:102 [binder, in MetaCoq.PCUIC.PCUICAst]
na:1024 [binder, in MetaCoq.PCUIC.PCUICReduction]
na:1029 [binder, in MetaCoq.PCUIC.PCUICReduction]
na:103 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
na:1033 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
na:104 [binder, in MetaCoq.Template.EtaExpand]
na:104 [binder, in MetaCoq.PCUIC.PCUICArities]
na:104 [binder, in MetaCoq.Template.TermEquality]
na:104 [binder, in MetaCoq.SafeChecker.PCUICSafeRetyping]
na:1042 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
na:105 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
na:106 [binder, in MetaCoq.PCUIC.PCUICTyping]
na:106 [binder, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
na:1069 [binder, in MetaCoq.PCUIC.PCUICReduction]
na:107 [binder, in MetaCoq.Template.EtaExpand]
na:107 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
na:1074 [binder, in MetaCoq.PCUIC.PCUICReduction]
na:108 [binder, in MetaCoq.PCUIC.PCUICValidity]
na:108 [binder, in MetaCoq.PCUIC.PCUICReduction]
na:108 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
na:109 [binder, in MetaCoq.PCUIC.PCUICArities]
na:1095 [binder, in MetaCoq.PCUIC.PCUICReduction]
na:11 [binder, in MetaCoq.Template.Reflect]
na:110 [binder, in MetaCoq.Template.TermEquality]
na:1100 [binder, in MetaCoq.PCUIC.PCUICReduction]
na:111 [binder, in MetaCoq.Template.EnvironmentTyping]
na:111 [binder, in MetaCoq.PCUIC.Bidirectional.BDUnique]
na:112 [binder, in MetaCoq.PCUIC.PCUICReduction]
na:1129 [binder, in MetaCoq.Erasure.ErasureFunction]
na:113 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
na:1131 [binder, in MetaCoq.PCUIC.PCUICReduction]
na:1135 [binder, in MetaCoq.PCUIC.PCUICReduction]
na:1139 [binder, in MetaCoq.PCUIC.PCUICReduction]
na:114 [binder, in MetaCoq.Template.EnvironmentTyping]
na:114 [binder, in MetaCoq.PCUIC.PCUICConversion]
na:114 [binder, in MetaCoq.PCUIC.PCUICCanonicity]
na:115 [binder, in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
na:116 [binder, in MetaCoq.PCUIC.PCUICArities]
na:1166 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
na:117 [binder, in MetaCoq.PCUIC.PCUICSpine]
na:1171 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
na:118 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
na:1187 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
na:1192 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
na:12 [binder, in MetaCoq.Template.Normal]
na:12 [binder, in MetaCoq.SafeChecker.PCUICWfReduction]
na:12 [binder, in MetaCoq.PCUIC.PCUICContextSubst]
na:120 [binder, in MetaCoq.PCUIC.PCUICConversion]
na:123 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
na:124 [binder, in MetaCoq.PCUIC.PCUICSpine]
na:125 [binder, in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
na:126 [binder, in MetaCoq.PCUIC.PCUICCanonicity]
na:128 [binder, in MetaCoq.PCUIC.PCUICArities]
na:128 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
na:13 [binder, in MetaCoq.Translations.param_binary]
na:13 [binder, in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
na:132 [binder, in MetaCoq.PCUIC.PCUICFirstorder]
na:133 [binder, in MetaCoq.Template.Typing]
na:133 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
na:134 [binder, in MetaCoq.PCUIC.PCUICAst]
na:136 [binder, in MetaCoq.PCUIC.Syntax.PCUICCases]
na:137 [binder, in MetaCoq.Template.Typing]
na:137 [binder, in MetaCoq.Erasure.Prelim]
na:138 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
na:14 [binder, in MetaCoq.Template.WfAst]
na:14 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
na:141 [binder, in MetaCoq.Template.Typing]
na:141 [binder, in MetaCoq.Erasure.Prelim]
na:142 [binder, in MetaCoq.PCUIC.PCUICEquality]
na:143 [binder, in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
na:143 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
na:143 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
na:144 [binder, in MetaCoq.Template.WcbvEval]
na:145 [binder, in MetaCoq.PCUIC.Syntax.PCUICCases]
na:146 [binder, in MetaCoq.Template.Typing]
na:146 [binder, in MetaCoq.Erasure.Prelim]
na:147 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
na:148 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
na:148 [binder, in MetaCoq.PCUIC.PCUICEquality]
na:15 [binder, in MetaCoq.Translations.param_binary]
na:15 [binder, in MetaCoq.SafeChecker.PCUICWfReduction]
na:15 [binder, in MetaCoq.Erasure.EWcbvEvalInd]
na:15 [binder, in MetaCoq.PCUIC.Bidirectional.BDUnique]
na:150 [binder, in MetaCoq.Template.EnvironmentTyping]
na:150 [binder, in MetaCoq.PCUIC.Syntax.PCUICCases]
na:151 [binder, in MetaCoq.Template.Typing]
na:151 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
na:151 [binder, in MetaCoq.Template.WcbvEval]
na:152 [binder, in MetaCoq.PCUIC.Syntax.PCUICCases]
na:154 [binder, in MetaCoq.PCUIC.PCUICEquality]
na:154 [binder, in MetaCoq.PCUIC.Syntax.PCUICCases]
na:155 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
na:1553 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
na:156 [binder, in MetaCoq.Template.EnvironmentTyping]
na:158 [binder, in MetaCoq.PCUIC.Syntax.PCUICCases]
na:159 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
na:16 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
na:16 [binder, in MetaCoq.SafeChecker.PCUICErrors]
na:161 [binder, in MetaCoq.PCUIC.PCUICReduction]
na:1611 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
na:162 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
na:163 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
na:164 [binder, in MetaCoq.PCUIC.Syntax.PCUICCases]
na:164 [binder, in MetaCoq.PCUIC.PCUICContexts]
na:166 [binder, in MetaCoq.PCUIC.PCUICReduction]
na:167 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
na:168 [binder, in MetaCoq.PCUIC.Syntax.PCUICCases]
na:169 [binder, in MetaCoq.Template.EtaExpand]
na:17 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
na:17 [binder, in MetaCoq.Template.WfAst]
na:170 [binder, in MetaCoq.PCUIC.Syntax.PCUICCases]
na:171 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
na:173 [binder, in MetaCoq.Template.EtaExpand]
na:1741 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
na:175 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
na:176 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
na:1763 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
na:177 [binder, in MetaCoq.Template.EtaExpand]
na:179 [binder, in MetaCoq.PCUIC.PCUICConversion]
na:18 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
na:18 [binder, in MetaCoq.SafeChecker.PCUICWfReduction]
na:180 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
na:181 [binder, in MetaCoq.PCUIC.PCUICNormal]
na:182 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
na:184 [binder, in MetaCoq.PCUIC.PCUICConversion]
na:184 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
na:187 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
na:187 [binder, in MetaCoq.Template.Ast]
na:188 [binder, in MetaCoq.PCUIC.PCUICNormal]
na:189 [binder, in MetaCoq.Erasure.EEtaExpanded]
na:19 [binder, in MetaCoq.PCUIC.PCUICEtaExpand]
na:19 [binder, in MetaCoq.Template.Reflect]
na:19 [binder, in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
na:190 [binder, in MetaCoq.Template.Ast]
na:190 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
na:191 [binder, in MetaCoq.Erasure.EEtaExpanded]
na:192 [binder, in MetaCoq.PCUIC.PCUICSafeLemmata]
na:192 [binder, in MetaCoq.Erasure.Extract]
na:192 [binder, in MetaCoq.PCUIC.PCUICConversion]
na:193 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
na:193 [binder, in MetaCoq.Template.Ast]
na:194 [binder, in MetaCoq.Erasure.Extract]
na:197 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
na:199 [binder, in MetaCoq.PCUIC.PCUICNormal]
na:2 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
na:20 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
na:20 [binder, in MetaCoq.Template.WfAst]
na:20 [binder, in MetaCoq.PCUIC.PCUICNormal]
na:200 [binder, in MetaCoq.PCUIC.PCUICConversion]
na:202 [binder, in MetaCoq.Template.Typing]
na:204 [binder, in MetaCoq.PCUIC.PCUICNormal]
na:2042 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
na:2050 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
na:206 [binder, in MetaCoq.Template.Typing]
na:206 [binder, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
na:209 [binder, in MetaCoq.PCUIC.PCUICConversion]
na:209 [binder, in MetaCoq.PCUIC.PCUICCanonicity]
na:21 [binder, in MetaCoq.Erasure.EWcbvEvalInd]
na:210 [binder, in MetaCoq.Erasure.EArities]
na:211 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
na:214 [binder, in MetaCoq.PCUIC.PCUICNormal]
na:214 [binder, in MetaCoq.PCUIC.PCUICReduction]
na:215 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
na:218 [binder, in MetaCoq.PCUIC.PCUICConversion]
na:219 [binder, in MetaCoq.PCUIC.PCUICReduction]
na:22 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
na:22 [binder, in MetaCoq.Template.BasicAst]
na:22 [binder, in MetaCoq.PCUIC.PCUICEtaExpand]
na:22 [binder, in MetaCoq.SafeChecker.PCUICWfReduction]
na:222 [binder, in MetaCoq.Erasure.EEtaExpanded]
na:223 [binder, in MetaCoq.PCUIC.PCUICNormal]
na:224 [binder, in MetaCoq.Erasure.EEtaExpanded]
na:224 [binder, in MetaCoq.PCUIC.PCUICReduction]
na:226 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
na:228 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
na:23 [binder, in MetaCoq.PCUIC.PCUICArities]
na:23 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
na:23 [binder, in MetaCoq.PCUIC.PCUICNormal]
na:230 [binder, in MetaCoq.PCUIC.PCUICReduction]
na:236 [binder, in MetaCoq.PCUIC.PCUICReduction]
na:238 [binder, in MetaCoq.PCUIC.PCUICConversion]
na:24 [binder, in MetaCoq.SafeChecker.PCUICErrors]
na:24 [binder, in MetaCoq.Erasure.EWcbvEval]
na:247 [binder, in MetaCoq.Template.Typing]
na:247 [binder, in MetaCoq.PCUIC.PCUICConversion]
na:248 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
na:25 [binder, in MetaCoq.PCUIC.PCUICEtaExpand]
na:25 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
na:251 [binder, in MetaCoq.PCUIC.PCUICConversion]
na:253 [binder, in MetaCoq.Template.Typing]
na:256 [binder, in MetaCoq.PCUIC.PCUICConversion]
na:257 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
na:257 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
na:26 [binder, in MetaCoq.PCUIC.PCUICProgress]
na:26 [binder, in MetaCoq.Erasure.EPretty]
na:26 [binder, in MetaCoq.SafeChecker.PCUICWfReduction]
na:262 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
na:262 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
na:263 [binder, in MetaCoq.PCUIC.PCUICConversion]
na:265 [binder, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
na:267 [binder, in MetaCoq.Template.EnvironmentTyping]
na:269 [binder, in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
na:269 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
na:27 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
na:27 [binder, in MetaCoq.Erasure.Extract]
na:270 [binder, in MetaCoq.PCUIC.PCUICConversion]
na:273 [binder, in MetaCoq.Template.EnvironmentTyping]
na:277 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
na:28 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
na:28 [binder, in MetaCoq.Template.Pretty]
na:280 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
na:280 [binder, in MetaCoq.PCUIC.PCUICReduction]
na:283 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
na:283 [binder, in MetaCoq.PCUIC.PCUICConversion]
na:284 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
na:285 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
na:285 [binder, in MetaCoq.PCUIC.PCUICReduction]
na:288 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
na:289 [binder, in MetaCoq.PCUIC.PCUICConversion]
na:29 [binder, in MetaCoq.Erasure.EWcbvEval]
na:29 [binder, in MetaCoq.PCUIC.utils.PCUICPretty]
na:3 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
na:3 [binder, in MetaCoq.PCUIC.Syntax.PCUICNamelessDef]
na:302 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
na:305 [binder, in MetaCoq.Template.Typing]
na:308 [binder, in MetaCoq.Template.EnvironmentTyping]
na:309 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
na:31 [binder, in MetaCoq.Erasure.Extract]
na:310 [binder, in MetaCoq.Template.Typing]
na:312 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
na:313 [binder, in MetaCoq.Template.EnvironmentTyping]
na:315 [binder, in MetaCoq.Template.Typing]
na:318 [binder, in MetaCoq.Template.Environment]
na:32 [binder, in MetaCoq.PCUIC.Syntax.PCUICViews]
na:32 [binder, in MetaCoq.Erasure.Prelim]
na:320 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
na:320 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
na:321 [binder, in MetaCoq.Template.Typing]
na:321 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
na:321 [binder, in MetaCoq.Template.Environment]
na:325 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
na:326 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
na:327 [binder, in MetaCoq.Template.Typing]
na:329 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
na:329 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
na:329 [binder, in MetaCoq.Template.Environment]
na:33 [binder, in MetaCoq.SafeChecker.PCUICErrors]
na:330 [binder, in MetaCoq.PCUIC.PCUICConversion]
na:331 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
na:333 [binder, in MetaCoq.Template.Environment]
na:336 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
na:337 [binder, in MetaCoq.PCUIC.PCUICConversion]
na:338 [binder, in MetaCoq.PCUIC.PCUICReduction]
na:34 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
na:34 [binder, in MetaCoq.PCUIC.utils.PCUICPretty]
na:341 [binder, in MetaCoq.PCUIC.PCUICSR]
na:341 [binder, in MetaCoq.PCUIC.PCUICReduction]
na:341 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
na:343 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
na:346 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
na:346 [binder, in MetaCoq.PCUIC.PCUICSR]
na:348 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
na:348 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
na:350 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
na:352 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
na:353 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
na:357 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
na:36 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
na:36 [binder, in MetaCoq.Template.Pretty]
na:360 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
na:364 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
na:365 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
na:369 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
na:370 [binder, in MetaCoq.PCUIC.PCUICSpine]
na:373 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
na:373 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
na:373 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
na:373 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
na:376 [binder, in MetaCoq.PCUIC.PCUICSpine]
na:378 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
na:379 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
na:38 [binder, in MetaCoq.PCUIC.PCUICInversion]
na:381 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
na:385 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
na:387 [binder, in MetaCoq.Template.Typing]
na:389 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
na:39 [binder, in MetaCoq.Translations.times_bool_fun]
na:390 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
na:391 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
na:392 [binder, in MetaCoq.Template.Typing]
na:392 [binder, in MetaCoq.PCUIC.PCUICNormal]
na:393 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
na:394 [binder, in MetaCoq.PCUIC.PCUICSR]
na:395 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
na:395 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
na:396 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
na:397 [binder, in MetaCoq.PCUIC.PCUICNormal]
na:397 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
na:399 [binder, in MetaCoq.PCUIC.PCUICSR]
na:40 [binder, in MetaCoq.Erasure.ErasureFunction]
na:400 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
na:403 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
na:404 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
na:404 [binder, in MetaCoq.PCUIC.PCUICSR]
na:407 [binder, in MetaCoq.PCUIC.PCUICConversion]
na:408 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
na:41 [binder, in MetaCoq.Template.Typing]
na:41 [binder, in MetaCoq.PCUIC.PCUICNormal]
na:410 [binder, in MetaCoq.Template.EnvironmentTyping]
na:410 [binder, in MetaCoq.PCUIC.PCUICSR]
na:416 [binder, in MetaCoq.Template.EnvironmentTyping]
na:416 [binder, in MetaCoq.PCUIC.PCUICSR]
na:417 [binder, in MetaCoq.PCUIC.PCUICConversion]
na:42 [binder, in MetaCoq.PCUIC.Syntax.PCUICViews]
na:42 [binder, in MetaCoq.PCUIC.TemplateToPCUIC]
na:42 [binder, in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
na:420 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
na:421 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
na:423 [binder, in MetaCoq.PCUIC.PCUICConversion]
na:425 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
na:43 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
na:43 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
na:43 [binder, in MetaCoq.Template.Pretty]
na:431 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
na:437 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
na:437 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
na:438 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
na:439 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
na:439 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
na:44 [binder, in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
na:445 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
na:446 [binder, in MetaCoq.PCUIC.PCUICInductives]
na:447 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
na:45 [binder, in MetaCoq.PCUIC.PCUICInversion]
na:45 [binder, in MetaCoq.Template.Reflect]
na:450 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
na:450 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
na:453 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
na:455 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
na:457 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
na:458 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
na:46 [binder, in MetaCoq.Translations.times_bool_fun]
na:460 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
na:460 [binder, in MetaCoq.PCUIC.PCUICSR]
na:464 [binder, in MetaCoq.PCUIC.PCUICConversion]
na:465 [binder, in MetaCoq.PCUIC.PCUICSR]
na:466 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
na:47 [binder, in MetaCoq.PCUIC.PCUICNormal]
na:47 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
na:471 [binder, in MetaCoq.PCUIC.PCUICConversion]
na:48 [binder, in MetaCoq.Template.Normal]
na:481 [binder, in MetaCoq.Template.EnvironmentTyping]
na:483 [binder, in MetaCoq.PCUIC.PCUICSpine]
na:485 [binder, in MetaCoq.Template.EnvironmentTyping]
na:487 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
na:49 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
na:49 [binder, in MetaCoq.Template.TermEquality]
na:491 [binder, in MetaCoq.PCUIC.PCUICInductives]
na:494 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
na:495 [binder, in MetaCoq.Template.EnvironmentTyping]
na:497 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
na:499 [binder, in MetaCoq.Template.EnvironmentTyping]
na:5 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
na:5 [binder, in MetaCoq.PCUIC.PCUICContextReduction]
na:5 [binder, in MetaCoq.PCUIC.PCUICReduction]
na:50 [binder, in MetaCoq.PCUIC.PCUICArities]
na:50 [binder, in MetaCoq.PCUIC.PCUICReduction]
na:502 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
na:507 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
na:51 [binder, in MetaCoq.Template.Normal]
na:51 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
na:51 [binder, in MetaCoq.Template.WcbvEval]
na:510 [binder, in MetaCoq.PCUIC.PCUICTyping]
na:511 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
na:517 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
na:517 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
na:52 [binder, in MetaCoq.Template.Typing]
na:52 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
na:52 [binder, in MetaCoq.PCUIC.PCUICEquality]
na:523 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
na:524 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
na:53 [binder, in MetaCoq.Template.TermEquality]
na:530 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
na:533 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
na:537 [binder, in MetaCoq.PCUIC.PCUICSpine]
na:539 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
na:54 [binder, in MetaCoq.PCUIC.PCUICReduction]
na:544 [binder, in MetaCoq.PCUIC.PCUICSpine]
na:548 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
na:55 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
na:55 [binder, in MetaCoq.PCUIC.PCUICInversion]
na:56 [binder, in MetaCoq.PCUIC.PCUICEquality]
na:573 [binder, in MetaCoq.PCUIC.PCUICSpine]
na:58 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
na:58 [binder, in MetaCoq.Template.WcbvEval]
na:58 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
na:58 [binder, in MetaCoq.PCUIC.PCUICReduction]
na:587 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
na:59 [binder, in MetaCoq.PCUIC.utils.PCUICOnOne]
na:59 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
na:6 [binder, in MetaCoq.SafeChecker.PCUICWfReduction]
na:6 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
na:6 [binder, in MetaCoq.PCUIC.PCUICContextSubst]
na:6 [binder, in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
na:602 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
na:61 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
na:62 [binder, in MetaCoq.PCUIC.PCUICInversion]
na:63 [binder, in MetaCoq.Template.Environment]
na:63 [binder, in MetaCoq.PCUIC.PCUICReduction]
na:64 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
na:64 [binder, in MetaCoq.PCUIC.utils.PCUICOnOne]
na:64 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
na:64 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
na:655 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
na:658 [binder, in MetaCoq.Erasure.ErasureFunction]
na:66 [binder, in MetaCoq.PCUIC.PCUICFirstorder]
na:66 [binder, in MetaCoq.PCUIC.utils.PCUICPretty]
na:661 [binder, in MetaCoq.Erasure.ErasureFunction]
na:661 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
na:67 [binder, in MetaCoq.PCUIC.PCUICArities]
na:68 [binder, in MetaCoq.PCUIC.PCUICReduction]
na:69 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
na:691 [binder, in MetaCoq.Template.Typing]
na:7 [binder, in MetaCoq.SafeChecker.PCUICErrors]
na:70 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
na:709 [binder, in MetaCoq.PCUIC.PCUICEquality]
na:71 [binder, in MetaCoq.Erasure.EDeps]
na:72 [binder, in MetaCoq.PCUIC.PCUICConversion]
na:72 [binder, in MetaCoq.Erasure.EOptimizePropDiscr]
na:73 [binder, in MetaCoq.PCUIC.PCUICInversion]
na:74 [binder, in MetaCoq.Erasure.EDeps]
na:743 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
na:753 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
na:76 [binder, in MetaCoq.PCUIC.PCUICConversion]
na:783 [binder, in MetaCoq.PCUIC.PCUICConversion]
na:785 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
na:791 [binder, in MetaCoq.PCUIC.PCUICConversion]
na:797 [binder, in MetaCoq.PCUIC.PCUICConversion]
na:8 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
na:80 [binder, in MetaCoq.PCUIC.PCUICConversion]
na:81 [binder, in MetaCoq.PCUIC.PCUICEtaExpand]
na:81 [binder, in MetaCoq.PCUIC.PCUICInversion]
na:81 [binder, in MetaCoq.PCUIC.PCUICFirstorder]
na:83 [binder, in MetaCoq.Template.Typing]
na:833 [binder, in MetaCoq.PCUIC.PCUICConversion]
na:837 [binder, in MetaCoq.PCUIC.PCUICReduction]
na:838 [binder, in MetaCoq.PCUIC.PCUICTyping]
na:84 [binder, in MetaCoq.Erasure.Extract]
na:840 [binder, in MetaCoq.PCUIC.PCUICConversion]
na:85 [binder, in MetaCoq.PCUIC.PCUICEtaExpand]
na:85 [binder, in MetaCoq.PCUIC.PCUICFirstorder]
na:85 [binder, in MetaCoq.PCUIC.Bidirectional.BDUnique]
na:856 [binder, in MetaCoq.PCUIC.PCUICSR]
na:86 [binder, in MetaCoq.PCUIC.PCUICArities]
na:863 [binder, in MetaCoq.PCUIC.PCUICConversion]
na:869 [binder, in MetaCoq.PCUIC.PCUICReduction]
na:88 [binder, in MetaCoq.Template.Typing]
na:887 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
na:888 [binder, in MetaCoq.PCUIC.PCUICSR]
na:89 [binder, in MetaCoq.PCUIC.PCUICElimination]
na:89 [binder, in MetaCoq.PCUIC.PCUICEtaExpand]
na:89 [binder, in MetaCoq.PCUIC.PCUICTyping]
na:899 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
na:9 [binder, in MetaCoq.Template.Normal]
na:9 [binder, in MetaCoq.PCUIC.PCUICAlpha]
na:9 [binder, in MetaCoq.SafeChecker.PCUICWfReduction]
na:9 [binder, in MetaCoq.PCUIC.PCUICReduction]
na:90 [binder, in MetaCoq.Erasure.Extract]
na:919 [binder, in MetaCoq.PCUIC.PCUICConversion]
na:92 [binder, in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
na:92 [binder, in MetaCoq.PCUIC.PCUICElimination]
na:92 [binder, in MetaCoq.PCUIC.PCUICArities]
na:939 [binder, in MetaCoq.Template.Typing]
na:94 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
na:94 [binder, in MetaCoq.PCUIC.PCUICConversion]
na:94 [binder, in MetaCoq.PCUIC.PCUICTyping]
na:96 [binder, in MetaCoq.PCUIC.PCUICAst]
na:97 [binder, in MetaCoq.PCUIC.PCUICArities]
na:98 [binder, in MetaCoq.Template.TermEquality]
na:99 [binder, in MetaCoq.PCUIC.Syntax.PCUICViews]
na:99 [binder, in MetaCoq.PCUIC.PCUICAst]
na:99 [binder, in MetaCoq.PCUIC.PCUICTyping]
na:99 [binder, in MetaCoq.PCUIC.Bidirectional.BDUnique]
na:99 [binder, in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
na:998 [binder, in MetaCoq.PCUIC.PCUICReduction]
Nbar [module, in MetaCoq.Template.utils.wGraph]
Nbar_max_le [lemma, in MetaCoq.Template.common.uGraph]
Nbar_max_spec'' [lemma, in MetaCoq.Template.common.uGraph]
Nbar_max_spec' [lemma, in MetaCoq.Template.common.uGraph]
Nbar_max_spec [lemma, in MetaCoq.Template.common.uGraph]
Nbar.add [definition, in MetaCoq.Template.utils.wGraph]
Nbar.add_max_distr_r [definition, in MetaCoq.Template.utils.wGraph]
Nbar.add_0_l [lemma, in MetaCoq.Template.utils.wGraph]
Nbar.add_0_r [definition, in MetaCoq.Template.utils.wGraph]
Nbar.add_assoc [definition, in MetaCoq.Template.utils.wGraph]
Nbar.add_finite [lemma, in MetaCoq.Template.utils.wGraph]
Nbar.eq_max [lemma, in MetaCoq.Template.utils.wGraph]
Nbar.fold_max_le' [lemma, in MetaCoq.Template.utils.wGraph]
Nbar.fold_max_le [lemma, in MetaCoq.Template.utils.wGraph]
Nbar.fold_max_In [lemma, in MetaCoq.Template.utils.wGraph]
Nbar.le [definition, in MetaCoq.Template.utils.wGraph]
Nbar.le_antisymm [lemma, in MetaCoq.Template.utils.wGraph]
Nbar.le_plus_r [lemma, in MetaCoq.Template.utils.wGraph]
Nbar.le_lt_dec [lemma, in MetaCoq.Template.utils.wGraph]
Nbar.le_dec [lemma, in MetaCoq.Template.utils.wGraph]
Nbar.le_trans [instance, in MetaCoq.Template.utils.wGraph]
Nbar.le_refl [instance, in MetaCoq.Template.utils.wGraph]
Nbar.lt [definition, in MetaCoq.Template.utils.wGraph]
Nbar.max [definition, in MetaCoq.Template.utils.wGraph]
Nbar.max_idempotent [definition, in MetaCoq.Template.utils.wGraph]
Nbar.max_le' [definition, in MetaCoq.Template.utils.wGraph]
Nbar.max_lub [definition, in MetaCoq.Template.utils.wGraph]
Nbar.max_None [lemma, in MetaCoq.Template.utils.wGraph]
Nbar.plus_le_compat [definition, in MetaCoq.Template.utils.wGraph]
Nbar.plus_le_compat_l [definition, in MetaCoq.Template.utils.wGraph]
Nbar.S [definition, in MetaCoq.Template.utils.wGraph]
Nbar.sub [definition, in MetaCoq.Template.utils.wGraph]
Nbar.sub_diag [lemma, in MetaCoq.Template.utils.wGraph]
Nbar.t [definition, in MetaCoq.Template.utils.wGraph]
_ < _ (nbar_scope) [notation, in MetaCoq.Template.utils.wGraph]
_ <= _ (nbar_scope) [notation, in MetaCoq.Template.utils.wGraph]
_ - _ (nbar_scope) [notation, in MetaCoq.Template.utils.wGraph]
_ + _ (nbar_scope) [notation, in MetaCoq.Template.utils.wGraph]
nb:12 [binder, in MetaCoq.Template.Reflect]
nb:20 [binder, in MetaCoq.Template.Reflect]
needed:6 [binder, in MetaCoq.Template.EtaExpand]
negb_is_true [lemma, in MetaCoq.PCUIC.PCUICNormal]
negb_False [lemma, in MetaCoq.PCUIC.PCUICCanonicity]
neg_forall [definition, in MetaCoq.Template.common.uGraph]
neqb [lemma, in MetaCoq.Template.utils.ReflectEq]
neutral [inductive, in MetaCoq.Template.Normal]
neval_to_stuck_fix_app [lemma, in MetaCoq.Erasure.EEtaExpandedFix]
neval_to_stuck_fix [lemma, in MetaCoq.Erasure.EEtaExpandedFix]
new_cstr [definition, in MetaCoq.Examples.add_constructor]
ne_proj [constructor, in MetaCoq.Template.Normal]
ne_case [constructor, in MetaCoq.Template.Normal]
ne_app [constructor, in MetaCoq.Template.Normal]
ne_const [constructor, in MetaCoq.Template.Normal]
ne_evar [constructor, in MetaCoq.Template.Normal]
ne_var [constructor, in MetaCoq.Template.Normal]
ne_rel [constructor, in MetaCoq.Template.Normal]
ne:717 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
nf_cofix [constructor, in MetaCoq.Template.Normal]
nf_fix [constructor, in MetaCoq.Template.Normal]
nf_indapp [constructor, in MetaCoq.Template.Normal]
nf_cstrapp [constructor, in MetaCoq.Template.Normal]
nf_lam [constructor, in MetaCoq.Template.Normal]
nf_prod [constructor, in MetaCoq.Template.Normal]
nf_sort [constructor, in MetaCoq.Template.Normal]
nf_ne [constructor, in MetaCoq.Template.Normal]
nf':113 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
nf':248 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
nf':306 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
nf':308 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
nf':374 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
nf:105 [binder, in MetaCoq.Template.Checker]
nf:112 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
nf:247 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
nf:305 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
nf:307 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
nf:373 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
nil_prefix [lemma, in MetaCoq.Template.utils.MCList]
nisApp_mkApps [lemma, in MetaCoq.PCUIC.utils.PCUICAstUtils]
nisArityHead_mkApps [lemma, in MetaCoq.PCUIC.PCUICWcbvEval]
nisBox_mkApps [lemma, in MetaCoq.Erasure.EAstUtils]
nisErasable_Propositional [lemma, in MetaCoq.Erasure.EArities]
nisFixApp_nisFix [lemma, in MetaCoq.Erasure.EEtaExpandedFix]
nisFix_mkApps [lemma, in MetaCoq.Erasure.EAstUtils]
nisLambda_mkApps [lemma, in MetaCoq.PCUIC.PCUICWcbvEval]
nisLambda_mkApps [lemma, in MetaCoq.Erasure.EAstUtils]
nIs_conv_to_Arity_isWfArity_elim [lemma, in MetaCoq.Erasure.EArities]
nIs_conv_to_Arity_nArity [lemma, in MetaCoq.Erasure.EArities]
ni:1106 [binder, in MetaCoq.Template.utils.All_Forall]
nl [definition, in MetaCoq.Template.utils.MCString]
nl [definition, in MetaCoq.PCUIC.Syntax.PCUICNamelessDef]
nlctx [definition, in MetaCoq.PCUIC.Syntax.PCUICNamelessDef]
nlctx_smash_context [lemma, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nlctx_binders [definition, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nlctx_length [lemma, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nlctx_lift_context [lemma, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nlctx_subst_context [lemma, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nlctx_subst_instance [lemma, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nlctx_fix_context_alt [lemma, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nlctx_app_context [lemma, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nlctx_spec [lemma, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nldecl [abbreviation, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nlg [definition, in MetaCoq.PCUIC.Syntax.PCUICNamelessDef]
nlg_wf_local [lemma, in MetaCoq.PCUIC.Typing.PCUICNamelessTyp]
nlict [definition, in MetaCoq.PCUIC.PCUICAst]
nl_two [lemma, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_is_allowed_elimination [lemma, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_global_ext_levels [lemma, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_global_levels [lemma, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_cumul_ctx [lemma, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_conv_ctx [lemma, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_cumul_decls [lemma, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_conv_decls [lemma, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_cumul [lemma, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_conv [lemma, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_red1 [lemma, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_wf_branches [lemma, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_wf_branch [lemma, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_wf_predicate [lemma, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_forget_types [lemma, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_case_branch_type [lemma, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_case_branch_context [lemma, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_cstr_branch_context [lemma, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_case_predicate_context [lemma, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_inst_case_context [lemma, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_inds [lemma, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_expand_lets_ctx [lemma, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_lift_context [lemma, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_subst_telescope [lemma, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_subst_context [lemma, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_expand_lets [lemma, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_expand_lets_k [lemma, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_extended_subst [lemma, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_it_mkProd_or_LetIn [lemma, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_to_extended_list [lemma, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_declared_constructor [lemma, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_declared_inductive [lemma, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_fix_context [lemma, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_pred_set_pparams [lemma, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_pred_set_preturn [lemma, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_decompose_app [lemma, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_eq_context [lemma, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_eq_decl' [lemma, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_eq_decl [lemma, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_subst [lemma, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_lift [lemma, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_subst_instance [lemma, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_mkApps [lemma, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_it_mkLambda_or_LetIn [lemma, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_decompose_prod_assum [lemma, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_compare_term [lemma, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_eq_term [lemma, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_leq_term [lemma, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_eq_term_upto_univ [lemma, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_context_assumptions [lemma, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_destArity [lemma, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_lookup_env [lemma, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_spec [lemma, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
nl_wf_cofixpoint [lemma, in MetaCoq.PCUIC.Typing.PCUICNamelessTyp]
nl_check_one_cofix [lemma, in MetaCoq.PCUIC.Typing.PCUICNamelessTyp]
nl_wf_fixpoint [lemma, in MetaCoq.PCUIC.Typing.PCUICNamelessTyp]
nl_check_one_fix [lemma, in MetaCoq.PCUIC.Typing.PCUICNamelessTyp]
nl_global_env [definition, in MetaCoq.PCUIC.Syntax.PCUICNamelessDef]
nl_global_declarations [definition, in MetaCoq.PCUIC.Syntax.PCUICNamelessDef]
nl_global_decl [definition, in MetaCoq.PCUIC.Syntax.PCUICNamelessDef]
nl_mutual_inductive_body [definition, in MetaCoq.PCUIC.Syntax.PCUICNamelessDef]
nl_one_inductive_body [definition, in MetaCoq.PCUIC.Syntax.PCUICNamelessDef]
nl_projection_body [definition, in MetaCoq.PCUIC.Syntax.PCUICNamelessDef]
nl_constructor_body [definition, in MetaCoq.PCUIC.Syntax.PCUICNamelessDef]
nl_constant_body [definition, in MetaCoq.PCUIC.Syntax.PCUICNamelessDef]
nl_branch [definition, in MetaCoq.PCUIC.Syntax.PCUICNamelessDef]
nl_predicate [definition, in MetaCoq.PCUIC.Syntax.PCUICNamelessDef]
nl:20 [binder, in MetaCoq.PCUIC.Syntax.PCUICNamelessDef]
nl:22 [binder, in MetaCoq.PCUIC.Syntax.PCUICNamelessDef]
nm:10 [binder, in MetaCoq.Template.TemplateMonad.Extractable]
nm:13 [binder, in MetaCoq.Template.TemplateMonad.Extractable]
nm:15 [binder, in MetaCoq.Template.TemplateMonad.Extractable]
nm:17 [binder, in MetaCoq.Template.TemplateMonad.Extractable]
nm:18 [binder, in MetaCoq.Template.TemplateMonad.Extractable]
nm:21 [binder, in MetaCoq.Template.TemplateMonad.Extractable]
nm:24 [binder, in MetaCoq.Template.TemplateMonad.Extractable]
nNamed [constructor, in MetaCoq.Template.BasicAst]
nNamed [definition, in MetaCoq.Translations.translation_utils]
nNamed [definition, in MetaCoq.Translations.param_binary]
nnil:15 [binder, in MetaCoq.Erasure.ESpineView]
nnil:42 [binder, in MetaCoq.Erasure.ESpineView]
no [abbreviation, in MetaCoq.SafeChecker.PCUICSafeConversion]
noccur_shift [definition, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
noccur_between [definition, in MetaCoq.Template.Ast]
noccur_between [definition, in MetaCoq.PCUIC.PCUICAst]
nocc_between [definition, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
nocc_betweenp [definition, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
noconf:54 [binder, in MetaCoq.PCUIC.Syntax.PCUICReflect]
nodelta_flags [definition, in MetaCoq.Template.Checker]
nonEmptyLevelExprSet [record, in MetaCoq.Template.Universes]
NonEmptySetFacts [module, in MetaCoq.Template.Universes]
NonEmptySetFacts.add [definition, in MetaCoq.Template.Universes]
NonEmptySetFacts.add_list_spec [lemma, in MetaCoq.Template.Universes]
NonEmptySetFacts.add_list [definition, in MetaCoq.Template.Universes]
NonEmptySetFacts.add_spec [lemma, in MetaCoq.Template.Universes]
NonEmptySetFacts.elements_not_empty [lemma, in MetaCoq.Template.Universes]
NonEmptySetFacts.eq_univ'' [lemma, in MetaCoq.Template.Universes]
NonEmptySetFacts.eq_univ' [lemma, in MetaCoq.Template.Universes]
NonEmptySetFacts.eq_univ [lemma, in MetaCoq.Template.Universes]
NonEmptySetFacts.In_to_nonempty_list_rev [lemma, in MetaCoq.Template.Universes]
NonEmptySetFacts.In_to_nonempty_list [lemma, in MetaCoq.Template.Universes]
NonEmptySetFacts.LevelExprSet_For_all_exprs [lemma, in MetaCoq.Template.Universes]
NonEmptySetFacts.LevelExprSet_for_all_false [lemma, in MetaCoq.Template.Universes]
NonEmptySetFacts.map [definition, in MetaCoq.Template.Universes]
NonEmptySetFacts.map_spec [lemma, in MetaCoq.Template.Universes]
NonEmptySetFacts.non_empty_union [definition, in MetaCoq.Template.Universes]
NonEmptySetFacts.not_Empty_is_empty [lemma, in MetaCoq.Template.Universes]
NonEmptySetFacts.singleton [definition, in MetaCoq.Template.Universes]
NonEmptySetFacts.singleton_to_nonempty_list [lemma, in MetaCoq.Template.Universes]
NonEmptySetFacts.to_nonempty_list_spec' [lemma, in MetaCoq.Template.Universes]
NonEmptySetFacts.to_nonempty_list_spec [lemma, in MetaCoq.Template.Universes]
NonEmptySetFacts.to_nonempty_list [definition, in MetaCoq.Template.Universes]
NonEmptySetFacts.univ_expr_eqb_comm [lemma, in MetaCoq.Template.Universes]
NonEmptySetFacts.univ_expr_eqb_true_iff [lemma, in MetaCoq.Template.Universes]
nonnil:173 [binder, in MetaCoq.Erasure.EInduction]
nonnil:261 [binder, in MetaCoq.Erasure.EInduction]
NonRec [inductive, in MetaCoq.Examples.demo]
normal [inductive, in MetaCoq.Template.Normal]
Normal [section, in MetaCoq.Template.Normal]
Normal [section, in MetaCoq.PCUIC.PCUICNormal]
Normal [library]
normalisation [axiom, in MetaCoq.PCUIC.PCUICSN]
Normalisation [section, in MetaCoq.PCUIC.PCUICSN]
normalisation_upto [lemma, in MetaCoq.PCUIC.PCUICSN]
normalizing_flags [record, in MetaCoq.PCUIC.PCUICSN]
nor_check_univs [projection, in MetaCoq.PCUIC.PCUICSN]
nor:138 [binder, in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
nor:17 [binder, in MetaCoq.SafeChecker.SafeTemplateChecker]
nor:19 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
nor:199 [binder, in MetaCoq.Erasure.ErasureFunction]
nor:21 [binder, in MetaCoq.Erasure.ErasureFunction]
nor:222 [binder, in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
nor:23 [binder, in MetaCoq.SafeChecker.PCUICConsistency]
nor:303 [binder, in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
nor:34 [binder, in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
nor:49 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
nor:54 [binder, in MetaCoq.SafeChecker.PCUICSafeRetyping]
nor:63 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
nor:7 [binder, in MetaCoq.SafeChecker.Extraction]
nor:8 [binder, in MetaCoq.SafeChecker.SafeTemplateChecker]
not [definition, in MetaCoq.Examples.tauto]
NotAnArity [constructor, in MetaCoq.SafeChecker.PCUICErrors]
NotAnInductive [constructor, in MetaCoq.SafeChecker.PCUICErrors]
NotAnInductive [constructor, in MetaCoq.Template.Checker]
NotAProduct [constructor, in MetaCoq.SafeChecker.PCUICErrors]
NotAProduct [constructor, in MetaCoq.Template.Checker]
NotASort [constructor, in MetaCoq.SafeChecker.PCUICErrors]
NotASort [constructor, in MetaCoq.Template.Checker]
NotConvertible [constructor, in MetaCoq.SafeChecker.PCUICErrors]
NotConvertible [constructor, in MetaCoq.Template.Checker]
NotCumulSmaller [constructor, in MetaCoq.SafeChecker.PCUICErrors]
NotEnoughFuel [constructor, in MetaCoq.Translations.translation_utils]
NotEnoughFuel [constructor, in MetaCoq.Template.Checker]
NotFoundConstant [constructor, in MetaCoq.SafeChecker.PCUICErrors]
NotFoundConstants [constructor, in MetaCoq.SafeChecker.PCUICErrors]
NotFunext [definition, in MetaCoq.Translations.times_bool_fun]
notSolvable [constructor, in MetaCoq.Examples.tauto]
NotSolvable [inductive, in MetaCoq.Examples.tauto]
NotSupported [constructor, in MetaCoq.Template.Checker]
not_empty_map [lemma, in MetaCoq.Template.utils.MCList]
not_cofinite:128 [binder, in MetaCoq.PCUIC.PCUICInversion]
not_cofinite:60 [binder, in MetaCoq.PCUIC.PCUICTyping]
not_var_global_ext_levels [lemma, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
not_var_global_levels [lemma, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
no_prop_leq_type [section, in MetaCoq.Template.Universes]
no_prop_leq_type.Hcf' [variable, in MetaCoq.PCUIC.PCUICElimination]
no_prop_leq_type.Hcf [variable, in MetaCoq.PCUIC.PCUICElimination]
no_prop_leq_type [section, in MetaCoq.PCUIC.PCUICElimination]
_ ;;; _ |- _ ~~ _ (type_scope) [notation, in MetaCoq.PCUIC.PCUICCumulProp]
no_prop_leq_type.Hcf' [variable, in MetaCoq.PCUIC.PCUICCumulProp]
no_prop_leq_type.Hcf [variable, in MetaCoq.PCUIC.PCUICCumulProp]
no_prop_leq_type [section, in MetaCoq.PCUIC.PCUICCumulProp]
no:11 [binder, in MetaCoq.PCUIC.PCUICSN]
no:12 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
no:1476 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
no:5 [binder, in MetaCoq.PCUIC.PCUICSN]
no:63 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
no:68 [binder, in MetaCoq.SafeChecker.PCUICWfReduction]
no:98 [binder, in MetaCoq.SafeChecker.PCUICWfReduction]
npars_ass:268 [binder, in MetaCoq.Template.Environment]
npars_ass:262 [binder, in MetaCoq.Template.Environment]
npars_ass:258 [binder, in MetaCoq.Template.Environment]
npars:105 [binder, in MetaCoq.PCUIC.PCUICInductives]
npars:110 [binder, in MetaCoq.PCUIC.PCUICInductives]
npars:113 [binder, in MetaCoq.PCUIC.PCUICInductives]
npars:117 [binder, in MetaCoq.Template.Environment]
npars:122 [binder, in MetaCoq.Template.Environment]
npars:134 [binder, in MetaCoq.Template.Environment]
npars:182 [binder, in MetaCoq.PCUIC.PCUICTyping]
npars:188 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
npars:210 [binder, in MetaCoq.Template.TypingWf]
npars:272 [binder, in MetaCoq.Template.Environment]
npars:277 [binder, in MetaCoq.Template.Environment]
npars:55 [binder, in MetaCoq.PCUIC.PCUICInductives]
npars:697 [binder, in MetaCoq.Template.Typing]
npars:71 [binder, in MetaCoq.Erasure.EPretty]
npars:88 [binder, in MetaCoq.PCUIC.PCUICInductives]
npars:91 [binder, in MetaCoq.PCUIC.PCUICInductives]
npars:95 [binder, in MetaCoq.PCUIC.PCUICInductives]
npars:99 [binder, in MetaCoq.PCUIC.PCUICInductives]
npar:150 [binder, in MetaCoq.Erasure.EGlobalEnv]
npar:175 [binder, in MetaCoq.Template.WcbvEval]
npar:246 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
npar:255 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
npar:263 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
npar:33 [binder, in MetaCoq.Template.Typing]
npar:35 [binder, in MetaCoq.PCUIC.Syntax.PCUICCases]
ns:12 [binder, in MetaCoq.PCUIC.utils.PCUICPretty]
ns:58 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
ns:59 [binder, in MetaCoq.Template.AstUtils]
ns:9 [binder, in MetaCoq.Erasure.EPretty]
ns:9 [binder, in MetaCoq.Template.Pretty]
nth_map' [lemma, in MetaCoq.Template.EtaExpand]
nth_error_smash_context [lemma, in MetaCoq.PCUIC.utils.PCUICAstUtils]
nth_error_ass_subst_context [lemma, in MetaCoq.PCUIC.utils.PCUICAstUtils]
nth_error_map_InP [lemma, in MetaCoq.PCUIC.utils.PCUICAstUtils]
nth_error_removelast [lemma, in MetaCoq.PCUIC.utils.PCUICAstUtils]
nth_error_map_All [lemma, in MetaCoq.Template.utils.All_Forall]
nth_error_alli [lemma, in MetaCoq.Template.utils.All_Forall]
nth_error_all [lemma, in MetaCoq.Template.utils.All_Forall]
nth_error_forall [lemma, in MetaCoq.Template.utils.All_Forall]
nth_error_forallb [lemma, in MetaCoq.Template.utils.All_Forall]
nth_nth_error' [lemma, in MetaCoq.Template.utils.MCList]
nth_nth_error [lemma, in MetaCoq.Template.utils.MCList]
nth_error_unfold_inv [lemma, in MetaCoq.Template.utils.MCList]
nth_error_unfold [lemma, in MetaCoq.Template.utils.MCList]
nth_error_snoc [lemma, in MetaCoq.Template.utils.MCList]
nth_error_rev_inv [lemma, in MetaCoq.Template.utils.MCList]
nth_error_rev [lemma, in MetaCoq.Template.utils.MCList]
nth_error_app_inv [lemma, in MetaCoq.Template.utils.MCList]
nth_error_app_lt [lemma, in MetaCoq.Template.utils.MCList]
nth_error_app_ge [lemma, in MetaCoq.Template.utils.MCList]
nth_error_skipn [lemma, in MetaCoq.Template.utils.MCList]
nth_error_removelast [lemma, in MetaCoq.Template.utils.MCList]
nth_error_skipn_add [lemma, in MetaCoq.Template.utils.MCList]
nth_map' [lemma, in MetaCoq.Template.utils.MCList]
nth_error_nil [lemma, in MetaCoq.Template.utils.MCList]
nth_error_app_left [lemma, in MetaCoq.Template.utils.MCList]
nth_error_spec [lemma, in MetaCoq.Template.utils.MCList]
nth_error_Some' [lemma, in MetaCoq.Template.utils.MCList]
nth_error_Some_non_nil [lemma, in MetaCoq.Template.utils.MCList]
nth_error_Some_length [lemma, in MetaCoq.Template.utils.MCList]
nth_error_mapi [lemma, in MetaCoq.Template.utils.MCList]
nth_error_mapi_rec [lemma, in MetaCoq.Template.utils.MCList]
nth_error_Spec_None [constructor, in MetaCoq.Template.utils.MCList]
nth_error_Spec_Some [constructor, in MetaCoq.Template.utils.MCList]
nth_error_Spec [inductive, in MetaCoq.Template.utils.MCList]
nth_error_map [lemma, in MetaCoq.Template.utils.MCList]
nth_error_safe_nth [lemma, in MetaCoq.Template.utils.MCList]
nth_error_map2 [lemma, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
nth_error_All_local_env_over [lemma, in MetaCoq.Template.Typing]
nth_error_All_local_env [lemma, in MetaCoq.Template.Typing]
nth_error_subst_context [lemma, in MetaCoq.PCUIC.PCUICSubstitution]
nth_error_on_free_vars_ctx [lemma, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
nth_error_projs_inst [lemma, in MetaCoq.PCUIC.PCUICInductives]
nth_errror_arities_context [lemma, in MetaCoq.PCUIC.PCUICInductives]
nth_error_rev_map [lemma, in MetaCoq.PCUIC.PCUICInductives]
nth_error_All_local_env [lemma, in MetaCoq.PCUIC.PCUICValidity]
nth_error_expand_lets [lemma, in MetaCoq.PCUIC.PCUICInductiveInversion]
nth_error_subst_instance [lemma, in MetaCoq.PCUIC.PCUICInductiveInversion]
nth_error_fold_context_k [lemma, in MetaCoq.PCUIC.PCUICParallelReduction]
nth_error_pred1_ctx_all_defs [lemma, in MetaCoq.PCUIC.PCUICParallelReduction]
nth_error_pred1_ctx_l [lemma, in MetaCoq.PCUIC.PCUICParallelReduction]
nth_error_pred1_ctx [lemma, in MetaCoq.PCUIC.PCUICParallelReduction]
nth_error_idsn_eq_Some [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
nth_error_idsn_None [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
nth_error_idsn_Some [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
nth_ren_ids_lt [lemma, in MetaCoq.PCUIC.PCUICSigmaCalculus]
nth_error_closed_context [lemma, in MetaCoq.PCUIC.PCUICInversion]
nth_error_weak_context [lemma, in MetaCoq.PCUIC.PCUICAlpha]
nth_error_inds [lemma, in MetaCoq.PCUIC.PCUICFirstorder]
nth_error_smash_onfvs [lemma, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
nth_error_closed_context_lift [lemma, in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
nth_error_Some_add [lemma, in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
nth_error_closed_context [lemma, in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
nth_error_inst_context [lemma, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
nth_error_list_size [lemma, in MetaCoq.Examples.tauto]
nth_map_option_out [lemma, in MetaCoq.Template.utils.MCOption]
nth_error_All_local_env_over [lemma, in MetaCoq.PCUIC.PCUICTyping]
nth_error_All_local_env [lemma, in MetaCoq.PCUIC.PCUICTyping]
nth_error_size [lemma, in MetaCoq.PCUIC.utils.PCUICSize]
nth_error_All_local_env [lemma, in MetaCoq.PCUIC.PCUICContextConversion]
nth_error_app_context [lemma, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
nth_error_appP [lemma, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
nth_error_app_spec_out [constructor, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
nth_error_app_spec_right [constructor, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
nth_error_app_spec_left [constructor, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
nth_error_app_spec [inductive, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
nth_error_lift_context_eq [lemma, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
nth_error_lift_context [lemma, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
nth_error_rename_context [lemma, in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
nth_error_depth [lemma, in MetaCoq.PCUIC.Syntax.PCUICDepth]
nth_error_fix_subst [lemma, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
nth_error_cofix_subst [lemma, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
nth_error_map_fix [lemma, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
nth_error_assumption_context [lemma, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
nth_error_arities_context [lemma, in MetaCoq.SafeChecker.PCUICSafeChecker]
nth_error_map2 [lemma, in MetaCoq.PCUIC.PCUICReduction]
nth_error_firstn_skipn [lemma, in MetaCoq.PCUIC.PCUICReduction]
nth_error_all_rels_spec [lemma, in MetaCoq.PCUIC.PCUICSpine]
nth:214 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
nth:285 [binder, in MetaCoq.Template.Environment]
nxy:1175 [binder, in MetaCoq.Template.utils.wGraph]
N':1038 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
N':1049 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
n':108 [binder, in MetaCoq.PCUIC.Syntax.PCUICReflect]
n':110 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n':111 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n':125 [binder, in MetaCoq.Template.LiftSubst]
n':126 [binder, in MetaCoq.Template.LiftSubst]
n':1310 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
n':14 [binder, in MetaCoq.Erasure.EReflect]
n':154 [binder, in MetaCoq.Erasure.ELiftSubst]
n':155 [binder, in MetaCoq.Erasure.ELiftSubst]
n':166 [binder, in MetaCoq.Template.utils.wGraph]
n':174 [binder, in MetaCoq.Template.utils.wGraph]
n':23 [binder, in MetaCoq.Erasure.EReflect]
N':252 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
n':281 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
n':29 [binder, in MetaCoq.Template.Universes]
n':332 [binder, in MetaCoq.Template.EtaExpand]
n':35 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
N':377 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
n':405 [binder, in MetaCoq.PCUIC.PCUICEquality]
N':441 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
n':457 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
n':615 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
n':79 [binder, in MetaCoq.Template.Universes]
N':841 [binder, in MetaCoq.PCUIC.PCUICReduction]
N':9 [binder, in MetaCoq.PCUIC.PCUICContextReduction]
n0:10 [binder, in MetaCoq.Template.utils.MCList]
N0:255 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
N0:287 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
N0:32 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
n0:342 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
n0:391 [binder, in MetaCoq.Template.EtaExpand]
n0:431 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
N0:446 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
N0:490 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
n0:62 [binder, in MetaCoq.Template.monad_utils]
N0:847 [binder, in MetaCoq.PCUIC.PCUICReduction]
N0:867 [binder, in MetaCoq.PCUIC.PCUICReduction]
N1:103 [binder, in MetaCoq.PCUIC.PCUICReduction]
N1:105 [binder, in MetaCoq.PCUIC.PCUICConversion]
N1:111 [binder, in MetaCoq.PCUIC.PCUICReduction]
N1:14 [binder, in MetaCoq.Template.Reduction]
N1:19 [binder, in MetaCoq.Template.Reduction]
N1:197 [binder, in MetaCoq.Template.Typing]
N1:205 [binder, in MetaCoq.Template.Typing]
N1:216 [binder, in MetaCoq.Template.Typing]
N1:237 [binder, in MetaCoq.PCUIC.PCUICNormal]
N1:256 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
N1:273 [binder, in MetaCoq.PCUIC.PCUICReduction]
N1:283 [binder, in MetaCoq.PCUIC.PCUICReduction]
N1:288 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
N1:33 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
N1:378 [binder, in MetaCoq.Template.Typing]
N1:390 [binder, in MetaCoq.Template.Typing]
n1:396 [binder, in MetaCoq.Template.EtaExpand]
n1:399 [binder, in MetaCoq.Template.EtaExpand]
N1:4 [binder, in MetaCoq.Template.Reduction]
n1:402 [binder, in MetaCoq.Template.EtaExpand]
N1:406 [binder, in MetaCoq.Template.Typing]
N1:447 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
N1:453 [binder, in MetaCoq.PCUIC.PCUICSR]
N1:463 [binder, in MetaCoq.PCUIC.PCUICSR]
N1:491 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
N1:848 [binder, in MetaCoq.PCUIC.PCUICReduction]
N1:868 [binder, in MetaCoq.PCUIC.PCUICReduction]
N1:9 [binder, in MetaCoq.Template.Reduction]
N1:98 [binder, in MetaCoq.PCUIC.PCUICConversion]
N2:106 [binder, in MetaCoq.PCUIC.PCUICConversion]
N2:106 [binder, in MetaCoq.PCUIC.PCUICReduction]
N2:114 [binder, in MetaCoq.PCUIC.PCUICReduction]
N2:200 [binder, in MetaCoq.Template.Typing]
N2:208 [binder, in MetaCoq.Template.Typing]
N2:219 [binder, in MetaCoq.Template.Typing]
N2:241 [binder, in MetaCoq.PCUIC.PCUICNormal]
N2:25 [binder, in MetaCoq.Template.Reduction]
N2:277 [binder, in MetaCoq.PCUIC.PCUICReduction]
N2:287 [binder, in MetaCoq.PCUIC.PCUICReduction]
N2:382 [binder, in MetaCoq.Template.Typing]
N2:394 [binder, in MetaCoq.Template.Typing]
N2:410 [binder, in MetaCoq.Template.Typing]
N2:457 [binder, in MetaCoq.PCUIC.PCUICSR]
N2:467 [binder, in MetaCoq.PCUIC.PCUICSR]
N2:861 [binder, in MetaCoq.PCUIC.PCUICReduction]
n:1 [binder, in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
n:1 [binder, in MetaCoq.Template.utils.wGraph]
n:1 [binder, in MetaCoq.Examples.tauto]
n:1 [binder, in MetaCoq.Erasure.ELiftSubst]
n:1 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
n:10 [binder, in MetaCoq.Template.utils.MCArith]
n:10 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
n:10 [binder, in MetaCoq.Template.Checker]
n:10 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
n:10 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:10 [binder, in MetaCoq.Template.Induction]
N:100 [binder, in MetaCoq.Erasure.ELiftSubst]
n:100 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
n:1004 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
n:1006 [binder, in MetaCoq.Template.Typing]
n:101 [binder, in MetaCoq.Erasure.EInduction]
n:101 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
n:101 [binder, in MetaCoq.SafeChecker.PCUICWfEnv]
n:101 [binder, in MetaCoq.Translations.param_cheap_packed]
n:101 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
n:101 [binder, in MetaCoq.PCUIC.Syntax.PCUICDepth]
n:101 [binder, in MetaCoq.Template.AstUtils]
n:1010 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
N:1016 [binder, in MetaCoq.PCUIC.PCUICConversion]
n:1016 [binder, in MetaCoq.PCUIC.PCUICTyping]
n:102 [binder, in MetaCoq.PCUIC.PCUICInductives]
n:102 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:102 [binder, in MetaCoq.Erasure.ELiftSubst]
n:102 [binder, in MetaCoq.PCUIC.Syntax.PCUICReflect]
n:102 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:102 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
n:1020 [binder, in MetaCoq.Template.utils.wGraph]
N:1021 [binder, in MetaCoq.PCUIC.PCUICConversion]
n:1022 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
n:1025 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
N:1027 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
n:103 [binder, in MetaCoq.PCUIC.PCUICElimination]
n:103 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
n:103 [binder, in MetaCoq.PCUIC.utils.PCUICOnOne]
n:103 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
N:1037 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
n:104 [binder, in MetaCoq.Erasure.EInduction]
n:104 [binder, in MetaCoq.Erasure.ELiftSubst]
n:104 [binder, in MetaCoq.PCUIC.PCUICContexts]
n:1045 [binder, in MetaCoq.Template.utils.wGraph]
N:1048 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
n:1049 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
n:105 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
n:105 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
N:105 [binder, in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
n:105 [binder, in MetaCoq.PCUIC.PCUICCanonicity]
n:105 [binder, in MetaCoq.PCUIC.Syntax.PCUICDepth]
N:105 [binder, in MetaCoq.Template.LiftSubst]
n:106 [binder, in MetaCoq.PCUIC.PCUICProgress]
n:106 [binder, in MetaCoq.Examples.tauto]
n:106 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
n:106 [binder, in MetaCoq.PCUIC.PCUICContexts]
n:107 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
n:107 [binder, in MetaCoq.Erasure.EWellformed]
n:107 [binder, in MetaCoq.Translations.param_cheap_packed]
n:107 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
n:1072 [binder, in MetaCoq.Template.utils.All_Forall]
n:108 [binder, in MetaCoq.PCUIC.PCUICInductives]
n:108 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
n:108 [binder, in MetaCoq.Template.LiftSubst]
n:1082 [binder, in MetaCoq.Template.utils.All_Forall]
n:1088 [binder, in MetaCoq.Template.Typing]
n:109 [binder, in MetaCoq.Template.WfAst]
n:109 [binder, in MetaCoq.PCUIC.PCUICAlpha]
N:109 [binder, in MetaCoq.Erasure.ELiftSubst]
n:1096 [binder, in MetaCoq.Template.Typing]
n:11 [binder, in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
n:11 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
n:11 [binder, in MetaCoq.Erasure.EDeps]
n:11 [binder, in MetaCoq.PCUIC.PCUICEtaExpand]
n:11 [binder, in MetaCoq.Template.utils.MCArith]
n:11 [binder, in MetaCoq.Erasure.EEtaExpanded]
n:11 [binder, in MetaCoq.Template.LiftSubst]
n:110 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
n:110 [binder, in MetaCoq.Erasure.Extract]
n:110 [binder, in MetaCoq.PCUIC.PCUICFirstorder]
n:110 [binder, in MetaCoq.Erasure.ELiftSubst]
n:110 [binder, in MetaCoq.PCUIC.Syntax.PCUICDepth]
n:111 [binder, in MetaCoq.Template.WfAst]
n:111 [binder, in MetaCoq.PCUIC.utils.PCUICOnOne]
n:111 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
n:112 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
n:112 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:112 [binder, in MetaCoq.Template.Checker]
n:112 [binder, in MetaCoq.PCUIC.PCUICCanonicity]
n:112 [binder, in MetaCoq.Erasure.ERemoveParams]
n:1120 [binder, in MetaCoq.PCUIC.PCUICConfluence]
n:1125 [binder, in MetaCoq.PCUIC.PCUICConfluence]
n:113 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
n:113 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
n:113 [binder, in MetaCoq.PCUIC.PCUICAst]
n:113 [binder, in MetaCoq.Erasure.ERemoveParams]
N:113 [binder, in MetaCoq.Template.LiftSubst]
n:114 [binder, in MetaCoq.Erasure.EInduction]
N:114 [binder, in MetaCoq.Erasure.ELiftSubst]
n:114 [binder, in MetaCoq.PCUIC.Syntax.PCUICDepth]
n:1141 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
n:115 [binder, in MetaCoq.Template.common.uGraph]
n:1151 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
n:1154 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
n:1159 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
n:1159 [binder, in MetaCoq.Template.utils.wGraph]
n:116 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
n:116 [binder, in MetaCoq.PCUIC.PCUICInductives]
n:116 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
n:116 [binder, in MetaCoq.PCUIC.PCUICFirstorder]
n:116 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
N:116 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:116 [binder, in MetaCoq.Template.LiftSubst]
n:117 [binder, in MetaCoq.Erasure.EConstructorsAsBlocks]
N:117 [binder, in MetaCoq.Erasure.ELiftSubst]
n:1171 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
n:1171 [binder, in MetaCoq.PCUIC.PCUICReduction]
n:1175 [binder, in MetaCoq.PCUIC.PCUICConfluence]
n:1179 [binder, in MetaCoq.PCUIC.PCUICConfluence]
n:118 [binder, in MetaCoq.Erasure.ELiftSubst]
n:118 [binder, in MetaCoq.PCUIC.Syntax.PCUICDepth]
n:1184 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
n:1185 [binder, in MetaCoq.PCUIC.PCUICReduction]
n:119 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
n:1190 [binder, in MetaCoq.Erasure.ErasureFunction]
n:12 [binder, in MetaCoq.Translations.param_binary]
n:12 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
n:12 [binder, in MetaCoq.Template.Typing]
n:12 [binder, in MetaCoq.Template.utils.MCArith]
n:12 [binder, in MetaCoq.Erasure.Extract]
n:12 [binder, in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
N:12 [binder, in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
n:12 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
n:12 [binder, in MetaCoq.Examples.add_constructor]
n:120 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
n:120 [binder, in MetaCoq.Erasure.EConstructorsAsBlocks]
n:120 [binder, in MetaCoq.Template.common.uGraph]
n:1206 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
n:1207 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
n:121 [binder, in MetaCoq.PCUIC.PCUICEquality]
n:121 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
N:122 [binder, in MetaCoq.Erasure.ELiftSubst]
n:122 [binder, in MetaCoq.Erasure.Prelim]
n:1223 [binder, in MetaCoq.Template.utils.All_Forall]
n:1224 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
n:123 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
n:123 [binder, in MetaCoq.Erasure.ELiftSubst]
n:1235 [binder, in MetaCoq.Template.utils.All_Forall]
n:1236 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
n:1239 [binder, in MetaCoq.Template.utils.All_Forall]
n:124 [binder, in MetaCoq.Erasure.EGlobalEnv]
n:124 [binder, in MetaCoq.Erasure.ERemoveParams]
n:1252 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
N:1256 [binder, in MetaCoq.PCUIC.PCUICConversion]
n:1257 [binder, in MetaCoq.Template.Typing]
N:1259 [binder, in MetaCoq.PCUIC.PCUICConversion]
n:126 [binder, in MetaCoq.Erasure.EInduction]
N:126 [binder, in MetaCoq.Erasure.ELiftSubst]
n:1261 [binder, in MetaCoq.Template.utils.All_Forall]
N:1262 [binder, in MetaCoq.PCUIC.PCUICConversion]
n:1262 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
N:1265 [binder, in MetaCoq.PCUIC.PCUICConversion]
n:127 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
n:127 [binder, in MetaCoq.Template.WfAst]
n:127 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
n:127 [binder, in MetaCoq.Erasure.ELiftSubst]
n:1271 [binder, in MetaCoq.Template.utils.All_Forall]
n:1274 [binder, in MetaCoq.Template.Typing]
n:1277 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
n:128 [binder, in MetaCoq.PCUIC.PCUICSafeLemmata]
n:128 [binder, in MetaCoq.PCUIC.PCUICNormal]
n:1280 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
n:1283 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
n:1285 [binder, in MetaCoq.Template.utils.All_Forall]
n:1286 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
n:1289 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
n:129 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
n:1290 [binder, in MetaCoq.Template.utils.All_Forall]
n:1292 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
n:1295 [binder, in MetaCoq.Template.utils.All_Forall]
n:1299 [binder, in MetaCoq.Template.Typing]
n:13 [binder, in MetaCoq.Template.utils.MCArith]
n:13 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
n:13 [binder, in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
n:13 [binder, in MetaCoq.Template.utils.wGraph]
n:13 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
n:13 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
n:13 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:13 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
n:13 [binder, in MetaCoq.Template.Induction]
n:130 [binder, in MetaCoq.Erasure.EInduction]
n:1304 [binder, in MetaCoq.Template.Typing]
n:1304 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
n:1306 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
n:1309 [binder, in MetaCoq.Template.utils.All_Forall]
n:1309 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
n:131 [binder, in MetaCoq.Template.WfAst]
n:131 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
n:131 [binder, in MetaCoq.Template.common.uGraph]
n:131 [binder, in MetaCoq.Erasure.EGlobalEnv]
N:131 [binder, in MetaCoq.Template.LiftSubst]
n:1310 [binder, in MetaCoq.Template.utils.All_Forall]
n:1316 [binder, in MetaCoq.Template.utils.All_Forall]
n:1317 [binder, in MetaCoq.Template.utils.All_Forall]
n:132 [binder, in MetaCoq.Erasure.Extract]
n:132 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:1323 [binder, in MetaCoq.Template.utils.All_Forall]
n:1324 [binder, in MetaCoq.Template.utils.All_Forall]
n:1327 [binder, in MetaCoq.Template.Typing]
n:134 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
n:134 [binder, in MetaCoq.PCUIC.Syntax.PCUICDepth]
n:1341 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
n:1344 [binder, in MetaCoq.Template.utils.All_Forall]
n:1345 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
n:1346 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
n:135 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
n:1350 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
n:1352 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
N:136 [binder, in MetaCoq.Template.Typing]
n:136 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
n:137 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
n:137 [binder, in MetaCoq.Template.EnvironmentTyping]
n:137 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
n:137 [binder, in MetaCoq.Template.TypingWf]
n:138 [binder, in MetaCoq.Template.utils.MCList]
N:138 [binder, in MetaCoq.Erasure.ELiftSubst]
n:138 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:1384 [binder, in MetaCoq.Template.utils.All_Forall]
n:1385 [binder, in MetaCoq.Template.utils.All_Forall]
n:139 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
n:139 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
n:139 [binder, in MetaCoq.Erasure.EWellformed]
n:139 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
n:139 [binder, in MetaCoq.Erasure.ERemoveParams]
n:1395 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
n:14 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
n:14 [binder, in MetaCoq.PCUIC.Typing.PCUICInstTyp]
n:14 [binder, in MetaCoq.Translations.param_binary]
n:14 [binder, in MetaCoq.Template.LiftSubst]
N:140 [binder, in MetaCoq.Template.Typing]
n:140 [binder, in MetaCoq.Erasure.ELiftSubst]
n:141 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
n:141 [binder, in MetaCoq.Erasure.Extract]
n:142 [binder, in MetaCoq.Template.utils.MCList]
n:142 [binder, in MetaCoq.Examples.tauto]
n:142 [binder, in MetaCoq.Template.TypingWf]
n:142 [binder, in MetaCoq.PCUIC.PCUICContexts]
n:143 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
n:143 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
n:143 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
N:143 [binder, in MetaCoq.Erasure.ELiftSubst]
n:144 [binder, in MetaCoq.Template.common.uGraph]
n:144 [binder, in MetaCoq.Erasure.ERemoveParams]
n:1449 [binder, in MetaCoq.Template.utils.All_Forall]
n:145 [binder, in MetaCoq.Erasure.EEtaExpanded]
n:145 [binder, in MetaCoq.Template.monad_utils]
n:146 [binder, in MetaCoq.Erasure.ELiftSubst]
n:146 [binder, in MetaCoq.Erasure.EGlobalEnv]
n:146 [binder, in MetaCoq.Erasure.ERemoveParams]
n:146 [binder, in MetaCoq.PCUIC.Syntax.PCUICDepth]
n:146 [binder, in MetaCoq.Template.TypingWf]
n:147 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
n:147 [binder, in MetaCoq.PCUIC.PCUICTyping]
n:147 [binder, in MetaCoq.PCUIC.PCUICCanonicity]
n:148 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
n:148 [binder, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
n:149 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
n:149 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
n:15 [binder, in MetaCoq.PCUIC.PCUICElimination]
n:15 [binder, in MetaCoq.Erasure.EInduction]
n:15 [binder, in MetaCoq.Template.utils.MCArith]
n:15 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
n:15 [binder, in MetaCoq.PCUIC.Conversion.PCUICOnFreeVarsConv]
n:15 [binder, in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
n:15 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
n:15 [binder, in MetaCoq.Erasure.EOptimizePropDiscr]
n:150 [binder, in MetaCoq.Template.Universes]
n:150 [binder, in MetaCoq.PCUIC.PCUICCanonicity]
n:150 [binder, in MetaCoq.Erasure.EEtaExpanded]
n:150 [binder, in MetaCoq.Template.TypingWf]
n:150 [binder, in MetaCoq.Template.LiftSubst]
n:151 [binder, in MetaCoq.Template.EtaExpand]
n:151 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
n:151 [binder, in MetaCoq.PCUIC.Syntax.PCUICDepth]
n:152 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
n:152 [binder, in MetaCoq.Template.monad_utils]
n:153 [binder, in MetaCoq.Template.EtaExpand]
n:153 [binder, in MetaCoq.PCUIC.PCUICTyping]
n:154 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:154 [binder, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
n:155 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
n:1551 [binder, in MetaCoq.Template.utils.All_Forall]
n:1557 [binder, in MetaCoq.Template.utils.All_Forall]
n:156 [binder, in MetaCoq.Erasure.EInlineProjections]
n:156 [binder, in MetaCoq.Erasure.ELiftSubst]
n:156 [binder, in MetaCoq.Template.monad_utils]
n:156 [binder, in MetaCoq.Template.TypingWf]
n:157 [binder, in MetaCoq.Template.utils.All_Forall]
n:157 [binder, in MetaCoq.Erasure.EConstructorsAsBlocks]
n:157 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:158 [binder, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
n:158 [binder, in MetaCoq.Template.LiftSubst]
n:159 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
n:159 [binder, in MetaCoq.Template.WfAst]
N:159 [binder, in MetaCoq.Erasure.ELiftSubst]
n:16 [binder, in MetaCoq.Template.Normal]
n:16 [binder, in MetaCoq.Template.utils.wGraph]
N:16 [binder, in MetaCoq.PCUIC.PCUICConversion]
n:16 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
n:16 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:16 [binder, in MetaCoq.Erasure.EOptimizePropDiscr]
n:16 [binder, in MetaCoq.Template.Induction]
n:160 [binder, in MetaCoq.Template.utils.MCList]
n:160 [binder, in MetaCoq.PCUIC.PCUICInversion]
n:161 [binder, in MetaCoq.Erasure.EInlineProjections]
n:161 [binder, in MetaCoq.Template.Checker]
n:161 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
n:161 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:162 [binder, in MetaCoq.Template.utils.All_Forall]
n:162 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
n:162 [binder, in MetaCoq.Erasure.EConstructorsAsBlocks]
n:162 [binder, in MetaCoq.PCUIC.PCUICFirstorder]
n:162 [binder, in MetaCoq.Template.utils.wGraph]
n:163 [binder, in MetaCoq.PCUIC.PCUICElimination]
n:164 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
n:164 [binder, in MetaCoq.Erasure.EConstructorsAsBlocks]
n:164 [binder, in MetaCoq.SafeChecker.PCUICErrors]
n:164 [binder, in MetaCoq.PCUIC.PCUICAst]
n:165 [binder, in MetaCoq.Erasure.EDeps]
n:165 [binder, in MetaCoq.Erasure.ErasureProperties]
n:165 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
n:165 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:165 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
n:1655 [binder, in MetaCoq.Template.utils.All_Forall]
n:166 [binder, in MetaCoq.Template.monad_utils]
n:1663 [binder, in MetaCoq.Template.utils.All_Forall]
n:167 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
n:1671 [binder, in MetaCoq.Template.utils.All_Forall]
n:1679 [binder, in MetaCoq.Template.utils.All_Forall]
n:168 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
n:169 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
n:169 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
n:169 [binder, in MetaCoq.Erasure.EEtaExpanded]
n:169 [binder, in MetaCoq.Erasure.EOptimizePropDiscr]
n:17 [binder, in MetaCoq.Erasure.EInlineProjections]
n:17 [binder, in MetaCoq.Template.utils.MCArith]
n:17 [binder, in MetaCoq.PCUIC.PCUICFirstorder]
n:17 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
n:17 [binder, in MetaCoq.PCUIC.Syntax.PCUICUnivSubst]
n:170 [binder, in MetaCoq.Template.utils.wGraph]
n:170 [binder, in MetaCoq.Template.monad_utils]
n:170 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
n:170 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:1719 [binder, in MetaCoq.Template.utils.All_Forall]
n:172 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
N:172 [binder, in MetaCoq.PCUIC.PCUICConversion]
n:173 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
n:173 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
n:173 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
n:1739 [binder, in MetaCoq.Template.utils.All_Forall]
n:174 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
n:174 [binder, in MetaCoq.Erasure.ELiftSubst]
n:174 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
n:174 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:174 [binder, in MetaCoq.Erasure.EOptimizePropDiscr]
n:1747 [binder, in MetaCoq.Template.utils.All_Forall]
n:176 [binder, in MetaCoq.Template.utils.All_Forall]
n:176 [binder, in MetaCoq.Erasure.EConstructorsAsBlocks]
n:176 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
n:1763 [binder, in MetaCoq.Template.utils.All_Forall]
n:177 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
n:177 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
N:177 [binder, in MetaCoq.PCUIC.PCUICConversion]
n:1771 [binder, in MetaCoq.Template.utils.All_Forall]
n:178 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
n:178 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:178 [binder, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
n:178 [binder, in MetaCoq.Template.LiftSubst]
n:1786 [binder, in MetaCoq.Template.utils.All_Forall]
n:179 [binder, in MetaCoq.PCUIC.PCUICEtaExpand]
n:179 [binder, in MetaCoq.Template.Ast]
n:179 [binder, in MetaCoq.Examples.tauto]
n:18 [binder, in MetaCoq.Template.EtaExpand]
n:18 [binder, in MetaCoq.Erasure.EPretty]
n:18 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
n:18 [binder, in MetaCoq.Template.utils.MCString]
n:18 [binder, in MetaCoq.Erasure.ESpineView]
n:180 [binder, in MetaCoq.Template.utils.All_Forall]
n:180 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
n:180 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
n:180 [binder, in MetaCoq.PCUIC.PCUICContexts]
n:1805 [binder, in MetaCoq.Template.utils.All_Forall]
n:1813 [binder, in MetaCoq.Template.utils.All_Forall]
n:182 [binder, in MetaCoq.Template.monad_utils]
n:182 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:183 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
n:183 [binder, in MetaCoq.Examples.tauto]
n:184 [binder, in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
n:184 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
n:184 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
n:185 [binder, in MetaCoq.PCUIC.PCUICAlpha]
n:185 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
n:185 [binder, in MetaCoq.Erasure.EEtaExpanded]
n:1855 [binder, in MetaCoq.Template.utils.All_Forall]
n:186 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
N:186 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:188 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
n:188 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
n:188 [binder, in MetaCoq.Template.monad_utils]
n:188 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:189 [binder, in MetaCoq.Erasure.EConstructorsAsBlocks]
n:189 [binder, in MetaCoq.Erasure.Extract]
n:189 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
n:189 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
n:1894 [binder, in MetaCoq.Template.utils.All_Forall]
n:19 [binder, in MetaCoq.Template.Typing]
n:19 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
n:19 [binder, in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
n:19 [binder, in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
n:19 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
n:19 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:19 [binder, in MetaCoq.Erasure.EGenericMapEnv]
n:190 [binder, in MetaCoq.Template.utils.MCList]
n:1901 [binder, in MetaCoq.Template.utils.All_Forall]
n:191 [binder, in MetaCoq.Erasure.EInduction]
n:192 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
n:192 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
n:193 [binder, in MetaCoq.PCUIC.PCUICProgress]
n:193 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
n:193 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
n:193 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:194 [binder, in MetaCoq.Template.utils.MCList]
n:194 [binder, in MetaCoq.Template.monad_utils]
n:1949 [binder, in MetaCoq.Template.utils.All_Forall]
n:195 [binder, in MetaCoq.Erasure.EInduction]
n:195 [binder, in MetaCoq.Erasure.EConstructorsAsBlocks]
n:195 [binder, in MetaCoq.PCUIC.PCUICAlpha]
n:196 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
n:196 [binder, in MetaCoq.SafeChecker.PCUICErrors]
n:1963 [binder, in MetaCoq.Template.utils.All_Forall]
n:1964 [binder, in MetaCoq.Template.utils.All_Forall]
n:197 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
n:197 [binder, in MetaCoq.Template.utils.wGraph]
n:1970 [binder, in MetaCoq.Template.utils.All_Forall]
n:1974 [binder, in MetaCoq.Template.utils.All_Forall]
n:198 [binder, in MetaCoq.Erasure.EInduction]
n:198 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
n:198 [binder, in MetaCoq.PCUIC.Syntax.PCUICDepth]
n:1982 [binder, in MetaCoq.Template.utils.All_Forall]
n:2 [binder, in MetaCoq.Erasure.EInduction]
n:2 [binder, in MetaCoq.PCUIC.PCUICRedTypeIrrelevance]
n:2 [binder, in MetaCoq.Translations.param_binary]
n:2 [binder, in MetaCoq.SafeChecker.PCUICConsistency]
n:2 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
n:2 [binder, in MetaCoq.PCUIC.TemplateToPCUICExpanded]
n:2 [binder, in MetaCoq.PCUIC.PCUICContexts]
n:2 [binder, in MetaCoq.Translations.param_original]
n:2 [binder, in MetaCoq.Template.LiftSubst]
n:2 [binder, in MetaCoq.Template.Induction]
n:20 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
n:20 [binder, in MetaCoq.Template.utils.wGraph]
n:20 [binder, in MetaCoq.Template.Environment]
N:20 [binder, in MetaCoq.Template.UnivSubst]
n:20 [binder, in MetaCoq.Template.Pretty]
N:200 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:200 [binder, in MetaCoq.PCUIC.Syntax.PCUICDepth]
n:2002 [binder, in MetaCoq.Template.utils.All_Forall]
n:201 [binder, in MetaCoq.PCUIC.PCUICProgress]
n:201 [binder, in MetaCoq.Erasure.EInduction]
n:201 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
n:201 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:2014 [binder, in MetaCoq.Template.utils.All_Forall]
n:202 [binder, in MetaCoq.Template.utils.MCList]
n:2022 [binder, in MetaCoq.Template.utils.All_Forall]
n:2026 [binder, in MetaCoq.Template.utils.All_Forall]
n:203 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
n:203 [binder, in MetaCoq.PCUIC.Syntax.PCUICDepth]
n:2032 [binder, in MetaCoq.Template.utils.All_Forall]
n:205 [binder, in MetaCoq.Template.Checker]
n:205 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
n:206 [binder, in MetaCoq.Template.Universes]
n:206 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
n:206 [binder, in MetaCoq.PCUIC.Syntax.PCUICDepth]
n:208 [binder, in MetaCoq.Template.Environment]
n:209 [binder, in MetaCoq.PCUIC.PCUICNormal]
n:209 [binder, in MetaCoq.PCUIC.Syntax.PCUICDepth]
n:21 [binder, in MetaCoq.Template.utils.MCString]
n:21 [binder, in MetaCoq.PCUIC.PCUICInversion]
n:21 [binder, in MetaCoq.PCUIC.utils.PCUICSize]
n:21 [binder, in MetaCoq.PCUIC.TemplateToPCUICExpanded]
n:21 [binder, in MetaCoq.Erasure.EReflect]
n:21 [binder, in MetaCoq.PCUIC.utils.PCUICPretty]
n:210 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
n:211 [binder, in MetaCoq.Erasure.EInduction]
n:211 [binder, in MetaCoq.Template.utils.MCList]
n:211 [binder, in MetaCoq.PCUIC.PCUICAst]
n:211 [binder, in MetaCoq.Erasure.EWcbvEval]
n:213 [binder, in MetaCoq.Erasure.EWcbvEval]
n:2138 [binder, in MetaCoq.Template.utils.All_Forall]
n:214 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:214 [binder, in MetaCoq.Template.Environment]
n:2149 [binder, in MetaCoq.Template.utils.All_Forall]
n:215 [binder, in MetaCoq.Template.utils.MCList]
n:215 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
n:215 [binder, in MetaCoq.Template.Checker]
n:215 [binder, in MetaCoq.PCUIC.PCUICTyping]
n:215 [binder, in MetaCoq.Erasure.EWcbvEval]
n:2158 [binder, in MetaCoq.Template.utils.All_Forall]
n:216 [binder, in MetaCoq.Template.Environment]
N:217 [binder, in MetaCoq.PCUIC.PCUICReduction]
n:2177 [binder, in MetaCoq.Template.utils.All_Forall]
n:218 [binder, in MetaCoq.Erasure.EEtaExpanded]
n:218 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
n:2186 [binder, in MetaCoq.Template.utils.All_Forall]
n:219 [binder, in MetaCoq.Template.Checker]
n:2193 [binder, in MetaCoq.Template.utils.All_Forall]
n:22 [binder, in MetaCoq.Template.utils.MCList]
n:22 [binder, in MetaCoq.Erasure.EInlineProjections]
n:22 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
n:22 [binder, in MetaCoq.Erasure.Extract]
n:22 [binder, in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
n:22 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
n:22 [binder, in MetaCoq.Template.LiftSubst]
n:220 [binder, in MetaCoq.PCUIC.PCUICInductives]
n:220 [binder, in MetaCoq.Template.Ast]
n:220 [binder, in MetaCoq.Template.Environment]
n:2202 [binder, in MetaCoq.Template.utils.All_Forall]
n:221 [binder, in MetaCoq.Template.utils.MCList]
n:221 [binder, in MetaCoq.PCUIC.Syntax.PCUICDepth]
n:2211 [binder, in MetaCoq.Template.utils.All_Forall]
n:2217 [binder, in MetaCoq.Template.utils.All_Forall]
n:222 [binder, in MetaCoq.Erasure.EInduction]
n:222 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
N:222 [binder, in MetaCoq.PCUIC.PCUICReduction]
n:2225 [binder, in MetaCoq.Template.utils.All_Forall]
n:223 [binder, in MetaCoq.Template.Environment]
n:2233 [binder, in MetaCoq.Template.utils.All_Forall]
n:224 [binder, in MetaCoq.PCUIC.PCUICInductives]
N:224 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
n:2243 [binder, in MetaCoq.Template.utils.All_Forall]
n:2247 [binder, in MetaCoq.Template.utils.All_Forall]
n:225 [binder, in MetaCoq.Erasure.EInduction]
n:225 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
n:225 [binder, in MetaCoq.Template.utils.MCList]
n:227 [binder, in MetaCoq.PCUIC.PCUICInductives]
n:227 [binder, in MetaCoq.Template.Checker]
n:228 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:229 [binder, in MetaCoq.Template.utils.MCList]
n:229 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
n:229 [binder, in MetaCoq.PCUIC.PCUICAlpha]
n:229 [binder, in MetaCoq.PCUIC.Syntax.PCUICCases]
n:23 [binder, in MetaCoq.Template.EtaExpand]
n:23 [binder, in MetaCoq.Template.Universes]
n:23 [binder, in MetaCoq.Template.Environment]
N:23 [binder, in MetaCoq.PCUIC.PCUICSpine]
n:230 [binder, in MetaCoq.PCUIC.PCUICProgress]
n:230 [binder, in MetaCoq.PCUIC.PCUICInductives]
n:230 [binder, in MetaCoq.PCUIC.Syntax.PCUICDepth]
n:231 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:232 [binder, in MetaCoq.Template.Universes]
n:232 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
N:232 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
n:232 [binder, in MetaCoq.PCUIC.Syntax.PCUICDepth]
n:233 [binder, in MetaCoq.Template.utils.MCList]
N:233 [binder, in MetaCoq.Template.TypingWf]
n:234 [binder, in MetaCoq.PCUIC.PCUICInductives]
n:234 [binder, in MetaCoq.PCUIC.PCUICAlpha]
n:234 [binder, in MetaCoq.Template.Checker]
n:234 [binder, in MetaCoq.Template.TypingWf]
n:2346 [binder, in MetaCoq.Template.utils.All_Forall]
n:235 [binder, in MetaCoq.Template.common.uGraph]
n:235 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:2351 [binder, in MetaCoq.Template.utils.All_Forall]
n:2356 [binder, in MetaCoq.Template.utils.All_Forall]
n:236 [binder, in MetaCoq.Template.Universes]
n:236 [binder, in MetaCoq.PCUIC.Syntax.PCUICCases]
n:237 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
n:237 [binder, in MetaCoq.Template.utils.MCList]
n:237 [binder, in MetaCoq.PCUIC.PCUICInductives]
n:237 [binder, in MetaCoq.PCUIC.PCUICTyping]
n:237 [binder, in MetaCoq.Erasure.EWcbvEval]
n:238 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
n:24 [binder, in MetaCoq.Erasure.EInduction]
n:24 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
n:24 [binder, in MetaCoq.PCUIC.PCUICInversion]
n:24 [binder, in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
n:24 [binder, in MetaCoq.Template.utils.wGraph]
n:24 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
n:24 [binder, in MetaCoq.Examples.tauto]
n:24 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
n:24 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
n:240 [binder, in MetaCoq.Erasure.EConstructorsAsBlocks]
n:2407 [binder, in MetaCoq.Template.utils.All_Forall]
n:241 [binder, in MetaCoq.PCUIC.PCUICProgress]
n:241 [binder, in MetaCoq.Template.utils.MCList]
n:241 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
n:241 [binder, in MetaCoq.PCUIC.PCUICInductives]
n:241 [binder, in MetaCoq.PCUIC.PCUICSR]
n:241 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
n:2414 [binder, in MetaCoq.Template.utils.All_Forall]
n:242 [binder, in MetaCoq.PCUIC.PCUICAst]
n:242 [binder, in MetaCoq.PCUIC.PCUICSR]
n:244 [binder, in MetaCoq.Template.utils.MCList]
n:244 [binder, in MetaCoq.Erasure.EConstructorsAsBlocks]
n:244 [binder, in MetaCoq.Template.utils.wGraph]
n:245 [binder, in MetaCoq.PCUIC.PCUICInductives]
n:245 [binder, in MetaCoq.PCUIC.Syntax.PCUICCases]
n:245 [binder, in MetaCoq.PCUIC.PCUICSR]
n:246 [binder, in MetaCoq.Template.utils.MCList]
n:247 [binder, in MetaCoq.Template.Universes]
n:247 [binder, in MetaCoq.Erasure.EConstructorsAsBlocks]
n:247 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:247 [binder, in MetaCoq.PCUIC.Syntax.PCUICCases]
n:249 [binder, in MetaCoq.PCUIC.PCUICInductives]
n:249 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
n:25 [binder, in MetaCoq.PCUIC.PCUICElimination]
n:25 [binder, in MetaCoq.Erasure.EArities]
n:25 [binder, in MetaCoq.Template.Typing]
n:25 [binder, in MetaCoq.PCUIC.PCUICCasesContexts]
n:25 [binder, in MetaCoq.PCUIC.PCUICContexts]
n:250 [binder, in MetaCoq.PCUIC.PCUICProgress]
n:250 [binder, in MetaCoq.PCUIC.Syntax.PCUICCases]
N:251 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
n:251 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
n:252 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
n:253 [binder, in MetaCoq.PCUIC.PCUICInductives]
n:253 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
n:254 [binder, in MetaCoq.Template.utils.MCList]
n:254 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
n:254 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:256 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
n:256 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
n:256 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
n:2560 [binder, in MetaCoq.Template.utils.All_Forall]
n:257 [binder, in MetaCoq.PCUIC.PCUICInductives]
n:257 [binder, in MetaCoq.Template.Ast]
n:259 [binder, in MetaCoq.PCUIC.PCUICProgress]
n:259 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
n:26 [binder, in MetaCoq.Template.utils.All_Forall]
n:26 [binder, in MetaCoq.Template.utils.bytestring]
n:26 [binder, in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
n:26 [binder, in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
n:26 [binder, in MetaCoq.Examples.add_constructor]
n:260 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
n:260 [binder, in MetaCoq.PCUIC.PCUICInductives]
n:260 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
n:262 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
n:262 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
n:262 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:263 [binder, in MetaCoq.PCUIC.PCUICInductives]
n:263 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
n:264 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
n:264 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
n:264 [binder, in MetaCoq.Template.TypingWf]
n:265 [binder, in MetaCoq.Template.utils.All_Forall]
n:265 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
n:265 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
n:265 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
N:268 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
n:268 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:269 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
n:269 [binder, in MetaCoq.Erasure.EEtaExpanded]
n:27 [binder, in MetaCoq.Template.Universes]
n:27 [binder, in MetaCoq.Erasure.EInduction]
n:27 [binder, in MetaCoq.Erasure.EArities]
n:27 [binder, in MetaCoq.PCUIC.PCUICNormal]
n:27 [binder, in MetaCoq.Template.Environment]
n:27 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
n:27 [binder, in MetaCoq.Template.LiftSubst]
n:27 [binder, in MetaCoq.Template.Induction]
N:270 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
n:270 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:271 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
n:272 [binder, in MetaCoq.Template.BasicAst]
n:272 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
n:273 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
n:273 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
n:274 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
n:275 [binder, in MetaCoq.Template.utils.All_Forall]
n:275 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
n:276 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
n:276 [binder, in MetaCoq.Erasure.EEtaExpanded]
n:277 [binder, in MetaCoq.Template.BasicAst]
n:277 [binder, in MetaCoq.Template.utils.MCList]
n:277 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
n:277 [binder, in MetaCoq.PCUIC.PCUICInductives]
n:277 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:278 [binder, in MetaCoq.Template.Checker]
n:279 [binder, in MetaCoq.Template.BasicAst]
n:279 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:28 [binder, in MetaCoq.Template.Universes]
n:28 [binder, in MetaCoq.Erasure.EInlineProjections]
n:28 [binder, in MetaCoq.Template.Normal]
n:28 [binder, in MetaCoq.Template.utils.wGraph]
n:28 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:280 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
n:280 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
n:281 [binder, in MetaCoq.Template.BasicAst]
n:281 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
n:282 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:283 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:283 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
n:284 [binder, in MetaCoq.Template.utils.MCList]
N:284 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
n:284 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:285 [binder, in MetaCoq.Template.utils.All_Forall]
n:285 [binder, in MetaCoq.Template.common.uGraph]
n:285 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
n:286 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:288 [binder, in MetaCoq.Template.Ast]
n:288 [binder, in MetaCoq.Template.common.uGraph]
n:288 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
n:288 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:289 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
n:291 [binder, in MetaCoq.Template.utils.MCList]
n:291 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:292 [binder, in MetaCoq.Template.BasicAst]
n:292 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
n:292 [binder, in MetaCoq.Template.common.uGraph]
n:294 [binder, in MetaCoq.Erasure.EArities]
n:294 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
n:294 [binder, in MetaCoq.Template.WcbvEval]
n:294 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:295 [binder, in MetaCoq.Template.common.uGraph]
n:296 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:296 [binder, in MetaCoq.Template.WcbvEval]
n:297 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
n:298 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:3 [binder, in MetaCoq.Erasure.ESpineView]
n:3 [binder, in MetaCoq.Template.Pretty]
n:30 [binder, in MetaCoq.Examples.demo]
n:30 [binder, in MetaCoq.Template.TypingWf]
n:30 [binder, in MetaCoq.Template.AstUtils]
n:300 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
n:300 [binder, in MetaCoq.Erasure.EArities]
n:300 [binder, in MetaCoq.Template.common.uGraph]
n:300 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:300 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
n:302 [binder, in MetaCoq.Template.utils.MCList]
n:302 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:304 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
n:304 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
n:304 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
n:305 [binder, in MetaCoq.Template.common.uGraph]
n:305 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:306 [binder, in MetaCoq.Template.utils.All_Forall]
n:306 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:307 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
n:307 [binder, in MetaCoq.PCUIC.PCUICInductives]
n:307 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:307 [binder, in MetaCoq.Template.WcbvEval]
N:308 [binder, in MetaCoq.Template.Typing]
n:308 [binder, in MetaCoq.Template.common.uGraph]
n:31 [binder, in MetaCoq.Template.utils.MCList]
n:31 [binder, in MetaCoq.PCUIC.PCUICInversion]
n:31 [binder, in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
n:31 [binder, in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
n:31 [binder, in MetaCoq.Erasure.ESpineView]
n:31 [binder, in MetaCoq.Template.Checker]
n:31 [binder, in MetaCoq.PCUIC.Typing.PCUICWeakeningTyp]
n:31 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
n:31 [binder, in MetaCoq.Template.TypingWf]
n:310 [binder, in MetaCoq.Template.BasicAst]
n:310 [binder, in MetaCoq.Template.utils.All_Forall]
n:310 [binder, in MetaCoq.Template.utils.MCList]
n:310 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
n:311 [binder, in MetaCoq.Template.common.uGraph]
n:311 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:312 [binder, in MetaCoq.Template.BasicAst]
n:312 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
n:312 [binder, in MetaCoq.Template.Environment]
N:313 [binder, in MetaCoq.Template.Typing]
n:313 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:313 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
n:314 [binder, in MetaCoq.Template.BasicAst]
n:314 [binder, in MetaCoq.PCUIC.PCUICSR]
n:314 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
n:315 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
n:315 [binder, in MetaCoq.Erasure.ERemoveParams]
n:316 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:317 [binder, in MetaCoq.Template.utils.MCList]
n:317 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
n:317 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
n:318 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
n:319 [binder, in MetaCoq.Template.Universes]
n:319 [binder, in MetaCoq.Erasure.ERemoveParams]
n:32 [binder, in MetaCoq.Template.utils.MCList]
n:32 [binder, in MetaCoq.Template.utils.wGraph]
n:32 [binder, in MetaCoq.Template.Environment]
n:32 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
n:321 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
n:321 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
n:321 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
n:322 [binder, in MetaCoq.Template.Universes]
n:322 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
n:323 [binder, in MetaCoq.Template.utils.MCList]
n:323 [binder, in MetaCoq.Erasure.ERemoveParams]
n:324 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
n:324 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
n:325 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
n:325 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
n:326 [binder, in MetaCoq.Template.common.uGraph]
n:326 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
n:327 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
n:33 [binder, in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
n:33 [binder, in MetaCoq.Erasure.ESpineView]
n:33 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
n:33 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
n:33 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:330 [binder, in MetaCoq.Template.EtaExpand]
n:330 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
n:330 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
n:332 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
n:332 [binder, in MetaCoq.Template.utils.MCList]
n:332 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
n:334 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:334 [binder, in MetaCoq.Erasure.EWcbvEval]
n:335 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
n:335 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
n:336 [binder, in MetaCoq.Template.EtaExpand]
n:336 [binder, in MetaCoq.Template.common.uGraph]
n:336 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
n:337 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
n:337 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
n:338 [binder, in MetaCoq.Template.utils.MCList]
n:338 [binder, in MetaCoq.Erasure.EWcbvEval]
n:34 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
n:34 [binder, in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
n:34 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:340 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
n:341 [binder, in MetaCoq.Template.EtaExpand]
n:341 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
n:341 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
n:342 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
n:343 [binder, in MetaCoq.PCUIC.PCUICProgress]
n:344 [binder, in MetaCoq.Template.EtaExpand]
n:344 [binder, in MetaCoq.Template.utils.MCList]
n:344 [binder, in MetaCoq.Template.TypingWf]
n:345 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
n:346 [binder, in MetaCoq.Template.EtaExpand]
n:346 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
n:347 [binder, in MetaCoq.Template.TypingWf]
n:348 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
n:349 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
n:35 [binder, in MetaCoq.PCUIC.PCUICElimination]
n:35 [binder, in MetaCoq.PCUIC.PCUICConvCumInversion]
n:35 [binder, in MetaCoq.Erasure.ELiftSubst]
n:35 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
n:350 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
n:351 [binder, in MetaCoq.PCUIC.PCUICProgress]
n:351 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
n:353 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
n:353 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
n:355 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
n:356 [binder, in MetaCoq.Template.Universes]
n:356 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
n:356 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
n:357 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:358 [binder, in MetaCoq.Template.Universes]
n:358 [binder, in MetaCoq.Template.utils.MCList]
n:358 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
n:358 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
N:358 [binder, in MetaCoq.PCUIC.PCUICReduction]
n:359 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
n:359 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:36 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
n:36 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
n:36 [binder, in MetaCoq.PCUIC.Syntax.PCUICDepth]
n:36 [binder, in MetaCoq.Template.Induction]
n:360 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
n:360 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
n:360 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
n:362 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:363 [binder, in MetaCoq.PCUIC.PCUICNormal]
N:364 [binder, in MetaCoq.PCUIC.PCUICReduction]
n:365 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
n:365 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
n:366 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
n:366 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
n:366 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:367 [binder, in MetaCoq.Template.EtaExpand]
n:367 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
n:367 [binder, in MetaCoq.Erasure.ERemoveParams]
n:369 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
n:37 [binder, in MetaCoq.Erasure.ESubstitution]
n:37 [binder, in MetaCoq.PCUIC.PCUICValidity]
n:37 [binder, in MetaCoq.PCUIC.Conversion.PCUICOnFreeVarsConv]
n:37 [binder, in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
n:37 [binder, in MetaCoq.Template.TypingWf]
n:370 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
n:371 [binder, in MetaCoq.Template.utils.MCList]
n:372 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
n:373 [binder, in MetaCoq.Erasure.EWcbvEval]
n:374 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
n:374 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:374 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
n:374 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
n:375 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
n:375 [binder, in MetaCoq.Erasure.ERemoveParams]
N:376 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
n:377 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:377 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
n:378 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
n:378 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
n:379 [binder, in MetaCoq.Erasure.ERemoveParams]
n:38 [binder, in MetaCoq.Erasure.EInlineProjections]
n:38 [binder, in MetaCoq.Template.utils.bytestring]
n:38 [binder, in MetaCoq.PCUIC.PCUICFirstorder]
n:38 [binder, in MetaCoq.Template.utils.wGraph]
n:38 [binder, in MetaCoq.Erasure.ELiftSubst]
n:38 [binder, in MetaCoq.Template.TypingWf]
n:38 [binder, in MetaCoq.Template.Induction]
n:381 [binder, in MetaCoq.Template.EtaExpand]
n:382 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
n:384 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:385 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
n:386 [binder, in MetaCoq.Template.EtaExpand]
n:389 [binder, in MetaCoq.Template.EtaExpand]
n:389 [binder, in MetaCoq.Template.utils.MCList]
n:389 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
n:39 [binder, in MetaCoq.Translations.translation_utils]
n:39 [binder, in MetaCoq.PCUIC.PCUICEquality]
n:39 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:39 [binder, in MetaCoq.Template.LiftSubst]
n:391 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:392 [binder, in MetaCoq.Erasure.ERemoveParams]
n:393 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
n:393 [binder, in MetaCoq.PCUIC.PCUICSpine]
n:395 [binder, in MetaCoq.PCUIC.PCUICEquality]
n:395 [binder, in MetaCoq.Erasure.EWcbvEval]
n:396 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
N:397 [binder, in MetaCoq.PCUIC.PCUICSR]
n:397 [binder, in MetaCoq.Erasure.ERemoveParams]
n:398 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
n:398 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
n:399 [binder, in MetaCoq.PCUIC.PCUICEquality]
n:4 [binder, in MetaCoq.Erasure.EInduction]
n:4 [binder, in MetaCoq.Erasure.ESpineView]
n:4 [binder, in MetaCoq.Translations.param_cheap_packed]
n:4 [binder, in MetaCoq.PCUIC.PCUICCanonicity]
n:4 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
n:4 [binder, in MetaCoq.Examples.add_constructor]
n:4 [binder, in MetaCoq.Template.Induction]
n:40 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:40 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
n:40 [binder, in MetaCoq.Erasure.ELiftSubst]
n:40 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
n:400 [binder, in MetaCoq.Template.utils.MCList]
n:400 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
n:400 [binder, in MetaCoq.PCUIC.PCUICSpine]
n:402 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
n:402 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
N:402 [binder, in MetaCoq.PCUIC.PCUICSR]
n:403 [binder, in MetaCoq.Template.EtaExpand]
n:403 [binder, in MetaCoq.PCUIC.PCUICNormal]
n:404 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
n:404 [binder, in MetaCoq.PCUIC.PCUICEquality]
n:404 [binder, in MetaCoq.PCUIC.PCUICSpine]
n:408 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
n:409 [binder, in MetaCoq.Template.utils.MCList]
n:41 [binder, in MetaCoq.Translations.translation_utils]
n:41 [binder, in MetaCoq.Template.utils.wGraph]
n:41 [binder, in MetaCoq.Erasure.Prelim]
n:41 [binder, in MetaCoq.Template.Induction]
n:410 [binder, in MetaCoq.PCUIC.PCUICSpine]
n:411 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
n:411 [binder, in MetaCoq.PCUIC.PCUICEquality]
n:411 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:413 [binder, in MetaCoq.PCUIC.PCUICSpine]
n:414 [binder, in MetaCoq.Template.utils.All_Forall]
n:419 [binder, in MetaCoq.PCUIC.PCUICEquality]
n:42 [binder, in MetaCoq.Erasure.EInlineProjections]
n:42 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
n:42 [binder, in MetaCoq.Template.utils.wGraph]
n:420 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
n:420 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:422 [binder, in MetaCoq.Template.utils.MCList]
N:422 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
n:422 [binder, in MetaCoq.PCUIC.PCUICSpine]
n:423 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:423 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
n:424 [binder, in MetaCoq.Template.utils.All_Forall]
n:424 [binder, in MetaCoq.Template.utils.MCList]
n:427 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
n:427 [binder, in MetaCoq.Erasure.ERemoveParams]
n:429 [binder, in MetaCoq.PCUIC.PCUICEquality]
n:429 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
n:43 [binder, in MetaCoq.Template.utils.wGraph]
n:43 [binder, in MetaCoq.Erasure.ESpineView]
n:43 [binder, in MetaCoq.Template.Environment]
n:43 [binder, in MetaCoq.PCUIC.Syntax.PCUICDepth]
n:43 [binder, in MetaCoq.Template.Induction]
n:431 [binder, in MetaCoq.Template.utils.MCList]
n:433 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
n:434 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
n:434 [binder, in MetaCoq.PCUIC.PCUICEquality]
n:435 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
n:436 [binder, in MetaCoq.Template.utils.MCList]
n:437 [binder, in MetaCoq.Template.utils.wGraph]
n:44 [binder, in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
n:44 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
n:44 [binder, in MetaCoq.Erasure.ELiftSubst]
n:44 [binder, in MetaCoq.PCUIC.Syntax.PCUICUnivSubst]
N:440 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
n:441 [binder, in MetaCoq.PCUIC.PCUICEquality]
n:442 [binder, in MetaCoq.Template.utils.MCList]
n:443 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:446 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:446 [binder, in MetaCoq.Template.utils.wGraph]
n:447 [binder, in MetaCoq.Template.utils.MCList]
n:447 [binder, in MetaCoq.PCUIC.PCUICEquality]
N:449 [binder, in MetaCoq.Template.Typing]
n:45 [binder, in MetaCoq.Erasure.Extract]
n:45 [binder, in MetaCoq.PCUIC.PCUICNormal]
n:45 [binder, in MetaCoq.Template.utils.wGraph]
N:45 [binder, in MetaCoq.PCUIC.PCUICConversion]
n:45 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:450 [binder, in MetaCoq.Template.utils.MCList]
n:452 [binder, in MetaCoq.PCUIC.PCUICEquality]
n:452 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:453 [binder, in MetaCoq.Template.utils.MCList]
n:455 [binder, in MetaCoq.Template.utils.All_Forall]
n:456 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
n:456 [binder, in MetaCoq.Template.utils.All_Forall]
n:456 [binder, in MetaCoq.Template.utils.MCList]
n:456 [binder, in MetaCoq.Template.common.uGraph]
n:456 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:4562 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
n:4564 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
n:457 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
n:458 [binder, in MetaCoq.Template.utils.MCList]
N:46 [binder, in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
n:46 [binder, in MetaCoq.Template.utils.wGraph]
n:46 [binder, in MetaCoq.Erasure.ESpineView]
n:46 [binder, in MetaCoq.Template.Environment]
n:461 [binder, in MetaCoq.PCUIC.PCUICEquality]
n:461 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:462 [binder, in MetaCoq.PCUIC.PCUICInductives]
n:463 [binder, in MetaCoq.Template.utils.MCList]
n:464 [binder, in MetaCoq.PCUIC.PCUICInductives]
n:464 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
n:464 [binder, in MetaCoq.Template.utils.wGraph]
n:466 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
n:468 [binder, in MetaCoq.PCUIC.PCUICInductives]
n:468 [binder, in MetaCoq.Template.utils.wGraph]
n:469 [binder, in MetaCoq.PCUIC.PCUICNormal]
n:469 [binder, in MetaCoq.PCUIC.PCUICEquality]
n:469 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
n:47 [binder, in MetaCoq.Template.utils.All_Forall]
n:47 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
n:47 [binder, in MetaCoq.PCUIC.PCUICFirstorder]
n:47 [binder, in MetaCoq.Erasure.ELiftSubst]
n:47 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
n:470 [binder, in MetaCoq.Template.utils.MCList]
n:470 [binder, in MetaCoq.PCUIC.PCUICTyping]
n:471 [binder, in MetaCoq.PCUIC.PCUICNormal]
N:472 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
n:473 [binder, in MetaCoq.Template.EtaExpand]
n:473 [binder, in MetaCoq.Template.utils.MCList]
n:475 [binder, in MetaCoq.PCUIC.PCUICNormal]
n:476 [binder, in MetaCoq.Template.utils.wGraph]
n:477 [binder, in MetaCoq.Template.EtaExpand]
n:477 [binder, in MetaCoq.Template.utils.MCList]
n:477 [binder, in MetaCoq.PCUIC.PCUICSpine]
N:478 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
n:478 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:479 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
n:48 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
n:48 [binder, in MetaCoq.Erasure.ESpineView]
n:48 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:48 [binder, in MetaCoq.Erasure.EOptimizePropDiscr]
n:481 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:481 [binder, in MetaCoq.PCUIC.PCUICTyping]
n:482 [binder, in MetaCoq.Template.utils.All_Forall]
n:484 [binder, in MetaCoq.Template.utils.All_Forall]
N:484 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
n:484 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
n:485 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:485 [binder, in MetaCoq.Template.utils.wGraph]
n:487 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:488 [binder, in MetaCoq.Template.utils.wGraph]
n:49 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
n:49 [binder, in MetaCoq.Template.utils.wGraph]
N:49 [binder, in MetaCoq.PCUIC.PCUICConversion]
n:49 [binder, in MetaCoq.Template.LiftSubst]
n:49 [binder, in MetaCoq.Template.Induction]
n:490 [binder, in MetaCoq.Template.utils.All_Forall]
N:490 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
n:490 [binder, in MetaCoq.Template.utils.wGraph]
n:490 [binder, in MetaCoq.PCUIC.PCUICTyping]
n:491 [binder, in MetaCoq.Template.utils.All_Forall]
n:492 [binder, in MetaCoq.Template.utils.wGraph]
n:494 [binder, in MetaCoq.Examples.tauto]
n:495 [binder, in MetaCoq.Template.Universes]
n:495 [binder, in MetaCoq.Template.utils.All_Forall]
N:496 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
n:496 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:499 [binder, in MetaCoq.PCUIC.PCUICTyping]
n:5 [binder, in MetaCoq.Erasure.EPretty]
n:5 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
n:5 [binder, in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
n:5 [binder, in MetaCoq.Template.utils.wGraph]
n:5 [binder, in MetaCoq.Erasure.ESpineView]
n:5 [binder, in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
n:5 [binder, in MetaCoq.Template.LiftSubst]
n:50 [binder, in MetaCoq.Erasure.ELiftSubst]
n:50 [binder, in MetaCoq.Erasure.Prelim]
n:500 [binder, in MetaCoq.Template.Universes]
n:500 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:502 [binder, in MetaCoq.Template.EnvironmentTyping]
n:502 [binder, in MetaCoq.PCUIC.PCUICInductives]
n:504 [binder, in MetaCoq.Template.utils.MCList]
n:504 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
n:505 [binder, in MetaCoq.Template.EnvironmentTyping]
n:505 [binder, in MetaCoq.PCUIC.PCUICSpine]
n:506 [binder, in MetaCoq.Template.Universes]
n:506 [binder, in MetaCoq.Template.utils.MCList]
n:506 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
n:507 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
n:507 [binder, in MetaCoq.Template.EnvironmentTyping]
n:51 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
n:51 [binder, in MetaCoq.PCUIC.PCUICContextSubst]
n:510 [binder, in MetaCoq.Template.utils.MCList]
n:510 [binder, in MetaCoq.Template.EnvironmentTyping]
n:514 [binder, in MetaCoq.Template.EnvironmentTyping]
n:514 [binder, in MetaCoq.PCUIC.PCUICInductives]
n:515 [binder, in MetaCoq.Examples.tauto]
n:518 [binder, in MetaCoq.Examples.tauto]
n:52 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
n:52 [binder, in MetaCoq.Template.utils.wGraph]
n:52 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
n:52 [binder, in MetaCoq.PCUIC.PCUICSR]
N:52 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:52 [binder, in MetaCoq.Erasure.EOptimizePropDiscr]
n:52 [binder, in MetaCoq.Erasure.Prelim]
n:52 [binder, in MetaCoq.Template.Induction]
n:521 [binder, in MetaCoq.Template.utils.All_Forall]
N:525 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
n:526 [binder, in MetaCoq.Template.utils.MCList]
n:529 [binder, in MetaCoq.PCUIC.PCUICAst]
n:53 [binder, in MetaCoq.PCUIC.PCUICPrincipality]
n:53 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
N:53 [binder, in MetaCoq.PCUIC.PCUICReduction]
n:530 [binder, in MetaCoq.Template.utils.wGraph]
N:531 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
n:537 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
n:538 [binder, in MetaCoq.Template.EtaExpand]
n:54 [binder, in MetaCoq.Template.utils.All_Forall]
n:54 [binder, in MetaCoq.Erasure.EOptimizePropDiscr]
N:540 [binder, in MetaCoq.PCUIC.PCUICSpine]
n:541 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
n:542 [binder, in MetaCoq.Template.utils.All_Forall]
n:545 [binder, in MetaCoq.Template.utils.All_Forall]
n:545 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
N:547 [binder, in MetaCoq.PCUIC.PCUICSpine]
n:55 [binder, in MetaCoq.Template.utils.MCList]
n:55 [binder, in MetaCoq.Template.Normal]
N:55 [binder, in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
n:55 [binder, in MetaCoq.Template.utils.wGraph]
n:55 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
N:55 [binder, in MetaCoq.PCUIC.PCUICConversion]
n:55 [binder, in MetaCoq.PCUIC.PCUICContextReduction]
n:55 [binder, in MetaCoq.Template.Induction]
n:550 [binder, in MetaCoq.Template.utils.wGraph]
n:552 [binder, in MetaCoq.Template.utils.All_Forall]
n:555 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
n:557 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
n:558 [binder, in MetaCoq.Template.utils.All_Forall]
n:559 [binder, in MetaCoq.Template.Universes]
n:559 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
N:56 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:56 [binder, in MetaCoq.Erasure.EWcbvEval]
n:560 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
n:561 [binder, in MetaCoq.Template.Universes]
n:562 [binder, in MetaCoq.Template.utils.wGraph]
n:563 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
n:563 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
n:563 [binder, in MetaCoq.Template.utils.wGraph]
n:567 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
N:57 [binder, in MetaCoq.Template.LiftSubst]
N:57 [binder, in MetaCoq.PCUIC.PCUICReduction]
n:57 [binder, in MetaCoq.Erasure.Prelim]
n:571 [binder, in MetaCoq.Template.common.uGraph]
n:572 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
n:573 [binder, in MetaCoq.Template.utils.wGraph]
n:574 [binder, in MetaCoq.Template.common.uGraph]
n:576 [binder, in MetaCoq.Template.common.uGraph]
n:578 [binder, in MetaCoq.Template.common.uGraph]
n:579 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:58 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
n:58 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
n:58 [binder, in MetaCoq.Template.utils.wGraph]
n:58 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:58 [binder, in MetaCoq.Template.LiftSubst]
n:581 [binder, in MetaCoq.PCUIC.PCUICSpine]
n:582 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:583 [binder, in MetaCoq.Template.common.uGraph]
n:585 [binder, in MetaCoq.PCUIC.PCUICTyping]
n:586 [binder, in MetaCoq.PCUIC.PCUICInductives]
n:586 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:588 [binder, in MetaCoq.Template.common.uGraph]
n:588 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:588 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
n:589 [binder, in MetaCoq.Template.utils.wGraph]
n:59 [binder, in MetaCoq.Erasure.Extract]
n:59 [binder, in MetaCoq.Template.TypingWf]
n:59 [binder, in MetaCoq.PCUIC.PCUICSpine]
n:591 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
n:591 [binder, in MetaCoq.Template.utils.wGraph]
n:591 [binder, in MetaCoq.PCUIC.PCUICConfluence]
n:592 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:593 [binder, in MetaCoq.PCUIC.PCUICTyping]
n:599 [binder, in MetaCoq.Template.utils.MCList]
n:599 [binder, in MetaCoq.PCUIC.PCUICInductives]
n:599 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
n:6 [binder, in MetaCoq.Erasure.EInduction]
n:6 [binder, in MetaCoq.Template.WfAst]
n:6 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
n:6 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
n:6 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:6 [binder, in MetaCoq.SafeChecker.PCUICConsistency]
n:6 [binder, in MetaCoq.PCUIC.utils.PCUICPretty]
n:60 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
n:60 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:600 [binder, in MetaCoq.PCUIC.PCUICSpine]
n:601 [binder, in MetaCoq.Template.utils.wGraph]
n:602 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
n:603 [binder, in MetaCoq.PCUIC.PCUICConfluence]
n:605 [binder, in MetaCoq.Template.Typing]
n:607 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
n:61 [binder, in MetaCoq.Template.utils.All_Forall]
N:61 [binder, in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
N:61 [binder, in MetaCoq.PCUIC.PCUICConversion]
n:61 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
n:61 [binder, in MetaCoq.Template.TypingWf]
n:61 [binder, in MetaCoq.Template.AstUtils]
n:61 [binder, in MetaCoq.Erasure.Prelim]
n:610 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
n:610 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
n:611 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
n:612 [binder, in MetaCoq.Template.Typing]
n:613 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
n:613 [binder, in MetaCoq.PCUIC.PCUICConfluence]
n:614 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
n:615 [binder, in MetaCoq.PCUIC.PCUICConfluence]
n:616 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
n:617 [binder, in MetaCoq.Template.Typing]
n:617 [binder, in MetaCoq.PCUIC.PCUICConfluence]
n:619 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
n:619 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
n:619 [binder, in MetaCoq.PCUIC.PCUICConfluence]
n:62 [binder, in MetaCoq.Erasure.EInlineProjections]
n:62 [binder, in MetaCoq.Template.utils.wGraph]
n:62 [binder, in MetaCoq.Erasure.EWcbvEvalInd]
n:62 [binder, in MetaCoq.PCUIC.Typing.PCUICWeakeningTyp]
N:62 [binder, in MetaCoq.Template.LiftSubst]
n:621 [binder, in MetaCoq.PCUIC.PCUICEquality]
n:621 [binder, in MetaCoq.PCUIC.PCUICConfluence]
n:622 [binder, in MetaCoq.Template.Typing]
n:623 [binder, in MetaCoq.PCUIC.PCUICConfluence]
n:625 [binder, in MetaCoq.PCUIC.PCUICConfluence]
n:626 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
n:627 [binder, in MetaCoq.PCUIC.PCUICConfluence]
n:629 [binder, in MetaCoq.PCUIC.PCUICConfluence]
n:63 [binder, in MetaCoq.PCUIC.PCUICInductives]
n:63 [binder, in MetaCoq.Template.utils.wGraph]
n:63 [binder, in MetaCoq.PCUIC.PCUICSpine]
n:63 [binder, in MetaCoq.Erasure.Prelim]
n:631 [binder, in MetaCoq.PCUIC.PCUICConfluence]
N:633 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
n:634 [binder, in MetaCoq.PCUIC.PCUICEquality]
n:634 [binder, in MetaCoq.PCUIC.PCUICConversion]
n:634 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
N:637 [binder, in MetaCoq.PCUIC.PCUICSR]
n:64 [binder, in MetaCoq.Template.EtaExpand]
n:64 [binder, in MetaCoq.Erasure.Extract]
N:64 [binder, in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
n:64 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
n:640 [binder, in MetaCoq.Template.utils.wGraph]
n:641 [binder, in MetaCoq.Template.utils.MCList]
n:641 [binder, in MetaCoq.PCUIC.PCUICConfluence]
N:642 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
n:645 [binder, in MetaCoq.Template.utils.MCList]
n:649 [binder, in MetaCoq.Template.utils.MCList]
n:65 [binder, in MetaCoq.Erasure.EArities]
n:65 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
N:65 [binder, in MetaCoq.PCUIC.PCUICConversion]
N:65 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:65 [binder, in MetaCoq.Template.LiftSubst]
n:650 [binder, in MetaCoq.PCUIC.PCUICSpine]
N:651 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
n:653 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
n:656 [binder, in MetaCoq.Template.utils.MCList]
n:66 [binder, in MetaCoq.Erasure.EDeps]
n:66 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:66 [binder, in MetaCoq.Template.Induction]
n:663 [binder, in MetaCoq.PCUIC.PCUICSR]
n:664 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
n:664 [binder, in MetaCoq.PCUIC.PCUICSpine]
n:67 [binder, in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
n:67 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
n:67 [binder, in MetaCoq.Template.Normal]
n:67 [binder, in MetaCoq.Template.utils.wGraph]
n:67 [binder, in MetaCoq.Erasure.EWellformed]
n:67 [binder, in MetaCoq.Template.TypingWf]
n:67 [binder, in MetaCoq.Template.LiftSubst]
n:671 [binder, in MetaCoq.PCUIC.PCUICSpine]
n:673 [binder, in MetaCoq.Template.utils.MCList]
n:673 [binder, in MetaCoq.Template.Typing]
n:679 [binder, in MetaCoq.Template.Typing]
n:68 [binder, in MetaCoq.Template.utils.All_Forall]
N:68 [binder, in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
n:68 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
n:68 [binder, in MetaCoq.Erasure.EAstUtils]
n:68 [binder, in MetaCoq.Template.TypingWf]
n:68 [binder, in MetaCoq.Erasure.Prelim]
n:680 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
n:684 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
n:686 [binder, in MetaCoq.Template.utils.All_Forall]
n:686 [binder, in MetaCoq.Template.utils.MCList]
n:688 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
n:688 [binder, in MetaCoq.PCUIC.PCUICSpine]
n:69 [binder, in MetaCoq.Examples.tauto]
n:69 [binder, in MetaCoq.Erasure.ELiftSubst]
n:690 [binder, in MetaCoq.Template.utils.wGraph]
n:691 [binder, in MetaCoq.Template.utils.MCList]
n:691 [binder, in MetaCoq.PCUIC.PCUICSpine]
n:693 [binder, in MetaCoq.Template.utils.All_Forall]
N:693 [binder, in MetaCoq.PCUIC.PCUICConfluence]
n:693 [binder, in MetaCoq.PCUIC.PCUICSR]
n:695 [binder, in MetaCoq.Template.utils.MCList]
n:697 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
N:698 [binder, in MetaCoq.PCUIC.PCUICConfluence]
n:7 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
n:7 [binder, in MetaCoq.PCUIC.Conversion.PCUICOnFreeVarsConv]
n:7 [binder, in MetaCoq.Erasure.ESpineView]
n:7 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
n:7 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:7 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
n:70 [binder, in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
n:70 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
n:70 [binder, in MetaCoq.PCUIC.PCUICEtaExpand]
n:70 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
n:70 [binder, in MetaCoq.PCUIC.Typing.PCUICWeakeningTyp]
N:70 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:70 [binder, in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
n:70 [binder, in MetaCoq.Template.LiftSubst]
N:700 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
n:702 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
n:704 [binder, in MetaCoq.Template.utils.MCList]
N:705 [binder, in MetaCoq.PCUIC.PCUICConfluence]
n:707 [binder, in MetaCoq.Template.utils.wGraph]
N:709 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
n:709 [binder, in MetaCoq.Template.utils.wGraph]
N:709 [binder, in MetaCoq.PCUIC.PCUICConfluence]
n:71 [binder, in MetaCoq.Template.WfAst]
n:71 [binder, in MetaCoq.Template.utils.wGraph]
n:71 [binder, in MetaCoq.PCUIC.PCUICConversion]
n:71 [binder, in MetaCoq.Erasure.EGenericMapEnv]
N:715 [binder, in MetaCoq.PCUIC.PCUICConfluence]
N:717 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
n:72 [binder, in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
n:72 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
N:72 [binder, in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
n:721 [binder, in MetaCoq.PCUIC.PCUICEquality]
N:723 [binder, in MetaCoq.PCUIC.PCUICConfluence]
N:727 [binder, in MetaCoq.PCUIC.PCUICConfluence]
n:73 [binder, in MetaCoq.Template.WfAst]
n:73 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
n:73 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
n:73 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
n:73 [binder, in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
N:73 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:732 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
N:733 [binder, in MetaCoq.PCUIC.PCUICConfluence]
n:733 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
n:74 [binder, in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
n:74 [binder, in MetaCoq.Template.utils.All_Forall]
N:74 [binder, in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
n:74 [binder, in MetaCoq.PCUIC.PCUICInductives]
n:74 [binder, in MetaCoq.Erasure.ELiftSubst]
n:74 [binder, in MetaCoq.PCUIC.PCUICSR]
n:74 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:741 [binder, in MetaCoq.Template.utils.wGraph]
N:741 [binder, in MetaCoq.PCUIC.PCUICConfluence]
n:745 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
n:745 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
N:748 [binder, in MetaCoq.PCUIC.PCUICConfluence]
n:75 [binder, in MetaCoq.Erasure.Extract]
n:75 [binder, in MetaCoq.Template.utils.wGraph]
n:75 [binder, in MetaCoq.PCUIC.PCUICConversion]
n:75 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
n:75 [binder, in MetaCoq.Erasure.EAstUtils]
N:75 [binder, in MetaCoq.Template.LiftSubst]
n:75 [binder, in MetaCoq.Template.Induction]
n:752 [binder, in MetaCoq.Template.utils.wGraph]
n:753 [binder, in MetaCoq.Template.utils.wGraph]
N:755 [binder, in MetaCoq.PCUIC.PCUICConfluence]
n:758 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
n:76 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
n:76 [binder, in MetaCoq.Erasure.ELiftSubst]
n:76 [binder, in MetaCoq.Erasure.EGenericMapEnv]
n:76 [binder, in MetaCoq.Template.LiftSubst]
N:760 [binder, in MetaCoq.PCUIC.PCUICConfluence]
N:765 [binder, in MetaCoq.PCUIC.PCUICConfluence]
n:77 [binder, in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
n:77 [binder, in MetaCoq.PCUIC.PCUICProgress]
n:77 [binder, in MetaCoq.Template.utils.All_Forall]
n:77 [binder, in MetaCoq.Template.TermEquality]
n:77 [binder, in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
n:77 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
n:77 [binder, in MetaCoq.Template.Induction]
N:770 [binder, in MetaCoq.PCUIC.PCUICConfluence]
n:773 [binder, in MetaCoq.Template.utils.wGraph]
n:775 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
n:778 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
n:78 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
n:78 [binder, in MetaCoq.Template.Universes]
N:78 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:780 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
n:785 [binder, in MetaCoq.Template.utils.MCList]
n:79 [binder, in MetaCoq.Template.WfAst]
n:79 [binder, in MetaCoq.Template.utils.wGraph]
n:79 [binder, in MetaCoq.PCUIC.PCUICConversion]
n:79 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
n:79 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:796 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
n:798 [binder, in MetaCoq.PCUIC.PCUICTyping]
n:8 [binder, in MetaCoq.Erasure.EInduction]
n:8 [binder, in MetaCoq.Template.WfAst]
n:8 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
n:8 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
n:8 [binder, in MetaCoq.PCUIC.PCUICFirstorder]
n:8 [binder, in MetaCoq.Template.UnivSubst]
N:8 [binder, in MetaCoq.PCUIC.PCUICContextReduction]
n:8 [binder, in MetaCoq.Template.LiftSubst]
n:80 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
n:80 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
N:80 [binder, in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
N:80 [binder, in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
n:80 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
N:80 [binder, in MetaCoq.Template.LiftSubst]
n:802 [binder, in MetaCoq.Template.utils.wGraph]
n:802 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
n:806 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
n:807 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
n:809 [binder, in MetaCoq.PCUIC.PCUICTyping]
n:81 [binder, in MetaCoq.Template.utils.wGraph]
n:81 [binder, in MetaCoq.Template.Environment]
n:81 [binder, in MetaCoq.PCUIC.PCUICCanonicity]
n:818 [binder, in MetaCoq.PCUIC.PCUICTyping]
n:82 [binder, in MetaCoq.Template.WfAst]
n:82 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
n:82 [binder, in MetaCoq.Erasure.ELiftSubst]
n:82 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
N:82 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:82 [binder, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
n:822 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
n:827 [binder, in MetaCoq.PCUIC.PCUICTyping]
n:827 [binder, in MetaCoq.PCUIC.PCUICSR]
n:827 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
n:83 [binder, in MetaCoq.Erasure.ESubstitution]
n:83 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
n:83 [binder, in MetaCoq.Template.utils.wGraph]
n:83 [binder, in MetaCoq.PCUIC.Typing.PCUICWeakeningTyp]
n:83 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
n:83 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
N:83 [binder, in MetaCoq.Template.LiftSubst]
n:830 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
n:834 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
n:837 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
n:84 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
n:84 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
n:84 [binder, in MetaCoq.Template.LiftSubst]
N:840 [binder, in MetaCoq.PCUIC.PCUICReduction]
n:848 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
n:85 [binder, in MetaCoq.Template.WfAst]
n:85 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
n:85 [binder, in MetaCoq.Template.utils.wGraph]
n:85 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
n:856 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
n:857 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
n:86 [binder, in MetaCoq.PCUIC.PCUICInductives]
n:86 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:86 [binder, in MetaCoq.PCUIC.PCUICTyping]
n:86 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
n:865 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
n:867 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
n:87 [binder, in MetaCoq.Template.utils.All_Forall]
n:87 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
N:87 [binder, in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
N:87 [binder, in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
n:872 [binder, in MetaCoq.Template.utils.All_Forall]
n:873 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
n:88 [binder, in MetaCoq.PCUIC.PCUICProgress]
n:88 [binder, in MetaCoq.Template.utils.All_Forall]
n:88 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:88 [binder, in MetaCoq.PCUIC.Conversion.PCUICInstConv]
n:88 [binder, in MetaCoq.Template.Environment]
N:88 [binder, in MetaCoq.Template.LiftSubst]
n:88 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
n:880 [binder, in MetaCoq.Template.utils.All_Forall]
n:883 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
n:885 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
n:885 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
n:889 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
n:89 [binder, in MetaCoq.Erasure.ELiftSubst]
n:89 [binder, in MetaCoq.Template.LiftSubst]
n:895 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
N:896 [binder, in MetaCoq.PCUIC.PCUICConversion]
n:897 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
n:899 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
n:9 [binder, in MetaCoq.Translations.param_binary]
n:9 [binder, in MetaCoq.Template.utils.All_Forall]
n:9 [binder, in MetaCoq.Template.utils.MCArith]
n:9 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
n:9 [binder, in MetaCoq.Template.utils.wGraph]
n:9 [binder, in MetaCoq.Erasure.ESpineView]
n:9 [binder, in MetaCoq.Erasure.EReflect]
n:90 [binder, in MetaCoq.Template.EtaExpand]
n:90 [binder, in MetaCoq.PCUIC.PCUICWfUniverses]
n:90 [binder, in MetaCoq.Erasure.EWellformed]
n:90 [binder, in MetaCoq.PCUIC.Typing.PCUICWeakeningTyp]
n:90 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
n:90 [binder, in MetaCoq.PCUIC.PCUICSR]
n:90 [binder, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
n:901 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
N:902 [binder, in MetaCoq.PCUIC.PCUICConversion]
n:908 [binder, in MetaCoq.PCUIC.PCUICTyping]
N:909 [binder, in MetaCoq.PCUIC.PCUICConversion]
n:91 [binder, in MetaCoq.Template.EtaExpand]
n:91 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
n:91 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
n:91 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:91 [binder, in MetaCoq.PCUIC.PCUICAst]
n:912 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
n:913 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
n:916 [binder, in MetaCoq.Template.utils.MCList]
N:916 [binder, in MetaCoq.PCUIC.PCUICConversion]
n:916 [binder, in MetaCoq.PCUIC.PCUICTyping]
n:92 [binder, in MetaCoq.Template.utils.All_Forall]
n:92 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
n:92 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
n:92 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:92 [binder, in MetaCoq.Erasure.ELiftSubst]
N:92 [binder, in MetaCoq.Template.LiftSubst]
n:921 [binder, in MetaCoq.Template.utils.MCList]
N:923 [binder, in MetaCoq.PCUIC.PCUICConversion]
n:924 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
N:93 [binder, in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
n:93 [binder, in MetaCoq.PCUIC.PCUICAst]
n:93 [binder, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
n:93 [binder, in MetaCoq.Template.LiftSubst]
n:930 [binder, in MetaCoq.PCUIC.PCUICTyping]
n:930 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
n:936 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
n:938 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
n:94 [binder, in MetaCoq.Erasure.EInduction]
n:94 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
n:94 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
n:94 [binder, in MetaCoq.Erasure.EWellformed]
N:94 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:95 [binder, in MetaCoq.Erasure.EOptimizePropDiscr]
n:95 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
n:955 [binder, in MetaCoq.PCUIC.PCUICTyping]
n:96 [binder, in MetaCoq.Template.WfAst]
n:96 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:96 [binder, in MetaCoq.Template.Checker]
N:96 [binder, in MetaCoq.Erasure.ELiftSubst]
n:96 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:96 [binder, in MetaCoq.Template.AstUtils]
n:969 [binder, in MetaCoq.Template.Typing]
n:97 [binder, in MetaCoq.Erasure.ESubstitution]
n:97 [binder, in MetaCoq.PCUIC.PCUICProgress]
n:97 [binder, in MetaCoq.Erasure.ELiftSubst]
n:97 [binder, in MetaCoq.PCUIC.PCUICCanonicity]
n:97 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
N:974 [binder, in MetaCoq.PCUIC.PCUICConfluence]
n:98 [binder, in MetaCoq.Erasure.EInduction]
n:98 [binder, in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
n:98 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
n:98 [binder, in MetaCoq.PCUIC.PCUICSR]
n:98 [binder, in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
n:984 [binder, in MetaCoq.PCUIC.PCUICTyping]
n:988 [binder, in MetaCoq.Template.Typing]
n:989 [binder, in MetaCoq.PCUIC.PCUICTyping]
n:99 [binder, in MetaCoq.Template.utils.All_Forall]
n:99 [binder, in MetaCoq.Erasure.EArities]
N:99 [binder, in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
n:99 [binder, in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:99 [binder, in MetaCoq.PCUIC.Typing.PCUICWeakeningTyp]
n:99 [binder, in MetaCoq.PCUIC.Syntax.PCUICClosed]
N:99 [binder, in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:995 [binder, in MetaCoq.PCUIC.PCUICTyping]
n:997 [binder, in MetaCoq.Template.Typing]



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)