| 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 (binder)
nameless:4 [in MetaCoq.PCUIC.Syntax.PCUICNamelessDef]names:110 [in MetaCoq.PCUIC.utils.PCUICPretty]
names:124 [in MetaCoq.Template.Pretty]
names:132 [in MetaCoq.Template.Pretty]
names:80 [in MetaCoq.Template.Pretty]
name:47 [in MetaCoq.Examples.demo]
napp':206 [in MetaCoq.Template.TermEquality]
napp':215 [in MetaCoq.Template.TermEquality]
napp':222 [in MetaCoq.Template.TermEquality]
napp':333 [in MetaCoq.PCUIC.PCUICEquality]
napp':349 [in MetaCoq.PCUIC.PCUICEquality]
napp':360 [in MetaCoq.PCUIC.PCUICEquality]
napp':374 [in MetaCoq.PCUIC.PCUICEquality]
napp':381 [in MetaCoq.PCUIC.PCUICEquality]
napp':386 [in MetaCoq.PCUIC.PCUICEquality]
napp:10 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
napp:103 [in MetaCoq.PCUIC.PCUICCumulativity]
napp:103 [in MetaCoq.PCUIC.PCUICConvCumInversion]
napp:1112 [in MetaCoq.PCUIC.PCUICConversion]
napp:118 [in MetaCoq.PCUIC.PCUICEquality]
napp:1237 [in MetaCoq.PCUIC.PCUICConfluence]
napp:129 [in MetaCoq.Erasure.Prelim]
napp:134 [in MetaCoq.SafeChecker.PCUICEqualityDec]
napp:14 [in MetaCoq.Erasure.ESpineView]
napp:14 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
napp:150 [in MetaCoq.PCUIC.PCUICCumulativity]
napp:154 [in MetaCoq.Template.TermEquality]
napp:16 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
napp:163 [in MetaCoq.Template.TermEquality]
napp:172 [in MetaCoq.Erasure.EInduction]
napp:173 [in MetaCoq.SafeChecker.PCUICEqualityDec]
napp:179 [in MetaCoq.Template.TermEquality]
napp:180 [in MetaCoq.SafeChecker.PCUICEqualityDec]
napp:188 [in MetaCoq.Template.TermEquality]
napp:188 [in MetaCoq.PCUIC.PCUICEquality]
napp:193 [in MetaCoq.SafeChecker.PCUICEqualityDec]
napp:2 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
napp:202 [in MetaCoq.Template.TermEquality]
napp:205 [in MetaCoq.Template.TermEquality]
napp:208 [in MetaCoq.SafeChecker.PCUICEqualityDec]
napp:214 [in MetaCoq.Template.TermEquality]
napp:221 [in MetaCoq.Template.TermEquality]
napp:221 [in MetaCoq.PCUIC.PCUICEquality]
napp:228 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
napp:231 [in MetaCoq.SafeChecker.PCUICEqualityDec]
napp:232 [in MetaCoq.Template.TermEquality]
napp:240 [in MetaCoq.PCUIC.PCUICAlpha]
napp:242 [in MetaCoq.PCUIC.PCUICEquality]
napp:244 [in MetaCoq.Template.TermEquality]
napp:25 [in MetaCoq.PCUIC.PCUICEquality]
napp:251 [in MetaCoq.PCUIC.PCUICEquality]
napp:260 [in MetaCoq.Erasure.EInduction]
napp:263 [in MetaCoq.PCUIC.PCUICEquality]
napp:266 [in MetaCoq.SafeChecker.PCUICEqualityDec]
napp:27 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
napp:272 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
napp:273 [in MetaCoq.PCUIC.PCUICEquality]
napp:274 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
napp:277 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
napp:28 [in MetaCoq.Template.TermEquality]
napp:280 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
napp:280 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
napp:287 [in MetaCoq.PCUIC.PCUICEquality]
napp:287 [in MetaCoq.SafeChecker.PCUICEqualityDec]
napp:288 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
napp:296 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
napp:303 [in MetaCoq.SafeChecker.PCUICEqualityDec]
napp:309 [in MetaCoq.PCUIC.PCUICConfluence]
napp:310 [in MetaCoq.SafeChecker.PCUICEqualityDec]
napp:316 [in MetaCoq.PCUIC.PCUICEquality]
napp:319 [in MetaCoq.SafeChecker.PCUICEqualityDec]
napp:32 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
napp:322 [in MetaCoq.PCUIC.PCUICEquality]
napp:33 [in MetaCoq.SafeChecker.PCUICEqualityDec]
napp:331 [in MetaCoq.PCUIC.PCUICConfluence]
napp:332 [in MetaCoq.PCUIC.PCUICEquality]
napp:341 [in MetaCoq.PCUIC.PCUICEquality]
napp:348 [in MetaCoq.PCUIC.PCUICEquality]
napp:35 [in MetaCoq.PCUIC.PCUICEquality]
napp:351 [in MetaCoq.PCUIC.PCUICEquality]
napp:351 [in MetaCoq.PCUIC.PCUICConfluence]
napp:359 [in MetaCoq.PCUIC.PCUICEquality]
napp:37 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
napp:373 [in MetaCoq.PCUIC.PCUICEquality]
napp:377 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
napp:38 [in MetaCoq.Template.TermEquality]
napp:380 [in MetaCoq.PCUIC.PCUICEquality]
napp:385 [in MetaCoq.PCUIC.PCUICEquality]
napp:388 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
napp:39 [in MetaCoq.SafeChecker.PCUICEqualityDec]
napp:391 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
napp:394 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
napp:395 [in MetaCoq.PCUIC.PCUICConfluence]
napp:399 [in MetaCoq.SafeChecker.PCUICEqualityDec]
napp:4 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
napp:40 [in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
napp:403 [in MetaCoq.SafeChecker.PCUICEqualityDec]
napp:41 [in MetaCoq.Erasure.ESpineView]
napp:416 [in MetaCoq.PCUIC.PCUICConfluence]
napp:44 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
napp:45 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
napp:458 [in MetaCoq.PCUIC.PCUICEquality]
napp:467 [in MetaCoq.PCUIC.PCUICConfluence]
napp:487 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
napp:488 [in MetaCoq.PCUIC.PCUICConfluence]
napp:489 [in MetaCoq.PCUIC.PCUICEquality]
napp:49 [in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
napp:495 [in MetaCoq.PCUIC.PCUICEquality]
napp:505 [in MetaCoq.PCUIC.PCUICEquality]
napp:509 [in MetaCoq.PCUIC.PCUICEquality]
napp:518 [in MetaCoq.PCUIC.PCUICEquality]
napp:529 [in MetaCoq.PCUIC.PCUICNormal]
napp:537 [in MetaCoq.PCUIC.PCUICNormal]
napp:546 [in MetaCoq.PCUIC.PCUICConfluence]
napp:56 [in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
napp:570 [in MetaCoq.PCUIC.PCUICEquality]
napp:59 [in MetaCoq.PCUIC.PCUICPrincipality]
napp:61 [in MetaCoq.SafeChecker.PCUICEqualityDec]
napp:64 [in MetaCoq.PCUIC.PCUICCumulProp]
napp:64 [in MetaCoq.SafeChecker.PCUICEqualityDec]
napp:653 [in MetaCoq.PCUIC.PCUICInductiveInversion]
napp:655 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
napp:66 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
napp:679 [in MetaCoq.SafeChecker.PCUICSafeConversion]
napp:680 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
napp:687 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
napp:690 [in MetaCoq.PCUIC.PCUICEquality]
napp:690 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
napp:693 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
napp:702 [in MetaCoq.PCUIC.PCUICEquality]
napp:703 [in MetaCoq.PCUIC.PCUICInductiveInversion]
napp:71 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
napp:71 [in MetaCoq.SafeChecker.PCUICEqualityDec]
napp:72 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
napp:74 [in MetaCoq.Template.TermEquality]
napp:74 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
napp:79 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
napp:86 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
napp:88 [in MetaCoq.PCUIC.PCUICConvCumInversion]
napp:97 [in MetaCoq.PCUIC.PCUICCumulativity]
nargs:139 [in MetaCoq.Erasure.EConstructorsAsBlocks]
nargs:141 [in MetaCoq.PCUIC.PCUICWcbvEval]
nargs:145 [in MetaCoq.Erasure.EWcbvEval]
nargs:170 [in MetaCoq.PCUIC.PCUICWcbvEval]
nargs:189 [in MetaCoq.Erasure.EWcbvEval]
nargs:242 [in MetaCoq.Template.WcbvEval]
nargs:269 [in MetaCoq.Template.WcbvEval]
narg:100 [in MetaCoq.Erasure.EWcbvEvalInd]
narg:100 [in MetaCoq.Erasure.EWcbvEval]
narg:102 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
narg:105 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
narg:105 [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
narg:106 [in MetaCoq.PCUIC.PCUICWcbvEval]
narg:107 [in MetaCoq.PCUIC.PCUICNormal]
narg:108 [in MetaCoq.Template.Typing]
narg:108 [in MetaCoq.Template.WcbvEval]
narg:109 [in MetaCoq.Erasure.EWcbvEvalInd]
narg:112 [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
narg:114 [in MetaCoq.PCUIC.PCUICWcbvEval]
narg:115 [in MetaCoq.Template.Typing]
narg:116 [in MetaCoq.Template.WcbvEval]
narg:119 [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
narg:122 [in MetaCoq.Template.Typing]
narg:123 [in MetaCoq.PCUIC.PCUICWcbvEval]
narg:123 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
narg:125 [in MetaCoq.Template.WcbvEval]
narg:130 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
narg:131 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
narg:136 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
narg:137 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
narg:141 [in MetaCoq.PCUIC.PCUICSubstitution]
narg:144 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
narg:147 [in MetaCoq.PCUIC.PCUICSubstitution]
narg:149 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
narg:152 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
narg:161 [in MetaCoq.PCUIC.PCUICSubstitution]
narg:184 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
narg:185 [in MetaCoq.PCUIC.PCUICReduction]
narg:191 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
narg:193 [in MetaCoq.Template.WcbvEval]
narg:193 [in MetaCoq.PCUIC.PCUICReduction]
narg:198 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
narg:201 [in MetaCoq.PCUIC.PCUICReduction]
narg:202 [in MetaCoq.Template.WcbvEval]
narg:207 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
narg:207 [in MetaCoq.PCUIC.PCUICCanonicity]
narg:209 [in MetaCoq.PCUIC.PCUICParallelReduction]
narg:210 [in MetaCoq.Template.WcbvEval]
narg:212 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
narg:219 [in MetaCoq.Template.WcbvEval]
narg:220 [in MetaCoq.PCUIC.PCUICParallelReduction]
narg:221 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
narg:230 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
narg:232 [in MetaCoq.PCUIC.PCUICNormal]
narg:233 [in MetaCoq.PCUIC.PCUICParallelReduction]
narg:240 [in MetaCoq.PCUIC.PCUICWcbvEval]
narg:247 [in MetaCoq.PCUIC.PCUICWcbvEval]
narg:25 [in MetaCoq.PCUIC.PCUICReduction]
narg:250 [in MetaCoq.Erasure.EWcbvEval]
narg:252 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
narg:255 [in MetaCoq.Erasure.EWcbvEval]
narg:260 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
narg:276 [in MetaCoq.Template.Typing]
narg:28 [in MetaCoq.Template.TypingWf]
narg:284 [in MetaCoq.Template.Typing]
narg:289 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
narg:292 [in MetaCoq.Template.Typing]
narg:294 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
narg:295 [in MetaCoq.PCUIC.PCUICWcbvEval]
narg:300 [in MetaCoq.PCUIC.PCUICWcbvEval]
narg:303 [in MetaCoq.Template.WcbvEval]
narg:32 [in MetaCoq.PCUIC.PCUICReduction]
narg:325 [in MetaCoq.PCUIC.PCUICWcbvEval]
narg:327 [in MetaCoq.PCUIC.PCUICNormal]
narg:339 [in MetaCoq.PCUIC.PCUICWcbvEval]
narg:35 [in MetaCoq.Template.TypingWf]
narg:365 [in MetaCoq.PCUIC.PCUICSR]
narg:373 [in MetaCoq.PCUIC.PCUICSR]
narg:374 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
narg:379 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
narg:381 [in MetaCoq.PCUIC.PCUICSR]
narg:384 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
narg:385 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
narg:387 [in MetaCoq.PCUIC.PCUICParallelReduction]
narg:39 [in MetaCoq.PCUIC.PCUICReduction]
narg:392 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
narg:400 [in MetaCoq.PCUIC.PCUICParallelReduction]
narg:400 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
narg:415 [in MetaCoq.PCUIC.PCUICParallelReduction]
narg:44 [in MetaCoq.Erasure.EDeps]
narg:46 [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
narg:51 [in MetaCoq.Erasure.EDeps]
narg:53 [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
narg:74 [in MetaCoq.Erasure.EWcbvEval]
narg:75 [in MetaCoq.Erasure.Prelim]
narg:76 [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
narg:81 [in MetaCoq.Erasure.EWcbvEvalInd]
narg:84 [in MetaCoq.Erasure.EWcbvEval]
narg:89 [in MetaCoq.PCUIC.PCUICNormal]
narg:91 [in MetaCoq.Erasure.EWcbvEval]
narg:92 [in MetaCoq.Erasure.EWcbvEvalInd]
narg:938 [in MetaCoq.PCUIC.PCUICParallelReduction]
narg:98 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
narg:98 [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
narg:99 [in MetaCoq.Template.WcbvEval]
nas':113 [in MetaCoq.SafeChecker.PCUICEqualityDec]
nas':115 [in MetaCoq.SafeChecker.PCUICEqualityDec]
nas:1 [in MetaCoq.PCUIC.PCUICCasesContexts]
nAs:10 [in MetaCoq.PCUIC.utils.PCUICPretty]
nas:112 [in MetaCoq.SafeChecker.PCUICEqualityDec]
nas:114 [in MetaCoq.SafeChecker.PCUICEqualityDec]
nas:12 [in MetaCoq.PCUIC.PCUICCasesContexts]
nas:144 [in MetaCoq.PCUIC.PCUICAlpha]
nas:196 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
nas:201 [in MetaCoq.PCUIC.PCUICSR]
nas:203 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
nas:206 [in MetaCoq.PCUIC.PCUICSR]
nas:207 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
nas:210 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
nas:215 [in MetaCoq.PCUIC.PCUICSR]
nas:218 [in MetaCoq.PCUIC.PCUICContexts]
nas:221 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
nas:225 [in MetaCoq.PCUIC.PCUICContexts]
nas:229 [in MetaCoq.PCUIC.PCUICContexts]
nas:232 [in MetaCoq.PCUIC.PCUICContexts]
nas:288 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
nas:291 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
nas:297 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
nas:314 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
nas:362 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
nas:365 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
nas:371 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
nas:388 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
nas:45 [in MetaCoq.PCUIC.PCUICValidity]
nas:45 [in MetaCoq.PCUIC.PCUICCasesContexts]
nas:49 [in MetaCoq.Erasure.EPretty]
nas:52 [in MetaCoq.PCUIC.PCUICValidity]
nas:55 [in MetaCoq.Erasure.EPretty]
nAs:56 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
nAs:57 [in MetaCoq.Template.AstUtils]
nas:597 [in MetaCoq.PCUIC.PCUICSR]
nas:659 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
nas:663 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
nAs:7 [in MetaCoq.Template.Pretty]
nas:79 [in MetaCoq.Erasure.Prelim]
nas:797 [in MetaCoq.PCUIC.PCUICInductiveInversion]
nas:8 [in MetaCoq.PCUIC.PCUICCasesContexts]
nas:891 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
nas:895 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
nas:905 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
nas:907 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
nas:910 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
na':100 [in MetaCoq.PCUIC.Bidirectional.BDUnique]
na':102 [in MetaCoq.PCUIC.PCUICConversion]
na':102 [in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
na':1034 [in MetaCoq.PCUIC.PCUICParallelReduction]
na':1043 [in MetaCoq.PCUIC.PCUICParallelReduction]
na':105 [in MetaCoq.Template.TermEquality]
na':106 [in MetaCoq.SafeChecker.PCUICEqualityDec]
na':108 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
na':109 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
na':109 [in MetaCoq.SafeChecker.PCUICEqualityDec]
na':11 [in MetaCoq.SafeChecker.PCUICErrors]
na':111 [in MetaCoq.Template.TermEquality]
na':114 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
na':138 [in MetaCoq.Erasure.Prelim]
na':142 [in MetaCoq.Erasure.Prelim]
na':143 [in MetaCoq.PCUIC.PCUICEquality]
na':147 [in MetaCoq.Erasure.Prelim]
na':149 [in MetaCoq.PCUIC.PCUICEquality]
na':155 [in MetaCoq.PCUIC.PCUICEquality]
na':18 [in MetaCoq.PCUIC.Bidirectional.BDUnique]
na':20 [in MetaCoq.SafeChecker.PCUICErrors]
na':204 [in MetaCoq.PCUIC.PCUICConversion]
na':213 [in MetaCoq.PCUIC.PCUICConversion]
na':214 [in MetaCoq.PCUIC.PCUICCumulProp]
na':219 [in MetaCoq.PCUIC.PCUICConversion]
na':266 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
na':270 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
na':270 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
na':278 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
na':28 [in MetaCoq.SafeChecker.PCUICErrors]
na':286 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
na':3 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
na':323 [in MetaCoq.PCUIC.PCUICCumulProp]
na':330 [in MetaCoq.Template.Environment]
na':333 [in MetaCoq.PCUIC.PCUICCumulProp]
na':334 [in MetaCoq.Template.Environment]
na':342 [in MetaCoq.SafeChecker.PCUICEqualityDec]
na':37 [in MetaCoq.SafeChecker.PCUICErrors]
na':396 [in MetaCoq.PCUIC.PCUICInductiveInversion]
na':408 [in MetaCoq.PCUIC.PCUICConversion]
na':409 [in MetaCoq.PCUIC.PCUICInductiveInversion]
na':411 [in MetaCoq.Template.EnvironmentTyping]
na':417 [in MetaCoq.Template.EnvironmentTyping]
na':418 [in MetaCoq.PCUIC.PCUICConversion]
na':42 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
na':421 [in MetaCoq.PCUIC.PCUICInductiveInversion]
na':432 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
na':439 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
na':446 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
na':46 [in MetaCoq.Erasure.EPretty]
na':46 [in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
na':47 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
na':47 [in MetaCoq.Erasure.EPretty]
na':47 [in MetaCoq.Template.Typing]
na':48 [in MetaCoq.Template.Reflect]
na':51 [in MetaCoq.PCUIC.PCUICArities]
na':51 [in MetaCoq.Template.TermEquality]
na':54 [in MetaCoq.PCUIC.PCUICEquality]
na':55 [in MetaCoq.PCUIC.utils.PCUICPretty]
na':56 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
na':56 [in MetaCoq.Template.TermEquality]
na':56 [in MetaCoq.PCUIC.utils.PCUICPretty]
na':58 [in MetaCoq.Template.Typing]
na':59 [in MetaCoq.PCUIC.PCUICEquality]
na':59 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
na':60 [in MetaCoq.PCUIC.utils.PCUICOnOne]
na':61 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
na':65 [in MetaCoq.PCUIC.utils.PCUICOnOne]
na':65 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
na':69 [in MetaCoq.Template.Pretty]
na':7 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
na':70 [in MetaCoq.Template.Pretty]
na':71 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
na':71 [in MetaCoq.Template.Pretty]
na':744 [in MetaCoq.PCUIC.PCUICParallelReduction]
na':75 [in MetaCoq.PCUIC.utils.PCUICPretty]
na':754 [in MetaCoq.PCUIC.PCUICParallelReduction]
na':76 [in MetaCoq.PCUIC.utils.PCUICPretty]
na':77 [in MetaCoq.PCUIC.utils.PCUICPretty]
na':786 [in MetaCoq.PCUIC.PCUICConversion]
na':834 [in MetaCoq.PCUIC.PCUICConversion]
na':84 [in MetaCoq.Template.Pretty]
na':841 [in MetaCoq.PCUIC.PCUICConversion]
na':86 [in MetaCoq.PCUIC.Bidirectional.BDUnique]
na':95 [in MetaCoq.PCUIC.PCUICConversion]
na':96 [in MetaCoq.Template.Pretty]
na':97 [in MetaCoq.Template.Pretty]
na':99 [in MetaCoq.Template.TermEquality]
na1:511 [in MetaCoq.PCUIC.PCUICConversion]
na1:545 [in MetaCoq.SafeChecker.PCUICSafeConversion]
na1:551 [in MetaCoq.SafeChecker.PCUICSafeConversion]
na1:818 [in MetaCoq.PCUIC.PCUICConversion]
na1:826 [in MetaCoq.PCUIC.PCUICConversion]
na1:848 [in MetaCoq.PCUIC.PCUICConversion]
na1:871 [in MetaCoq.PCUIC.PCUICConversion]
na1:879 [in MetaCoq.PCUIC.PCUICConversion]
na2:512 [in MetaCoq.PCUIC.PCUICConversion]
na2:548 [in MetaCoq.SafeChecker.PCUICSafeConversion]
na2:554 [in MetaCoq.SafeChecker.PCUICSafeConversion]
na2:819 [in MetaCoq.PCUIC.PCUICConversion]
na2:827 [in MetaCoq.PCUIC.PCUICConversion]
na2:849 [in MetaCoq.PCUIC.PCUICConversion]
na2:872 [in MetaCoq.PCUIC.PCUICConversion]
na2:880 [in MetaCoq.PCUIC.PCUICConversion]
na:1 [in MetaCoq.PCUIC.Syntax.PCUICNamelessDef]
na:10 [in MetaCoq.PCUIC.Syntax.PCUICViews]
na:10 [in MetaCoq.PCUIC.PCUICGeneration]
na:100 [in MetaCoq.PCUIC.PCUICArities]
na:100 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
na:1003 [in MetaCoq.PCUIC.PCUICReduction]
na:101 [in MetaCoq.Template.EtaExpand]
na:101 [in MetaCoq.PCUIC.PCUICConversion]
na:102 [in MetaCoq.PCUIC.PCUICAst]
na:1024 [in MetaCoq.PCUIC.PCUICReduction]
na:1029 [in MetaCoq.PCUIC.PCUICReduction]
na:103 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
na:1033 [in MetaCoq.PCUIC.PCUICParallelReduction]
na:104 [in MetaCoq.Template.EtaExpand]
na:104 [in MetaCoq.PCUIC.PCUICArities]
na:104 [in MetaCoq.Template.TermEquality]
na:104 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
na:1042 [in MetaCoq.PCUIC.PCUICParallelReduction]
na:105 [in MetaCoq.SafeChecker.PCUICEqualityDec]
na:106 [in MetaCoq.PCUIC.PCUICTyping]
na:106 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
na:1069 [in MetaCoq.PCUIC.PCUICReduction]
na:107 [in MetaCoq.Template.EtaExpand]
na:107 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
na:1074 [in MetaCoq.PCUIC.PCUICReduction]
na:108 [in MetaCoq.PCUIC.PCUICValidity]
na:108 [in MetaCoq.PCUIC.PCUICReduction]
na:108 [in MetaCoq.SafeChecker.PCUICEqualityDec]
na:109 [in MetaCoq.PCUIC.PCUICArities]
na:1095 [in MetaCoq.PCUIC.PCUICReduction]
na:11 [in MetaCoq.Template.Reflect]
na:110 [in MetaCoq.Template.TermEquality]
na:1100 [in MetaCoq.PCUIC.PCUICReduction]
na:111 [in MetaCoq.Template.EnvironmentTyping]
na:111 [in MetaCoq.PCUIC.Bidirectional.BDUnique]
na:112 [in MetaCoq.PCUIC.PCUICReduction]
na:1129 [in MetaCoq.Erasure.ErasureFunction]
na:113 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
na:1131 [in MetaCoq.PCUIC.PCUICReduction]
na:1135 [in MetaCoq.PCUIC.PCUICReduction]
na:1139 [in MetaCoq.PCUIC.PCUICReduction]
na:114 [in MetaCoq.Template.EnvironmentTyping]
na:114 [in MetaCoq.PCUIC.PCUICConversion]
na:114 [in MetaCoq.PCUIC.PCUICCanonicity]
na:115 [in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
na:116 [in MetaCoq.PCUIC.PCUICArities]
na:1166 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
na:117 [in MetaCoq.PCUIC.PCUICSpine]
na:1171 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
na:118 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
na:1187 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
na:1192 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
na:12 [in MetaCoq.Template.Normal]
na:12 [in MetaCoq.SafeChecker.PCUICWfReduction]
na:12 [in MetaCoq.PCUIC.PCUICContextSubst]
na:120 [in MetaCoq.PCUIC.PCUICConversion]
na:123 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
na:124 [in MetaCoq.PCUIC.PCUICSpine]
na:125 [in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
na:126 [in MetaCoq.PCUIC.PCUICCanonicity]
na:128 [in MetaCoq.PCUIC.PCUICArities]
na:128 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
na:13 [in MetaCoq.Translations.param_binary]
na:13 [in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
na:132 [in MetaCoq.PCUIC.PCUICFirstorder]
na:133 [in MetaCoq.Template.Typing]
na:133 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
na:134 [in MetaCoq.PCUIC.PCUICAst]
na:136 [in MetaCoq.PCUIC.Syntax.PCUICCases]
na:137 [in MetaCoq.Template.Typing]
na:137 [in MetaCoq.Erasure.Prelim]
na:138 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
na:14 [in MetaCoq.Template.WfAst]
na:14 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
na:141 [in MetaCoq.Template.Typing]
na:141 [in MetaCoq.Erasure.Prelim]
na:142 [in MetaCoq.PCUIC.PCUICEquality]
na:143 [in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
na:143 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
na:143 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
na:144 [in MetaCoq.Template.WcbvEval]
na:145 [in MetaCoq.PCUIC.Syntax.PCUICCases]
na:146 [in MetaCoq.Template.Typing]
na:146 [in MetaCoq.Erasure.Prelim]
na:147 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
na:148 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
na:148 [in MetaCoq.PCUIC.PCUICEquality]
na:15 [in MetaCoq.Translations.param_binary]
na:15 [in MetaCoq.SafeChecker.PCUICWfReduction]
na:15 [in MetaCoq.Erasure.EWcbvEvalInd]
na:15 [in MetaCoq.PCUIC.Bidirectional.BDUnique]
na:150 [in MetaCoq.Template.EnvironmentTyping]
na:150 [in MetaCoq.PCUIC.Syntax.PCUICCases]
na:151 [in MetaCoq.Template.Typing]
na:151 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
na:151 [in MetaCoq.Template.WcbvEval]
na:152 [in MetaCoq.PCUIC.Syntax.PCUICCases]
na:154 [in MetaCoq.PCUIC.PCUICEquality]
na:154 [in MetaCoq.PCUIC.Syntax.PCUICCases]
na:155 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
na:1553 [in MetaCoq.SafeChecker.PCUICSafeReduce]
na:156 [in MetaCoq.Template.EnvironmentTyping]
na:158 [in MetaCoq.PCUIC.Syntax.PCUICCases]
na:159 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
na:16 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
na:16 [in MetaCoq.SafeChecker.PCUICErrors]
na:161 [in MetaCoq.PCUIC.PCUICReduction]
na:1611 [in MetaCoq.SafeChecker.PCUICSafeReduce]
na:162 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
na:163 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
na:164 [in MetaCoq.PCUIC.Syntax.PCUICCases]
na:164 [in MetaCoq.PCUIC.PCUICContexts]
na:166 [in MetaCoq.PCUIC.PCUICReduction]
na:167 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
na:168 [in MetaCoq.PCUIC.Syntax.PCUICCases]
na:169 [in MetaCoq.Template.EtaExpand]
na:17 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
na:17 [in MetaCoq.Template.WfAst]
na:170 [in MetaCoq.PCUIC.Syntax.PCUICCases]
na:171 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
na:173 [in MetaCoq.Template.EtaExpand]
na:1741 [in MetaCoq.SafeChecker.PCUICSafeReduce]
na:175 [in MetaCoq.PCUIC.PCUICParallelReduction]
na:176 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
na:1763 [in MetaCoq.SafeChecker.PCUICSafeConversion]
na:177 [in MetaCoq.Template.EtaExpand]
na:179 [in MetaCoq.PCUIC.PCUICConversion]
na:18 [in MetaCoq.Erasure.EEtaExpandedFix]
na:18 [in MetaCoq.SafeChecker.PCUICWfReduction]
na:180 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
na:181 [in MetaCoq.PCUIC.PCUICNormal]
na:182 [in MetaCoq.PCUIC.PCUICParallelReduction]
na:184 [in MetaCoq.PCUIC.PCUICConversion]
na:184 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
na:187 [in MetaCoq.PCUIC.PCUICWcbvEval]
na:187 [in MetaCoq.Template.Ast]
na:188 [in MetaCoq.PCUIC.PCUICNormal]
na:189 [in MetaCoq.Erasure.EEtaExpanded]
na:19 [in MetaCoq.PCUIC.PCUICEtaExpand]
na:19 [in MetaCoq.Template.Reflect]
na:19 [in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
na:190 [in MetaCoq.Template.Ast]
na:190 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
na:191 [in MetaCoq.Erasure.EEtaExpanded]
na:192 [in MetaCoq.PCUIC.PCUICSafeLemmata]
na:192 [in MetaCoq.Erasure.Extract]
na:192 [in MetaCoq.PCUIC.PCUICConversion]
na:193 [in MetaCoq.PCUIC.PCUICWcbvEval]
na:193 [in MetaCoq.Template.Ast]
na:194 [in MetaCoq.Erasure.Extract]
na:197 [in MetaCoq.PCUIC.PCUICWcbvEval]
na:199 [in MetaCoq.PCUIC.PCUICNormal]
na:2 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
na:20 [in MetaCoq.Erasure.EEtaExpandedFix]
na:20 [in MetaCoq.Template.WfAst]
na:20 [in MetaCoq.PCUIC.PCUICNormal]
na:200 [in MetaCoq.PCUIC.PCUICConversion]
na:202 [in MetaCoq.Template.Typing]
na:204 [in MetaCoq.PCUIC.PCUICNormal]
na:2042 [in MetaCoq.SafeChecker.PCUICSafeConversion]
na:2050 [in MetaCoq.SafeChecker.PCUICSafeConversion]
na:206 [in MetaCoq.Template.Typing]
na:206 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
na:209 [in MetaCoq.PCUIC.PCUICConversion]
na:209 [in MetaCoq.PCUIC.PCUICCanonicity]
na:21 [in MetaCoq.Erasure.EWcbvEvalInd]
na:210 [in MetaCoq.Erasure.EArities]
na:211 [in MetaCoq.PCUIC.PCUICCumulProp]
na:214 [in MetaCoq.PCUIC.PCUICNormal]
na:214 [in MetaCoq.PCUIC.PCUICReduction]
na:215 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
na:218 [in MetaCoq.PCUIC.PCUICConversion]
na:219 [in MetaCoq.PCUIC.PCUICReduction]
na:22 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
na:22 [in MetaCoq.Template.BasicAst]
na:22 [in MetaCoq.PCUIC.PCUICEtaExpand]
na:22 [in MetaCoq.SafeChecker.PCUICWfReduction]
na:222 [in MetaCoq.Erasure.EEtaExpanded]
na:223 [in MetaCoq.PCUIC.PCUICNormal]
na:224 [in MetaCoq.Erasure.EEtaExpanded]
na:224 [in MetaCoq.PCUIC.PCUICReduction]
na:226 [in MetaCoq.SafeChecker.PCUICSafeReduce]
na:228 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
na:23 [in MetaCoq.PCUIC.PCUICArities]
na:23 [in MetaCoq.PCUIC.PCUICSubstitution]
na:23 [in MetaCoq.PCUIC.PCUICNormal]
na:230 [in MetaCoq.PCUIC.PCUICReduction]
na:236 [in MetaCoq.PCUIC.PCUICReduction]
na:238 [in MetaCoq.PCUIC.PCUICConversion]
na:24 [in MetaCoq.SafeChecker.PCUICErrors]
na:24 [in MetaCoq.Erasure.EWcbvEval]
na:247 [in MetaCoq.Template.Typing]
na:247 [in MetaCoq.PCUIC.PCUICConversion]
na:248 [in MetaCoq.PCUIC.PCUICParallelReduction]
na:25 [in MetaCoq.PCUIC.PCUICEtaExpand]
na:25 [in MetaCoq.PCUIC.PCUICCumulProp]
na:251 [in MetaCoq.PCUIC.PCUICConversion]
na:253 [in MetaCoq.Template.Typing]
na:256 [in MetaCoq.PCUIC.PCUICConversion]
na:257 [in MetaCoq.PCUIC.PCUICSubstitution]
na:257 [in MetaCoq.PCUIC.PCUICParallelReduction]
na:26 [in MetaCoq.PCUIC.PCUICProgress]
na:26 [in MetaCoq.Erasure.EPretty]
na:26 [in MetaCoq.SafeChecker.PCUICWfReduction]
na:262 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
na:262 [in MetaCoq.PCUIC.PCUICSubstitution]
na:263 [in MetaCoq.PCUIC.PCUICConversion]
na:265 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
na:267 [in MetaCoq.Template.EnvironmentTyping]
na:269 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
na:269 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
na:27 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
na:27 [in MetaCoq.Erasure.Extract]
na:270 [in MetaCoq.PCUIC.PCUICConversion]
na:273 [in MetaCoq.Template.EnvironmentTyping]
na:277 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
na:28 [in MetaCoq.PCUIC.PCUICSubstitution]
na:28 [in MetaCoq.Template.Pretty]
na:280 [in MetaCoq.PCUIC.PCUICCumulProp]
na:280 [in MetaCoq.PCUIC.PCUICReduction]
na:283 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
na:283 [in MetaCoq.PCUIC.PCUICConversion]
na:284 [in MetaCoq.PCUIC.PCUICParallelReduction]
na:285 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
na:285 [in MetaCoq.PCUIC.PCUICReduction]
na:288 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
na:289 [in MetaCoq.PCUIC.PCUICConversion]
na:29 [in MetaCoq.Erasure.EWcbvEval]
na:29 [in MetaCoq.PCUIC.utils.PCUICPretty]
na:3 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
na:3 [in MetaCoq.PCUIC.Syntax.PCUICNamelessDef]
na:302 [in MetaCoq.PCUIC.PCUICWcbvEval]
na:305 [in MetaCoq.Template.Typing]
na:308 [in MetaCoq.Template.EnvironmentTyping]
na:309 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
na:31 [in MetaCoq.Erasure.Extract]
na:310 [in MetaCoq.Template.Typing]
na:312 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
na:313 [in MetaCoq.Template.EnvironmentTyping]
na:315 [in MetaCoq.Template.Typing]
na:318 [in MetaCoq.Template.Environment]
na:32 [in MetaCoq.PCUIC.Syntax.PCUICViews]
na:32 [in MetaCoq.Erasure.Prelim]
na:320 [in MetaCoq.PCUIC.PCUICCumulProp]
na:320 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
na:321 [in MetaCoq.Template.Typing]
na:321 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
na:321 [in MetaCoq.Template.Environment]
na:325 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
na:326 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
na:327 [in MetaCoq.Template.Typing]
na:329 [in MetaCoq.PCUIC.PCUICCumulProp]
na:329 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
na:329 [in MetaCoq.Template.Environment]
na:33 [in MetaCoq.SafeChecker.PCUICErrors]
na:330 [in MetaCoq.PCUIC.PCUICConversion]
na:331 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
na:333 [in MetaCoq.Template.Environment]
na:336 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
na:337 [in MetaCoq.PCUIC.PCUICConversion]
na:338 [in MetaCoq.PCUIC.PCUICReduction]
na:34 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
na:34 [in MetaCoq.PCUIC.utils.PCUICPretty]
na:341 [in MetaCoq.PCUIC.PCUICSR]
na:341 [in MetaCoq.PCUIC.PCUICReduction]
na:341 [in MetaCoq.SafeChecker.PCUICEqualityDec]
na:343 [in MetaCoq.PCUIC.PCUICParallelReduction]
na:346 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
na:346 [in MetaCoq.PCUIC.PCUICSR]
na:348 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
na:348 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
na:350 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
na:352 [in MetaCoq.PCUIC.PCUICParallelReduction]
na:353 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
na:357 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
na:36 [in MetaCoq.PCUIC.PCUICSubstitution]
na:36 [in MetaCoq.Template.Pretty]
na:360 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
na:364 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
na:365 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
na:369 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
na:370 [in MetaCoq.PCUIC.PCUICSpine]
na:373 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
na:373 [in MetaCoq.PCUIC.PCUICSubstitution]
na:373 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
na:373 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
na:376 [in MetaCoq.PCUIC.PCUICSpine]
na:378 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
na:379 [in MetaCoq.PCUIC.PCUICSubstitution]
na:38 [in MetaCoq.PCUIC.PCUICInversion]
na:381 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
na:385 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
na:387 [in MetaCoq.Template.Typing]
na:389 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
na:39 [in MetaCoq.Translations.times_bool_fun]
na:390 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
na:391 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
na:392 [in MetaCoq.Template.Typing]
na:392 [in MetaCoq.PCUIC.PCUICNormal]
na:393 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
na:394 [in MetaCoq.PCUIC.PCUICSR]
na:395 [in MetaCoq.PCUIC.PCUICInductiveInversion]
na:395 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
na:396 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
na:397 [in MetaCoq.PCUIC.PCUICNormal]
na:397 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
na:399 [in MetaCoq.PCUIC.PCUICSR]
na:40 [in MetaCoq.Erasure.ErasureFunction]
na:400 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
na:403 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
na:404 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
na:404 [in MetaCoq.PCUIC.PCUICSR]
na:407 [in MetaCoq.PCUIC.PCUICConversion]
na:408 [in MetaCoq.PCUIC.PCUICInductiveInversion]
na:41 [in MetaCoq.Template.Typing]
na:41 [in MetaCoq.PCUIC.PCUICNormal]
na:410 [in MetaCoq.Template.EnvironmentTyping]
na:410 [in MetaCoq.PCUIC.PCUICSR]
na:416 [in MetaCoq.Template.EnvironmentTyping]
na:416 [in MetaCoq.PCUIC.PCUICSR]
na:417 [in MetaCoq.PCUIC.PCUICConversion]
na:42 [in MetaCoq.PCUIC.Syntax.PCUICViews]
na:42 [in MetaCoq.PCUIC.TemplateToPCUIC]
na:42 [in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
na:420 [in MetaCoq.PCUIC.PCUICInductiveInversion]
na:421 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
na:423 [in MetaCoq.PCUIC.PCUICConversion]
na:425 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
na:43 [in MetaCoq.PCUIC.PCUICSubstitution]
na:43 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
na:43 [in MetaCoq.Template.Pretty]
na:431 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
na:437 [in MetaCoq.PCUIC.PCUICParallelReduction]
na:437 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
na:438 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
na:439 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
na:439 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
na:44 [in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
na:445 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
na:446 [in MetaCoq.PCUIC.PCUICInductives]
na:447 [in MetaCoq.SafeChecker.PCUICSafeChecker]
na:45 [in MetaCoq.PCUIC.PCUICInversion]
na:45 [in MetaCoq.Template.Reflect]
na:450 [in MetaCoq.PCUIC.PCUICParallelReduction]
na:450 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
na:453 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
na:455 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
na:457 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
na:458 [in MetaCoq.SafeChecker.PCUICSafeChecker]
na:46 [in MetaCoq.Translations.times_bool_fun]
na:460 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
na:460 [in MetaCoq.PCUIC.PCUICSR]
na:464 [in MetaCoq.PCUIC.PCUICConversion]
na:465 [in MetaCoq.PCUIC.PCUICSR]
na:466 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
na:47 [in MetaCoq.PCUIC.PCUICNormal]
na:47 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
na:471 [in MetaCoq.PCUIC.PCUICConversion]
na:48 [in MetaCoq.Template.Normal]
na:481 [in MetaCoq.Template.EnvironmentTyping]
na:483 [in MetaCoq.PCUIC.PCUICSpine]
na:485 [in MetaCoq.Template.EnvironmentTyping]
na:487 [in MetaCoq.PCUIC.PCUICParallelReduction]
na:49 [in MetaCoq.PCUIC.PCUICSubstitution]
na:49 [in MetaCoq.Template.TermEquality]
na:491 [in MetaCoq.PCUIC.PCUICInductives]
na:494 [in MetaCoq.SafeChecker.PCUICSafeChecker]
na:495 [in MetaCoq.Template.EnvironmentTyping]
na:497 [in MetaCoq.SafeChecker.PCUICSafeChecker]
na:499 [in MetaCoq.Template.EnvironmentTyping]
na:5 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
na:5 [in MetaCoq.PCUIC.PCUICContextReduction]
na:5 [in MetaCoq.PCUIC.PCUICReduction]
na:50 [in MetaCoq.PCUIC.PCUICArities]
na:50 [in MetaCoq.PCUIC.PCUICReduction]
na:502 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
na:507 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
na:51 [in MetaCoq.Template.Normal]
na:51 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
na:51 [in MetaCoq.Template.WcbvEval]
na:510 [in MetaCoq.PCUIC.PCUICTyping]
na:511 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
na:517 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
na:517 [in MetaCoq.SafeChecker.PCUICSafeChecker]
na:52 [in MetaCoq.Template.Typing]
na:52 [in MetaCoq.PCUIC.PCUICWcbvEval]
na:52 [in MetaCoq.PCUIC.PCUICEquality]
na:523 [in MetaCoq.SafeChecker.PCUICSafeChecker]
na:524 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
na:53 [in MetaCoq.Template.TermEquality]
na:530 [in MetaCoq.SafeChecker.PCUICSafeChecker]
na:533 [in MetaCoq.PCUIC.PCUICSubstitution]
na:537 [in MetaCoq.PCUIC.PCUICSpine]
na:539 [in MetaCoq.PCUIC.PCUICSubstitution]
na:54 [in MetaCoq.PCUIC.PCUICReduction]
na:544 [in MetaCoq.PCUIC.PCUICSpine]
na:548 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
na:55 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
na:55 [in MetaCoq.PCUIC.PCUICInversion]
na:56 [in MetaCoq.PCUIC.PCUICEquality]
na:573 [in MetaCoq.PCUIC.PCUICSpine]
na:58 [in MetaCoq.PCUIC.PCUICWcbvEval]
na:58 [in MetaCoq.Template.WcbvEval]
na:58 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
na:58 [in MetaCoq.PCUIC.PCUICReduction]
na:587 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
na:59 [in MetaCoq.PCUIC.utils.PCUICOnOne]
na:59 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
na:6 [in MetaCoq.SafeChecker.PCUICWfReduction]
na:6 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
na:6 [in MetaCoq.PCUIC.PCUICContextSubst]
na:6 [in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
na:602 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
na:61 [in MetaCoq.Erasure.EEtaExpandedFix]
na:62 [in MetaCoq.PCUIC.PCUICInversion]
na:63 [in MetaCoq.Template.Environment]
na:63 [in MetaCoq.PCUIC.PCUICReduction]
na:64 [in MetaCoq.Erasure.EEtaExpandedFix]
na:64 [in MetaCoq.PCUIC.utils.PCUICOnOne]
na:64 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
na:64 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
na:655 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
na:658 [in MetaCoq.Erasure.ErasureFunction]
na:66 [in MetaCoq.PCUIC.PCUICFirstorder]
na:66 [in MetaCoq.PCUIC.utils.PCUICPretty]
na:661 [in MetaCoq.Erasure.ErasureFunction]
na:661 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
na:67 [in MetaCoq.PCUIC.PCUICArities]
na:68 [in MetaCoq.PCUIC.PCUICReduction]
na:69 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
na:691 [in MetaCoq.Template.Typing]
na:7 [in MetaCoq.SafeChecker.PCUICErrors]
na:70 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
na:709 [in MetaCoq.PCUIC.PCUICEquality]
na:71 [in MetaCoq.Erasure.EDeps]
na:72 [in MetaCoq.PCUIC.PCUICConversion]
na:72 [in MetaCoq.Erasure.EOptimizePropDiscr]
na:73 [in MetaCoq.PCUIC.PCUICInversion]
na:74 [in MetaCoq.Erasure.EDeps]
na:743 [in MetaCoq.PCUIC.PCUICParallelReduction]
na:753 [in MetaCoq.PCUIC.PCUICParallelReduction]
na:76 [in MetaCoq.PCUIC.PCUICConversion]
na:783 [in MetaCoq.PCUIC.PCUICConversion]
na:785 [in MetaCoq.PCUIC.PCUICInductiveInversion]
na:791 [in MetaCoq.PCUIC.PCUICConversion]
na:797 [in MetaCoq.PCUIC.PCUICConversion]
na:8 [in MetaCoq.PCUIC.PCUICSubstitution]
na:80 [in MetaCoq.PCUIC.PCUICConversion]
na:81 [in MetaCoq.PCUIC.PCUICEtaExpand]
na:81 [in MetaCoq.PCUIC.PCUICInversion]
na:81 [in MetaCoq.PCUIC.PCUICFirstorder]
na:83 [in MetaCoq.Template.Typing]
na:833 [in MetaCoq.PCUIC.PCUICConversion]
na:837 [in MetaCoq.PCUIC.PCUICReduction]
na:838 [in MetaCoq.PCUIC.PCUICTyping]
na:84 [in MetaCoq.Erasure.Extract]
na:840 [in MetaCoq.PCUIC.PCUICConversion]
na:85 [in MetaCoq.PCUIC.PCUICEtaExpand]
na:85 [in MetaCoq.PCUIC.PCUICFirstorder]
na:85 [in MetaCoq.PCUIC.Bidirectional.BDUnique]
na:856 [in MetaCoq.PCUIC.PCUICSR]
na:86 [in MetaCoq.PCUIC.PCUICArities]
na:863 [in MetaCoq.PCUIC.PCUICConversion]
na:869 [in MetaCoq.PCUIC.PCUICReduction]
na:88 [in MetaCoq.Template.Typing]
na:887 [in MetaCoq.PCUIC.PCUICParallelReduction]
na:888 [in MetaCoq.PCUIC.PCUICSR]
na:89 [in MetaCoq.PCUIC.PCUICElimination]
na:89 [in MetaCoq.PCUIC.PCUICEtaExpand]
na:89 [in MetaCoq.PCUIC.PCUICTyping]
na:899 [in MetaCoq.PCUIC.PCUICParallelReduction]
na:9 [in MetaCoq.Template.Normal]
na:9 [in MetaCoq.PCUIC.PCUICAlpha]
na:9 [in MetaCoq.SafeChecker.PCUICWfReduction]
na:9 [in MetaCoq.PCUIC.PCUICReduction]
na:90 [in MetaCoq.Erasure.Extract]
na:919 [in MetaCoq.PCUIC.PCUICConversion]
na:92 [in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
na:92 [in MetaCoq.PCUIC.PCUICElimination]
na:92 [in MetaCoq.PCUIC.PCUICArities]
na:939 [in MetaCoq.Template.Typing]
na:94 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
na:94 [in MetaCoq.PCUIC.PCUICConversion]
na:94 [in MetaCoq.PCUIC.PCUICTyping]
na:96 [in MetaCoq.PCUIC.PCUICAst]
na:97 [in MetaCoq.PCUIC.PCUICArities]
na:98 [in MetaCoq.Template.TermEquality]
na:99 [in MetaCoq.PCUIC.Syntax.PCUICViews]
na:99 [in MetaCoq.PCUIC.PCUICAst]
na:99 [in MetaCoq.PCUIC.PCUICTyping]
na:99 [in MetaCoq.PCUIC.Bidirectional.BDUnique]
na:99 [in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
na:998 [in MetaCoq.PCUIC.PCUICReduction]
nb:12 [in MetaCoq.Template.Reflect]
nb:20 [in MetaCoq.Template.Reflect]
needed:6 [in MetaCoq.Template.EtaExpand]
ne:717 [in MetaCoq.SafeChecker.PCUICSafeConversion]
nf':113 [in MetaCoq.PCUIC.PCUICCumulProp]
nf':248 [in MetaCoq.PCUIC.PCUICCumulProp]
nf':306 [in MetaCoq.PCUIC.PCUICCumulProp]
nf':308 [in MetaCoq.PCUIC.PCUICCumulProp]
nf':374 [in MetaCoq.PCUIC.PCUICInductiveInversion]
nf:105 [in MetaCoq.Template.Checker]
nf:112 [in MetaCoq.PCUIC.PCUICCumulProp]
nf:247 [in MetaCoq.PCUIC.PCUICCumulProp]
nf:305 [in MetaCoq.PCUIC.PCUICCumulProp]
nf:307 [in MetaCoq.PCUIC.PCUICCumulProp]
nf:373 [in MetaCoq.PCUIC.PCUICInductiveInversion]
ni:1106 [in MetaCoq.Template.utils.All_Forall]
nl:20 [in MetaCoq.PCUIC.Syntax.PCUICNamelessDef]
nl:22 [in MetaCoq.PCUIC.Syntax.PCUICNamelessDef]
nm:10 [in MetaCoq.Template.TemplateMonad.Extractable]
nm:13 [in MetaCoq.Template.TemplateMonad.Extractable]
nm:15 [in MetaCoq.Template.TemplateMonad.Extractable]
nm:17 [in MetaCoq.Template.TemplateMonad.Extractable]
nm:18 [in MetaCoq.Template.TemplateMonad.Extractable]
nm:21 [in MetaCoq.Template.TemplateMonad.Extractable]
nm:24 [in MetaCoq.Template.TemplateMonad.Extractable]
nnil:15 [in MetaCoq.Erasure.ESpineView]
nnil:42 [in MetaCoq.Erasure.ESpineView]
noconf:54 [in MetaCoq.PCUIC.Syntax.PCUICReflect]
nonnil:173 [in MetaCoq.Erasure.EInduction]
nonnil:261 [in MetaCoq.Erasure.EInduction]
nor:138 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
nor:17 [in MetaCoq.SafeChecker.SafeTemplateChecker]
nor:19 [in MetaCoq.SafeChecker.PCUICSafeConversion]
nor:199 [in MetaCoq.Erasure.ErasureFunction]
nor:21 [in MetaCoq.Erasure.ErasureFunction]
nor:222 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
nor:23 [in MetaCoq.SafeChecker.PCUICConsistency]
nor:303 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
nor:34 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
nor:49 [in MetaCoq.SafeChecker.PCUICSafeChecker]
nor:54 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
nor:63 [in MetaCoq.SafeChecker.PCUICTypeChecker]
nor:7 [in MetaCoq.SafeChecker.Extraction]
nor:8 [in MetaCoq.SafeChecker.SafeTemplateChecker]
not_cofinite:128 [in MetaCoq.PCUIC.PCUICInversion]
not_cofinite:60 [in MetaCoq.PCUIC.PCUICTyping]
no:11 [in MetaCoq.PCUIC.PCUICSN]
no:12 [in MetaCoq.SafeChecker.PCUICSafeReduce]
no:1476 [in MetaCoq.SafeChecker.PCUICSafeReduce]
no:5 [in MetaCoq.PCUIC.PCUICSN]
no:63 [in MetaCoq.SafeChecker.PCUICSafeReduce]
no:68 [in MetaCoq.SafeChecker.PCUICWfReduction]
no:98 [in MetaCoq.SafeChecker.PCUICWfReduction]
npars_ass:268 [in MetaCoq.Template.Environment]
npars_ass:262 [in MetaCoq.Template.Environment]
npars_ass:258 [in MetaCoq.Template.Environment]
npars:105 [in MetaCoq.PCUIC.PCUICInductives]
npars:110 [in MetaCoq.PCUIC.PCUICInductives]
npars:113 [in MetaCoq.PCUIC.PCUICInductives]
npars:117 [in MetaCoq.Template.Environment]
npars:122 [in MetaCoq.Template.Environment]
npars:134 [in MetaCoq.Template.Environment]
npars:182 [in MetaCoq.PCUIC.PCUICTyping]
npars:188 [in MetaCoq.PCUIC.PCUICWfUniverses]
npars:210 [in MetaCoq.Template.TypingWf]
npars:272 [in MetaCoq.Template.Environment]
npars:277 [in MetaCoq.Template.Environment]
npars:55 [in MetaCoq.PCUIC.PCUICInductives]
npars:697 [in MetaCoq.Template.Typing]
npars:71 [in MetaCoq.Erasure.EPretty]
npars:88 [in MetaCoq.PCUIC.PCUICInductives]
npars:91 [in MetaCoq.PCUIC.PCUICInductives]
npars:95 [in MetaCoq.PCUIC.PCUICInductives]
npars:99 [in MetaCoq.PCUIC.PCUICInductives]
npar:150 [in MetaCoq.Erasure.EGlobalEnv]
npar:175 [in MetaCoq.Template.WcbvEval]
npar:246 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
npar:255 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
npar:263 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
npar:33 [in MetaCoq.Template.Typing]
npar:35 [in MetaCoq.PCUIC.Syntax.PCUICCases]
ns:12 [in MetaCoq.PCUIC.utils.PCUICPretty]
ns:58 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
ns:59 [in MetaCoq.Template.AstUtils]
ns:9 [in MetaCoq.Erasure.EPretty]
ns:9 [in MetaCoq.Template.Pretty]
nth:214 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
nth:285 [in MetaCoq.Template.Environment]
nxy:1175 [in MetaCoq.Template.utils.wGraph]
N':1038 [in MetaCoq.PCUIC.PCUICParallelReduction]
N':1049 [in MetaCoq.PCUIC.PCUICParallelReduction]
n':108 [in MetaCoq.PCUIC.Syntax.PCUICReflect]
n':110 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n':111 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n':125 [in MetaCoq.Template.LiftSubst]
n':126 [in MetaCoq.Template.LiftSubst]
n':1310 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
n':14 [in MetaCoq.Erasure.EReflect]
n':154 [in MetaCoq.Erasure.ELiftSubst]
n':155 [in MetaCoq.Erasure.ELiftSubst]
n':166 [in MetaCoq.Template.utils.wGraph]
n':174 [in MetaCoq.Template.utils.wGraph]
n':23 [in MetaCoq.Erasure.EReflect]
N':252 [in MetaCoq.PCUIC.PCUICParallelReduction]
n':281 [in MetaCoq.PCUIC.PCUICWcbvEval]
n':29 [in MetaCoq.Template.Universes]
n':332 [in MetaCoq.Template.EtaExpand]
n':35 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
N':377 [in MetaCoq.PCUIC.PCUICSubstitution]
n':405 [in MetaCoq.PCUIC.PCUICEquality]
N':441 [in MetaCoq.PCUIC.PCUICParallelReduction]
n':457 [in MetaCoq.Erasure.EEtaExpandedFix]
n':615 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
n':79 [in MetaCoq.Template.Universes]
N':841 [in MetaCoq.PCUIC.PCUICReduction]
N':9 [in MetaCoq.PCUIC.PCUICContextReduction]
n0:10 [in MetaCoq.Template.utils.MCList]
N0:255 [in MetaCoq.PCUIC.PCUICParallelReduction]
N0:287 [in MetaCoq.PCUIC.PCUICParallelReduction]
N0:32 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
n0:342 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
n0:391 [in MetaCoq.Template.EtaExpand]
n0:431 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
N0:446 [in MetaCoq.PCUIC.PCUICParallelReduction]
N0:490 [in MetaCoq.PCUIC.PCUICParallelReduction]
n0:62 [in MetaCoq.Template.monad_utils]
N0:847 [in MetaCoq.PCUIC.PCUICReduction]
N0:867 [in MetaCoq.PCUIC.PCUICReduction]
N1:103 [in MetaCoq.PCUIC.PCUICReduction]
N1:105 [in MetaCoq.PCUIC.PCUICConversion]
N1:111 [in MetaCoq.PCUIC.PCUICReduction]
N1:14 [in MetaCoq.Template.Reduction]
N1:19 [in MetaCoq.Template.Reduction]
N1:197 [in MetaCoq.Template.Typing]
N1:205 [in MetaCoq.Template.Typing]
N1:216 [in MetaCoq.Template.Typing]
N1:237 [in MetaCoq.PCUIC.PCUICNormal]
N1:256 [in MetaCoq.PCUIC.PCUICParallelReduction]
N1:273 [in MetaCoq.PCUIC.PCUICReduction]
N1:283 [in MetaCoq.PCUIC.PCUICReduction]
N1:288 [in MetaCoq.PCUIC.PCUICParallelReduction]
N1:33 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
N1:378 [in MetaCoq.Template.Typing]
N1:390 [in MetaCoq.Template.Typing]
n1:396 [in MetaCoq.Template.EtaExpand]
n1:399 [in MetaCoq.Template.EtaExpand]
N1:4 [in MetaCoq.Template.Reduction]
n1:402 [in MetaCoq.Template.EtaExpand]
N1:406 [in MetaCoq.Template.Typing]
N1:447 [in MetaCoq.PCUIC.PCUICParallelReduction]
N1:453 [in MetaCoq.PCUIC.PCUICSR]
N1:463 [in MetaCoq.PCUIC.PCUICSR]
N1:491 [in MetaCoq.PCUIC.PCUICParallelReduction]
N1:848 [in MetaCoq.PCUIC.PCUICReduction]
N1:868 [in MetaCoq.PCUIC.PCUICReduction]
N1:9 [in MetaCoq.Template.Reduction]
N1:98 [in MetaCoq.PCUIC.PCUICConversion]
N2:106 [in MetaCoq.PCUIC.PCUICConversion]
N2:106 [in MetaCoq.PCUIC.PCUICReduction]
N2:114 [in MetaCoq.PCUIC.PCUICReduction]
N2:200 [in MetaCoq.Template.Typing]
N2:208 [in MetaCoq.Template.Typing]
N2:219 [in MetaCoq.Template.Typing]
N2:241 [in MetaCoq.PCUIC.PCUICNormal]
N2:25 [in MetaCoq.Template.Reduction]
N2:277 [in MetaCoq.PCUIC.PCUICReduction]
N2:287 [in MetaCoq.PCUIC.PCUICReduction]
N2:382 [in MetaCoq.Template.Typing]
N2:394 [in MetaCoq.Template.Typing]
N2:410 [in MetaCoq.Template.Typing]
N2:457 [in MetaCoq.PCUIC.PCUICSR]
N2:467 [in MetaCoq.PCUIC.PCUICSR]
N2:861 [in MetaCoq.PCUIC.PCUICReduction]
n:1 [in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
n:1 [in MetaCoq.Template.utils.wGraph]
n:1 [in MetaCoq.Examples.tauto]
n:1 [in MetaCoq.Erasure.ELiftSubst]
n:1 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
n:10 [in MetaCoq.Template.utils.MCArith]
n:10 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
n:10 [in MetaCoq.Template.Checker]
n:10 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
n:10 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:10 [in MetaCoq.Template.Induction]
N:100 [in MetaCoq.Erasure.ELiftSubst]
n:100 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
n:1004 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
n:1006 [in MetaCoq.Template.Typing]
n:101 [in MetaCoq.Erasure.EInduction]
n:101 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
n:101 [in MetaCoq.SafeChecker.PCUICWfEnv]
n:101 [in MetaCoq.Translations.param_cheap_packed]
n:101 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
n:101 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
n:101 [in MetaCoq.Template.AstUtils]
n:1010 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
N:1016 [in MetaCoq.PCUIC.PCUICConversion]
n:1016 [in MetaCoq.PCUIC.PCUICTyping]
n:102 [in MetaCoq.PCUIC.PCUICInductives]
n:102 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:102 [in MetaCoq.Erasure.ELiftSubst]
n:102 [in MetaCoq.PCUIC.Syntax.PCUICReflect]
n:102 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:102 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
n:1020 [in MetaCoq.Template.utils.wGraph]
N:1021 [in MetaCoq.PCUIC.PCUICConversion]
n:1022 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
n:1025 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
N:1027 [in MetaCoq.PCUIC.PCUICParallelReduction]
n:103 [in MetaCoq.PCUIC.PCUICElimination]
n:103 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
n:103 [in MetaCoq.PCUIC.utils.PCUICOnOne]
n:103 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
N:1037 [in MetaCoq.PCUIC.PCUICParallelReduction]
n:104 [in MetaCoq.Erasure.EInduction]
n:104 [in MetaCoq.Erasure.ELiftSubst]
n:104 [in MetaCoq.PCUIC.PCUICContexts]
n:1045 [in MetaCoq.Template.utils.wGraph]
N:1048 [in MetaCoq.PCUIC.PCUICParallelReduction]
n:1049 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
n:105 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
n:105 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
N:105 [in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
n:105 [in MetaCoq.PCUIC.PCUICCanonicity]
n:105 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
N:105 [in MetaCoq.Template.LiftSubst]
n:106 [in MetaCoq.PCUIC.PCUICProgress]
n:106 [in MetaCoq.Examples.tauto]
n:106 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
n:106 [in MetaCoq.PCUIC.PCUICContexts]
n:107 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
n:107 [in MetaCoq.Erasure.EWellformed]
n:107 [in MetaCoq.Translations.param_cheap_packed]
n:107 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
n:1072 [in MetaCoq.Template.utils.All_Forall]
n:108 [in MetaCoq.PCUIC.PCUICInductives]
n:108 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
n:108 [in MetaCoq.Template.LiftSubst]
n:1082 [in MetaCoq.Template.utils.All_Forall]
n:1088 [in MetaCoq.Template.Typing]
n:109 [in MetaCoq.Template.WfAst]
n:109 [in MetaCoq.PCUIC.PCUICAlpha]
N:109 [in MetaCoq.Erasure.ELiftSubst]
n:1096 [in MetaCoq.Template.Typing]
n:11 [in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
n:11 [in MetaCoq.Erasure.EEtaExpandedFix]
n:11 [in MetaCoq.Erasure.EDeps]
n:11 [in MetaCoq.PCUIC.PCUICEtaExpand]
n:11 [in MetaCoq.Template.utils.MCArith]
n:11 [in MetaCoq.Erasure.EEtaExpanded]
n:11 [in MetaCoq.Template.LiftSubst]
n:110 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
n:110 [in MetaCoq.Erasure.Extract]
n:110 [in MetaCoq.PCUIC.PCUICFirstorder]
n:110 [in MetaCoq.Erasure.ELiftSubst]
n:110 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
n:111 [in MetaCoq.Template.WfAst]
n:111 [in MetaCoq.PCUIC.utils.PCUICOnOne]
n:111 [in MetaCoq.SafeChecker.PCUICEqualityDec]
n:112 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
n:112 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:112 [in MetaCoq.Template.Checker]
n:112 [in MetaCoq.PCUIC.PCUICCanonicity]
n:112 [in MetaCoq.Erasure.ERemoveParams]
n:1120 [in MetaCoq.PCUIC.PCUICConfluence]
n:1125 [in MetaCoq.PCUIC.PCUICConfluence]
n:113 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
n:113 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
n:113 [in MetaCoq.PCUIC.PCUICAst]
n:113 [in MetaCoq.Erasure.ERemoveParams]
N:113 [in MetaCoq.Template.LiftSubst]
n:114 [in MetaCoq.Erasure.EInduction]
N:114 [in MetaCoq.Erasure.ELiftSubst]
n:114 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
n:1141 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
n:115 [in MetaCoq.Template.common.uGraph]
n:1151 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
n:1154 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
n:1159 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
n:1159 [in MetaCoq.Template.utils.wGraph]
n:116 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
n:116 [in MetaCoq.PCUIC.PCUICInductives]
n:116 [in MetaCoq.PCUIC.PCUICInductiveInversion]
n:116 [in MetaCoq.PCUIC.PCUICFirstorder]
n:116 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
N:116 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:116 [in MetaCoq.Template.LiftSubst]
n:117 [in MetaCoq.Erasure.EConstructorsAsBlocks]
N:117 [in MetaCoq.Erasure.ELiftSubst]
n:1171 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
n:1171 [in MetaCoq.PCUIC.PCUICReduction]
n:1175 [in MetaCoq.PCUIC.PCUICConfluence]
n:1179 [in MetaCoq.PCUIC.PCUICConfluence]
n:118 [in MetaCoq.Erasure.ELiftSubst]
n:118 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
n:1184 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
n:1185 [in MetaCoq.PCUIC.PCUICReduction]
n:119 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
n:1190 [in MetaCoq.Erasure.ErasureFunction]
n:12 [in MetaCoq.Translations.param_binary]
n:12 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
n:12 [in MetaCoq.Template.Typing]
n:12 [in MetaCoq.Template.utils.MCArith]
n:12 [in MetaCoq.Erasure.Extract]
n:12 [in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
N:12 [in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
n:12 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
n:12 [in MetaCoq.Examples.add_constructor]
n:120 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
n:120 [in MetaCoq.Erasure.EConstructorsAsBlocks]
n:120 [in MetaCoq.Template.common.uGraph]
n:1206 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
n:1207 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
n:121 [in MetaCoq.PCUIC.PCUICEquality]
n:121 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
N:122 [in MetaCoq.Erasure.ELiftSubst]
n:122 [in MetaCoq.Erasure.Prelim]
n:1223 [in MetaCoq.Template.utils.All_Forall]
n:1224 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
n:123 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
n:123 [in MetaCoq.Erasure.ELiftSubst]
n:1235 [in MetaCoq.Template.utils.All_Forall]
n:1236 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
n:1239 [in MetaCoq.Template.utils.All_Forall]
n:124 [in MetaCoq.Erasure.EGlobalEnv]
n:124 [in MetaCoq.Erasure.ERemoveParams]
n:1252 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
N:1256 [in MetaCoq.PCUIC.PCUICConversion]
n:1257 [in MetaCoq.Template.Typing]
N:1259 [in MetaCoq.PCUIC.PCUICConversion]
n:126 [in MetaCoq.Erasure.EInduction]
N:126 [in MetaCoq.Erasure.ELiftSubst]
n:1261 [in MetaCoq.Template.utils.All_Forall]
N:1262 [in MetaCoq.PCUIC.PCUICConversion]
n:1262 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
N:1265 [in MetaCoq.PCUIC.PCUICConversion]
n:127 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
n:127 [in MetaCoq.Template.WfAst]
n:127 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
n:127 [in MetaCoq.Erasure.ELiftSubst]
n:1271 [in MetaCoq.Template.utils.All_Forall]
n:1274 [in MetaCoq.Template.Typing]
n:1277 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
n:128 [in MetaCoq.PCUIC.PCUICSafeLemmata]
n:128 [in MetaCoq.PCUIC.PCUICNormal]
n:1280 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
n:1283 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
n:1285 [in MetaCoq.Template.utils.All_Forall]
n:1286 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
n:1289 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
n:129 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
n:1290 [in MetaCoq.Template.utils.All_Forall]
n:1292 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
n:1295 [in MetaCoq.Template.utils.All_Forall]
n:1299 [in MetaCoq.Template.Typing]
n:13 [in MetaCoq.Template.utils.MCArith]
n:13 [in MetaCoq.PCUIC.PCUICInductiveInversion]
n:13 [in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
n:13 [in MetaCoq.Template.utils.wGraph]
n:13 [in MetaCoq.PCUIC.PCUICContextConversion]
n:13 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
n:13 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:13 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
n:13 [in MetaCoq.Template.Induction]
n:130 [in MetaCoq.Erasure.EInduction]
n:1304 [in MetaCoq.Template.Typing]
n:1304 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
n:1306 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
n:1309 [in MetaCoq.Template.utils.All_Forall]
n:1309 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
n:131 [in MetaCoq.Template.WfAst]
n:131 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
n:131 [in MetaCoq.Template.common.uGraph]
n:131 [in MetaCoq.Erasure.EGlobalEnv]
N:131 [in MetaCoq.Template.LiftSubst]
n:1310 [in MetaCoq.Template.utils.All_Forall]
n:1316 [in MetaCoq.Template.utils.All_Forall]
n:1317 [in MetaCoq.Template.utils.All_Forall]
n:132 [in MetaCoq.Erasure.Extract]
n:132 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:1323 [in MetaCoq.Template.utils.All_Forall]
n:1324 [in MetaCoq.Template.utils.All_Forall]
n:1327 [in MetaCoq.Template.Typing]
n:134 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
n:134 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
n:1341 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
n:1344 [in MetaCoq.Template.utils.All_Forall]
n:1345 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
n:1346 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
n:135 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
n:1350 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
n:1352 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
N:136 [in MetaCoq.Template.Typing]
n:136 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
n:137 [in MetaCoq.PCUIC.PCUICSubstitution]
n:137 [in MetaCoq.Template.EnvironmentTyping]
n:137 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
n:137 [in MetaCoq.Template.TypingWf]
n:138 [in MetaCoq.Template.utils.MCList]
N:138 [in MetaCoq.Erasure.ELiftSubst]
n:138 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:1384 [in MetaCoq.Template.utils.All_Forall]
n:1385 [in MetaCoq.Template.utils.All_Forall]
n:139 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
n:139 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
n:139 [in MetaCoq.Erasure.EWellformed]
n:139 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
n:139 [in MetaCoq.Erasure.ERemoveParams]
n:1395 [in MetaCoq.SafeChecker.PCUICSafeReduce]
n:14 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
n:14 [in MetaCoq.PCUIC.Typing.PCUICInstTyp]
n:14 [in MetaCoq.Translations.param_binary]
n:14 [in MetaCoq.Template.LiftSubst]
N:140 [in MetaCoq.Template.Typing]
n:140 [in MetaCoq.Erasure.ELiftSubst]
n:141 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
n:141 [in MetaCoq.Erasure.Extract]
n:142 [in MetaCoq.Template.utils.MCList]
n:142 [in MetaCoq.Examples.tauto]
n:142 [in MetaCoq.Template.TypingWf]
n:142 [in MetaCoq.PCUIC.PCUICContexts]
n:143 [in MetaCoq.Erasure.EEtaExpandedFix]
n:143 [in MetaCoq.PCUIC.PCUICSubstitution]
n:143 [in MetaCoq.PCUIC.PCUICInductiveInversion]
N:143 [in MetaCoq.Erasure.ELiftSubst]
n:144 [in MetaCoq.Template.common.uGraph]
n:144 [in MetaCoq.Erasure.ERemoveParams]
n:1449 [in MetaCoq.Template.utils.All_Forall]
n:145 [in MetaCoq.Erasure.EEtaExpanded]
n:145 [in MetaCoq.Template.monad_utils]
n:146 [in MetaCoq.Erasure.ELiftSubst]
n:146 [in MetaCoq.Erasure.EGlobalEnv]
n:146 [in MetaCoq.Erasure.ERemoveParams]
n:146 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
n:146 [in MetaCoq.Template.TypingWf]
n:147 [in MetaCoq.Erasure.EEtaExpandedFix]
n:147 [in MetaCoq.PCUIC.PCUICTyping]
n:147 [in MetaCoq.PCUIC.PCUICCanonicity]
n:148 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
n:148 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
n:149 [in MetaCoq.PCUIC.PCUICSubstitution]
n:149 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
n:15 [in MetaCoq.PCUIC.PCUICElimination]
n:15 [in MetaCoq.Erasure.EInduction]
n:15 [in MetaCoq.Template.utils.MCArith]
n:15 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
n:15 [in MetaCoq.PCUIC.Conversion.PCUICOnFreeVarsConv]
n:15 [in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
n:15 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
n:15 [in MetaCoq.Erasure.EOptimizePropDiscr]
n:150 [in MetaCoq.Template.Universes]
n:150 [in MetaCoq.PCUIC.PCUICCanonicity]
n:150 [in MetaCoq.Erasure.EEtaExpanded]
n:150 [in MetaCoq.Template.TypingWf]
n:150 [in MetaCoq.Template.LiftSubst]
n:151 [in MetaCoq.Template.EtaExpand]
n:151 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
n:151 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
n:152 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
n:152 [in MetaCoq.Template.monad_utils]
n:153 [in MetaCoq.Template.EtaExpand]
n:153 [in MetaCoq.PCUIC.PCUICTyping]
n:154 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:154 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
n:155 [in MetaCoq.PCUIC.PCUICSubstitution]
n:1551 [in MetaCoq.Template.utils.All_Forall]
n:1557 [in MetaCoq.Template.utils.All_Forall]
n:156 [in MetaCoq.Erasure.EInlineProjections]
n:156 [in MetaCoq.Erasure.ELiftSubst]
n:156 [in MetaCoq.Template.monad_utils]
n:156 [in MetaCoq.Template.TypingWf]
n:157 [in MetaCoq.Template.utils.All_Forall]
n:157 [in MetaCoq.Erasure.EConstructorsAsBlocks]
n:157 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:158 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
n:158 [in MetaCoq.Template.LiftSubst]
n:159 [in MetaCoq.PCUIC.PCUICWfUniverses]
n:159 [in MetaCoq.Template.WfAst]
N:159 [in MetaCoq.Erasure.ELiftSubst]
n:16 [in MetaCoq.Template.Normal]
n:16 [in MetaCoq.Template.utils.wGraph]
N:16 [in MetaCoq.PCUIC.PCUICConversion]
n:16 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
n:16 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:16 [in MetaCoq.Erasure.EOptimizePropDiscr]
n:16 [in MetaCoq.Template.Induction]
n:160 [in MetaCoq.Template.utils.MCList]
n:160 [in MetaCoq.PCUIC.PCUICInversion]
n:161 [in MetaCoq.Erasure.EInlineProjections]
n:161 [in MetaCoq.Template.Checker]
n:161 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
n:161 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:162 [in MetaCoq.Template.utils.All_Forall]
n:162 [in MetaCoq.PCUIC.PCUICSubstitution]
n:162 [in MetaCoq.Erasure.EConstructorsAsBlocks]
n:162 [in MetaCoq.PCUIC.PCUICFirstorder]
n:162 [in MetaCoq.Template.utils.wGraph]
n:163 [in MetaCoq.PCUIC.PCUICElimination]
n:164 [in MetaCoq.PCUIC.PCUICWfUniverses]
n:164 [in MetaCoq.Erasure.EConstructorsAsBlocks]
n:164 [in MetaCoq.SafeChecker.PCUICErrors]
n:164 [in MetaCoq.PCUIC.PCUICAst]
n:165 [in MetaCoq.Erasure.EDeps]
n:165 [in MetaCoq.Erasure.ErasureProperties]
n:165 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
n:165 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:165 [in MetaCoq.SafeChecker.PCUICEqualityDec]
n:1655 [in MetaCoq.Template.utils.All_Forall]
n:166 [in MetaCoq.Template.monad_utils]
n:1663 [in MetaCoq.Template.utils.All_Forall]
n:167 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
n:1671 [in MetaCoq.Template.utils.All_Forall]
n:1679 [in MetaCoq.Template.utils.All_Forall]
n:168 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
n:169 [in MetaCoq.PCUIC.PCUICSubstitution]
n:169 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
n:169 [in MetaCoq.Erasure.EEtaExpanded]
n:169 [in MetaCoq.Erasure.EOptimizePropDiscr]
n:17 [in MetaCoq.Erasure.EInlineProjections]
n:17 [in MetaCoq.Template.utils.MCArith]
n:17 [in MetaCoq.PCUIC.PCUICFirstorder]
n:17 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
n:17 [in MetaCoq.PCUIC.Syntax.PCUICUnivSubst]
n:170 [in MetaCoq.Template.utils.wGraph]
n:170 [in MetaCoq.Template.monad_utils]
n:170 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
n:170 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:1719 [in MetaCoq.Template.utils.All_Forall]
n:172 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
N:172 [in MetaCoq.PCUIC.PCUICConversion]
n:173 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
n:173 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
n:173 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
n:1739 [in MetaCoq.Template.utils.All_Forall]
n:174 [in MetaCoq.PCUIC.PCUICSubstitution]
n:174 [in MetaCoq.Erasure.ELiftSubst]
n:174 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
n:174 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:174 [in MetaCoq.Erasure.EOptimizePropDiscr]
n:1747 [in MetaCoq.Template.utils.All_Forall]
n:176 [in MetaCoq.Template.utils.All_Forall]
n:176 [in MetaCoq.Erasure.EConstructorsAsBlocks]
n:176 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
n:1763 [in MetaCoq.Template.utils.All_Forall]
n:177 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
n:177 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
N:177 [in MetaCoq.PCUIC.PCUICConversion]
n:1771 [in MetaCoq.Template.utils.All_Forall]
n:178 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
n:178 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:178 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
n:178 [in MetaCoq.Template.LiftSubst]
n:1786 [in MetaCoq.Template.utils.All_Forall]
n:179 [in MetaCoq.PCUIC.PCUICEtaExpand]
n:179 [in MetaCoq.Template.Ast]
n:179 [in MetaCoq.Examples.tauto]
n:18 [in MetaCoq.Template.EtaExpand]
n:18 [in MetaCoq.Erasure.EPretty]
n:18 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
n:18 [in MetaCoq.Template.utils.MCString]
n:18 [in MetaCoq.Erasure.ESpineView]
n:180 [in MetaCoq.Template.utils.All_Forall]
n:180 [in MetaCoq.PCUIC.PCUICSubstitution]
n:180 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
n:180 [in MetaCoq.PCUIC.PCUICContexts]
n:1805 [in MetaCoq.Template.utils.All_Forall]
n:1813 [in MetaCoq.Template.utils.All_Forall]
n:182 [in MetaCoq.Template.monad_utils]
n:182 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:183 [in MetaCoq.PCUIC.PCUICSubstitution]
n:183 [in MetaCoq.Examples.tauto]
n:184 [in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
n:184 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
n:184 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
n:185 [in MetaCoq.PCUIC.PCUICAlpha]
n:185 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
n:185 [in MetaCoq.Erasure.EEtaExpanded]
n:1855 [in MetaCoq.Template.utils.All_Forall]
n:186 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
N:186 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:188 [in MetaCoq.PCUIC.PCUICSubstitution]
n:188 [in MetaCoq.SafeChecker.PCUICSafeReduce]
n:188 [in MetaCoq.Template.monad_utils]
n:188 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:189 [in MetaCoq.Erasure.EConstructorsAsBlocks]
n:189 [in MetaCoq.Erasure.Extract]
n:189 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
n:189 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
n:1894 [in MetaCoq.Template.utils.All_Forall]
n:19 [in MetaCoq.Template.Typing]
n:19 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
n:19 [in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
n:19 [in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
n:19 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
n:19 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:19 [in MetaCoq.Erasure.EGenericMapEnv]
n:190 [in MetaCoq.Template.utils.MCList]
n:1901 [in MetaCoq.Template.utils.All_Forall]
n:191 [in MetaCoq.Erasure.EInduction]
n:192 [in MetaCoq.PCUIC.PCUICSubstitution]
n:192 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
n:193 [in MetaCoq.PCUIC.PCUICProgress]
n:193 [in MetaCoq.PCUIC.PCUICWfUniverses]
n:193 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
n:193 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:194 [in MetaCoq.Template.utils.MCList]
n:194 [in MetaCoq.Template.monad_utils]
n:1949 [in MetaCoq.Template.utils.All_Forall]
n:195 [in MetaCoq.Erasure.EInduction]
n:195 [in MetaCoq.Erasure.EConstructorsAsBlocks]
n:195 [in MetaCoq.PCUIC.PCUICAlpha]
n:196 [in MetaCoq.PCUIC.PCUICSubstitution]
n:196 [in MetaCoq.SafeChecker.PCUICErrors]
n:1963 [in MetaCoq.Template.utils.All_Forall]
n:1964 [in MetaCoq.Template.utils.All_Forall]
n:197 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
n:197 [in MetaCoq.Template.utils.wGraph]
n:1970 [in MetaCoq.Template.utils.All_Forall]
n:1974 [in MetaCoq.Template.utils.All_Forall]
n:198 [in MetaCoq.Erasure.EInduction]
n:198 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
n:198 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
n:1982 [in MetaCoq.Template.utils.All_Forall]
n:2 [in MetaCoq.Erasure.EInduction]
n:2 [in MetaCoq.PCUIC.PCUICRedTypeIrrelevance]
n:2 [in MetaCoq.Translations.param_binary]
n:2 [in MetaCoq.SafeChecker.PCUICConsistency]
n:2 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
n:2 [in MetaCoq.PCUIC.TemplateToPCUICExpanded]
n:2 [in MetaCoq.PCUIC.PCUICContexts]
n:2 [in MetaCoq.Translations.param_original]
n:2 [in MetaCoq.Template.LiftSubst]
n:2 [in MetaCoq.Template.Induction]
n:20 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
n:20 [in MetaCoq.Template.utils.wGraph]
n:20 [in MetaCoq.Template.Environment]
N:20 [in MetaCoq.Template.UnivSubst]
n:20 [in MetaCoq.Template.Pretty]
N:200 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:200 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
n:2002 [in MetaCoq.Template.utils.All_Forall]
n:201 [in MetaCoq.PCUIC.PCUICProgress]
n:201 [in MetaCoq.Erasure.EInduction]
n:201 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
n:201 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:2014 [in MetaCoq.Template.utils.All_Forall]
n:202 [in MetaCoq.Template.utils.MCList]
n:2022 [in MetaCoq.Template.utils.All_Forall]
n:2026 [in MetaCoq.Template.utils.All_Forall]
n:203 [in MetaCoq.PCUIC.PCUICWfUniverses]
n:203 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
n:2032 [in MetaCoq.Template.utils.All_Forall]
n:205 [in MetaCoq.Template.Checker]
n:205 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
n:206 [in MetaCoq.Template.Universes]
n:206 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
n:206 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
n:208 [in MetaCoq.Template.Environment]
n:209 [in MetaCoq.PCUIC.PCUICNormal]
n:209 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
n:21 [in MetaCoq.Template.utils.MCString]
n:21 [in MetaCoq.PCUIC.PCUICInversion]
n:21 [in MetaCoq.PCUIC.utils.PCUICSize]
n:21 [in MetaCoq.PCUIC.TemplateToPCUICExpanded]
n:21 [in MetaCoq.Erasure.EReflect]
n:21 [in MetaCoq.PCUIC.utils.PCUICPretty]
n:210 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
n:211 [in MetaCoq.Erasure.EInduction]
n:211 [in MetaCoq.Template.utils.MCList]
n:211 [in MetaCoq.PCUIC.PCUICAst]
n:211 [in MetaCoq.Erasure.EWcbvEval]
n:213 [in MetaCoq.Erasure.EWcbvEval]
n:2138 [in MetaCoq.Template.utils.All_Forall]
n:214 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:214 [in MetaCoq.Template.Environment]
n:2149 [in MetaCoq.Template.utils.All_Forall]
n:215 [in MetaCoq.Template.utils.MCList]
n:215 [in MetaCoq.PCUIC.PCUICWfUniverses]
n:215 [in MetaCoq.Template.Checker]
n:215 [in MetaCoq.PCUIC.PCUICTyping]
n:215 [in MetaCoq.Erasure.EWcbvEval]
n:2158 [in MetaCoq.Template.utils.All_Forall]
n:216 [in MetaCoq.Template.Environment]
N:217 [in MetaCoq.PCUIC.PCUICReduction]
n:2177 [in MetaCoq.Template.utils.All_Forall]
n:218 [in MetaCoq.Erasure.EEtaExpanded]
n:218 [in MetaCoq.SafeChecker.PCUICEqualityDec]
n:2186 [in MetaCoq.Template.utils.All_Forall]
n:219 [in MetaCoq.Template.Checker]
n:2193 [in MetaCoq.Template.utils.All_Forall]
n:22 [in MetaCoq.Template.utils.MCList]
n:22 [in MetaCoq.Erasure.EInlineProjections]
n:22 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
n:22 [in MetaCoq.Erasure.Extract]
n:22 [in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
n:22 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
n:22 [in MetaCoq.Template.LiftSubst]
n:220 [in MetaCoq.PCUIC.PCUICInductives]
n:220 [in MetaCoq.Template.Ast]
n:220 [in MetaCoq.Template.Environment]
n:2202 [in MetaCoq.Template.utils.All_Forall]
n:221 [in MetaCoq.Template.utils.MCList]
n:221 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
n:2211 [in MetaCoq.Template.utils.All_Forall]
n:2217 [in MetaCoq.Template.utils.All_Forall]
n:222 [in MetaCoq.Erasure.EInduction]
n:222 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
N:222 [in MetaCoq.PCUIC.PCUICReduction]
n:2225 [in MetaCoq.Template.utils.All_Forall]
n:223 [in MetaCoq.Template.Environment]
n:2233 [in MetaCoq.Template.utils.All_Forall]
n:224 [in MetaCoq.PCUIC.PCUICInductives]
N:224 [in MetaCoq.PCUIC.PCUICCumulProp]
n:2243 [in MetaCoq.Template.utils.All_Forall]
n:2247 [in MetaCoq.Template.utils.All_Forall]
n:225 [in MetaCoq.Erasure.EInduction]
n:225 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
n:225 [in MetaCoq.Template.utils.MCList]
n:227 [in MetaCoq.PCUIC.PCUICInductives]
n:227 [in MetaCoq.Template.Checker]
n:228 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:229 [in MetaCoq.Template.utils.MCList]
n:229 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
n:229 [in MetaCoq.PCUIC.PCUICAlpha]
n:229 [in MetaCoq.PCUIC.Syntax.PCUICCases]
n:23 [in MetaCoq.Template.EtaExpand]
n:23 [in MetaCoq.Template.Universes]
n:23 [in MetaCoq.Template.Environment]
N:23 [in MetaCoq.PCUIC.PCUICSpine]
n:230 [in MetaCoq.PCUIC.PCUICProgress]
n:230 [in MetaCoq.PCUIC.PCUICInductives]
n:230 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
n:231 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:232 [in MetaCoq.Template.Universes]
n:232 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
N:232 [in MetaCoq.PCUIC.PCUICCumulProp]
n:232 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
n:233 [in MetaCoq.Template.utils.MCList]
N:233 [in MetaCoq.Template.TypingWf]
n:234 [in MetaCoq.PCUIC.PCUICInductives]
n:234 [in MetaCoq.PCUIC.PCUICAlpha]
n:234 [in MetaCoq.Template.Checker]
n:234 [in MetaCoq.Template.TypingWf]
n:2346 [in MetaCoq.Template.utils.All_Forall]
n:235 [in MetaCoq.Template.common.uGraph]
n:235 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:2351 [in MetaCoq.Template.utils.All_Forall]
n:2356 [in MetaCoq.Template.utils.All_Forall]
n:236 [in MetaCoq.Template.Universes]
n:236 [in MetaCoq.PCUIC.Syntax.PCUICCases]
n:237 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
n:237 [in MetaCoq.Template.utils.MCList]
n:237 [in MetaCoq.PCUIC.PCUICInductives]
n:237 [in MetaCoq.PCUIC.PCUICTyping]
n:237 [in MetaCoq.Erasure.EWcbvEval]
n:238 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
n:24 [in MetaCoq.Erasure.EInduction]
n:24 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
n:24 [in MetaCoq.PCUIC.PCUICInversion]
n:24 [in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
n:24 [in MetaCoq.Template.utils.wGraph]
n:24 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
n:24 [in MetaCoq.Examples.tauto]
n:24 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
n:24 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
n:240 [in MetaCoq.Erasure.EConstructorsAsBlocks]
n:2407 [in MetaCoq.Template.utils.All_Forall]
n:241 [in MetaCoq.PCUIC.PCUICProgress]
n:241 [in MetaCoq.Template.utils.MCList]
n:241 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
n:241 [in MetaCoq.PCUIC.PCUICInductives]
n:241 [in MetaCoq.PCUIC.PCUICSR]
n:241 [in MetaCoq.SafeChecker.PCUICEqualityDec]
n:2414 [in MetaCoq.Template.utils.All_Forall]
n:242 [in MetaCoq.PCUIC.PCUICAst]
n:242 [in MetaCoq.PCUIC.PCUICSR]
n:244 [in MetaCoq.Template.utils.MCList]
n:244 [in MetaCoq.Erasure.EConstructorsAsBlocks]
n:244 [in MetaCoq.Template.utils.wGraph]
n:245 [in MetaCoq.PCUIC.PCUICInductives]
n:245 [in MetaCoq.PCUIC.Syntax.PCUICCases]
n:245 [in MetaCoq.PCUIC.PCUICSR]
n:246 [in MetaCoq.Template.utils.MCList]
n:247 [in MetaCoq.Template.Universes]
n:247 [in MetaCoq.Erasure.EConstructorsAsBlocks]
n:247 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:247 [in MetaCoq.PCUIC.Syntax.PCUICCases]
n:249 [in MetaCoq.PCUIC.PCUICInductives]
n:249 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
n:25 [in MetaCoq.PCUIC.PCUICElimination]
n:25 [in MetaCoq.Erasure.EArities]
n:25 [in MetaCoq.Template.Typing]
n:25 [in MetaCoq.PCUIC.PCUICCasesContexts]
n:25 [in MetaCoq.PCUIC.PCUICContexts]
n:250 [in MetaCoq.PCUIC.PCUICProgress]
n:250 [in MetaCoq.PCUIC.Syntax.PCUICCases]
N:251 [in MetaCoq.PCUIC.PCUICParallelReduction]
n:251 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
n:252 [in MetaCoq.PCUIC.PCUICWcbvEval]
n:253 [in MetaCoq.PCUIC.PCUICInductives]
n:253 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
n:254 [in MetaCoq.Template.utils.MCList]
n:254 [in MetaCoq.PCUIC.PCUICWcbvEval]
n:254 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:256 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
n:256 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
n:256 [in MetaCoq.SafeChecker.PCUICEqualityDec]
n:2560 [in MetaCoq.Template.utils.All_Forall]
n:257 [in MetaCoq.PCUIC.PCUICInductives]
n:257 [in MetaCoq.Template.Ast]
n:259 [in MetaCoq.PCUIC.PCUICProgress]
n:259 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
n:26 [in MetaCoq.Template.utils.All_Forall]
n:26 [in MetaCoq.Template.utils.bytestring]
n:26 [in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
n:26 [in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
n:26 [in MetaCoq.Examples.add_constructor]
n:260 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
n:260 [in MetaCoq.PCUIC.PCUICInductives]
n:260 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
n:262 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
n:262 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
n:262 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:263 [in MetaCoq.PCUIC.PCUICInductives]
n:263 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
n:264 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
n:264 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
n:264 [in MetaCoq.Template.TypingWf]
n:265 [in MetaCoq.Template.utils.All_Forall]
n:265 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
n:265 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
n:265 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
N:268 [in MetaCoq.PCUIC.PCUICCumulProp]
n:268 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:269 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
n:269 [in MetaCoq.Erasure.EEtaExpanded]
n:27 [in MetaCoq.Template.Universes]
n:27 [in MetaCoq.Erasure.EInduction]
n:27 [in MetaCoq.Erasure.EArities]
n:27 [in MetaCoq.PCUIC.PCUICNormal]
n:27 [in MetaCoq.Template.Environment]
n:27 [in MetaCoq.SafeChecker.PCUICSafeChecker]
n:27 [in MetaCoq.Template.LiftSubst]
n:27 [in MetaCoq.Template.Induction]
N:270 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
n:270 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:271 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
n:272 [in MetaCoq.Template.BasicAst]
n:272 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
n:273 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
n:273 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
n:274 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
n:275 [in MetaCoq.Template.utils.All_Forall]
n:275 [in MetaCoq.SafeChecker.PCUICEqualityDec]
n:276 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
n:276 [in MetaCoq.Erasure.EEtaExpanded]
n:277 [in MetaCoq.Template.BasicAst]
n:277 [in MetaCoq.Template.utils.MCList]
n:277 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
n:277 [in MetaCoq.PCUIC.PCUICInductives]
n:277 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:278 [in MetaCoq.Template.Checker]
n:279 [in MetaCoq.Template.BasicAst]
n:279 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:28 [in MetaCoq.Template.Universes]
n:28 [in MetaCoq.Erasure.EInlineProjections]
n:28 [in MetaCoq.Template.Normal]
n:28 [in MetaCoq.Template.utils.wGraph]
n:28 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:280 [in MetaCoq.PCUIC.PCUICWcbvEval]
n:280 [in MetaCoq.SafeChecker.PCUICEqualityDec]
n:281 [in MetaCoq.Template.BasicAst]
n:281 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
n:282 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:283 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:283 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
n:284 [in MetaCoq.Template.utils.MCList]
N:284 [in MetaCoq.PCUIC.PCUICCumulProp]
n:284 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:285 [in MetaCoq.Template.utils.All_Forall]
n:285 [in MetaCoq.Template.common.uGraph]
n:285 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
n:286 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:288 [in MetaCoq.Template.Ast]
n:288 [in MetaCoq.Template.common.uGraph]
n:288 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
n:288 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:289 [in MetaCoq.PCUIC.PCUICSubstitution]
n:291 [in MetaCoq.Template.utils.MCList]
n:291 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:292 [in MetaCoq.Template.BasicAst]
n:292 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
n:292 [in MetaCoq.Template.common.uGraph]
n:294 [in MetaCoq.Erasure.EArities]
n:294 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
n:294 [in MetaCoq.Template.WcbvEval]
n:294 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:295 [in MetaCoq.Template.common.uGraph]
n:296 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:296 [in MetaCoq.Template.WcbvEval]
n:297 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
n:298 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:3 [in MetaCoq.Erasure.ESpineView]
n:3 [in MetaCoq.Template.Pretty]
n:30 [in MetaCoq.Examples.demo]
n:30 [in MetaCoq.Template.TypingWf]
n:30 [in MetaCoq.Template.AstUtils]
n:300 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
n:300 [in MetaCoq.Erasure.EArities]
n:300 [in MetaCoq.Template.common.uGraph]
n:300 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:300 [in MetaCoq.SafeChecker.PCUICSafeReduce]
n:302 [in MetaCoq.Template.utils.MCList]
n:302 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:304 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
n:304 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
n:304 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
n:305 [in MetaCoq.Template.common.uGraph]
n:305 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:306 [in MetaCoq.Template.utils.All_Forall]
n:306 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:307 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
n:307 [in MetaCoq.PCUIC.PCUICInductives]
n:307 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:307 [in MetaCoq.Template.WcbvEval]
N:308 [in MetaCoq.Template.Typing]
n:308 [in MetaCoq.Template.common.uGraph]
n:31 [in MetaCoq.Template.utils.MCList]
n:31 [in MetaCoq.PCUIC.PCUICInversion]
n:31 [in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
n:31 [in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
n:31 [in MetaCoq.Erasure.ESpineView]
n:31 [in MetaCoq.Template.Checker]
n:31 [in MetaCoq.PCUIC.Typing.PCUICWeakeningTyp]
n:31 [in MetaCoq.SafeChecker.PCUICSafeChecker]
n:31 [in MetaCoq.Template.TypingWf]
n:310 [in MetaCoq.Template.BasicAst]
n:310 [in MetaCoq.Template.utils.All_Forall]
n:310 [in MetaCoq.Template.utils.MCList]
n:310 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
n:311 [in MetaCoq.Template.common.uGraph]
n:311 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:312 [in MetaCoq.Template.BasicAst]
n:312 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
n:312 [in MetaCoq.Template.Environment]
N:313 [in MetaCoq.Template.Typing]
n:313 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:313 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
n:314 [in MetaCoq.Template.BasicAst]
n:314 [in MetaCoq.PCUIC.PCUICSR]
n:314 [in MetaCoq.SafeChecker.PCUICSafeChecker]
n:315 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
n:315 [in MetaCoq.Erasure.ERemoveParams]
n:316 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:317 [in MetaCoq.Template.utils.MCList]
n:317 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
n:317 [in MetaCoq.PCUIC.PCUICSubstitution]
n:318 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
n:319 [in MetaCoq.Template.Universes]
n:319 [in MetaCoq.Erasure.ERemoveParams]
n:32 [in MetaCoq.Template.utils.MCList]
n:32 [in MetaCoq.Template.utils.wGraph]
n:32 [in MetaCoq.Template.Environment]
n:32 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
n:321 [in MetaCoq.PCUIC.PCUICWcbvEval]
n:321 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
n:321 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
n:322 [in MetaCoq.Template.Universes]
n:322 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
n:323 [in MetaCoq.Template.utils.MCList]
n:323 [in MetaCoq.Erasure.ERemoveParams]
n:324 [in MetaCoq.PCUIC.PCUICSubstitution]
n:324 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
n:325 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
n:325 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
n:326 [in MetaCoq.Template.common.uGraph]
n:326 [in MetaCoq.SafeChecker.PCUICSafeChecker]
n:327 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
n:33 [in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
n:33 [in MetaCoq.Erasure.ESpineView]
n:33 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
n:33 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
n:33 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:330 [in MetaCoq.Template.EtaExpand]
n:330 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
n:330 [in MetaCoq.SafeChecker.PCUICEqualityDec]
n:332 [in MetaCoq.Erasure.EEtaExpandedFix]
n:332 [in MetaCoq.Template.utils.MCList]
n:332 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
n:334 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:334 [in MetaCoq.Erasure.EWcbvEval]
n:335 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
n:335 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
n:336 [in MetaCoq.Template.EtaExpand]
n:336 [in MetaCoq.Template.common.uGraph]
n:336 [in MetaCoq.SafeChecker.PCUICSafeChecker]
n:337 [in MetaCoq.Erasure.EEtaExpandedFix]
n:337 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
n:338 [in MetaCoq.Template.utils.MCList]
n:338 [in MetaCoq.Erasure.EWcbvEval]
n:34 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
n:34 [in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
n:34 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:340 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
n:341 [in MetaCoq.Template.EtaExpand]
n:341 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
n:341 [in MetaCoq.PCUIC.PCUICSubstitution]
n:342 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
n:343 [in MetaCoq.PCUIC.PCUICProgress]
n:344 [in MetaCoq.Template.EtaExpand]
n:344 [in MetaCoq.Template.utils.MCList]
n:344 [in MetaCoq.Template.TypingWf]
n:345 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
n:346 [in MetaCoq.Template.EtaExpand]
n:346 [in MetaCoq.PCUIC.PCUICWcbvEval]
n:347 [in MetaCoq.Template.TypingWf]
n:348 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
n:349 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
n:35 [in MetaCoq.PCUIC.PCUICElimination]
n:35 [in MetaCoq.PCUIC.PCUICConvCumInversion]
n:35 [in MetaCoq.Erasure.ELiftSubst]
n:35 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
n:350 [in MetaCoq.PCUIC.PCUICWcbvEval]
n:351 [in MetaCoq.PCUIC.PCUICProgress]
n:351 [in MetaCoq.PCUIC.PCUICInductiveInversion]
n:353 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
n:353 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
n:355 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
n:356 [in MetaCoq.Template.Universes]
n:356 [in MetaCoq.PCUIC.PCUICCumulProp]
n:356 [in MetaCoq.SafeChecker.PCUICEqualityDec]
n:357 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:358 [in MetaCoq.Template.Universes]
n:358 [in MetaCoq.Template.utils.MCList]
n:358 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
n:358 [in MetaCoq.PCUIC.PCUICWcbvEval]
N:358 [in MetaCoq.PCUIC.PCUICReduction]
n:359 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
n:359 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:36 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
n:36 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
n:36 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
n:36 [in MetaCoq.Template.Induction]
n:360 [in MetaCoq.Erasure.EEtaExpandedFix]
n:360 [in MetaCoq.PCUIC.PCUICInductiveInversion]
n:360 [in MetaCoq.PCUIC.PCUICContextConversion]
n:362 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:363 [in MetaCoq.PCUIC.PCUICNormal]
N:364 [in MetaCoq.PCUIC.PCUICReduction]
n:365 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
n:365 [in MetaCoq.Erasure.EEtaExpandedFix]
n:366 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
n:366 [in MetaCoq.PCUIC.PCUICInductiveInversion]
n:366 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:367 [in MetaCoq.Template.EtaExpand]
n:367 [in MetaCoq.PCUIC.PCUICSubstitution]
n:367 [in MetaCoq.Erasure.ERemoveParams]
n:369 [in MetaCoq.PCUIC.PCUICCumulProp]
n:37 [in MetaCoq.Erasure.ESubstitution]
n:37 [in MetaCoq.PCUIC.PCUICValidity]
n:37 [in MetaCoq.PCUIC.Conversion.PCUICOnFreeVarsConv]
n:37 [in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
n:37 [in MetaCoq.Template.TypingWf]
n:370 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
n:371 [in MetaCoq.Template.utils.MCList]
n:372 [in MetaCoq.SafeChecker.PCUICEqualityDec]
n:373 [in MetaCoq.Erasure.EWcbvEval]
n:374 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
n:374 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:374 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
n:374 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
n:375 [in MetaCoq.PCUIC.PCUICContextConversion]
n:375 [in MetaCoq.Erasure.ERemoveParams]
N:376 [in MetaCoq.PCUIC.PCUICSubstitution]
n:377 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:377 [in MetaCoq.SafeChecker.PCUICEqualityDec]
n:378 [in MetaCoq.Erasure.EEtaExpandedFix]
n:378 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
n:379 [in MetaCoq.Erasure.ERemoveParams]
n:38 [in MetaCoq.Erasure.EInlineProjections]
n:38 [in MetaCoq.Template.utils.bytestring]
n:38 [in MetaCoq.PCUIC.PCUICFirstorder]
n:38 [in MetaCoq.Template.utils.wGraph]
n:38 [in MetaCoq.Erasure.ELiftSubst]
n:38 [in MetaCoq.Template.TypingWf]
n:38 [in MetaCoq.Template.Induction]
n:381 [in MetaCoq.Template.EtaExpand]
n:382 [in MetaCoq.SafeChecker.PCUICEqualityDec]
n:384 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:385 [in MetaCoq.Erasure.EEtaExpandedFix]
n:386 [in MetaCoq.Template.EtaExpand]
n:389 [in MetaCoq.Template.EtaExpand]
n:389 [in MetaCoq.Template.utils.MCList]
n:389 [in MetaCoq.PCUIC.PCUICWcbvEval]
n:39 [in MetaCoq.Translations.translation_utils]
n:39 [in MetaCoq.PCUIC.PCUICEquality]
n:39 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:39 [in MetaCoq.Template.LiftSubst]
n:391 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:392 [in MetaCoq.Erasure.ERemoveParams]
n:393 [in MetaCoq.PCUIC.PCUICCumulProp]
n:393 [in MetaCoq.PCUIC.PCUICSpine]
n:395 [in MetaCoq.PCUIC.PCUICEquality]
n:395 [in MetaCoq.Erasure.EWcbvEval]
n:396 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
N:397 [in MetaCoq.PCUIC.PCUICSR]
n:397 [in MetaCoq.Erasure.ERemoveParams]
n:398 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
n:398 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
n:399 [in MetaCoq.PCUIC.PCUICEquality]
n:4 [in MetaCoq.Erasure.EInduction]
n:4 [in MetaCoq.Erasure.ESpineView]
n:4 [in MetaCoq.Translations.param_cheap_packed]
n:4 [in MetaCoq.PCUIC.PCUICCanonicity]
n:4 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
n:4 [in MetaCoq.Examples.add_constructor]
n:4 [in MetaCoq.Template.Induction]
n:40 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:40 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
n:40 [in MetaCoq.Erasure.ELiftSubst]
n:40 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
n:400 [in MetaCoq.Template.utils.MCList]
n:400 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
n:400 [in MetaCoq.PCUIC.PCUICSpine]
n:402 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
n:402 [in MetaCoq.PCUIC.PCUICCumulProp]
N:402 [in MetaCoq.PCUIC.PCUICSR]
n:403 [in MetaCoq.Template.EtaExpand]
n:403 [in MetaCoq.PCUIC.PCUICNormal]
n:404 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
n:404 [in MetaCoq.PCUIC.PCUICEquality]
n:404 [in MetaCoq.PCUIC.PCUICSpine]
n:408 [in MetaCoq.Erasure.EEtaExpandedFix]
n:409 [in MetaCoq.Template.utils.MCList]
n:41 [in MetaCoq.Translations.translation_utils]
n:41 [in MetaCoq.Template.utils.wGraph]
n:41 [in MetaCoq.Erasure.Prelim]
n:41 [in MetaCoq.Template.Induction]
n:410 [in MetaCoq.PCUIC.PCUICSpine]
n:411 [in MetaCoq.PCUIC.PCUICCumulProp]
n:411 [in MetaCoq.PCUIC.PCUICEquality]
n:411 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:413 [in MetaCoq.PCUIC.PCUICSpine]
n:414 [in MetaCoq.Template.utils.All_Forall]
n:419 [in MetaCoq.PCUIC.PCUICEquality]
n:42 [in MetaCoq.Erasure.EInlineProjections]
n:42 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
n:42 [in MetaCoq.Template.utils.wGraph]
n:420 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
n:420 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:422 [in MetaCoq.Template.utils.MCList]
N:422 [in MetaCoq.PCUIC.PCUICContextConversion]
n:422 [in MetaCoq.PCUIC.PCUICSpine]
n:423 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:423 [in MetaCoq.PCUIC.PCUICContextConversion]
n:424 [in MetaCoq.Template.utils.All_Forall]
n:424 [in MetaCoq.Template.utils.MCList]
n:427 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
n:427 [in MetaCoq.Erasure.ERemoveParams]
n:429 [in MetaCoq.PCUIC.PCUICEquality]
n:429 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
n:43 [in MetaCoq.Template.utils.wGraph]
n:43 [in MetaCoq.Erasure.ESpineView]
n:43 [in MetaCoq.Template.Environment]
n:43 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
n:43 [in MetaCoq.Template.Induction]
n:431 [in MetaCoq.Template.utils.MCList]
n:433 [in MetaCoq.PCUIC.PCUICInductiveInversion]
n:434 [in MetaCoq.Erasure.EEtaExpandedFix]
n:434 [in MetaCoq.PCUIC.PCUICEquality]
n:435 [in MetaCoq.PCUIC.PCUICInductiveInversion]
n:436 [in MetaCoq.Template.utils.MCList]
n:437 [in MetaCoq.Template.utils.wGraph]
n:44 [in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
n:44 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
n:44 [in MetaCoq.Erasure.ELiftSubst]
n:44 [in MetaCoq.PCUIC.Syntax.PCUICUnivSubst]
N:440 [in MetaCoq.PCUIC.PCUICParallelReduction]
n:441 [in MetaCoq.PCUIC.PCUICEquality]
n:442 [in MetaCoq.Template.utils.MCList]
n:443 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:446 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:446 [in MetaCoq.Template.utils.wGraph]
n:447 [in MetaCoq.Template.utils.MCList]
n:447 [in MetaCoq.PCUIC.PCUICEquality]
N:449 [in MetaCoq.Template.Typing]
n:45 [in MetaCoq.Erasure.Extract]
n:45 [in MetaCoq.PCUIC.PCUICNormal]
n:45 [in MetaCoq.Template.utils.wGraph]
N:45 [in MetaCoq.PCUIC.PCUICConversion]
n:45 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:450 [in MetaCoq.Template.utils.MCList]
n:452 [in MetaCoq.PCUIC.PCUICEquality]
n:452 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:453 [in MetaCoq.Template.utils.MCList]
n:455 [in MetaCoq.Template.utils.All_Forall]
n:456 [in MetaCoq.Erasure.EEtaExpandedFix]
n:456 [in MetaCoq.Template.utils.All_Forall]
n:456 [in MetaCoq.Template.utils.MCList]
n:456 [in MetaCoq.Template.common.uGraph]
n:456 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:4562 [in MetaCoq.SafeChecker.PCUICSafeConversion]
n:4564 [in MetaCoq.SafeChecker.PCUICSafeConversion]
n:457 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
n:458 [in MetaCoq.Template.utils.MCList]
N:46 [in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
n:46 [in MetaCoq.Template.utils.wGraph]
n:46 [in MetaCoq.Erasure.ESpineView]
n:46 [in MetaCoq.Template.Environment]
n:461 [in MetaCoq.PCUIC.PCUICEquality]
n:461 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:462 [in MetaCoq.PCUIC.PCUICInductives]
n:463 [in MetaCoq.Template.utils.MCList]
n:464 [in MetaCoq.PCUIC.PCUICInductives]
n:464 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
n:464 [in MetaCoq.Template.utils.wGraph]
n:466 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
n:468 [in MetaCoq.PCUIC.PCUICInductives]
n:468 [in MetaCoq.Template.utils.wGraph]
n:469 [in MetaCoq.PCUIC.PCUICNormal]
n:469 [in MetaCoq.PCUIC.PCUICEquality]
n:469 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
n:47 [in MetaCoq.Template.utils.All_Forall]
n:47 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
n:47 [in MetaCoq.PCUIC.PCUICFirstorder]
n:47 [in MetaCoq.Erasure.ELiftSubst]
n:47 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
n:470 [in MetaCoq.Template.utils.MCList]
n:470 [in MetaCoq.PCUIC.PCUICTyping]
n:471 [in MetaCoq.PCUIC.PCUICNormal]
N:472 [in MetaCoq.PCUIC.PCUICSubstitution]
n:473 [in MetaCoq.Template.EtaExpand]
n:473 [in MetaCoq.Template.utils.MCList]
n:475 [in MetaCoq.PCUIC.PCUICNormal]
n:476 [in MetaCoq.Template.utils.wGraph]
n:477 [in MetaCoq.Template.EtaExpand]
n:477 [in MetaCoq.Template.utils.MCList]
n:477 [in MetaCoq.PCUIC.PCUICSpine]
N:478 [in MetaCoq.PCUIC.PCUICSubstitution]
n:478 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:479 [in MetaCoq.Erasure.EEtaExpandedFix]
n:48 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
n:48 [in MetaCoq.Erasure.ESpineView]
n:48 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:48 [in MetaCoq.Erasure.EOptimizePropDiscr]
n:481 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:481 [in MetaCoq.PCUIC.PCUICTyping]
n:482 [in MetaCoq.Template.utils.All_Forall]
n:484 [in MetaCoq.Template.utils.All_Forall]
N:484 [in MetaCoq.PCUIC.PCUICSubstitution]
n:484 [in MetaCoq.SafeChecker.PCUICSafeChecker]
n:485 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:485 [in MetaCoq.Template.utils.wGraph]
n:487 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:488 [in MetaCoq.Template.utils.wGraph]
n:49 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
n:49 [in MetaCoq.Template.utils.wGraph]
N:49 [in MetaCoq.PCUIC.PCUICConversion]
n:49 [in MetaCoq.Template.LiftSubst]
n:49 [in MetaCoq.Template.Induction]
n:490 [in MetaCoq.Template.utils.All_Forall]
N:490 [in MetaCoq.PCUIC.PCUICSubstitution]
n:490 [in MetaCoq.Template.utils.wGraph]
n:490 [in MetaCoq.PCUIC.PCUICTyping]
n:491 [in MetaCoq.Template.utils.All_Forall]
n:492 [in MetaCoq.Template.utils.wGraph]
n:494 [in MetaCoq.Examples.tauto]
n:495 [in MetaCoq.Template.Universes]
n:495 [in MetaCoq.Template.utils.All_Forall]
N:496 [in MetaCoq.PCUIC.PCUICSubstitution]
n:496 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:499 [in MetaCoq.PCUIC.PCUICTyping]
n:5 [in MetaCoq.Erasure.EPretty]
n:5 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
n:5 [in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
n:5 [in MetaCoq.Template.utils.wGraph]
n:5 [in MetaCoq.Erasure.ESpineView]
n:5 [in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
n:5 [in MetaCoq.Template.LiftSubst]
n:50 [in MetaCoq.Erasure.ELiftSubst]
n:50 [in MetaCoq.Erasure.Prelim]
n:500 [in MetaCoq.Template.Universes]
n:500 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:502 [in MetaCoq.Template.EnvironmentTyping]
n:502 [in MetaCoq.PCUIC.PCUICInductives]
n:504 [in MetaCoq.Template.utils.MCList]
n:504 [in MetaCoq.PCUIC.PCUICInductiveInversion]
n:505 [in MetaCoq.Template.EnvironmentTyping]
n:505 [in MetaCoq.PCUIC.PCUICSpine]
n:506 [in MetaCoq.Template.Universes]
n:506 [in MetaCoq.Template.utils.MCList]
n:506 [in MetaCoq.PCUIC.PCUICInductiveInversion]
n:507 [in MetaCoq.PCUIC.PCUICSubstitution]
n:507 [in MetaCoq.Template.EnvironmentTyping]
n:51 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
n:51 [in MetaCoq.PCUIC.PCUICContextSubst]
n:510 [in MetaCoq.Template.utils.MCList]
n:510 [in MetaCoq.Template.EnvironmentTyping]
n:514 [in MetaCoq.Template.EnvironmentTyping]
n:514 [in MetaCoq.PCUIC.PCUICInductives]
n:515 [in MetaCoq.Examples.tauto]
n:518 [in MetaCoq.Examples.tauto]
n:52 [in MetaCoq.Erasure.EEtaExpandedFix]
n:52 [in MetaCoq.Template.utils.wGraph]
n:52 [in MetaCoq.SafeChecker.PCUICSafeReduce]
n:52 [in MetaCoq.PCUIC.PCUICSR]
N:52 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:52 [in MetaCoq.Erasure.EOptimizePropDiscr]
n:52 [in MetaCoq.Erasure.Prelim]
n:52 [in MetaCoq.Template.Induction]
n:521 [in MetaCoq.Template.utils.All_Forall]
N:525 [in MetaCoq.PCUIC.PCUICSubstitution]
n:526 [in MetaCoq.Template.utils.MCList]
n:529 [in MetaCoq.PCUIC.PCUICAst]
n:53 [in MetaCoq.PCUIC.PCUICPrincipality]
n:53 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
N:53 [in MetaCoq.PCUIC.PCUICReduction]
n:530 [in MetaCoq.Template.utils.wGraph]
N:531 [in MetaCoq.PCUIC.PCUICSubstitution]
n:537 [in MetaCoq.SafeChecker.PCUICSafeChecker]
n:538 [in MetaCoq.Template.EtaExpand]
n:54 [in MetaCoq.Template.utils.All_Forall]
n:54 [in MetaCoq.Erasure.EOptimizePropDiscr]
N:540 [in MetaCoq.PCUIC.PCUICSpine]
n:541 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
n:542 [in MetaCoq.Template.utils.All_Forall]
n:545 [in MetaCoq.Template.utils.All_Forall]
n:545 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
N:547 [in MetaCoq.PCUIC.PCUICSpine]
n:55 [in MetaCoq.Template.utils.MCList]
n:55 [in MetaCoq.Template.Normal]
N:55 [in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
n:55 [in MetaCoq.Template.utils.wGraph]
n:55 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
N:55 [in MetaCoq.PCUIC.PCUICConversion]
n:55 [in MetaCoq.PCUIC.PCUICContextReduction]
n:55 [in MetaCoq.Template.Induction]
n:550 [in MetaCoq.Template.utils.wGraph]
n:552 [in MetaCoq.Template.utils.All_Forall]
n:555 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
n:557 [in MetaCoq.SafeChecker.PCUICSafeChecker]
n:558 [in MetaCoq.Template.utils.All_Forall]
n:559 [in MetaCoq.Template.Universes]
n:559 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
N:56 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:56 [in MetaCoq.Erasure.EWcbvEval]
n:560 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
n:561 [in MetaCoq.Template.Universes]
n:562 [in MetaCoq.Template.utils.wGraph]
n:563 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
n:563 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
n:563 [in MetaCoq.Template.utils.wGraph]
n:567 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
N:57 [in MetaCoq.Template.LiftSubst]
N:57 [in MetaCoq.PCUIC.PCUICReduction]
n:57 [in MetaCoq.Erasure.Prelim]
n:571 [in MetaCoq.Template.common.uGraph]
n:572 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
n:573 [in MetaCoq.Template.utils.wGraph]
n:574 [in MetaCoq.Template.common.uGraph]
n:576 [in MetaCoq.Template.common.uGraph]
n:578 [in MetaCoq.Template.common.uGraph]
n:579 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:58 [in MetaCoq.PCUIC.PCUICSubstitution]
n:58 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
n:58 [in MetaCoq.Template.utils.wGraph]
n:58 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:58 [in MetaCoq.Template.LiftSubst]
n:581 [in MetaCoq.PCUIC.PCUICSpine]
n:582 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:583 [in MetaCoq.Template.common.uGraph]
n:585 [in MetaCoq.PCUIC.PCUICTyping]
n:586 [in MetaCoq.PCUIC.PCUICInductives]
n:586 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:588 [in MetaCoq.Template.common.uGraph]
n:588 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:588 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
n:589 [in MetaCoq.Template.utils.wGraph]
n:59 [in MetaCoq.Erasure.Extract]
n:59 [in MetaCoq.Template.TypingWf]
n:59 [in MetaCoq.PCUIC.PCUICSpine]
n:591 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
n:591 [in MetaCoq.Template.utils.wGraph]
n:591 [in MetaCoq.PCUIC.PCUICConfluence]
n:592 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:593 [in MetaCoq.PCUIC.PCUICTyping]
n:599 [in MetaCoq.Template.utils.MCList]
n:599 [in MetaCoq.PCUIC.PCUICInductives]
n:599 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
n:6 [in MetaCoq.Erasure.EInduction]
n:6 [in MetaCoq.Template.WfAst]
n:6 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
n:6 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
n:6 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:6 [in MetaCoq.SafeChecker.PCUICConsistency]
n:6 [in MetaCoq.PCUIC.utils.PCUICPretty]
n:60 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
n:60 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:600 [in MetaCoq.PCUIC.PCUICSpine]
n:601 [in MetaCoq.Template.utils.wGraph]
n:602 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
n:603 [in MetaCoq.PCUIC.PCUICConfluence]
n:605 [in MetaCoq.Template.Typing]
n:607 [in MetaCoq.PCUIC.PCUICParallelReduction]
n:61 [in MetaCoq.Template.utils.All_Forall]
N:61 [in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
N:61 [in MetaCoq.PCUIC.PCUICConversion]
n:61 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
n:61 [in MetaCoq.Template.TypingWf]
n:61 [in MetaCoq.Template.AstUtils]
n:61 [in MetaCoq.Erasure.Prelim]
n:610 [in MetaCoq.PCUIC.PCUICSubstitution]
n:610 [in MetaCoq.PCUIC.PCUICParallelReduction]
n:611 [in MetaCoq.PCUIC.PCUICParallelReduction]
n:612 [in MetaCoq.Template.Typing]
n:613 [in MetaCoq.PCUIC.PCUICParallelReduction]
n:613 [in MetaCoq.PCUIC.PCUICConfluence]
n:614 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
n:615 [in MetaCoq.PCUIC.PCUICConfluence]
n:616 [in MetaCoq.SafeChecker.PCUICSafeChecker]
n:617 [in MetaCoq.Template.Typing]
n:617 [in MetaCoq.PCUIC.PCUICConfluence]
n:619 [in MetaCoq.PCUIC.PCUICSubstitution]
n:619 [in MetaCoq.PCUIC.PCUICParallelReduction]
n:619 [in MetaCoq.PCUIC.PCUICConfluence]
n:62 [in MetaCoq.Erasure.EInlineProjections]
n:62 [in MetaCoq.Template.utils.wGraph]
n:62 [in MetaCoq.Erasure.EWcbvEvalInd]
n:62 [in MetaCoq.PCUIC.Typing.PCUICWeakeningTyp]
N:62 [in MetaCoq.Template.LiftSubst]
n:621 [in MetaCoq.PCUIC.PCUICEquality]
n:621 [in MetaCoq.PCUIC.PCUICConfluence]
n:622 [in MetaCoq.Template.Typing]
n:623 [in MetaCoq.PCUIC.PCUICConfluence]
n:625 [in MetaCoq.PCUIC.PCUICConfluence]
n:626 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
n:627 [in MetaCoq.PCUIC.PCUICConfluence]
n:629 [in MetaCoq.PCUIC.PCUICConfluence]
n:63 [in MetaCoq.PCUIC.PCUICInductives]
n:63 [in MetaCoq.Template.utils.wGraph]
n:63 [in MetaCoq.PCUIC.PCUICSpine]
n:63 [in MetaCoq.Erasure.Prelim]
n:631 [in MetaCoq.PCUIC.PCUICConfluence]
N:633 [in MetaCoq.PCUIC.PCUICSubstitution]
n:634 [in MetaCoq.PCUIC.PCUICEquality]
n:634 [in MetaCoq.PCUIC.PCUICConversion]
n:634 [in MetaCoq.SafeChecker.PCUICSafeChecker]
N:637 [in MetaCoq.PCUIC.PCUICSR]
n:64 [in MetaCoq.Template.EtaExpand]
n:64 [in MetaCoq.Erasure.Extract]
N:64 [in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
n:64 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
n:640 [in MetaCoq.Template.utils.wGraph]
n:641 [in MetaCoq.Template.utils.MCList]
n:641 [in MetaCoq.PCUIC.PCUICConfluence]
N:642 [in MetaCoq.PCUIC.PCUICSubstitution]
n:645 [in MetaCoq.Template.utils.MCList]
n:649 [in MetaCoq.Template.utils.MCList]
n:65 [in MetaCoq.Erasure.EArities]
n:65 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
N:65 [in MetaCoq.PCUIC.PCUICConversion]
N:65 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:65 [in MetaCoq.Template.LiftSubst]
n:650 [in MetaCoq.PCUIC.PCUICSpine]
N:651 [in MetaCoq.PCUIC.PCUICSubstitution]
n:653 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
n:656 [in MetaCoq.Template.utils.MCList]
n:66 [in MetaCoq.Erasure.EDeps]
n:66 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:66 [in MetaCoq.Template.Induction]
n:663 [in MetaCoq.PCUIC.PCUICSR]
n:664 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
n:664 [in MetaCoq.PCUIC.PCUICSpine]
n:67 [in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
n:67 [in MetaCoq.PCUIC.PCUICSubstitution]
n:67 [in MetaCoq.Template.Normal]
n:67 [in MetaCoq.Template.utils.wGraph]
n:67 [in MetaCoq.Erasure.EWellformed]
n:67 [in MetaCoq.Template.TypingWf]
n:67 [in MetaCoq.Template.LiftSubst]
n:671 [in MetaCoq.PCUIC.PCUICSpine]
n:673 [in MetaCoq.Template.utils.MCList]
n:673 [in MetaCoq.Template.Typing]
n:679 [in MetaCoq.Template.Typing]
n:68 [in MetaCoq.Template.utils.All_Forall]
N:68 [in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
n:68 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
n:68 [in MetaCoq.Erasure.EAstUtils]
n:68 [in MetaCoq.Template.TypingWf]
n:68 [in MetaCoq.Erasure.Prelim]
n:680 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
n:684 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
n:686 [in MetaCoq.Template.utils.All_Forall]
n:686 [in MetaCoq.Template.utils.MCList]
n:688 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
n:688 [in MetaCoq.PCUIC.PCUICSpine]
n:69 [in MetaCoq.Examples.tauto]
n:69 [in MetaCoq.Erasure.ELiftSubst]
n:690 [in MetaCoq.Template.utils.wGraph]
n:691 [in MetaCoq.Template.utils.MCList]
n:691 [in MetaCoq.PCUIC.PCUICSpine]
n:693 [in MetaCoq.Template.utils.All_Forall]
N:693 [in MetaCoq.PCUIC.PCUICConfluence]
n:693 [in MetaCoq.PCUIC.PCUICSR]
n:695 [in MetaCoq.Template.utils.MCList]
n:697 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
N:698 [in MetaCoq.PCUIC.PCUICConfluence]
n:7 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
n:7 [in MetaCoq.PCUIC.Conversion.PCUICOnFreeVarsConv]
n:7 [in MetaCoq.Erasure.ESpineView]
n:7 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
n:7 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:7 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
n:70 [in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
n:70 [in MetaCoq.PCUIC.PCUICSubstitution]
n:70 [in MetaCoq.PCUIC.PCUICEtaExpand]
n:70 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
n:70 [in MetaCoq.PCUIC.Typing.PCUICWeakeningTyp]
N:70 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:70 [in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
n:70 [in MetaCoq.Template.LiftSubst]
N:700 [in MetaCoq.PCUIC.PCUICParallelReduction]
n:702 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
n:704 [in MetaCoq.Template.utils.MCList]
N:705 [in MetaCoq.PCUIC.PCUICConfluence]
n:707 [in MetaCoq.Template.utils.wGraph]
N:709 [in MetaCoq.PCUIC.PCUICParallelReduction]
n:709 [in MetaCoq.Template.utils.wGraph]
N:709 [in MetaCoq.PCUIC.PCUICConfluence]
n:71 [in MetaCoq.Template.WfAst]
n:71 [in MetaCoq.Template.utils.wGraph]
n:71 [in MetaCoq.PCUIC.PCUICConversion]
n:71 [in MetaCoq.Erasure.EGenericMapEnv]
N:715 [in MetaCoq.PCUIC.PCUICConfluence]
N:717 [in MetaCoq.PCUIC.PCUICParallelReduction]
n:72 [in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
n:72 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
N:72 [in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
n:721 [in MetaCoq.PCUIC.PCUICEquality]
N:723 [in MetaCoq.PCUIC.PCUICConfluence]
N:727 [in MetaCoq.PCUIC.PCUICConfluence]
n:73 [in MetaCoq.Template.WfAst]
n:73 [in MetaCoq.PCUIC.PCUICSubstitution]
n:73 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
n:73 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
n:73 [in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
N:73 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:732 [in MetaCoq.PCUIC.PCUICInductiveInversion]
N:733 [in MetaCoq.PCUIC.PCUICConfluence]
n:733 [in MetaCoq.SafeChecker.PCUICTypeChecker]
n:74 [in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
n:74 [in MetaCoq.Template.utils.All_Forall]
N:74 [in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
n:74 [in MetaCoq.PCUIC.PCUICInductives]
n:74 [in MetaCoq.Erasure.ELiftSubst]
n:74 [in MetaCoq.PCUIC.PCUICSR]
n:74 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:741 [in MetaCoq.Template.utils.wGraph]
N:741 [in MetaCoq.PCUIC.PCUICConfluence]
n:745 [in MetaCoq.PCUIC.PCUICInductiveInversion]
n:745 [in MetaCoq.SafeChecker.PCUICTypeChecker]
N:748 [in MetaCoq.PCUIC.PCUICConfluence]
n:75 [in MetaCoq.Erasure.Extract]
n:75 [in MetaCoq.Template.utils.wGraph]
n:75 [in MetaCoq.PCUIC.PCUICConversion]
n:75 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
n:75 [in MetaCoq.Erasure.EAstUtils]
N:75 [in MetaCoq.Template.LiftSubst]
n:75 [in MetaCoq.Template.Induction]
n:752 [in MetaCoq.Template.utils.wGraph]
n:753 [in MetaCoq.Template.utils.wGraph]
N:755 [in MetaCoq.PCUIC.PCUICConfluence]
n:758 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
n:76 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
n:76 [in MetaCoq.Erasure.ELiftSubst]
n:76 [in MetaCoq.Erasure.EGenericMapEnv]
n:76 [in MetaCoq.Template.LiftSubst]
N:760 [in MetaCoq.PCUIC.PCUICConfluence]
N:765 [in MetaCoq.PCUIC.PCUICConfluence]
n:77 [in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
n:77 [in MetaCoq.PCUIC.PCUICProgress]
n:77 [in MetaCoq.Template.utils.All_Forall]
n:77 [in MetaCoq.Template.TermEquality]
n:77 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
n:77 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
n:77 [in MetaCoq.Template.Induction]
N:770 [in MetaCoq.PCUIC.PCUICConfluence]
n:773 [in MetaCoq.Template.utils.wGraph]
n:775 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
n:778 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
n:78 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
n:78 [in MetaCoq.Template.Universes]
N:78 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:780 [in MetaCoq.PCUIC.PCUICParallelReduction]
n:785 [in MetaCoq.Template.utils.MCList]
n:79 [in MetaCoq.Template.WfAst]
n:79 [in MetaCoq.Template.utils.wGraph]
n:79 [in MetaCoq.PCUIC.PCUICConversion]
n:79 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
n:79 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:796 [in MetaCoq.PCUIC.PCUICParallelReduction]
n:798 [in MetaCoq.PCUIC.PCUICTyping]
n:8 [in MetaCoq.Erasure.EInduction]
n:8 [in MetaCoq.Template.WfAst]
n:8 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
n:8 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
n:8 [in MetaCoq.PCUIC.PCUICFirstorder]
n:8 [in MetaCoq.Template.UnivSubst]
N:8 [in MetaCoq.PCUIC.PCUICContextReduction]
n:8 [in MetaCoq.Template.LiftSubst]
n:80 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
n:80 [in MetaCoq.PCUIC.PCUICSubstitution]
N:80 [in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
N:80 [in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
n:80 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
N:80 [in MetaCoq.Template.LiftSubst]
n:802 [in MetaCoq.Template.utils.wGraph]
n:802 [in MetaCoq.SafeChecker.PCUICSafeChecker]
n:806 [in MetaCoq.PCUIC.PCUICParallelReduction]
n:807 [in MetaCoq.PCUIC.PCUICParallelReduction]
n:809 [in MetaCoq.PCUIC.PCUICTyping]
n:81 [in MetaCoq.Template.utils.wGraph]
n:81 [in MetaCoq.Template.Environment]
n:81 [in MetaCoq.PCUIC.PCUICCanonicity]
n:818 [in MetaCoq.PCUIC.PCUICTyping]
n:82 [in MetaCoq.Template.WfAst]
n:82 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
n:82 [in MetaCoq.Erasure.ELiftSubst]
n:82 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
N:82 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:82 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
n:822 [in MetaCoq.SafeChecker.PCUICTypeChecker]
n:827 [in MetaCoq.PCUIC.PCUICTyping]
n:827 [in MetaCoq.PCUIC.PCUICSR]
n:827 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
n:83 [in MetaCoq.Erasure.ESubstitution]
n:83 [in MetaCoq.PCUIC.PCUICCumulProp]
n:83 [in MetaCoq.Template.utils.wGraph]
n:83 [in MetaCoq.PCUIC.Typing.PCUICWeakeningTyp]
n:83 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
n:83 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
N:83 [in MetaCoq.Template.LiftSubst]
n:830 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
n:834 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
n:837 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
n:84 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
n:84 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
n:84 [in MetaCoq.Template.LiftSubst]
N:840 [in MetaCoq.PCUIC.PCUICReduction]
n:848 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
n:85 [in MetaCoq.Template.WfAst]
n:85 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
n:85 [in MetaCoq.Template.utils.wGraph]
n:85 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
n:856 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
n:857 [in MetaCoq.SafeChecker.PCUICSafeChecker]
n:86 [in MetaCoq.PCUIC.PCUICInductives]
n:86 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:86 [in MetaCoq.PCUIC.PCUICTyping]
n:86 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
n:865 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
n:867 [in MetaCoq.SafeChecker.PCUICSafeChecker]
n:87 [in MetaCoq.Template.utils.All_Forall]
n:87 [in MetaCoq.PCUIC.PCUICWfUniverses]
N:87 [in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
N:87 [in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
n:872 [in MetaCoq.Template.utils.All_Forall]
n:873 [in MetaCoq.SafeChecker.PCUICSafeChecker]
n:88 [in MetaCoq.PCUIC.PCUICProgress]
n:88 [in MetaCoq.Template.utils.All_Forall]
n:88 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:88 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
n:88 [in MetaCoq.Template.Environment]
N:88 [in MetaCoq.Template.LiftSubst]
n:88 [in MetaCoq.SafeChecker.PCUICEqualityDec]
n:880 [in MetaCoq.Template.utils.All_Forall]
n:883 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
n:885 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
n:885 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
n:889 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
n:89 [in MetaCoq.Erasure.ELiftSubst]
n:89 [in MetaCoq.Template.LiftSubst]
n:895 [in MetaCoq.SafeChecker.PCUICSafeChecker]
N:896 [in MetaCoq.PCUIC.PCUICConversion]
n:897 [in MetaCoq.PCUIC.PCUICInductiveInversion]
n:899 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
n:9 [in MetaCoq.Translations.param_binary]
n:9 [in MetaCoq.Template.utils.All_Forall]
n:9 [in MetaCoq.Template.utils.MCArith]
n:9 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
n:9 [in MetaCoq.Template.utils.wGraph]
n:9 [in MetaCoq.Erasure.ESpineView]
n:9 [in MetaCoq.Erasure.EReflect]
n:90 [in MetaCoq.Template.EtaExpand]
n:90 [in MetaCoq.PCUIC.PCUICWfUniverses]
n:90 [in MetaCoq.Erasure.EWellformed]
n:90 [in MetaCoq.PCUIC.Typing.PCUICWeakeningTyp]
n:90 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
n:90 [in MetaCoq.PCUIC.PCUICSR]
n:90 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
n:901 [in MetaCoq.PCUIC.PCUICInductiveInversion]
N:902 [in MetaCoq.PCUIC.PCUICConversion]
n:908 [in MetaCoq.PCUIC.PCUICTyping]
N:909 [in MetaCoq.PCUIC.PCUICConversion]
n:91 [in MetaCoq.Template.EtaExpand]
n:91 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
n:91 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
n:91 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:91 [in MetaCoq.PCUIC.PCUICAst]
n:912 [in MetaCoq.PCUIC.PCUICParallelReduction]
n:913 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
n:916 [in MetaCoq.Template.utils.MCList]
N:916 [in MetaCoq.PCUIC.PCUICConversion]
n:916 [in MetaCoq.PCUIC.PCUICTyping]
n:92 [in MetaCoq.Template.utils.All_Forall]
n:92 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
n:92 [in MetaCoq.PCUIC.PCUICSubstitution]
n:92 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:92 [in MetaCoq.Erasure.ELiftSubst]
N:92 [in MetaCoq.Template.LiftSubst]
n:921 [in MetaCoq.Template.utils.MCList]
N:923 [in MetaCoq.PCUIC.PCUICConversion]
n:924 [in MetaCoq.PCUIC.PCUICParallelReduction]
N:93 [in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
n:93 [in MetaCoq.PCUIC.PCUICAst]
n:93 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
n:93 [in MetaCoq.Template.LiftSubst]
n:930 [in MetaCoq.PCUIC.PCUICTyping]
n:930 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
n:936 [in MetaCoq.PCUIC.PCUICParallelReduction]
n:938 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
n:94 [in MetaCoq.Erasure.EInduction]
n:94 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
n:94 [in MetaCoq.PCUIC.PCUICCumulProp]
n:94 [in MetaCoq.Erasure.EWellformed]
N:94 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:95 [in MetaCoq.Erasure.EOptimizePropDiscr]
n:95 [in MetaCoq.SafeChecker.PCUICEqualityDec]
n:955 [in MetaCoq.PCUIC.PCUICTyping]
n:96 [in MetaCoq.Template.WfAst]
n:96 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:96 [in MetaCoq.Template.Checker]
N:96 [in MetaCoq.Erasure.ELiftSubst]
n:96 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:96 [in MetaCoq.Template.AstUtils]
n:969 [in MetaCoq.Template.Typing]
n:97 [in MetaCoq.Erasure.ESubstitution]
n:97 [in MetaCoq.PCUIC.PCUICProgress]
n:97 [in MetaCoq.Erasure.ELiftSubst]
n:97 [in MetaCoq.PCUIC.PCUICCanonicity]
n:97 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
N:974 [in MetaCoq.PCUIC.PCUICConfluence]
n:98 [in MetaCoq.Erasure.EInduction]
n:98 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
n:98 [in MetaCoq.PCUIC.PCUICCumulProp]
n:98 [in MetaCoq.PCUIC.PCUICSR]
n:98 [in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
n:984 [in MetaCoq.PCUIC.PCUICTyping]
n:988 [in MetaCoq.Template.Typing]
n:989 [in MetaCoq.PCUIC.PCUICTyping]
n:99 [in MetaCoq.Template.utils.All_Forall]
n:99 [in MetaCoq.Erasure.EArities]
N:99 [in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
n:99 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
n:99 [in MetaCoq.PCUIC.Typing.PCUICWeakeningTyp]
n:99 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
N:99 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
n:995 [in MetaCoq.PCUIC.PCUICTyping]
n:997 [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) |