| 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) |
D (binder)
da:46 [in MetaCoq.Erasure.EInduction]da:48 [in MetaCoq.Erasure.EInduction]
dbody':1060 [in MetaCoq.Erasure.ErasureFunction]
dbody':1061 [in MetaCoq.Erasure.ErasureFunction]
dbody':1075 [in MetaCoq.Erasure.ErasureFunction]
dbody':447 [in MetaCoq.Erasure.ErasureFunction]
dbody':448 [in MetaCoq.Erasure.ErasureFunction]
dbody':457 [in MetaCoq.Erasure.ErasureFunction]
dbody:339 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
debug:13 [in MetaCoq.Translations.param_original]
debug:27 [in MetaCoq.Translations.param_binary]
declc:59 [in MetaCoq.PCUIC.PCUICInductiveInversion]
declc:68 [in MetaCoq.PCUIC.PCUICInductiveInversion]
decli:17 [in MetaCoq.Erasure.ErasureFunction]
decli:30 [in MetaCoq.PCUIC.PCUICInductives]
decli:42 [in MetaCoq.PCUIC.PCUICInductives]
declm:408 [in MetaCoq.PCUIC.PCUICInductives]
declm:422 [in MetaCoq.PCUIC.PCUICInductives]
declm:54 [in MetaCoq.SafeChecker.PCUICTypeChecker]
declm:732 [in MetaCoq.PCUIC.PCUICSR]
decls':1419 [in MetaCoq.Erasure.ErasureFunction]
decls':145 [in MetaCoq.PCUIC.PCUICFirstorder]
decls:1020 [in MetaCoq.Erasure.ErasureFunction]
decls:1025 [in MetaCoq.SafeChecker.PCUICSafeChecker]
decls:1033 [in MetaCoq.Erasure.ErasureFunction]
decls:1040 [in MetaCoq.Erasure.ErasureFunction]
decls:1138 [in MetaCoq.Erasure.ErasureFunction]
decls:1154 [in MetaCoq.Erasure.ErasureFunction]
decls:1177 [in MetaCoq.Erasure.ErasureFunction]
decls:120 [in MetaCoq.Erasure.EEtaExpandedFix]
decls:1208 [in MetaCoq.Erasure.ErasureFunction]
decls:1220 [in MetaCoq.Erasure.ErasureFunction]
decls:1233 [in MetaCoq.Erasure.ErasureFunction]
decls:1248 [in MetaCoq.Erasure.ErasureFunction]
decls:1259 [in MetaCoq.Erasure.ErasureFunction]
decls:1269 [in MetaCoq.Erasure.ErasureFunction]
decls:1277 [in MetaCoq.Erasure.ErasureFunction]
decls:1283 [in MetaCoq.Erasure.ErasureFunction]
decls:1290 [in MetaCoq.Erasure.ErasureFunction]
decls:1304 [in MetaCoq.Erasure.ErasureFunction]
decls:1324 [in MetaCoq.Erasure.ErasureFunction]
decls:1341 [in MetaCoq.Erasure.ErasureFunction]
decls:137 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
decls:1381 [in MetaCoq.Erasure.ErasureFunction]
decls:1403 [in MetaCoq.Erasure.ErasureFunction]
decls:1411 [in MetaCoq.Erasure.ErasureFunction]
decls:1418 [in MetaCoq.Erasure.ErasureFunction]
decls:1420 [in MetaCoq.Erasure.ErasureFunction]
decls:1423 [in MetaCoq.Erasure.ErasureFunction]
decls:1430 [in MetaCoq.Erasure.ErasureFunction]
decls:144 [in MetaCoq.PCUIC.PCUICFirstorder]
decls:1491 [in MetaCoq.Erasure.ErasureFunction]
decls:1499 [in MetaCoq.Erasure.ErasureFunction]
decls:1505 [in MetaCoq.Erasure.ErasureFunction]
decls:1513 [in MetaCoq.Erasure.ErasureFunction]
decls:1519 [in MetaCoq.Erasure.ErasureFunction]
decls:1532 [in MetaCoq.Erasure.ErasureFunction]
decls:1537 [in MetaCoq.Erasure.ErasureFunction]
decls:180 [in MetaCoq.SafeChecker.PCUICWfEnv]
decls:265 [in MetaCoq.Erasure.EEtaExpanded]
decls:432 [in MetaCoq.Template.Checker]
decls:506 [in MetaCoq.Template.EtaExpand]
decls:512 [in MetaCoq.Template.EtaExpand]
decls:518 [in MetaCoq.Template.EtaExpand]
decls:67 [in MetaCoq.Template.AstUtils]
decls:781 [in MetaCoq.Erasure.ErasureFunction]
decls:821 [in MetaCoq.Erasure.ErasureFunction]
decls:934 [in MetaCoq.Erasure.ErasureFunction]
decls:952 [in MetaCoq.Erasure.ErasureFunction]
decl':10 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
decl':132 [in MetaCoq.Erasure.EDeps]
decl':1486 [in MetaCoq.Erasure.ErasureFunction]
decl':170 [in MetaCoq.Erasure.EDeps]
decl':172 [in MetaCoq.Erasure.EDeps]
decl':19 [in MetaCoq.PCUIC.Syntax.PCUICInstDef]
decl':205 [in MetaCoq.PCUIC.PCUICInductiveInversion]
decl':43 [in MetaCoq.SafeChecker.PCUICErrors]
decl':47 [in MetaCoq.SafeChecker.PCUICErrors]
decl':51 [in MetaCoq.SafeChecker.PCUICErrors]
decl':60 [in MetaCoq.PCUIC.TemplateToPCUIC]
decl':760 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
decl':783 [in MetaCoq.PCUIC.PCUICParallelReduction]
decl':8 [in MetaCoq.PCUIC.Syntax.PCUICRenameDef]
decl':829 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
decl':932 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
decl':940 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
decl1:206 [in MetaCoq.PCUIC.PCUICInductiveInversion]
decl1:3 [in MetaCoq.PCUIC.PCUICGlobalEnv]
decl2:207 [in MetaCoq.PCUIC.PCUICInductiveInversion]
decl2:4 [in MetaCoq.PCUIC.PCUICGlobalEnv]
decl:10 [in MetaCoq.Template.EnvironmentTyping]
decl:10 [in MetaCoq.Erasure.EGlobalEnv]
decl:100 [in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
decl:101 [in MetaCoq.PCUIC.PCUICWeakeningEnv]
decl:1017 [in MetaCoq.PCUIC.PCUICTyping]
decl:102 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
decl:1029 [in MetaCoq.Template.Typing]
decl:104 [in MetaCoq.PCUIC.PCUICWeakeningEnv]
decl:104 [in MetaCoq.Erasure.EWcbvEval]
decl:106 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
decl:107 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
decl:1089 [in MetaCoq.Template.Typing]
decl:109 [in MetaCoq.PCUIC.PCUICWeakeningEnv]
decl:1097 [in MetaCoq.Template.Typing]
decl:111 [in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
decl:111 [in MetaCoq.Erasure.ErasureProperties]
decl:113 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
decl:113 [in MetaCoq.PCUIC.PCUICTyping]
decl:113 [in MetaCoq.PCUIC.PCUICCanonicity]
decl:114 [in MetaCoq.Translations.translation_utils]
decl:114 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
decl:114 [in MetaCoq.Erasure.EWcbvEvalInd]
decl:115 [in MetaCoq.PCUIC.PCUICWeakeningEnv]
decl:115 [in MetaCoq.Translations.times_bool_fun]
decl:116 [in MetaCoq.Erasure.EEtaExpandedFix]
decl:117 [in MetaCoq.Translations.times_bool_fun]
decl:117 [in MetaCoq.Erasure.EWellformed]
decl:120 [in MetaCoq.PCUIC.PCUICCanonicity]
decl:122 [in MetaCoq.PCUIC.PCUICWeakeningEnv]
decl:122 [in MetaCoq.Erasure.EGlobalEnv]
decl:125 [in MetaCoq.Template.Typing]
decl:1264 [in MetaCoq.Template.Typing]
decl:127 [in MetaCoq.PCUIC.PCUICFirstorder]
decl:127 [in MetaCoq.Template.Checker]
decl:1275 [in MetaCoq.Template.Typing]
decl:1278 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
decl:1281 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
decl:1284 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
decl:1287 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
decl:1290 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
decl:1293 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
decl:13 [in MetaCoq.Erasure.EPretty]
decl:13 [in MetaCoq.Erasure.EExtends]
decl:1305 [in MetaCoq.Template.Typing]
decl:131 [in MetaCoq.Erasure.EDeps]
decl:132 [in MetaCoq.PCUIC.PCUICCanonicity]
decl:1328 [in MetaCoq.Template.Typing]
decl:133 [in MetaCoq.Translations.times_bool_fun]
decl:134 [in MetaCoq.PCUIC.PCUICProgress]
decl:134 [in MetaCoq.PCUIC.PCUICWeakeningEnv]
decl:135 [in MetaCoq.Translations.times_bool_fun]
decl:135 [in MetaCoq.PCUIC.Syntax.PCUICCases]
decl:137 [in MetaCoq.PCUIC.Syntax.PCUICCases]
decl:139 [in MetaCoq.Translations.translation_utils]
decl:14 [in MetaCoq.Erasure.EEnvMap]
decl:14 [in MetaCoq.Erasure.EGlobalEnv]
decl:140 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
decl:1426 [in MetaCoq.Erasure.ErasureFunction]
decl:144 [in MetaCoq.PCUIC.Syntax.PCUICCases]
decl:145 [in MetaCoq.PCUIC.PCUICInductives]
decl:146 [in MetaCoq.PCUIC.Syntax.PCUICCases]
decl:147 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
decl:147 [in MetaCoq.Erasure.EWellformed]
decl:148 [in MetaCoq.PCUIC.PCUICTyping]
decl:1485 [in MetaCoq.Erasure.ErasureFunction]
decl:15 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
decl:150 [in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
decl:151 [in MetaCoq.PCUIC.Syntax.PCUICCases]
decl:153 [in MetaCoq.PCUIC.Syntax.PCUICCases]
decl:153 [in MetaCoq.Template.Environment]
decl:154 [in MetaCoq.PCUIC.PCUICTyping]
decl:155 [in MetaCoq.PCUIC.Syntax.PCUICCases]
decl:155 [in MetaCoq.Template.Environment]
decl:156 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
decl:157 [in MetaCoq.Template.Environment]
decl:158 [in MetaCoq.Template.WcbvEval]
decl:158 [in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
decl:159 [in MetaCoq.PCUIC.Syntax.PCUICCases]
decl:16 [in MetaCoq.PCUIC.Syntax.PCUICInstDef]
decl:160 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
decl:162 [in MetaCoq.PCUIC.PCUICInversion]
decl:164 [in MetaCoq.Template.Environment]
decl:165 [in MetaCoq.PCUIC.Syntax.PCUICCases]
decl:167 [in MetaCoq.PCUIC.PCUICWfUniverses]
decl:167 [in MetaCoq.PCUIC.PCUICEtaExpand]
decl:169 [in MetaCoq.PCUIC.Syntax.PCUICCases]
decl:17 [in MetaCoq.SafeChecker.PCUICConsistency]
decl:170 [in MetaCoq.PCUIC.PCUICInversion]
decl:171 [in MetaCoq.PCUIC.Syntax.PCUICCases]
decl:179 [in MetaCoq.PCUIC.PCUICSubstitution]
decl:183 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
decl:185 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
decl:19 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
decl:19 [in MetaCoq.Erasure.EExtends]
decl:194 [in MetaCoq.PCUIC.PCUICProgress]
decl:200 [in MetaCoq.PCUIC.PCUICWcbvEval]
decl:202 [in MetaCoq.PCUIC.PCUICProgress]
decl:203 [in MetaCoq.PCUIC.PCUICInductiveInversion]
decl:205 [in MetaCoq.PCUIC.PCUICReduction]
decl:210 [in MetaCoq.SafeChecker.PCUICErrors]
decl:212 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
decl:229 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
decl:231 [in MetaCoq.PCUIC.PCUICProgress]
decl:233 [in MetaCoq.Template.BasicAst]
decl:235 [in MetaCoq.Template.BasicAst]
decl:235 [in MetaCoq.Erasure.EConstructorsAsBlocks]
decl:235 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
decl:237 [in MetaCoq.PCUIC.PCUICParallelReduction]
decl:24 [in MetaCoq.PCUIC.PCUICValidity]
decl:24 [in MetaCoq.PCUIC.Syntax.PCUICInstDef]
decl:242 [in MetaCoq.Erasure.Extract]
decl:243 [in MetaCoq.Template.BasicAst]
decl:247 [in MetaCoq.Template.TypingWf]
decl:26 [in MetaCoq.PCUIC.PCUICInversion]
decl:261 [in MetaCoq.Erasure.EEtaExpanded]
decl:267 [in MetaCoq.Template.EtaExpand]
decl:267 [in MetaCoq.PCUIC.PCUICInductiveInversion]
decl:276 [in MetaCoq.PCUIC.PCUICInductiveInversion]
decl:284 [in MetaCoq.PCUIC.PCUICProgress]
decl:296 [in MetaCoq.Template.Typing]
decl:3 [in MetaCoq.Template.EnvironmentTyping]
decl:30 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
decl:30 [in MetaCoq.PCUIC.PCUICValidity]
decl:302 [in MetaCoq.PCUIC.PCUICInductives]
decl:308 [in MetaCoq.PCUIC.PCUICWcbvEval]
decl:31 [in MetaCoq.PCUIC.Syntax.PCUICInstDef]
decl:316 [in MetaCoq.PCUIC.PCUICSubstitution]
decl:316 [in MetaCoq.Template.WcbvEval]
decl:32 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
decl:32 [in MetaCoq.Template.Normal]
decl:32 [in MetaCoq.Erasure.EGlobalEnv]
decl:32 [in MetaCoq.Examples.add_constructor]
decl:320 [in MetaCoq.PCUIC.PCUICInductives]
decl:323 [in MetaCoq.PCUIC.PCUICSubstitution]
decl:34 [in MetaCoq.Template.EnvMap]
decl:342 [in MetaCoq.Erasure.EWcbvEval]
decl:344 [in MetaCoq.PCUIC.PCUICProgress]
decl:347 [in MetaCoq.Erasure.EArities]
decl:349 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
decl:349 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
decl:349 [in MetaCoq.Erasure.ERemoveParams]
decl:35 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
decl:35 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
decl:35 [in MetaCoq.Erasure.EGlobalEnv]
decl:35 [in MetaCoq.PCUIC.utils.PCUICPretty]
decl:351 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
decl:352 [in MetaCoq.PCUIC.PCUICProgress]
decl:352 [in MetaCoq.PCUIC.PCUICInductives]
decl:355 [in MetaCoq.Erasure.ERemoveParams]
decl:36 [in MetaCoq.Template.EnvMap]
decl:364 [in MetaCoq.PCUIC.PCUICProgress]
decl:368 [in MetaCoq.PCUIC.PCUICNormal]
decl:37 [in MetaCoq.Template.Pretty]
decl:380 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
decl:385 [in MetaCoq.PCUIC.PCUICSR]
decl:398 [in MetaCoq.PCUIC.PCUICWcbvEval]
decl:4 [in MetaCoq.Erasure.EExtends]
decl:40 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
decl:404 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
decl:41 [in MetaCoq.SafeChecker.PCUICErrors]
decl:41 [in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
decl:415 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
decl:417 [in MetaCoq.PCUIC.PCUICSpine]
decl:42 [in MetaCoq.Template.Pretty]
decl:42 [in MetaCoq.PCUIC.PCUICReduction]
decl:420 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
decl:421 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
decl:421 [in MetaCoq.PCUIC.PCUICParallelReduction]
decl:428 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
decl:428 [in MetaCoq.Template.EtaExpand]
decl:438 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
decl:440 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
decl:45 [in MetaCoq.SafeChecker.PCUICErrors]
decl:454 [in MetaCoq.SafeChecker.PCUICSafeChecker]
decl:46 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
decl:464 [in MetaCoq.SafeChecker.PCUICSafeChecker]
decl:47 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
decl:471 [in MetaCoq.PCUIC.PCUICTyping]
decl:48 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
decl:48 [in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
decl:484 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
decl:486 [in MetaCoq.Template.EtaExpand]
decl:49 [in MetaCoq.PCUIC.PCUICInductives]
decl:49 [in MetaCoq.SafeChecker.PCUICErrors]
decl:495 [in MetaCoq.Template.EtaExpand]
decl:496 [in MetaCoq.Examples.tauto]
decl:5 [in MetaCoq.Erasure.EInlineProjections]
decl:509 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
decl:51 [in MetaCoq.Template.EtaExpand]
decl:513 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
decl:514 [in MetaCoq.SafeChecker.PCUICTypeChecker]
decl:526 [in MetaCoq.PCUIC.PCUICTyping]
decl:53 [in MetaCoq.PCUIC.PCUICNormal]
decl:539 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
decl:54 [in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
decl:543 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
decl:548 [in MetaCoq.PCUIC.PCUICSubstitution]
decl:55 [in MetaCoq.PCUIC.PCUICCanonicity]
decl:57 [in MetaCoq.PCUIC.PCUICSubstitution]
decl:575 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
decl:58 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
decl:58 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
decl:58 [in MetaCoq.PCUIC.TemplateToPCUIC]
decl:582 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
decl:583 [in MetaCoq.Template.EnvironmentTyping]
decl:584 [in MetaCoq.PCUIC.PCUICSpine]
decl:586 [in MetaCoq.PCUIC.PCUICTyping]
decl:59 [in MetaCoq.PCUIC.PCUICCanonicity]
decl:594 [in MetaCoq.PCUIC.PCUICTyping]
decl:6 [in MetaCoq.Template.EnvironmentTyping]
decl:60 [in MetaCoq.Template.Environment]
decl:60 [in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
decl:606 [in MetaCoq.Template.Typing]
decl:61 [in MetaCoq.PCUIC.Typing.PCUICWeakeningTyp]
decl:614 [in MetaCoq.PCUIC.PCUICConfluence]
decl:618 [in MetaCoq.PCUIC.PCUICConfluence]
decl:62 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
decl:622 [in MetaCoq.PCUIC.PCUICConfluence]
decl:626 [in MetaCoq.PCUIC.PCUICConfluence]
decl:63 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
decl:630 [in MetaCoq.PCUIC.PCUICConfluence]
decl:634 [in MetaCoq.Template.Typing]
decl:65 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
decl:65 [in MetaCoq.PCUIC.PCUICWcbvEval]
decl:65 [in MetaCoq.Template.WcbvEval]
decl:65 [in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
decl:658 [in MetaCoq.Template.EnvironmentTyping]
decl:66 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
decl:66 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
decl:674 [in MetaCoq.Template.Typing]
decl:68 [in MetaCoq.Erasure.EPretty]
decl:680 [in MetaCoq.Template.Typing]
decl:7 [in MetaCoq.PCUIC.Syntax.PCUICRenameDef]
decl:7 [in MetaCoq.Erasure.EGlobalEnv]
decl:70 [in MetaCoq.Template.AstUtils]
decl:70 [in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
decl:71 [in MetaCoq.Template.Normal]
decl:710 [in MetaCoq.PCUIC.PCUICEquality]
decl:74 [in MetaCoq.Template.EtaExpand]
decl:74 [in MetaCoq.PCUIC.TemplateToPCUICExpanded]
decl:75 [in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
decl:759 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
decl:766 [in MetaCoq.Template.Universes]
decl:77 [in MetaCoq.PCUIC.PCUICSubstitution]
decl:77 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
decl:78 [in MetaCoq.PCUIC.PCUICProgress]
decl:782 [in MetaCoq.PCUIC.PCUICParallelReduction]
decl:79 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
decl:799 [in MetaCoq.PCUIC.PCUICTyping]
decl:8 [in MetaCoq.Erasure.EExtends]
decl:80 [in MetaCoq.Erasure.EPretty]
decl:81 [in MetaCoq.Translations.translation_utils]
decl:81 [in MetaCoq.Translations.times_bool_fun]
decl:828 [in MetaCoq.PCUIC.PCUICSR]
decl:828 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
decl:83 [in MetaCoq.PCUIC.PCUICCanonicity]
decl:849 [in MetaCoq.PCUIC.PCUICTyping]
decl:85 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
decl:85 [in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
decl:851 [in MetaCoq.Erasure.ErasureFunction]
decl:854 [in MetaCoq.PCUIC.PCUICParallelReduction]
decl:86 [in MetaCoq.Translations.times_bool_fun]
decl:87 [in MetaCoq.PCUIC.PCUICTyping]
decl:9 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
decl:909 [in MetaCoq.PCUIC.PCUICTyping]
decl:91 [in MetaCoq.PCUIC.PCUICWeakeningEnv]
decl:917 [in MetaCoq.PCUIC.PCUICTyping]
decl:92 [in MetaCoq.PCUIC.PCUICInversion]
decl:92 [in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
decl:93 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
decl:931 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
decl:935 [in MetaCoq.PCUIC.PCUICTyping]
decl:939 [in MetaCoq.Erasure.ErasureFunction]
decl:939 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
decl:94 [in MetaCoq.PCUIC.PCUICWeakeningEnv]
decl:956 [in MetaCoq.PCUIC.PCUICTyping]
decl:97 [in MetaCoq.Translations.translation_utils]
decl:970 [in MetaCoq.Template.Typing]
decl:996 [in MetaCoq.PCUIC.PCUICTyping]
default:2 [in MetaCoq.Template.utils.MCOption]
default:386 [in MetaCoq.Template.utils.MCList]
default:74 [in MetaCoq.PCUIC.Syntax.PCUICViews]
default:8 [in MetaCoq.PCUIC.TemplateToPCUIC]
defs:117 [in MetaCoq.Erasure.EDeps]
defs:12 [in MetaCoq.Template.WcbvEval]
defs:12 [in MetaCoq.Erasure.ECSubst]
defs:122 [in MetaCoq.Erasure.EDeps]
defs:135 [in MetaCoq.PCUIC.PCUICConvCumInversion]
defs:137 [in MetaCoq.PCUIC.PCUICConvCumInversion]
defs:147 [in MetaCoq.PCUIC.PCUICConvCumInversion]
defs:149 [in MetaCoq.PCUIC.PCUICConvCumInversion]
defs:229 [in MetaCoq.Erasure.Extract]
defs:23 [in MetaCoq.PCUIC.PCUICWcbvEval]
defs:232 [in MetaCoq.Erasure.Extract]
defs:274 [in MetaCoq.PCUIC.PCUICNormal]
defs:280 [in MetaCoq.PCUIC.PCUICNormal]
defs:36 [in MetaCoq.Erasure.EPretty]
defs:36 [in MetaCoq.Erasure.EDeps]
defs:39 [in MetaCoq.Erasure.EDeps]
defs:42 [in MetaCoq.Erasure.EDeps]
defs:49 [in MetaCoq.Erasure.EDeps]
defs:50 [in MetaCoq.PCUIC.utils.PCUICPretty]
defs:60 [in MetaCoq.Template.Pretty]
defs:64 [in MetaCoq.PCUIC.PCUICNormal]
def_ty:179 [in MetaCoq.Template.EtaExpand]
def_ty:109 [in MetaCoq.Template.EtaExpand]
def_ty:91 [in MetaCoq.PCUIC.PCUICEtaExpand]
def_ty:27 [in MetaCoq.PCUIC.PCUICEtaExpand]
def_ty:195 [in MetaCoq.Template.Ast]
def':38 [in MetaCoq.Template.EtaExpand]
def':46 [in MetaCoq.Template.EtaExpand]
def:10 [in MetaCoq.Template.AstUtils]
def:100 [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
def:1008 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
def:107 [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
def:108 [in MetaCoq.Template.EtaExpand]
def:114 [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
def:118 [in MetaCoq.Erasure.EAstUtils]
def:121 [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
def:1222 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
def:1223 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
def:1234 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
def:1235 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
def:1237 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
def:1238 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
def:1239 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
def:1240 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
def:1241 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
def:1242 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
def:1250 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
def:1251 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
def:1260 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
def:1261 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
def:1276 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
def:1279 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
def:1282 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
def:1285 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
def:1288 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
def:1291 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
def:148 [in MetaCoq.PCUIC.PCUICAst]
def:178 [in MetaCoq.Template.EtaExpand]
def:19 [in MetaCoq.Template.EtaExpand]
def:192 [in MetaCoq.Erasure.EEtaExpanded]
def:194 [in MetaCoq.Template.Ast]
def:21 [in MetaCoq.Erasure.EEtaExpandedFix]
def:225 [in MetaCoq.Erasure.EEtaExpanded]
def:259 [in MetaCoq.Template.Universes]
def:26 [in MetaCoq.PCUIC.PCUICEtaExpand]
def:285 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
def:286 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
def:287 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
def:288 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
def:289 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
def:290 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
def:291 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
def:292 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
def:309 [in MetaCoq.Template.Ast]
def:32 [in MetaCoq.Erasure.EAst]
def:33 [in MetaCoq.Erasure.EPretty]
def:374 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
def:376 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
def:381 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
def:413 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
def:426 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
def:45 [in MetaCoq.Template.WfAst]
def:46 [in MetaCoq.Template.BasicAst]
def:479 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
def:48 [in MetaCoq.Template.WfAst]
def:48 [in MetaCoq.PCUIC.utils.PCUICPretty]
def:50 [in MetaCoq.Template.BasicAst]
def:506 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
def:56 [in MetaCoq.Template.WfAst]
def:57 [in MetaCoq.Template.WfAst]
def:57 [in MetaCoq.Template.Pretty]
def:589 [in MetaCoq.PCUIC.PCUICConfluence]
def:590 [in MetaCoq.PCUIC.PCUICConfluence]
def:601 [in MetaCoq.PCUIC.PCUICConfluence]
def:602 [in MetaCoq.PCUIC.PCUICConfluence]
def:616 [in MetaCoq.PCUIC.PCUICConfluence]
def:620 [in MetaCoq.PCUIC.PCUICConfluence]
def:624 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
def:624 [in MetaCoq.PCUIC.PCUICConfluence]
def:628 [in MetaCoq.PCUIC.PCUICConfluence]
def:632 [in MetaCoq.PCUIC.PCUICConfluence]
def:635 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
def:65 [in MetaCoq.Erasure.EEtaExpandedFix]
def:650 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
def:656 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
def:832 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
def:86 [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
def:89 [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
def:90 [in MetaCoq.PCUIC.PCUICEtaExpand]
deps':1276 [in MetaCoq.Erasure.ErasureFunction]
deps':1282 [in MetaCoq.Erasure.ErasureFunction]
deps':839 [in MetaCoq.Erasure.ErasureFunction]
deps':936 [in MetaCoq.Erasure.ErasureFunction]
deps:1019 [in MetaCoq.Erasure.ErasureFunction]
deps:1032 [in MetaCoq.Erasure.ErasureFunction]
deps:1038 [in MetaCoq.Erasure.ErasureFunction]
deps:1146 [in MetaCoq.Erasure.ErasureFunction]
deps:1161 [in MetaCoq.Erasure.ErasureFunction]
deps:1176 [in MetaCoq.Erasure.ErasureFunction]
deps:1228 [in MetaCoq.Erasure.ErasureFunction]
deps:1241 [in MetaCoq.Erasure.ErasureFunction]
deps:1247 [in MetaCoq.Erasure.ErasureFunction]
deps:1258 [in MetaCoq.Erasure.ErasureFunction]
deps:1268 [in MetaCoq.Erasure.ErasureFunction]
deps:1275 [in MetaCoq.Erasure.ErasureFunction]
deps:1281 [in MetaCoq.Erasure.ErasureFunction]
deps:1299 [in MetaCoq.Erasure.ErasureFunction]
deps:1301 [in MetaCoq.Erasure.ErasureFunction]
deps:1323 [in MetaCoq.Erasure.ErasureFunction]
deps:1340 [in MetaCoq.Erasure.ErasureFunction]
deps:1376 [in MetaCoq.Erasure.ErasureFunction]
deps:1398 [in MetaCoq.Erasure.ErasureFunction]
deps:1427 [in MetaCoq.Erasure.ErasureFunction]
deps:1437 [in MetaCoq.Erasure.ErasureFunction]
deps:1487 [in MetaCoq.Erasure.ErasureFunction]
deps:1496 [in MetaCoq.Erasure.ErasureFunction]
deps:1503 [in MetaCoq.Erasure.ErasureFunction]
deps:1510 [in MetaCoq.Erasure.ErasureFunction]
deps:1528 [in MetaCoq.Erasure.ErasureFunction]
deps:1531 [in MetaCoq.Erasure.ErasureFunction]
deps:779 [in MetaCoq.Erasure.ErasureFunction]
deps:789 [in MetaCoq.Erasure.ErasureFunction]
deps:819 [in MetaCoq.Erasure.ErasureFunction]
deps:834 [in MetaCoq.Erasure.ErasureFunction]
deps:838 [in MetaCoq.Erasure.ErasureFunction]
deps:844 [in MetaCoq.Erasure.ErasureFunction]
deps:933 [in MetaCoq.Erasure.ErasureFunction]
deps:951 [in MetaCoq.Erasure.ErasureFunction]
depthA:92 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
depthB:93 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
depth':866 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
depth:1 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
depth:10 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
depth:12 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
depth:14 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
depth:19 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
depth:39 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
depth:4 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
depth:77 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
depth:8 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
depth:85 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
depth:858 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
depth:864 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
Deq:1665 [in MetaCoq.Translations.MiniHoTT]
Deq:1671 [in MetaCoq.Translations.MiniHoTT]
Deq:1673 [in MetaCoq.Translations.MiniHoTT_paths]
Deq:1679 [in MetaCoq.Translations.MiniHoTT_paths]
df:1698 [in MetaCoq.Translations.MiniHoTT]
df:1706 [in MetaCoq.Translations.MiniHoTT_paths]
discr':121 [in MetaCoq.PCUIC.PCUICConvCumInversion]
discr':208 [in MetaCoq.PCUIC.PCUICWcbvEval]
discr':221 [in MetaCoq.PCUIC.PCUICWcbvEval]
discr':281 [in MetaCoq.Erasure.EArities]
discr':383 [in MetaCoq.PCUIC.PCUICNormal]
discr:101 [in MetaCoq.Erasure.EDeps]
discr:101 [in MetaCoq.Erasure.EWcbvEvalInd]
discr:105 [in MetaCoq.PCUIC.PCUICEtaExpand]
discr:110 [in MetaCoq.Erasure.EWcbvEvalInd]
discr:110 [in MetaCoq.Erasure.EWcbvEval]
discr:112 [in MetaCoq.PCUIC.PCUICWcbvEval]
discr:114 [in MetaCoq.Template.WcbvEval]
discr:116 [in MetaCoq.Erasure.EWcbvEval]
discr:117 [in MetaCoq.PCUIC.PCUICConvCumInversion]
discr:119 [in MetaCoq.Erasure.EWcbvEvalInd]
discr:121 [in MetaCoq.PCUIC.PCUICWcbvEval]
discr:121 [in MetaCoq.Erasure.EWcbvEval]
discr:123 [in MetaCoq.Template.WcbvEval]
discr:125 [in MetaCoq.Template.EtaExpand]
discr:131 [in MetaCoq.Erasure.EWcbvEvalInd]
discr:142 [in MetaCoq.Erasure.EWcbvEvalInd]
discr:156 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
discr:165 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
discr:166 [in MetaCoq.Template.WcbvEval]
discr:178 [in MetaCoq.Template.WcbvEval]
discr:199 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
discr:199 [in MetaCoq.Erasure.EEtaExpanded]
discr:200 [in MetaCoq.Template.EtaExpand]
discr:207 [in MetaCoq.PCUIC.PCUICWcbvEval]
discr:208 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
discr:208 [in MetaCoq.Template.Ast]
discr:208 [in MetaCoq.Template.WcbvEval]
discr:216 [in MetaCoq.Erasure.Extract]
discr:217 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
discr:217 [in MetaCoq.Template.WcbvEval]
discr:22 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
discr:220 [in MetaCoq.PCUIC.PCUICWcbvEval]
discr:222 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
discr:232 [in MetaCoq.Erasure.EEtaExpanded]
discr:28 [in MetaCoq.Erasure.EEtaExpandedFix]
discr:280 [in MetaCoq.Erasure.EArities]
discr:29 [in MetaCoq.Erasure.EWcbvEvalInd]
discr:324 [in MetaCoq.Erasure.EArities]
discr:37 [in MetaCoq.PCUIC.PCUICEtaExpand]
discr:37 [in MetaCoq.Erasure.EWcbvEval]
discr:382 [in MetaCoq.PCUIC.PCUICNormal]
discr:393 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
discr:45 [in MetaCoq.Erasure.EWcbvEvalInd]
discr:46 [in MetaCoq.Erasure.EWcbvEval]
discr:5 [in MetaCoq.PCUIC.PCUICProgress]
discr:51 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
discr:54 [in MetaCoq.Erasure.EWcbvEval]
discr:60 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
discr:60 [in MetaCoq.Erasure.EWcbvEvalInd]
discr:71 [in MetaCoq.PCUIC.PCUICWcbvEval]
discr:74 [in MetaCoq.Template.WcbvEval]
discr:75 [in MetaCoq.Erasure.EEtaExpandedFix]
discr:814 [in MetaCoq.SafeChecker.PCUICSafeConversion]
discr:83 [in MetaCoq.PCUIC.PCUICWcbvEval]
discr:84 [in MetaCoq.Template.WcbvEval]
discr:90 [in MetaCoq.Erasure.EWcbvEval]
discr:99 [in MetaCoq.Erasure.EWcbvEval]
dname:338 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
dname:341 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
domsort:225 [in MetaCoq.Template.Universes]
domsort:293 [in MetaCoq.Template.Universes]
dom':196 [in MetaCoq.PCUIC.PCUICConversion]
dom':205 [in MetaCoq.PCUIC.PCUICConversion]
dom':214 [in MetaCoq.PCUIC.PCUICConversion]
dom':221 [in MetaCoq.PCUIC.PCUICConversion]
dom:115 [in MetaCoq.PCUIC.PCUICConversion]
dom:115 [in MetaCoq.PCUIC.PCUICCanonicity]
dom:121 [in MetaCoq.PCUIC.PCUICConversion]
dom:127 [in MetaCoq.PCUIC.PCUICCanonicity]
dom:193 [in MetaCoq.PCUIC.PCUICConversion]
dom:201 [in MetaCoq.PCUIC.PCUICConversion]
dom:210 [in MetaCoq.PCUIC.PCUICConversion]
dom:210 [in MetaCoq.PCUIC.PCUICCanonicity]
dom:220 [in MetaCoq.PCUIC.PCUICConversion]
dom:346 [in MetaCoq.PCUIC.PCUICSpine]
dom:352 [in MetaCoq.PCUIC.PCUICSpine]
dom:365 [in MetaCoq.PCUIC.PCUICSpine]
dom:366 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
dom:465 [in MetaCoq.PCUIC.PCUICConversion]
dom:472 [in MetaCoq.PCUIC.PCUICConversion]
dom:495 [in MetaCoq.SafeChecker.PCUICSafeChecker]
dom:73 [in MetaCoq.Erasure.EOptimizePropDiscr]
dp':17 [in MetaCoq.Template.Kernames]
dp:1 [in MetaCoq.Template.Kernames]
dp:14 [in MetaCoq.Template.Kernames]
dp:4 [in MetaCoq.Template.Kernames]
dp:5 [in MetaCoq.Template.Kernames]
ds:117 [in MetaCoq.Template.Checker]
ds:439 [in MetaCoq.Template.utils.wGraph]
ds:448 [in MetaCoq.Template.utils.wGraph]
dtype:342 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
d':115 [in MetaCoq.PCUIC.utils.PCUICOnOne]
d':118 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
d':121 [in MetaCoq.PCUIC.utils.PCUICOnOne]
d':124 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
d':133 [in MetaCoq.PCUIC.utils.PCUICOnOne]
d':134 [in MetaCoq.PCUIC.PCUICConvCumInversion]
d':1340 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
d':135 [in MetaCoq.Erasure.Extract]
d':137 [in MetaCoq.Erasure.Extract]
d':1376 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
d':1380 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
d':14 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
d':144 [in MetaCoq.Erasure.Extract]
d':146 [in MetaCoq.Erasure.Extract]
d':146 [in MetaCoq.PCUIC.PCUICConvCumInversion]
d':15 [in MetaCoq.PCUIC.PCUICSpine]
d':154 [in MetaCoq.Translations.translation_utils]
d':1657 [in MetaCoq.Template.utils.All_Forall]
d':168 [in MetaCoq.PCUIC.PCUICConfluence]
d':172 [in MetaCoq.PCUIC.PCUICInductiveInversion]
d':1721 [in MetaCoq.Template.utils.All_Forall]
d':173 [in MetaCoq.PCUIC.PCUICConfluence]
d':1761 [in MetaCoq.SafeChecker.PCUICSafeConversion]
d':178 [in MetaCoq.PCUIC.PCUICConfluence]
d':183 [in MetaCoq.PCUIC.PCUICConfluence]
d':186 [in MetaCoq.PCUIC.PCUICInductiveInversion]
d':188 [in MetaCoq.PCUIC.PCUICConversion]
d':189 [in MetaCoq.SafeChecker.PCUICSafeChecker]
d':1928 [in MetaCoq.SafeChecker.PCUICSafeConversion]
d':1930 [in MetaCoq.SafeChecker.PCUICSafeConversion]
d':1933 [in MetaCoq.SafeChecker.PCUICSafeConversion]
d':1937 [in MetaCoq.SafeChecker.PCUICSafeConversion]
d':202 [in MetaCoq.SafeChecker.PCUICSafeChecker]
d':207 [in MetaCoq.PCUIC.PCUICConfluence]
d':210 [in MetaCoq.PCUIC.PCUICEquality]
d':213 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
d':2132 [in MetaCoq.SafeChecker.PCUICSafeConversion]
d':2144 [in MetaCoq.SafeChecker.PCUICSafeConversion]
d':221 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
d':221 [in MetaCoq.PCUIC.PCUICConfluence]
d':226 [in MetaCoq.PCUIC.PCUICConfluence]
d':2262 [in MetaCoq.Template.utils.All_Forall]
d':227 [in MetaCoq.SafeChecker.PCUICSafeChecker]
d':228 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
d':2290 [in MetaCoq.Template.utils.All_Forall]
d':2304 [in MetaCoq.Template.utils.All_Forall]
d':231 [in MetaCoq.PCUIC.PCUICConfluence]
d':2313 [in MetaCoq.Template.utils.All_Forall]
d':2322 [in MetaCoq.Template.utils.All_Forall]
d':236 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
d':236 [in MetaCoq.PCUIC.PCUICConfluence]
d':2396 [in MetaCoq.Template.utils.All_Forall]
d':241 [in MetaCoq.PCUIC.PCUICConfluence]
d':2411 [in MetaCoq.Template.utils.All_Forall]
d':2417 [in MetaCoq.Template.utils.All_Forall]
d':244 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
d':252 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
d':257 [in MetaCoq.Template.utils.MCList]
d':26 [in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
d':26 [in MetaCoq.PCUIC.utils.PCUICOnOne]
d':265 [in MetaCoq.PCUIC.PCUICConfluence]
d':27 [in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
d':273 [in MetaCoq.SafeChecker.PCUICTypeChecker]
d':279 [in MetaCoq.PCUIC.PCUICConfluence]
d':286 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
d':292 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
d':300 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
d':301 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
d':302 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
d':303 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
d':304 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
d':305 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
d':306 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
d':307 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
d':308 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
d':309 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
d':310 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
d':310 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
d':311 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
d':312 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
d':313 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
d':314 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
d':318 [in MetaCoq.PCUIC.PCUICContextConversion]
d':335 [in MetaCoq.PCUIC.PCUICCumulProp]
d':34 [in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
d':342 [in MetaCoq.Template.Environment]
d':348 [in MetaCoq.Template.Environment]
d':353 [in MetaCoq.Template.Environment]
d':360 [in MetaCoq.PCUIC.PCUICSubstitution]
d':369 [in MetaCoq.PCUIC.PCUICWcbvEval]
d':374 [in MetaCoq.SafeChecker.PCUICTypeChecker]
d':376 [in MetaCoq.PCUIC.PCUICWcbvEval]
d':377 [in MetaCoq.PCUIC.PCUICNormal]
d':380 [in MetaCoq.SafeChecker.PCUICTypeChecker]
d':384 [in MetaCoq.Template.EtaExpand]
d':387 [in MetaCoq.Template.BasicAst]
d':390 [in MetaCoq.SafeChecker.PCUICTypeChecker]
d':396 [in MetaCoq.Template.BasicAst]
d':399 [in MetaCoq.SafeChecker.PCUICTypeChecker]
d':405 [in MetaCoq.Template.BasicAst]
d':411 [in MetaCoq.PCUIC.PCUICNormal]
d':412 [in MetaCoq.Template.BasicAst]
d':422 [in MetaCoq.PCUIC.PCUICEquality]
d':449 [in MetaCoq.Erasure.ErasureFunction]
d':450 [in MetaCoq.PCUIC.PCUICInductives]
d':458 [in MetaCoq.Erasure.ErasureFunction]
d':493 [in MetaCoq.Template.Typing]
d':501 [in MetaCoq.Template.utils.MCList]
d':51 [in MetaCoq.PCUIC.utils.PCUICOnOne]
d':513 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
d':522 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
d':525 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
d':58 [in MetaCoq.Translations.translation_utils]
d':584 [in MetaCoq.PCUIC.PCUICEquality]
d':6 [in MetaCoq.PCUIC.PCUICRedTypeIrrelevance]
d':616 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
d':62 [in MetaCoq.Erasure.Extract]
d':624 [in MetaCoq.Erasure.ErasureFunction]
d':626 [in MetaCoq.PCUIC.PCUICParallelReduction]
d':630 [in MetaCoq.Erasure.ErasureFunction]
d':637 [in MetaCoq.PCUIC.PCUICParallelReduction]
d':651 [in MetaCoq.Erasure.ErasureFunction]
d':657 [in MetaCoq.Erasure.ErasureFunction]
d':663 [in MetaCoq.PCUIC.PCUICParallelReduction]
d':67 [in MetaCoq.Translations.translation_utils]
d':67 [in MetaCoq.Erasure.Extract]
d':72 [in MetaCoq.PCUIC.Syntax.PCUICReflect]
d':73 [in MetaCoq.PCUIC.PCUICContextReduction]
d':78 [in MetaCoq.PCUIC.PCUICEquality]
d':78 [in MetaCoq.PCUIC.PCUICAlpha]
d':838 [in MetaCoq.PCUIC.PCUICInductiveInversion]
d':88 [in MetaCoq.PCUIC.PCUICEquality]
d':888 [in MetaCoq.Erasure.ErasureFunction]
d':89 [in MetaCoq.PCUIC.PCUICAlpha]
d':900 [in MetaCoq.Erasure.ErasureFunction]
d':938 [in MetaCoq.PCUIC.PCUICConversion]
d':943 [in MetaCoq.PCUIC.PCUICConversion]
d':952 [in MetaCoq.PCUIC.PCUICConversion]
d':953 [in MetaCoq.PCUIC.PCUICParallelReduction]
d':96 [in MetaCoq.PCUIC.PCUICEquality]
d0:1048 [in MetaCoq.PCUIC.PCUICReduction]
d0:1119 [in MetaCoq.PCUIC.PCUICReduction]
d0:120 [in MetaCoq.PCUIC.PCUICEtaExpand]
d0:123 [in MetaCoq.PCUIC.PCUICEtaExpand]
d0:183 [in MetaCoq.PCUIC.PCUICParallelReduction]
d0:185 [in MetaCoq.PCUIC.PCUICEtaExpand]
d0:186 [in MetaCoq.PCUIC.PCUICEtaExpand]
d0:193 [in MetaCoq.PCUIC.PCUICEtaExpand]
d0:194 [in MetaCoq.PCUIC.PCUICEtaExpand]
d0:239 [in MetaCoq.PCUIC.PCUICConversion]
d0:258 [in MetaCoq.PCUIC.PCUICParallelReduction]
d0:296 [in MetaCoq.Template.EtaExpand]
d0:304 [in MetaCoq.Template.EtaExpand]
d0:353 [in MetaCoq.PCUIC.PCUICParallelReduction]
d0:372 [in MetaCoq.PCUIC.PCUICConfluence]
d0:377 [in MetaCoq.PCUIC.PCUICConfluence]
d0:380 [in MetaCoq.PCUIC.PCUICSubstitution]
d0:444 [in MetaCoq.PCUIC.PCUICConfluence]
d0:449 [in MetaCoq.PCUIC.PCUICConfluence]
d0:451 [in MetaCoq.PCUIC.PCUICParallelReduction]
d0:476 [in MetaCoq.Erasure.EEtaExpandedFix]
d0:87 [in MetaCoq.Erasure.EEtaExpandedFix]
d0:870 [in MetaCoq.PCUIC.PCUICReduction]
d0:90 [in MetaCoq.Erasure.EEtaExpandedFix]
d1:1049 [in MetaCoq.PCUIC.PCUICReduction]
d1:1120 [in MetaCoq.PCUIC.PCUICReduction]
d1:121 [in MetaCoq.PCUIC.PCUICEtaExpand]
d1:124 [in MetaCoq.PCUIC.PCUICEtaExpand]
d1:184 [in MetaCoq.PCUIC.PCUICParallelReduction]
d1:23 [in MetaCoq.Template.Reflect]
d1:240 [in MetaCoq.PCUIC.PCUICConversion]
d1:259 [in MetaCoq.PCUIC.PCUICParallelReduction]
d1:297 [in MetaCoq.Template.EtaExpand]
d1:305 [in MetaCoq.Template.EtaExpand]
d1:354 [in MetaCoq.PCUIC.PCUICParallelReduction]
d1:373 [in MetaCoq.PCUIC.PCUICConfluence]
d1:378 [in MetaCoq.PCUIC.PCUICConfluence]
d1:381 [in MetaCoq.PCUIC.PCUICSubstitution]
d1:39 [in MetaCoq.Erasure.ErasureCorrectness]
d1:40 [in MetaCoq.Erasure.ErasureCorrectness]
d1:41 [in MetaCoq.Erasure.ErasureCorrectness]
d1:42 [in MetaCoq.Erasure.ErasureCorrectness]
d1:445 [in MetaCoq.PCUIC.PCUICConfluence]
d1:450 [in MetaCoq.PCUIC.PCUICConfluence]
d1:452 [in MetaCoq.PCUIC.PCUICParallelReduction]
d1:871 [in MetaCoq.PCUIC.PCUICReduction]
D1:915 [in MetaCoq.Translations.MiniHoTT]
D1:923 [in MetaCoq.Translations.MiniHoTT_paths]
d2:24 [in MetaCoq.Template.Reflect]
D2:916 [in MetaCoq.Translations.MiniHoTT]
D2:924 [in MetaCoq.Translations.MiniHoTT_paths]
d:10 [in MetaCoq.PCUIC.Syntax.PCUICNamelessDef]
d:100 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
d:1000 [in MetaCoq.SafeChecker.PCUICSafeChecker]
d:1001 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
d:1008 [in MetaCoq.PCUIC.PCUICTyping]
d:101 [in MetaCoq.PCUIC.PCUICArities]
d:101 [in MetaCoq.Erasure.EConstructorsAsBlocks]
d:101 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
d:101 [in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
d:1019 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
d:102 [in MetaCoq.Template.Checker]
d:1022 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
d:1023 [in MetaCoq.Erasure.ErasureFunction]
d:1029 [in MetaCoq.Template.utils.wGraph]
d:1037 [in MetaCoq.Template.utils.wGraph]
d:104 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
d:104 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
d:104 [in MetaCoq.Erasure.EOptimizePropDiscr]
d:1041 [in MetaCoq.PCUIC.PCUICReduction]
d:1042 [in MetaCoq.PCUIC.PCUICReduction]
d:1043 [in MetaCoq.PCUIC.PCUICReduction]
d:1044 [in MetaCoq.PCUIC.PCUICReduction]
d:105 [in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
d:1056 [in MetaCoq.Erasure.ErasureFunction]
d:106 [in MetaCoq.Template.Environment]
d:106 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
d:107 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
d:1071 [in MetaCoq.SafeChecker.PCUICTypeChecker]
d:1073 [in MetaCoq.Erasure.ErasureFunction]
d:1078 [in MetaCoq.SafeChecker.PCUICTypeChecker]
d:109 [in MetaCoq.PCUIC.PCUICInductiveInversion]
d:109 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
d:11 [in MetaCoq.Template.EtaExpand]
d:11 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
d:11 [in MetaCoq.Template.TemplateCheckWf]
d:11 [in MetaCoq.Erasure.EAst]
d:11 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
d:11 [in MetaCoq.PCUIC.Syntax.PCUICNamelessDef]
d:110 [in MetaCoq.PCUIC.PCUICEtaExpand]
d:111 [in MetaCoq.Erasure.EEtaExpandedFix]
d:111 [in MetaCoq.Erasure.EGlobalEnv]
d:111 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
d:1112 [in MetaCoq.PCUIC.PCUICReduction]
d:1113 [in MetaCoq.PCUIC.PCUICReduction]
d:1114 [in MetaCoq.PCUIC.PCUICReduction]
d:1115 [in MetaCoq.PCUIC.PCUICReduction]
d:113 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
d:114 [in MetaCoq.PCUIC.utils.PCUICOnOne]
d:114 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
d:115 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
d:115 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
d:116 [in MetaCoq.Template.WfAst]
d:116 [in MetaCoq.PCUIC.PCUICConfluence]
d:1167 [in MetaCoq.Template.utils.wGraph]
d:117 [in MetaCoq.Translations.translation_utils]
d:117 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
d:1176 [in MetaCoq.PCUIC.PCUICConfluence]
D:118 [in MetaCoq.Template.utils.All_Forall]
d:1180 [in MetaCoq.PCUIC.PCUICConfluence]
d:1184 [in MetaCoq.Erasure.ErasureFunction]
d:119 [in MetaCoq.Erasure.EDeps]
d:119 [in MetaCoq.PCUIC.PCUICEtaExpand]
d:119 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
d:119 [in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
d:1195 [in MetaCoq.Template.Typing]
d:12 [in MetaCoq.PCUIC.Typing.PCUICNamelessTyp]
d:12 [in MetaCoq.PCUIC.PCUICContextReduction]
d:120 [in MetaCoq.Erasure.EDeps]
d:120 [in MetaCoq.PCUIC.utils.PCUICOnOne]
d:1204 [in MetaCoq.Template.Typing]
d:121 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
d:122 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
d:1227 [in MetaCoq.Template.Typing]
d:123 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
d:1236 [in MetaCoq.Template.Typing]
d:124 [in MetaCoq.Erasure.EDeps]
d:1249 [in MetaCoq.Translations.MiniHoTT]
d:125 [in MetaCoq.Translations.translation_utils]
d:125 [in MetaCoq.Erasure.EDeps]
d:1257 [in MetaCoq.Translations.MiniHoTT_paths]
d:127 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
d:127 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
d:128 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
d:129 [in MetaCoq.PCUIC.PCUICEtaExpand]
d:13 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
d:13 [in MetaCoq.PCUIC.PCUICAlpha]
d:13 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
d:13 [in MetaCoq.PCUIC.PCUICToTemplate]
D:13 [in MetaCoq.Template.utils.MCProd]
d:13 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
d:130 [in MetaCoq.PCUIC.PCUICEtaExpand]
d:1318 [in MetaCoq.Template.Typing]
d:132 [in MetaCoq.PCUIC.utils.PCUICOnOne]
d:133 [in MetaCoq.Template.EtaExpand]
d:133 [in MetaCoq.PCUIC.PCUICConvCumInversion]
d:133 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
d:1334 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
d:1339 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
d:134 [in MetaCoq.Template.EtaExpand]
d:134 [in MetaCoq.Erasure.Extract]
d:1343 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
d:136 [in MetaCoq.Template.EtaExpand]
d:136 [in MetaCoq.Erasure.Extract]
d:1375 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
d:1378 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
d:139 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
d:14 [in MetaCoq.PCUIC.PCUICToTemplate]
d:14 [in MetaCoq.PCUIC.PCUICSpine]
d:140 [in MetaCoq.Template.EtaExpand]
d:140 [in MetaCoq.PCUIC.PCUICWfUniverses]
d:1400 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
d:141 [in MetaCoq.Erasure.EEtaExpanded]
d:141 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
d:141 [in MetaCoq.Erasure.ERemoveParams]
d:143 [in MetaCoq.Template.BasicAst]
d:143 [in MetaCoq.PCUIC.PCUICArities]
d:143 [in MetaCoq.Erasure.Extract]
d:143 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
d:1443 [in MetaCoq.Erasure.ErasureFunction]
d:1449 [in MetaCoq.Erasure.ErasureFunction]
d:145 [in MetaCoq.Erasure.Extract]
d:145 [in MetaCoq.PCUIC.PCUICConvCumInversion]
d:145 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
d:145 [in MetaCoq.Template.TypingWf]
D:147 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
d:147 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
d:147 [in MetaCoq.Erasure.EEtaExpanded]
d:148 [in MetaCoq.Erasure.ERemoveParams]
d:149 [in MetaCoq.PCUIC.PCUICTyping]
d:149 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
d:149 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
d:149 [in MetaCoq.Template.TypingWf]
d:15 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
d:15 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
d:15 [in MetaCoq.PCUIC.PCUICToTemplate]
D:1507 [in MetaCoq.Translations.MiniHoTT]
d:151 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
d:151 [in MetaCoq.PCUIC.PCUICTyping]
d:151 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
D:1515 [in MetaCoq.Translations.MiniHoTT_paths]
D:1519 [in MetaCoq.Translations.MiniHoTT]
d:152 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
D:1527 [in MetaCoq.Translations.MiniHoTT_paths]
d:153 [in MetaCoq.Template.BasicAst]
d:153 [in MetaCoq.Erasure.ERemoveParams]
d:153 [in MetaCoq.Template.LiftSubst]
d:155 [in MetaCoq.PCUIC.PCUICTyping]
d:155 [in MetaCoq.Erasure.EEtaExpanded]
d:155 [in MetaCoq.Template.LiftSubst]
d:156 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
d:157 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
d:157 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
d:157 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
d:157 [in MetaCoq.SafeChecker.PCUICWfEnv]
d:157 [in MetaCoq.PCUIC.PCUICTyping]
d:157 [in MetaCoq.Template.LiftSubst]
d:159 [in MetaCoq.Erasure.EConstructorsAsBlocks]
d:16 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
d:16 [in MetaCoq.Erasure.Extract]
d:16 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
d:160 [in MetaCoq.PCUIC.PCUICWfUniverses]
d:160 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
d:160 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
d:161 [in MetaCoq.PCUIC.PCUICEtaExpand]
d:161 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
d:162 [in MetaCoq.Erasure.EEtaExpanded]
d:163 [in MetaCoq.SafeChecker.PCUICTypeChecker]
d:164 [in MetaCoq.Erasure.EInlineProjections]
d:164 [in MetaCoq.PCUIC.PCUICInversion]
d:164 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
d:165 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
d:165 [in MetaCoq.PCUIC.PCUICInversion]
d:1656 [in MetaCoq.Template.utils.All_Forall]
d:166 [in MetaCoq.Erasure.EConstructorsAsBlocks]
D:1663 [in MetaCoq.Translations.MiniHoTT]
D:1669 [in MetaCoq.Translations.MiniHoTT]
d:167 [in MetaCoq.Erasure.EInlineProjections]
d:167 [in MetaCoq.PCUIC.PCUICConfluence]
D:1671 [in MetaCoq.Translations.MiniHoTT_paths]
D:1677 [in MetaCoq.Translations.MiniHoTT_paths]
d:168 [in MetaCoq.PCUIC.PCUICArities]
d:169 [in MetaCoq.Template.EnvironmentTyping]
d:169 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
d:169 [in MetaCoq.Template.LiftSubst]
d:17 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
d:17 [in MetaCoq.PCUIC.PCUICAlpha]
d:17 [in MetaCoq.PCUIC.Syntax.PCUICNamelessDef]
d:170 [in MetaCoq.PCUIC.PCUICWfUniverses]
d:171 [in MetaCoq.Erasure.EConstructorsAsBlocks]
d:171 [in MetaCoq.PCUIC.PCUICInductiveInversion]
d:171 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
d:172 [in MetaCoq.Template.EnvironmentTyping]
d:172 [in MetaCoq.PCUIC.PCUICInversion]
d:172 [in MetaCoq.PCUIC.PCUICConfluence]
d:1720 [in MetaCoq.Template.utils.All_Forall]
d:173 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
d:173 [in MetaCoq.PCUIC.PCUICInversion]
d:173 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
d:176 [in MetaCoq.Template.EnvironmentTyping]
d:1760 [in MetaCoq.SafeChecker.PCUICSafeConversion]
d:177 [in MetaCoq.PCUIC.PCUICConfluence]
d:177 [in MetaCoq.Erasure.EOptimizePropDiscr]
d:178 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
d:179 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
d:18 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
d:18 [in MetaCoq.PCUIC.PCUICToTemplate]
d:18 [in MetaCoq.PCUIC.Conversion.PCUICClosedConv]
d:180 [in MetaCoq.PCUIC.PCUICConversion]
d:180 [in MetaCoq.Erasure.EOptimizePropDiscr]
d:181 [in MetaCoq.Erasure.EEtaExpanded]
d:182 [in MetaCoq.Template.BasicAst]
d:182 [in MetaCoq.PCUIC.PCUICCumulProp]
d:182 [in MetaCoq.SafeChecker.PCUICWfEnv]
d:182 [in MetaCoq.PCUIC.PCUICConfluence]
d:183 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
d:183 [in MetaCoq.Template.Environment]
d:185 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
d:185 [in MetaCoq.PCUIC.PCUICInductiveInversion]
d:185 [in MetaCoq.PCUIC.PCUICConversion]
d:186 [in MetaCoq.Template.BasicAst]
d:186 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
d:187 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
D:187 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
d:188 [in MetaCoq.Template.Environment]
d:188 [in MetaCoq.SafeChecker.PCUICSafeChecker]
d:189 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
d:189 [in MetaCoq.Template.BasicAst]
d:189 [in MetaCoq.Template.Environment]
d:1896 [in MetaCoq.Template.utils.All_Forall]
d:19 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
d:19 [in MetaCoq.PCUIC.Syntax.PCUICNamelessDef]
d:1902 [in MetaCoq.Template.utils.All_Forall]
d:1927 [in MetaCoq.SafeChecker.PCUICSafeConversion]
d:1929 [in MetaCoq.SafeChecker.PCUICSafeConversion]
d:193 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
d:1932 [in MetaCoq.SafeChecker.PCUICSafeConversion]
d:1936 [in MetaCoq.SafeChecker.PCUICSafeConversion]
D:1937 [in MetaCoq.Template.utils.All_Forall]
d:194 [in MetaCoq.Template.Environment]
d:194 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
D:1957 [in MetaCoq.Template.utils.All_Forall]
d:196 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
d:2 [in MetaCoq.Template.utils.MCCompare]
d:2 [in MetaCoq.Template.TemplateCheckWf]
d:2 [in MetaCoq.Erasure.EEnvMap]
d:20 [in MetaCoq.PCUIC.PCUICExpandLets]
d:20 [in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
d:20 [in MetaCoq.PCUIC.PCUICToTemplate]
D:20 [in MetaCoq.Template.utils.MCProd]
d:201 [in MetaCoq.SafeChecker.PCUICSafeChecker]
d:202 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
d:204 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
d:204 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
d:206 [in MetaCoq.PCUIC.PCUICConfluence]
d:206 [in MetaCoq.Erasure.EEtaExpanded]
d:208 [in MetaCoq.PCUIC.PCUICInductiveInversion]
d:209 [in MetaCoq.PCUIC.PCUICEquality]
d:209 [in MetaCoq.Erasure.EEtaExpanded]
d:21 [in MetaCoq.Template.EtaExpand]
d:21 [in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
d:21 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
d:21 [in MetaCoq.SafeChecker.PCUICConsistency]
d:21 [in MetaCoq.PCUIC.PCUICToTemplate]
d:210 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
d:210 [in MetaCoq.Template.EtaExpand]
D:210 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
d:212 [in MetaCoq.Template.EtaExpand]
d:212 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
d:2131 [in MetaCoq.SafeChecker.PCUICSafeConversion]
D:2134 [in MetaCoq.Template.utils.All_Forall]
d:214 [in MetaCoq.Template.EtaExpand]
d:214 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
d:2143 [in MetaCoq.SafeChecker.PCUICSafeConversion]
D:2146 [in MetaCoq.Template.utils.All_Forall]
D:215 [in MetaCoq.Template.utils.All_Forall]
d:216 [in MetaCoq.Template.EtaExpand]
d:218 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
d:218 [in MetaCoq.Template.EtaExpand]
d:219 [in MetaCoq.Erasure.EWcbvEval]
d:22 [in MetaCoq.PCUIC.utils.PCUICOnOne]
d:22 [in MetaCoq.PCUIC.PCUICInversion]
d:22 [in MetaCoq.Template.Environment]
d:220 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
d:220 [in MetaCoq.PCUIC.PCUICConfluence]
d:220 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
d:221 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
d:223 [in MetaCoq.Template.EtaExpand]
d:224 [in MetaCoq.Template.EtaExpand]
d:224 [in MetaCoq.Erasure.EWcbvEval]
d:225 [in MetaCoq.Template.BasicAst]
d:225 [in MetaCoq.Erasure.ErasureFunction]
d:225 [in MetaCoq.PCUIC.PCUICConfluence]
d:2255 [in MetaCoq.Template.utils.All_Forall]
d:226 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
D:226 [in MetaCoq.Template.utils.All_Forall]
d:226 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
d:226 [in MetaCoq.SafeChecker.PCUICSafeChecker]
d:2261 [in MetaCoq.Template.utils.All_Forall]
d:227 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
d:228 [in MetaCoq.Template.BasicAst]
d:2289 [in MetaCoq.Template.utils.All_Forall]
d:23 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
d:23 [in MetaCoq.PCUIC.PCUICTyping]
d:23 [in MetaCoq.Template.utils.MCProd]
d:230 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
d:230 [in MetaCoq.Erasure.ErasureFunction]
d:230 [in MetaCoq.PCUIC.PCUICConfluence]
d:230 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
d:2303 [in MetaCoq.Template.utils.All_Forall]
d:231 [in MetaCoq.Erasure.Extract]
d:231 [in MetaCoq.Template.Environment]
d:2312 [in MetaCoq.Template.utils.All_Forall]
d:232 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
d:232 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
d:2321 [in MetaCoq.Template.utils.All_Forall]
d:2328 [in MetaCoq.Template.utils.All_Forall]
d:2334 [in MetaCoq.Template.utils.All_Forall]
d:234 [in MetaCoq.Erasure.Extract]
d:2349 [in MetaCoq.Template.utils.All_Forall]
d:235 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
d:235 [in MetaCoq.PCUIC.PCUICConfluence]
d:2354 [in MetaCoq.Template.utils.All_Forall]
d:2359 [in MetaCoq.Template.utils.All_Forall]
D:237 [in MetaCoq.Template.utils.All_Forall]
D:237 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
d:2395 [in MetaCoq.Template.utils.All_Forall]
d:24 [in MetaCoq.PCUIC.PCUICExpandLets]
d:24 [in MetaCoq.PCUIC.Conversion.PCUICClosedConv]
d:240 [in MetaCoq.PCUIC.PCUICConfluence]
d:240 [in MetaCoq.Erasure.EEtaExpanded]
d:241 [in MetaCoq.Erasure.EEtaExpanded]
d:2410 [in MetaCoq.Template.utils.All_Forall]
d:2418 [in MetaCoq.Template.utils.All_Forall]
d:243 [in MetaCoq.Template.EtaExpand]
d:243 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
d:244 [in MetaCoq.Erasure.EEtaExpanded]
d:245 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
d:245 [in MetaCoq.SafeChecker.PCUICSafeConversion]
d:245 [in MetaCoq.Erasure.EEtaExpanded]
d:246 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
d:2467 [in MetaCoq.Template.utils.All_Forall]
d:247 [in MetaCoq.Template.BasicAst]
d:247 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
d:2472 [in MetaCoq.Template.utils.All_Forall]
d:249 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
d:25 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
d:25 [in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
d:25 [in MetaCoq.PCUIC.utils.PCUICOnOne]
d:250 [in MetaCoq.PCUIC.PCUICCumulProp]
d:251 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
d:252 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
d:253 [in MetaCoq.Template.BasicAst]
d:256 [in MetaCoq.Template.utils.MCList]
d:256 [in MetaCoq.Erasure.EEtaExpanded]
d:256 [in MetaCoq.Template.TypingWf]
D:2562 [in MetaCoq.Template.utils.All_Forall]
D:2566 [in MetaCoq.Template.utils.All_Forall]
d:257 [in MetaCoq.PCUIC.PCUICConversion]
d:258 [in MetaCoq.Template.BasicAst]
d:259 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
d:26 [in MetaCoq.PCUIC.PCUICCumulProp]
d:26 [in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
d:26 [in MetaCoq.Erasure.EExtends]
d:261 [in MetaCoq.Template.EtaExpand]
d:263 [in MetaCoq.PCUIC.PCUICTyping]
d:264 [in MetaCoq.PCUIC.PCUICConfluence]
D:266 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
d:268 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
d:268 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
d:269 [in MetaCoq.PCUIC.PCUICInductives]
d:27 [in MetaCoq.PCUIC.PCUICExpandLets]
d:27 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
d:27 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
d:27 [in MetaCoq.Erasure.EGlobalEnv]
d:27 [in MetaCoq.Erasure.EExtends]
d:27 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
d:27 [in MetaCoq.Erasure.EGenericMapEnv]
d:270 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
d:272 [in MetaCoq.PCUIC.PCUICInductives]
d:272 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
d:272 [in MetaCoq.SafeChecker.PCUICTypeChecker]
d:274 [in MetaCoq.PCUIC.PCUICInductives]
d:275 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
D:276 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
d:278 [in MetaCoq.PCUIC.PCUICConfluence]
d:279 [in MetaCoq.Template.EtaExpand]
d:28 [in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
d:28 [in MetaCoq.Template.EnvMap]
d:28 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
d:28 [in MetaCoq.PCUIC.Conversion.PCUICClosedConv]
d:28 [in MetaCoq.PCUIC.PCUICContexts]
d:284 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
d:285 [in MetaCoq.Erasure.EEtaExpandedFix]
d:285 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
d:285 [in MetaCoq.PCUIC.PCUICTyping]
d:286 [in MetaCoq.Erasure.EEtaExpandedFix]
d:289 [in MetaCoq.PCUIC.PCUICContextConversion]
d:29 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
d:29 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
D:2902 [in MetaCoq.Translations.MiniHoTT]
d:291 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
d:291 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
D:2910 [in MetaCoq.Translations.MiniHoTT_paths]
d:294 [in MetaCoq.Template.EtaExpand]
d:296 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
d:298 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
d:3 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
d:30 [in MetaCoq.PCUIC.PCUICExpandLets]
d:30 [in MetaCoq.Template.EnvMap]
d:30 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
d:300 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
d:301 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
d:301 [in MetaCoq.PCUIC.PCUICAst]
d:301 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
d:304 [in MetaCoq.Erasure.ERemoveParams]
d:306 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
d:306 [in MetaCoq.PCUIC.PCUICAst]
D:306 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
d:307 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
d:308 [in MetaCoq.PCUIC.PCUICInductives]
d:309 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
d:31 [in MetaCoq.Template.Typing]
d:31 [in MetaCoq.PCUIC.PCUICInductiveInversion]
d:31 [in MetaCoq.Template.Environment]
d:31 [in MetaCoq.PCUIC.PCUICTyping]
d:31 [in MetaCoq.Erasure.EExtends]
d:313 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
d:317 [in MetaCoq.PCUIC.PCUICContextConversion]
d:32 [in MetaCoq.PCUIC.PCUICExpandLets]
d:32 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
d:32 [in MetaCoq.Erasure.EExtends]
d:32 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
d:32 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
d:326 [in MetaCoq.PCUIC.PCUICSR]
d:329 [in MetaCoq.PCUIC.PCUICWcbvEval]
d:33 [in MetaCoq.PCUIC.PCUICExpandLets]
d:33 [in MetaCoq.PCUIC.PCUICInductiveInversion]
d:33 [in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
D:33 [in MetaCoq.Template.utils.MCProd]
d:33 [in MetaCoq.PCUIC.Syntax.PCUICNamelessDef]
d:331 [in MetaCoq.PCUIC.PCUICCumulProp]
d:331 [in MetaCoq.PCUIC.PCUICConversion]
d:332 [in MetaCoq.PCUIC.PCUICWcbvEval]
d:338 [in MetaCoq.PCUIC.PCUICConversion]
d:339 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
d:34 [in MetaCoq.Template.EtaExpand]
d:34 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
D:340 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
d:341 [in MetaCoq.Template.Environment]
d:342 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
d:344 [in MetaCoq.Erasure.EEtaExpandedFix]
d:347 [in MetaCoq.Template.Environment]
d:35 [in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
d:35 [in MetaCoq.Template.Pretty]
D:350 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
d:352 [in MetaCoq.PCUIC.PCUICInductiveInversion]
d:352 [in MetaCoq.Template.Environment]
d:357 [in MetaCoq.PCUIC.PCUICContextConversion]
d:359 [in MetaCoq.PCUIC.PCUICSubstitution]
d:359 [in MetaCoq.PCUIC.PCUICSpine]
d:36 [in MetaCoq.Template.EtaExpand]
d:36 [in MetaCoq.Erasure.EEtaExpandedFix]
d:36 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
d:361 [in MetaCoq.PCUIC.PCUICInductiveInversion]
d:362 [in MetaCoq.Erasure.EEtaExpandedFix]
d:364 [in MetaCoq.PCUIC.PCUICTyping]
d:368 [in MetaCoq.PCUIC.PCUICWcbvEval]
d:368 [in MetaCoq.SafeChecker.PCUICTypeChecker]
d:37 [in MetaCoq.Erasure.EEtaExpandedFix]
d:37 [in MetaCoq.Erasure.EPretty]
d:373 [in MetaCoq.SafeChecker.PCUICTypeChecker]
D:375 [in MetaCoq.Template.utils.All_Forall]
d:375 [in MetaCoq.PCUIC.PCUICWcbvEval]
d:376 [in MetaCoq.PCUIC.PCUICNormal]
d:377 [in MetaCoq.PCUIC.PCUICContextConversion]
d:379 [in MetaCoq.SafeChecker.PCUICTypeChecker]
d:38 [in MetaCoq.Erasure.EEtaExpandedFix]
d:38 [in MetaCoq.PCUIC.PCUICValidity]
d:38 [in MetaCoq.Template.utils.MCOption]
d:38 [in MetaCoq.Erasure.EExtends]
d:383 [in MetaCoq.Template.EtaExpand]
d:383 [in MetaCoq.SafeChecker.PCUICTypeChecker]
d:386 [in MetaCoq.Template.BasicAst]
D:387 [in MetaCoq.Template.utils.All_Forall]
d:389 [in MetaCoq.SafeChecker.PCUICTypeChecker]
d:39 [in MetaCoq.SafeChecker.PCUICWfEnv]
d:39 [in MetaCoq.PCUIC.PCUICContextSubst]
d:392 [in MetaCoq.PCUIC.PCUICAst]
d:395 [in MetaCoq.Template.BasicAst]
d:397 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
D:397 [in MetaCoq.Template.utils.All_Forall]
d:398 [in MetaCoq.Erasure.EEtaExpandedFix]
D:398 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
d:398 [in MetaCoq.SafeChecker.PCUICTypeChecker]
d:399 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
d:4 [in MetaCoq.SafeChecker.PCUICTypeChecker]
d:400 [in MetaCoq.Erasure.ERemoveParams]
d:403 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
d:404 [in MetaCoq.Template.BasicAst]
d:404 [in MetaCoq.Erasure.ERemoveParams]
d:405 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
D:405 [in MetaCoq.Template.utils.All_Forall]
D:408 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
d:41 [in MetaCoq.PCUIC.PCUICEtaExpand]
d:41 [in MetaCoq.Template.EnvMap]
d:41 [in MetaCoq.Template.Environment]
d:41 [in MetaCoq.PCUIC.PCUICContextReduction]
d:410 [in MetaCoq.PCUIC.PCUICNormal]
d:411 [in MetaCoq.Template.BasicAst]
d:412 [in MetaCoq.SafeChecker.PCUICSafeChecker]
d:417 [in MetaCoq.Erasure.EEtaExpandedFix]
d:418 [in MetaCoq.Erasure.EEtaExpandedFix]
d:42 [in MetaCoq.Template.EtaExpand]
d:42 [in MetaCoq.Erasure.EEtaExpandedFix]
d:42 [in MetaCoq.PCUIC.PCUICInductiveInversion]
d:421 [in MetaCoq.PCUIC.PCUICEquality]
d:422 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
d:424 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
d:427 [in MetaCoq.Erasure.EEtaExpandedFix]
d:429 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
d:430 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
d:431 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
d:432 [in MetaCoq.Erasure.ERemoveParams]
d:44 [in MetaCoq.Template.EtaExpand]
d:44 [in MetaCoq.Translations.translation_utils]
d:444 [in MetaCoq.PCUIC.PCUICTyping]
d:447 [in MetaCoq.Erasure.EEtaExpandedFix]
d:447 [in MetaCoq.PCUIC.PCUICInductives]
d:45 [in MetaCoq.PCUIC.TemplateToPCUIC]
d:46 [in MetaCoq.Erasure.EDeps]
d:47 [in MetaCoq.Erasure.EInlineProjections]
d:47 [in MetaCoq.PCUIC.PCUICInductiveInversion]
d:47 [in MetaCoq.PCUIC.TemplateToPCUIC]
d:471 [in MetaCoq.PCUIC.PCUICAst]
d:475 [in MetaCoq.Erasure.EEtaExpandedFix]
d:475 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
d:476 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
d:479 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
d:48 [in MetaCoq.PCUIC.PCUICEtaExpand]
d:48 [in MetaCoq.PCUIC.TemplateToPCUIC]
d:480 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
d:49 [in MetaCoq.PCUIC.PCUICEtaExpand]
d:49 [in MetaCoq.PCUIC.TemplateToPCUIC]
d:492 [in MetaCoq.Template.Typing]
d:497 [in MetaCoq.Template.utils.MCList]
d:5 [in MetaCoq.PCUIC.PCUICRedTypeIrrelevance]
d:5 [in MetaCoq.SafeChecker.PCUICWfEnv]
d:5 [in MetaCoq.PCUIC.Syntax.PCUICInstDef]
d:5 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
d:5 [in MetaCoq.PCUIC.Syntax.PCUICNamelessDef]
d:5 [in MetaCoq.Erasure.EGenericMapEnv]
d:50 [in MetaCoq.PCUIC.PCUICEtaExpand]
d:50 [in MetaCoq.PCUIC.utils.PCUICOnOne]
d:50 [in MetaCoq.Erasure.EWellformed]
d:500 [in MetaCoq.Template.utils.MCList]
d:505 [in MetaCoq.PCUIC.PCUICSubstitution]
d:506 [in MetaCoq.PCUIC.PCUICInductives]
d:51 [in MetaCoq.Template.Environment]
d:512 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
D:515 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
d:518 [in MetaCoq.Erasure.EEtaExpandedFix]
d:518 [in MetaCoq.PCUIC.PCUICInductives]
d:519 [in MetaCoq.Erasure.EEtaExpandedFix]
d:52 [in MetaCoq.PCUIC.TemplateToPCUIC]
d:521 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
d:524 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
d:526 [in MetaCoq.Template.EtaExpand]
d:529 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
d:53 [in MetaCoq.Erasure.EDeps]
d:53 [in MetaCoq.PCUIC.PCUICContextReduction]
d:532 [in MetaCoq.PCUIC.PCUICAst]
d:54 [in MetaCoq.PCUIC.PCUICEtaExpand]
d:543 [in MetaCoq.Template.EtaExpand]
d:543 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
d:55 [in MetaCoq.Template.BasicAst]
d:55 [in MetaCoq.PCUIC.TemplateToPCUIC]
d:55 [in MetaCoq.Template.Environment]
d:55 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
d:555 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
d:56 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
d:56 [in MetaCoq.Erasure.EAst]
d:56 [in MetaCoq.Erasure.EOptimizePropDiscr]
d:57 [in MetaCoq.Translations.translation_utils]
d:57 [in MetaCoq.PCUIC.TemplateToPCUIC]
d:57 [in MetaCoq.Erasure.EWellformed]
d:57 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
d:58 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
d:58 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
d:583 [in MetaCoq.PCUIC.PCUICEquality]
d:584 [in MetaCoq.Template.Typing]
d:59 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
d:591 [in MetaCoq.Template.Typing]
d:60 [in MetaCoq.Template.BasicAst]
d:61 [in MetaCoq.Erasure.Extract]
d:61 [in MetaCoq.Erasure.EAst]
d:612 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
d:612 [in MetaCoq.PCUIC.PCUICSR]
d:62 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
d:623 [in MetaCoq.Erasure.ErasureFunction]
d:625 [in MetaCoq.PCUIC.PCUICParallelReduction]
d:629 [in MetaCoq.Erasure.ErasureFunction]
d:636 [in MetaCoq.PCUIC.PCUICParallelReduction]
d:64 [in MetaCoq.PCUIC.PCUICSafeLemmata]
d:64 [in MetaCoq.PCUIC.TemplateToPCUIC]
D:641 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
d:65 [in MetaCoq.Template.BasicAst]
d:65 [in MetaCoq.PCUIC.PCUICAlpha]
d:650 [in MetaCoq.Erasure.ErasureFunction]
d:655 [in MetaCoq.Template.EnvironmentTyping]
d:656 [in MetaCoq.Erasure.ErasureFunction]
d:658 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
d:66 [in MetaCoq.Translations.translation_utils]
d:66 [in MetaCoq.PCUIC.PCUICEtaExpand]
d:66 [in MetaCoq.Erasure.Extract]
d:66 [in MetaCoq.PCUIC.TemplateToPCUICExpanded]
d:66 [in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
d:661 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
d:662 [in MetaCoq.PCUIC.PCUICParallelReduction]
d:668 [in MetaCoq.Template.EnvironmentTyping]
d:67 [in MetaCoq.PCUIC.PCUICAlpha]
d:675 [in MetaCoq.Template.utils.MCList]
d:675 [in MetaCoq.Template.Typing]
d:677 [in MetaCoq.Template.Typing]
d:679 [in MetaCoq.Template.utils.MCList]
d:68 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
d:68 [in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
d:681 [in MetaCoq.Template.Typing]
d:683 [in MetaCoq.Template.Typing]
d:69 [in MetaCoq.PCUIC.PCUICSubstitution]
d:69 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
d:694 [in MetaCoq.Erasure.ErasureFunction]
d:7 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
d:70 [in MetaCoq.Template.BasicAst]
d:70 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
d:70 [in MetaCoq.PCUIC.TemplateToPCUICExpanded]
d:701 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
d:71 [in MetaCoq.Erasure.EInlineProjections]
d:71 [in MetaCoq.PCUIC.Syntax.PCUICReflect]
d:72 [in MetaCoq.PCUIC.PCUICWfUniverses]
d:72 [in MetaCoq.PCUIC.utils.PCUICOnOne]
d:72 [in MetaCoq.PCUIC.PCUICContextReduction]
d:721 [in MetaCoq.Template.EnvironmentTyping]
D:723 [in MetaCoq.Template.utils.MCList]
d:729 [in MetaCoq.SafeChecker.PCUICSafeChecker]
d:73 [in MetaCoq.PCUIC.PCUICWfUniverses]
d:741 [in MetaCoq.Template.Typing]
d:741 [in MetaCoq.PCUIC.PCUICReduction]
d:748 [in MetaCoq.PCUIC.PCUICReduction]
d:76 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
d:76 [in MetaCoq.PCUIC.PCUICContextReduction]
d:768 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
d:769 [in MetaCoq.Template.Typing]
d:77 [in MetaCoq.Template.EnvironmentTyping]
d:77 [in MetaCoq.PCUIC.PCUICEquality]
d:77 [in MetaCoq.PCUIC.PCUICAlpha]
d:771 [in MetaCoq.Template.Universes]
d:775 [in MetaCoq.Template.Universes]
d:78 [in MetaCoq.Erasure.EGenericMapEnv]
D:793 [in MetaCoq.Translations.MiniHoTT]
d:795 [in MetaCoq.Erasure.ErasureFunction]
d:797 [in MetaCoq.Erasure.ErasureFunction]
d:799 [in MetaCoq.Erasure.ErasureFunction]
d:8 [in MetaCoq.Erasure.EAst]
d:8 [in MetaCoq.PCUIC.Syntax.PCUICInstDef]
d:8 [in MetaCoq.Template.TypingWf]
d:80 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
d:80 [in MetaCoq.Template.TypingWf]
d:80 [in MetaCoq.Erasure.EOptimizePropDiscr]
d:801 [in MetaCoq.Erasure.ErasureFunction]
D:801 [in MetaCoq.Translations.MiniHoTT_paths]
d:803 [in MetaCoq.Erasure.ErasureFunction]
d:805 [in MetaCoq.Erasure.ErasureFunction]
d:807 [in MetaCoq.Erasure.ErasureFunction]
d:809 [in MetaCoq.Erasure.ErasureFunction]
d:811 [in MetaCoq.Erasure.ErasureFunction]
d:812 [in MetaCoq.SafeChecker.PCUICTypeChecker]
d:813 [in MetaCoq.Erasure.ErasureFunction]
d:815 [in MetaCoq.Erasure.ErasureFunction]
d:817 [in MetaCoq.Erasure.ErasureFunction]
d:82 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
d:82 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
d:82 [in MetaCoq.Erasure.EPretty]
d:82 [in MetaCoq.PCUIC.PCUICFirstorder]
d:82 [in MetaCoq.PCUIC.TemplateToPCUICExpanded]
d:82 [in MetaCoq.Erasure.EGenericMapEnv]
d:83 [in MetaCoq.Template.BasicAst]
d:83 [in MetaCoq.PCUIC.PCUICSubstitution]
d:83 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
d:83 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
d:834 [in MetaCoq.Template.Typing]
d:837 [in MetaCoq.PCUIC.PCUICInductiveInversion]
D:84 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
d:84 [in MetaCoq.PCUIC.PCUICAlpha]
d:85 [in MetaCoq.PCUIC.PCUICSubstitution]
d:85 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
d:85 [in MetaCoq.Erasure.EGenericMapEnv]
d:86 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
d:86 [in MetaCoq.Erasure.EEtaExpandedFix]
d:86 [in MetaCoq.PCUIC.PCUICConversion]
d:87 [in MetaCoq.PCUIC.PCUICSubstitution]
d:87 [in MetaCoq.PCUIC.PCUICEquality]
d:87 [in MetaCoq.Erasure.ErasureProperties]
d:87 [in MetaCoq.PCUIC.TemplateToPCUICExpanded]
D:873 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
d:878 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
d:88 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
d:88 [in MetaCoq.Erasure.EEtaExpandedFix]
d:88 [in MetaCoq.PCUIC.PCUICAlpha]
d:88 [in MetaCoq.Erasure.ErasureProperties]
d:88 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
d:88 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
d:880 [in MetaCoq.Erasure.ErasureFunction]
d:887 [in MetaCoq.Erasure.ErasureFunction]
d:89 [in MetaCoq.Erasure.ErasureProperties]
d:89 [in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
d:892 [in MetaCoq.Erasure.ErasureFunction]
d:896 [in MetaCoq.Erasure.ErasureFunction]
d:899 [in MetaCoq.Erasure.ErasureFunction]
d:9 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
d:9 [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
d:9 [in MetaCoq.PCUIC.Typing.PCUICNamelessTyp]
d:90 [in MetaCoq.Erasure.ErasureProperties]
d:90 [in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
d:901 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
d:905 [in MetaCoq.Erasure.ErasureFunction]
d:91 [in MetaCoq.Erasure.EEtaExpandedFix]
d:919 [in MetaCoq.Template.Typing]
d:937 [in MetaCoq.Erasure.ErasureFunction]
d:937 [in MetaCoq.PCUIC.PCUICConversion]
d:942 [in MetaCoq.PCUIC.PCUICConversion]
d:946 [in MetaCoq.PCUIC.PCUICParallelReduction]
d:95 [in MetaCoq.PCUIC.PCUICEquality]
d:951 [in MetaCoq.PCUIC.PCUICConversion]
d:952 [in MetaCoq.PCUIC.PCUICParallelReduction]
d:96 [in MetaCoq.Erasure.EEtaExpandedFix]
d:96 [in MetaCoq.PCUIC.Typing.PCUICWeakeningTyp]
d:96 [in MetaCoq.Erasure.ERemoveParams]
d:96 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
d:961 [in MetaCoq.PCUIC.PCUICConversion]
d:964 [in MetaCoq.Erasure.ErasureFunction]
d:97 [in MetaCoq.Erasure.EEtaExpandedFix]
d:97 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
d:974 [in MetaCoq.Erasure.ErasureFunction]
d:98 [in MetaCoq.Erasure.EConstructorsAsBlocks]
d:987 [in MetaCoq.PCUIC.PCUICParallelReduction]
d:99 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
d:99 [in MetaCoq.Erasure.ERemoveParams]
d:990 [in MetaCoq.PCUIC.PCUICParallelReduction]
d:991 [in MetaCoq.PCUIC.PCUICTyping]
dΣ:490 [in MetaCoq.Template.EtaExpand]
| 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) |