| 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) |
I (binder)
ictx:14 [in MetaCoq.PCUIC.Syntax.PCUICCases]ictx:334 [in MetaCoq.Template.Ast]
idc:14 [in MetaCoq.Examples.add_constructor]
idc:20 [in MetaCoq.Examples.add_constructor]
idc:29 [in MetaCoq.Examples.add_constructor]
idecl':10 [in MetaCoq.PCUIC.PCUICGlobalEnv]
idecl':100 [in MetaCoq.Erasure.EDeps]
idecl':112 [in MetaCoq.Erasure.EDeps]
idecl':126 [in MetaCoq.PCUIC.PCUICConvCumInversion]
idecl':144 [in MetaCoq.Erasure.EDeps]
idecl':15 [in MetaCoq.PCUIC.PCUICGlobalEnv]
idecl':153 [in MetaCoq.Erasure.EDeps]
idecl':209 [in MetaCoq.Erasure.Extract]
idecl':215 [in MetaCoq.Erasure.Extract]
idecl':216 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
idecl':225 [in MetaCoq.Erasure.Extract]
idecl':23 [in MetaCoq.PCUIC.PCUICGlobalEnv]
idecl':308 [in MetaCoq.Erasure.EArities]
idecl':318 [in MetaCoq.Erasure.EArities]
idecl':359 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
idecl':43 [in MetaCoq.PCUIC.PCUICSR]
idecl':445 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
idecl':452 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
idecl':474 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
idecl':485 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
idecl':498 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
idecl':753 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
idecl':849 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
idecl':869 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
idecl':93 [in MetaCoq.Erasure.EDeps]
idecl:10 [in MetaCoq.Erasure.EInlineProjections]
idecl:1009 [in MetaCoq.PCUIC.PCUICInductiveInversion]
idecl:101 [in MetaCoq.Erasure.EArities]
idecl:101 [in MetaCoq.Template.WfAst]
idecl:101 [in MetaCoq.Erasure.EGlobalEnv]
idecl:102 [in MetaCoq.Erasure.EEtaExpandedFix]
idecl:1030 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
idecl:1030 [in MetaCoq.Erasure.ErasureFunction]
idecl:1037 [in MetaCoq.Template.Typing]
idecl:1047 [in MetaCoq.Template.Typing]
idecl:105 [in MetaCoq.PCUIC.PCUICInversion]
idecl:105 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
idecl:105 [in MetaCoq.Template.TypingWf]
idecl:1061 [in MetaCoq.Template.Typing]
idecl:1078 [in MetaCoq.Template.Typing]
idecl:108 [in MetaCoq.Erasure.EDeps]
idecl:108 [in MetaCoq.PCUIC.Syntax.PCUICCases]
idecl:108 [in MetaCoq.Erasure.EGlobalEnv]
idecl:1080 [in MetaCoq.SafeChecker.PCUICTypeChecker]
idecl:11 [in MetaCoq.PCUIC.PCUICElimination]
idecl:11 [in MetaCoq.PCUIC.PCUICInductiveInversion]
idecl:110 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
idecl:110 [in MetaCoq.Template.TypingWf]
idecl:111 [in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
idecl:113 [in MetaCoq.PCUIC.PCUICInversion]
idecl:114 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
idecl:115 [in MetaCoq.Erasure.EInlineProjections]
idecl:116 [in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
idecl:116 [in MetaCoq.PCUIC.Syntax.PCUICCases]
idecl:116 [in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
idecl:117 [in MetaCoq.PCUIC.PCUICTyping]
idecl:119 [in MetaCoq.PCUIC.PCUICAlpha]
idecl:12 [in MetaCoq.Erasure.ESubstitution]
idecl:12 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
idecl:121 [in MetaCoq.Template.EtaExpand]
idecl:121 [in MetaCoq.PCUIC.PCUICWeakeningEnv]
idecl:121 [in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
idecl:122 [in MetaCoq.PCUIC.PCUICTyping]
idecl:124 [in MetaCoq.PCUIC.PCUICInductiveInversion]
idecl:124 [in MetaCoq.PCUIC.PCUICConvCumInversion]
idecl:124 [in MetaCoq.Erasure.Prelim]
idecl:125 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
idecl:125 [in MetaCoq.Erasure.EWcbvEval]
idecl:1271 [in MetaCoq.SafeChecker.PCUICSafeConversion]
idecl:128 [in MetaCoq.PCUIC.PCUICWeakeningEnv]
idecl:13 [in MetaCoq.PCUIC.Syntax.PCUICCases]
idecl:130 [in MetaCoq.PCUIC.PCUICWcbvEval]
idecl:130 [in MetaCoq.PCUIC.Syntax.PCUICCases]
idecl:130 [in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
idecl:131 [in MetaCoq.PCUIC.PCUICTyping]
idecl:132 [in MetaCoq.PCUIC.PCUICAlpha]
idecl:132 [in MetaCoq.PCUIC.Syntax.PCUICCases]
idecl:132 [in MetaCoq.Template.WcbvEval]
idecl:133 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
idecl:1338 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
idecl:134 [in MetaCoq.Erasure.EWcbvEval]
idecl:135 [in MetaCoq.PCUIC.PCUICElimination]
idecl:136 [in MetaCoq.PCUIC.PCUICEtaExpand]
idecl:139 [in MetaCoq.PCUIC.Syntax.PCUICCases]
idecl:14 [in MetaCoq.Template.EnvironmentTyping]
idecl:14 [in MetaCoq.PCUIC.PCUICGlobalEnv]
idecl:140 [in MetaCoq.PCUIC.PCUICElimination]
idecl:140 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
idecl:141 [in MetaCoq.PCUIC.PCUICInductives]
idecl:142 [in MetaCoq.PCUIC.PCUICProgress]
idecl:142 [in MetaCoq.Erasure.EDeps]
idecl:142 [in MetaCoq.PCUIC.Syntax.PCUICCases]
idecl:142 [in MetaCoq.PCUIC.PCUICTyping]
idecl:143 [in MetaCoq.PCUIC.PCUICInversion]
idecl:144 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
idecl:144 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
idecl:145 [in MetaCoq.Template.EtaExpand]
idecl:145 [in MetaCoq.Erasure.ErasureProperties]
idecl:146 [in MetaCoq.Erasure.EWcbvEvalInd]
idecl:146 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
idecl:148 [in MetaCoq.PCUIC.PCUICWcbvEval]
idecl:148 [in MetaCoq.PCUIC.Syntax.PCUICCases]
idecl:148 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
idecl:15 [in MetaCoq.PCUIC.TemplateToPCUICExpanded]
idecl:150 [in MetaCoq.Erasure.EDeps]
idecl:151 [in MetaCoq.PCUIC.PCUICInductiveInversion]
idecl:151 [in MetaCoq.PCUIC.PCUICAlpha]
idecl:151 [in MetaCoq.Erasure.ERemoveParams]
idecl:151 [in MetaCoq.Erasure.EWcbvEval]
idecl:152 [in MetaCoq.PCUIC.PCUICProgress]
idecl:152 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
idecl:152 [in MetaCoq.PCUIC.PCUICEtaExpand]
idecl:152 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
idecl:154 [in MetaCoq.PCUIC.PCUICInversion]
idecl:156 [in MetaCoq.PCUIC.PCUICSR]
idecl:159 [in MetaCoq.Template.TypingWf]
idecl:16 [in MetaCoq.Erasure.EArities]
idecl:16 [in MetaCoq.Erasure.ErasureFunction]
idecl:160 [in MetaCoq.Erasure.EWcbvEvalInd]
idecl:163 [in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
idecl:164 [in MetaCoq.Template.WcbvEval]
idecl:165 [in MetaCoq.Erasure.EWcbvEval]
idecl:166 [in MetaCoq.PCUIC.PCUICProgress]
idecl:166 [in MetaCoq.PCUIC.PCUICElimination]
idecl:166 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
idecl:166 [in MetaCoq.Template.Typing]
idecl:166 [in MetaCoq.PCUIC.PCUICSR]
idecl:169 [in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
idecl:171 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
idecl:173 [in MetaCoq.Template.TypingWf]
idecl:174 [in MetaCoq.PCUIC.Syntax.PCUICCases]
idecl:176 [in MetaCoq.PCUIC.Syntax.PCUICCases]
idecl:177 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
idecl:178 [in MetaCoq.PCUIC.Syntax.PCUICCases]
idecl:178 [in MetaCoq.Template.TypingWf]
idecl:179 [in MetaCoq.PCUIC.PCUICInductives]
idecl:179 [in MetaCoq.Erasure.EWcbvEval]
idecl:18 [in MetaCoq.Erasure.EGlobalEnv]
idecl:18 [in MetaCoq.Erasure.EExtends]
idecl:180 [in MetaCoq.PCUIC.PCUICElimination]
idecl:180 [in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
idecl:181 [in MetaCoq.PCUIC.PCUICArities]
idecl:182 [in MetaCoq.PCUIC.PCUICAlpha]
idecl:182 [in MetaCoq.PCUIC.Syntax.PCUICCases]
idecl:182 [in MetaCoq.Template.TypingWf]
idecl:183 [in MetaCoq.PCUIC.PCUICProgress]
idecl:183 [in MetaCoq.Template.WcbvEval]
idecl:184 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
idecl:184 [in MetaCoq.Template.Typing]
idecl:185 [in MetaCoq.Erasure.EConstructorsAsBlocks]
idecl:186 [in MetaCoq.PCUIC.Syntax.PCUICCases]
idecl:188 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
idecl:188 [in MetaCoq.PCUIC.PCUICInductives]
idecl:189 [in MetaCoq.PCUIC.Syntax.PCUICCases]
idecl:189 [in MetaCoq.Template.TypingWf]
idecl:19 [in MetaCoq.Template.EnvironmentTyping]
idecl:19 [in MetaCoq.PCUIC.Syntax.PCUICCases]
idecl:190 [in MetaCoq.PCUIC.PCUICElimination]
idecl:191 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
idecl:191 [in MetaCoq.Erasure.EConstructorsAsBlocks]
idecl:192 [in MetaCoq.PCUIC.PCUICAlpha]
idecl:192 [in MetaCoq.PCUIC.Syntax.PCUICCases]
idecl:193 [in MetaCoq.PCUIC.PCUICSR]
idecl:194 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
idecl:195 [in MetaCoq.Template.EtaExpand]
idecl:195 [in MetaCoq.PCUIC.PCUICElimination]
idecl:195 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
idecl:195 [in MetaCoq.PCUIC.PCUICInductiveInversion]
idecl:195 [in MetaCoq.Template.TypingWf]
idecl:199 [in MetaCoq.Erasure.EWcbvEval]
idecl:201 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
idecl:205 [in MetaCoq.PCUIC.PCUICElimination]
idecl:206 [in MetaCoq.Erasure.Extract]
idecl:208 [in MetaCoq.PCUIC.PCUICInductives]
idecl:209 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
idecl:21 [in MetaCoq.PCUIC.PCUICElimination]
idecl:21 [in MetaCoq.PCUIC.TemplateToPCUIC]
idecl:21 [in MetaCoq.Erasure.EEnvMap]
idecl:211 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
idecl:211 [in MetaCoq.PCUIC.PCUICTyping]
idecl:212 [in MetaCoq.PCUIC.PCUICElimination]
idecl:213 [in MetaCoq.PCUIC.PCUICWcbvEval]
idecl:213 [in MetaCoq.Erasure.Extract]
idecl:213 [in MetaCoq.PCUIC.Syntax.PCUICCases]
idecl:213 [in MetaCoq.Erasure.EEtaExpanded]
idecl:215 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
idecl:215 [in MetaCoq.PCUIC.PCUICSubstitution]
idecl:215 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
idecl:216 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
idecl:217 [in MetaCoq.PCUIC.PCUICInductives]
idecl:218 [in MetaCoq.PCUIC.Syntax.PCUICCases]
idecl:218 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
idecl:22 [in MetaCoq.PCUIC.PCUICGlobalEnv]
idecl:22 [in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
idecl:220 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
idecl:221 [in MetaCoq.Erasure.Extract]
idecl:223 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
idecl:225 [in MetaCoq.PCUIC.PCUICSubstitution]
idecl:226 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
idecl:226 [in MetaCoq.Erasure.EConstructorsAsBlocks]
idecl:226 [in MetaCoq.Template.WcbvEval]
idecl:226 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
idecl:227 [in MetaCoq.PCUIC.Syntax.PCUICCases]
idecl:227 [in MetaCoq.PCUIC.PCUICTyping]
idecl:228 [in MetaCoq.PCUIC.PCUICWcbvEval]
idecl:23 [in MetaCoq.PCUIC.PCUICSafeLemmata]
idecl:23 [in MetaCoq.Erasure.EGlobalEnv]
idecl:230 [in MetaCoq.Template.EtaExpand]
idecl:233 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
idecl:234 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
idecl:234 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
idecl:2354 [in MetaCoq.SafeChecker.PCUICSafeConversion]
idecl:239 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
idecl:239 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
idecl:239 [in MetaCoq.Template.TypingWf]
idecl:240 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
idecl:241 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
idecl:244 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
idecl:245 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
idecl:249 [in MetaCoq.Template.WcbvEval]
idecl:249 [in MetaCoq.Erasure.EEtaExpanded]
idecl:252 [in MetaCoq.Template.EtaExpand]
idecl:253 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
idecl:257 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
idecl:258 [in MetaCoq.PCUIC.PCUICInductiveInversion]
idecl:259 [in MetaCoq.PCUIC.PCUICWfUniverses]
idecl:260 [in MetaCoq.PCUIC.PCUICWcbvEval]
idecl:260 [in MetaCoq.Erasure.EWcbvEval]
idecl:263 [in MetaCoq.Template.Typing]
idecl:268 [in MetaCoq.Erasure.EWcbvEval]
idecl:27 [in MetaCoq.Erasure.EEnvMap]
idecl:27 [in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
idecl:271 [in MetaCoq.Erasure.EEtaExpanded]
idecl:278 [in MetaCoq.Erasure.EEtaExpanded]
idecl:282 [in MetaCoq.PCUIC.PCUICInductiveInversion]
idecl:283 [in MetaCoq.PCUIC.PCUICInductives]
idecl:284 [in MetaCoq.Template.EtaExpand]
idecl:29 [in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
idecl:29 [in MetaCoq.Erasure.ErasureCorrectness]
idecl:29 [in MetaCoq.PCUIC.PCUICInductives]
idecl:290 [in MetaCoq.PCUIC.PCUICInductives]
idecl:292 [in MetaCoq.PCUIC.PCUICProgress]
idecl:3 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
idecl:300 [in MetaCoq.Template.TypingWf]
idecl:302 [in MetaCoq.PCUIC.PCUICProgress]
idecl:302 [in MetaCoq.Erasure.ERemoveParams]
idecl:303 [in MetaCoq.PCUIC.PCUICInductiveInversion]
idecl:306 [in MetaCoq.Erasure.EArities]
idecl:306 [in MetaCoq.Template.TypingWf]
idecl:31 [in MetaCoq.PCUIC.PCUICElimination]
idecl:310 [in MetaCoq.PCUIC.PCUICInductiveInversion]
idecl:313 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
idecl:314 [in MetaCoq.PCUIC.PCUICInductives]
idecl:315 [in MetaCoq.Erasure.EArities]
idecl:316 [in MetaCoq.PCUIC.PCUICProgress]
idecl:32 [in MetaCoq.PCUIC.PCUICGlobalEnv]
idecl:324 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
idecl:325 [in MetaCoq.PCUIC.PCUICInductives]
idecl:328 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
idecl:329 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
idecl:333 [in MetaCoq.PCUIC.PCUICProgress]
idecl:333 [in MetaCoq.Template.Ast]
idecl:335 [in MetaCoq.PCUIC.PCUICInductives]
idecl:338 [in MetaCoq.Erasure.EArities]
idecl:34 [in MetaCoq.PCUIC.PCUICCasesContexts]
idecl:341 [in MetaCoq.PCUIC.PCUICInductiveInversion]
idecl:342 [in MetaCoq.Template.Ast]
idecl:343 [in MetaCoq.Template.Typing]
idecl:345 [in MetaCoq.PCUIC.PCUICInductives]
idecl:347 [in MetaCoq.Template.Ast]
idecl:35 [in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
idecl:350 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
idecl:353 [in MetaCoq.Template.Ast]
idecl:36 [in MetaCoq.PCUIC.PCUICGlobalEnv]
idecl:36 [in MetaCoq.Erasure.EEnvMap]
idecl:360 [in MetaCoq.Erasure.ERemoveParams]
idecl:363 [in MetaCoq.Template.Typing]
idecl:366 [in MetaCoq.PCUIC.PCUICWcbvEval]
idecl:371 [in MetaCoq.Template.Ast]
idecl:372 [in MetaCoq.PCUIC.PCUICWcbvEval]
idecl:379 [in MetaCoq.Template.Ast]
idecl:38 [in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
idecl:38 [in MetaCoq.Template.WfAst]
idecl:38 [in MetaCoq.PCUIC.PCUICCasesContexts]
idecl:380 [in MetaCoq.Erasure.EEtaExpandedFix]
idecl:385 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
idecl:385 [in MetaCoq.PCUIC.PCUICProgress]
idecl:385 [in MetaCoq.PCUIC.PCUICInductives]
idecl:386 [in MetaCoq.Erasure.ERemoveParams]
idecl:387 [in MetaCoq.Erasure.EEtaExpandedFix]
idecl:39 [in MetaCoq.PCUIC.PCUICArities]
idecl:39 [in MetaCoq.Erasure.EGlobalEnv]
idecl:391 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
idecl:396 [in MetaCoq.PCUIC.PCUICProgress]
idecl:398 [in MetaCoq.PCUIC.PCUICInductives]
idecl:40 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
idecl:402 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
idecl:405 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
idecl:407 [in MetaCoq.PCUIC.PCUICInductives]
idecl:408 [in MetaCoq.PCUIC.PCUICProgress]
idecl:41 [in MetaCoq.PCUIC.PCUICInductives]
idecl:41 [in MetaCoq.PCUIC.Syntax.PCUICCases]
idecl:41 [in MetaCoq.PCUIC.PCUICGlobalEnv]
idecl:41 [in MetaCoq.SafeChecker.PCUICTypeChecker]
idecl:411 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
idecl:414 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
idecl:418 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
idecl:418 [in MetaCoq.Erasure.ERemoveParams]
idecl:42 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
idecl:42 [in MetaCoq.PCUIC.PCUICSR]
idecl:421 [in MetaCoq.Template.EtaExpand]
idecl:421 [in MetaCoq.PCUIC.PCUICInductives]
idecl:426 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
idecl:426 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
idecl:429 [in MetaCoq.SafeChecker.PCUICSafeChecker]
idecl:43 [in MetaCoq.PCUIC.PCUICElimination]
idecl:43 [in MetaCoq.PCUIC.PCUICConvCumInversion]
idecl:43 [in MetaCoq.PCUIC.PCUICCasesContexts]
idecl:433 [in MetaCoq.PCUIC.PCUICInductives]
idecl:44 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
idecl:44 [in MetaCoq.Erasure.EWellformed]
idecl:44 [in MetaCoq.Erasure.EGlobalEnv]
idecl:440 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
idecl:441 [in MetaCoq.PCUIC.PCUICInductiveInversion]
idecl:447 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
idecl:45 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
idecl:45 [in MetaCoq.Erasure.EWellformed]
idecl:450 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
idecl:455 [in MetaCoq.PCUIC.PCUICInductiveInversion]
idecl:458 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
idecl:46 [in MetaCoq.Erasure.EEtaExpandedFix]
idecl:46 [in MetaCoq.PCUIC.Syntax.PCUICCases]
idecl:468 [in MetaCoq.PCUIC.PCUICInductiveInversion]
idecl:469 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
idecl:474 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
idecl:478 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
idecl:48 [in MetaCoq.Template.EnvironmentTyping]
idecl:48 [in MetaCoq.PCUIC.PCUICTyping]
idecl:49 [in MetaCoq.Erasure.EEnvMap]
idecl:491 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
idecl:5 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
idecl:502 [in MetaCoq.Template.EtaExpand]
idecl:51 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
idecl:51 [in MetaCoq.Erasure.EGlobalEnv]
idecl:52 [in MetaCoq.Template.EnvironmentTyping]
idecl:52 [in MetaCoq.PCUIC.Syntax.PCUICCases]
idecl:53 [in MetaCoq.Template.WfAst]
idecl:53 [in MetaCoq.PCUIC.TemplateToPCUICExpanded]
idecl:53 [in MetaCoq.SafeChecker.PCUICTypeChecker]
idecl:534 [in MetaCoq.PCUIC.PCUICTyping]
idecl:544 [in MetaCoq.PCUIC.PCUICTyping]
idecl:55 [in MetaCoq.PCUIC.PCUICElimination]
idecl:555 [in MetaCoq.Template.EnvironmentTyping]
idecl:558 [in MetaCoq.PCUIC.PCUICTyping]
idecl:56 [in MetaCoq.Template.EnvironmentTyping]
idecl:56 [in MetaCoq.PCUIC.PCUICInductiveInversion]
idecl:56 [in MetaCoq.Erasure.EGlobalEnv]
idecl:568 [in MetaCoq.PCUIC.PCUICSR]
idecl:575 [in MetaCoq.PCUIC.PCUICTyping]
idecl:575 [in MetaCoq.PCUIC.PCUICSR]
idecl:576 [in MetaCoq.Template.EnvironmentTyping]
idecl:58 [in MetaCoq.Erasure.EEnvMap]
idecl:585 [in MetaCoq.PCUIC.PCUICSR]
idecl:59 [in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
idecl:59 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
idecl:59 [in MetaCoq.PCUIC.PCUICEtaExpand]
idecl:59 [in MetaCoq.Erasure.EGenericMapEnv]
idecl:600 [in MetaCoq.Template.EnvironmentTyping]
idecl:61 [in MetaCoq.Template.EnvironmentTyping]
idecl:612 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
idecl:62 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
idecl:623 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
idecl:628 [in MetaCoq.Template.EnvironmentTyping]
idecl:635 [in MetaCoq.PCUIC.PCUICInductives]
idecl:635 [in MetaCoq.SafeChecker.PCUICSafeChecker]
idecl:639 [in MetaCoq.Template.Typing]
idecl:643 [in MetaCoq.PCUIC.PCUICInductives]
idecl:645 [in MetaCoq.Template.Typing]
idecl:646 [in MetaCoq.PCUIC.PCUICSR]
idecl:650 [in MetaCoq.PCUIC.PCUICInductiveInversion]
idecl:653 [in MetaCoq.PCUIC.PCUICInductives]
idecl:655 [in MetaCoq.Template.Typing]
idecl:66 [in MetaCoq.Template.EnvironmentTyping]
idecl:66 [in MetaCoq.PCUIC.PCUICInductiveInversion]
idecl:667 [in MetaCoq.Template.Typing]
idecl:669 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
idecl:67 [in MetaCoq.PCUIC.PCUICElimination]
idecl:67 [in MetaCoq.Erasure.EArities]
idecl:67 [in MetaCoq.PCUIC.PCUICValidity]
idecl:670 [in MetaCoq.PCUIC.PCUICSR]
idecl:671 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
idecl:674 [in MetaCoq.PCUIC.PCUICInductiveInversion]
idecl:68 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
idecl:681 [in MetaCoq.PCUIC.PCUICInductiveInversion]
idecl:683 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
idecl:69 [in MetaCoq.Erasure.EGlobalEnv]
idecl:699 [in MetaCoq.PCUIC.PCUICInductiveInversion]
idecl:699 [in MetaCoq.PCUIC.PCUICSR]
idecl:7 [in MetaCoq.PCUIC.PCUICSafeLemmata]
idecl:70 [in MetaCoq.Template.EtaExpand]
idecl:70 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
idecl:70 [in MetaCoq.PCUIC.PCUICTyping]
idecl:71 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
idecl:714 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
idecl:717 [in MetaCoq.SafeChecker.PCUICTypeChecker]
idecl:72 [in MetaCoq.PCUIC.PCUICElimination]
idecl:72 [in MetaCoq.Template.EnvironmentTyping]
idecl:72 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
idecl:72 [in MetaCoq.Template.WcbvEval]
idecl:728 [in MetaCoq.PCUIC.PCUICInductiveInversion]
idecl:729 [in MetaCoq.PCUIC.PCUICSR]
idecl:73 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
idecl:73 [in MetaCoq.Erasure.EGlobalEnv]
idecl:737 [in MetaCoq.PCUIC.PCUICInductiveInversion]
idecl:74 [in MetaCoq.PCUIC.PCUICWcbvEval]
idecl:744 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
idecl:751 [in MetaCoq.PCUIC.PCUICInductiveInversion]
idecl:76 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
idecl:771 [in MetaCoq.SafeChecker.PCUICTypeChecker]
idecl:774 [in MetaCoq.PCUIC.PCUICInductiveInversion]
idecl:78 [in MetaCoq.PCUIC.PCUICInductiveInversion]
idecl:78 [in MetaCoq.Erasure.EGlobalEnv]
idecl:79 [in MetaCoq.PCUIC.PCUICInductives]
idecl:792 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
idecl:803 [in MetaCoq.SafeChecker.PCUICSafeChecker]
idecl:807 [in MetaCoq.PCUIC.PCUICInductiveInversion]
idecl:81 [in MetaCoq.PCUIC.Syntax.PCUICCases]
idecl:825 [in MetaCoq.SafeChecker.PCUICSafeChecker]
idecl:831 [in MetaCoq.SafeChecker.PCUICSafeChecker]
idecl:84 [in MetaCoq.Erasure.EGlobalEnv]
idecl:846 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
idecl:85 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
idecl:85 [in MetaCoq.Erasure.Prelim]
idecl:857 [in MetaCoq.PCUIC.PCUICTyping]
idecl:86 [in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
idecl:866 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
idecl:867 [in MetaCoq.PCUIC.PCUICTyping]
idecl:87 [in MetaCoq.PCUIC.Syntax.PCUICCases]
idecl:881 [in MetaCoq.PCUIC.PCUICTyping]
idecl:884 [in MetaCoq.SafeChecker.PCUICSafeChecker]
idecl:89 [in MetaCoq.PCUIC.PCUICWcbvEval]
idecl:895 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
idecl:898 [in MetaCoq.PCUIC.PCUICTyping]
idecl:9 [in MetaCoq.PCUIC.PCUICGlobalEnv]
idecl:90 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
idecl:90 [in MetaCoq.Erasure.EDeps]
idecl:90 [in MetaCoq.Template.WcbvEval]
idecl:903 [in MetaCoq.SafeChecker.PCUICSafeChecker]
idecl:908 [in MetaCoq.PCUIC.PCUICInductiveInversion]
idecl:91 [in MetaCoq.Erasure.EGlobalEnv]
idecl:91 [in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
idecl:915 [in MetaCoq.PCUIC.PCUICInductiveInversion]
idecl:92 [in MetaCoq.PCUIC.Syntax.PCUICCases]
idecl:93 [in MetaCoq.Erasure.Prelim]
idecl:930 [in MetaCoq.PCUIC.PCUICInductiveInversion]
idecl:940 [in MetaCoq.PCUIC.PCUICInductiveInversion]
idecl:940 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
idecl:948 [in MetaCoq.PCUIC.PCUICInductiveInversion]
idecl:949 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
idecl:958 [in MetaCoq.PCUIC.PCUICInductiveInversion]
idecl:96 [in MetaCoq.Template.Typing]
idecl:97 [in MetaCoq.Erasure.EGlobalEnv]
idecl:97 [in MetaCoq.Template.TypingWf]
idecl:976 [in MetaCoq.PCUIC.PCUICInductiveInversion]
idecl:978 [in MetaCoq.SafeChecker.PCUICSafeChecker]
idecl:98 [in MetaCoq.Erasure.EDeps]
idecl:98 [in MetaCoq.PCUIC.PCUICInversion]
idecl:98 [in MetaCoq.Erasure.Prelim]
idecl:980 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
idecl:989 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
idecl:99 [in MetaCoq.Erasure.ESubstitution]
idecl:992 [in MetaCoq.PCUIC.PCUICInductiveInversion]
ids:207 [in MetaCoq.SafeChecker.PCUICErrors]
ids:422 [in MetaCoq.Template.Universes]
ids:427 [in MetaCoq.Template.Universes]
idx':113 [in MetaCoq.SafeChecker.PCUICErrors]
idx':132 [in MetaCoq.PCUIC.PCUICConvCumInversion]
idx':144 [in MetaCoq.PCUIC.PCUICConvCumInversion]
idx':1946 [in MetaCoq.SafeChecker.PCUICSafeConversion]
idx':2127 [in MetaCoq.SafeChecker.PCUICSafeConversion]
idx':2141 [in MetaCoq.SafeChecker.PCUICSafeConversion]
idx':572 [in MetaCoq.SafeChecker.PCUICSafeConversion]
idx':576 [in MetaCoq.SafeChecker.PCUICSafeConversion]
idx':93 [in MetaCoq.SafeChecker.PCUICErrors]
idx0:92 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
idx1:93 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
idx:100 [in MetaCoq.Erasure.EEtaExpandedFix]
idx:100 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
idx:101 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
idx:1011 [in MetaCoq.PCUIC.PCUICReduction]
idx:1016 [in MetaCoq.PCUIC.PCUICReduction]
idx:102 [in MetaCoq.PCUIC.PCUICWcbvEval]
idx:102 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
idx:103 [in MetaCoq.SafeChecker.PCUICErrors]
idx:1037 [in MetaCoq.PCUIC.PCUICReduction]
idx:104 [in MetaCoq.Template.WcbvEval]
idx:104 [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
idx:1047 [in MetaCoq.PCUIC.PCUICReduction]
idx:106 [in MetaCoq.Template.Typing]
idx:106 [in MetaCoq.PCUIC.PCUICNormal]
idx:1061 [in MetaCoq.PCUIC.PCUICReduction]
idx:107 [in MetaCoq.Erasure.EWcbvEvalInd]
idx:108 [in MetaCoq.PCUIC.PCUICInductiveInversion]
idx:1082 [in MetaCoq.PCUIC.PCUICReduction]
idx:1087 [in MetaCoq.PCUIC.PCUICReduction]
idx:110 [in MetaCoq.PCUIC.PCUICWcbvEval]
idx:110 [in MetaCoq.SafeChecker.PCUICErrors]
idx:1108 [in MetaCoq.PCUIC.PCUICReduction]
idx:111 [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
idx:1118 [in MetaCoq.PCUIC.PCUICReduction]
idx:112 [in MetaCoq.Template.WcbvEval]
idx:113 [in MetaCoq.Template.Typing]
idx:113 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
idx:114 [in MetaCoq.SafeChecker.PCUICErrors]
idx:1142 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
idx:1153 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
idx:117 [in MetaCoq.PCUIC.PCUICEtaExpand]
idx:118 [in MetaCoq.Template.EtaExpand]
idx:118 [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
idx:119 [in MetaCoq.PCUIC.PCUICCanonicity]
idx:120 [in MetaCoq.Template.Typing]
idx:120 [in MetaCoq.PCUIC.PCUICWcbvEval]
idx:121 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
idx:122 [in MetaCoq.PCUIC.PCUICAst]
idx:122 [in MetaCoq.Template.WcbvEval]
idx:123 [in MetaCoq.SafeChecker.PCUICErrors]
idx:123 [in MetaCoq.PCUIC.PCUICReduction]
idx:124 [in MetaCoq.PCUIC.PCUICAst]
idx:126 [in MetaCoq.Erasure.EArities]
idx:128 [in MetaCoq.PCUIC.PCUICEtaExpand]
idx:128 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
idx:129 [in MetaCoq.Erasure.EGlobalEnv]
idx:130 [in MetaCoq.PCUIC.PCUICConvCumInversion]
idx:130 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
idx:130 [in MetaCoq.PCUIC.PCUICReduction]
idx:131 [in MetaCoq.Template.EtaExpand]
idx:131 [in MetaCoq.PCUIC.PCUICCanonicity]
idx:132 [in MetaCoq.Template.TermEquality]
idx:135 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
idx:135 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
idx:136 [in MetaCoq.Erasure.EGlobalEnv]
idx:137 [in MetaCoq.Template.TermEquality]
idx:137 [in MetaCoq.PCUIC.PCUICReduction]
idx:138 [in MetaCoq.Erasure.EGlobalEnv]
idx:138 [in MetaCoq.Erasure.ERemoveParams]
idx:139 [in MetaCoq.Template.EtaExpand]
idx:14 [in MetaCoq.PCUIC.PCUICGuardCondition]
idx:140 [in MetaCoq.PCUIC.PCUICSubstitution]
idx:140 [in MetaCoq.Erasure.EGlobalEnv]
idx:1416 [in MetaCoq.SafeChecker.PCUICSafeReduce]
idx:142 [in MetaCoq.PCUIC.PCUICConvCumInversion]
idx:142 [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
idx:143 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
idx:143 [in MetaCoq.Erasure.ERemoveParams]
idx:144 [in MetaCoq.Erasure.EEtaExpanded]
idx:144 [in MetaCoq.PCUIC.PCUICReduction]
idx:146 [in MetaCoq.Erasure.EEtaExpandedFix]
idx:146 [in MetaCoq.PCUIC.PCUICSubstitution]
idx:148 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
idx:149 [in MetaCoq.Erasure.EEtaExpanded]
idx:1512 [in MetaCoq.SafeChecker.PCUICSafeConversion]
idx:153 [in MetaCoq.PCUIC.PCUICWcbvEval]
idx:154 [in MetaCoq.Erasure.EWcbvEval]
idx:155 [in MetaCoq.PCUIC.PCUICWcbvEval]
idx:155 [in MetaCoq.PCUIC.PCUICCanonicity]
idx:156 [in MetaCoq.Erasure.EConstructorsAsBlocks]
idx:156 [in MetaCoq.Erasure.EWcbvEval]
idx:161 [in MetaCoq.Erasure.EConstructorsAsBlocks]
idx:168 [in MetaCoq.PCUIC.PCUICInversion]
idx:169 [in MetaCoq.Erasure.EEtaExpandedFix]
idx:17 [in MetaCoq.Template.Typing]
idx:17 [in MetaCoq.Template.WcbvEval]
idx:172 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
idx:173 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
idx:176 [in MetaCoq.PCUIC.PCUICEquality]
idx:1768 [in MetaCoq.SafeChecker.PCUICSafeConversion]
idx:1771 [in MetaCoq.SafeChecker.PCUICSafeConversion]
idx:180 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
idx:181 [in MetaCoq.PCUIC.PCUICEquality]
idx:182 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
idx:183 [in MetaCoq.PCUIC.PCUICReduction]
idx:186 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
idx:188 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
idx:189 [in MetaCoq.Template.WcbvEval]
idx:19 [in MetaCoq.Template.WcbvEval]
idx:191 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
idx:191 [in MetaCoq.PCUIC.PCUICReduction]
idx:192 [in MetaCoq.Template.EtaExpand]
idx:1942 [in MetaCoq.SafeChecker.PCUICSafeConversion]
idx:196 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
idx:198 [in MetaCoq.Template.WcbvEval]
idx:199 [in MetaCoq.PCUIC.PCUICReduction]
idx:20 [in MetaCoq.PCUIC.PCUICInductiveInversion]
idx:204 [in MetaCoq.Template.Ast]
idx:204 [in MetaCoq.PCUIC.PCUICCanonicity]
idx:205 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
idx:205 [in MetaCoq.Erasure.EEtaExpanded]
idx:206 [in MetaCoq.PCUIC.PCUICParallelReduction]
idx:206 [in MetaCoq.Template.WcbvEval]
idx:208 [in MetaCoq.Template.Checker]
idx:208 [in MetaCoq.Erasure.EEtaExpanded]
idx:209 [in MetaCoq.Template.EtaExpand]
idx:210 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
idx:211 [in MetaCoq.Erasure.EEtaExpanded]
idx:2124 [in MetaCoq.SafeChecker.PCUICSafeConversion]
idx:213 [in MetaCoq.Template.Ast]
idx:2138 [in MetaCoq.SafeChecker.PCUICSafeConversion]
idx:215 [in MetaCoq.Template.Ast]
idx:216 [in MetaCoq.Template.WcbvEval]
idx:217 [in MetaCoq.PCUIC.PCUICParallelReduction]
idx:218 [in MetaCoq.Erasure.EWcbvEval]
idx:219 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
idx:221 [in MetaCoq.Erasure.EWcbvEval]
idx:222 [in MetaCoq.Template.EtaExpand]
idx:223 [in MetaCoq.Erasure.EWcbvEval]
idx:226 [in MetaCoq.Template.Typing]
idx:226 [in MetaCoq.Erasure.EWcbvEval]
idx:228 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
idx:228 [in MetaCoq.Erasure.EWcbvEval]
idx:23 [in MetaCoq.Template.Normal]
idx:23 [in MetaCoq.PCUIC.PCUICReduction]
idx:230 [in MetaCoq.PCUIC.PCUICParallelReduction]
idx:230 [in MetaCoq.PCUIC.PCUICNormal]
idx:231 [in MetaCoq.Template.Typing]
idx:232 [in MetaCoq.PCUIC.PCUICWcbvEval]
idx:232 [in MetaCoq.SafeChecker.PCUICSafeReduce]
idx:233 [in MetaCoq.Erasure.EWcbvEval]
idx:234 [in MetaCoq.PCUIC.Syntax.PCUICCases]
idx:236 [in MetaCoq.Template.Typing]
idx:238 [in MetaCoq.PCUIC.PCUICWcbvEval]
idx:239 [in MetaCoq.Erasure.EEtaExpanded]
idx:24 [in MetaCoq.Template.Typing]
idx:241 [in MetaCoq.Template.Typing]
idx:241 [in MetaCoq.PCUIC.Syntax.PCUICCases]
idx:243 [in MetaCoq.Erasure.EEtaExpanded]
idx:244 [in MetaCoq.PCUIC.PCUICWcbvEval]
idx:244 [in MetaCoq.PCUIC.PCUICNormal]
idx:244 [in MetaCoq.Erasure.EWcbvEval]
idx:247 [in MetaCoq.Erasure.EEtaExpanded]
idx:248 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
idx:249 [in MetaCoq.Erasure.EWcbvEval]
idx:25 [in MetaCoq.Template.Normal]
idx:251 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
idx:251 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
idx:252 [in MetaCoq.Template.WcbvEval]
idx:254 [in MetaCoq.Erasure.EWcbvEval]
idx:255 [in MetaCoq.PCUIC.PCUICNormal]
idx:256 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
idx:256 [in MetaCoq.Template.WcbvEval]
idx:258 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
idx:259 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
idx:26 [in MetaCoq.Erasure.ESpineView]
idx:265 [in MetaCoq.PCUIC.PCUICNormal]
idx:267 [in MetaCoq.PCUIC.PCUICWcbvEval]
idx:267 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
idx:268 [in MetaCoq.Erasure.EEtaExpanded]
idx:27 [in MetaCoq.Template.TypingWf]
idx:274 [in MetaCoq.Template.Typing]
idx:274 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
idx:275 [in MetaCoq.Erasure.EEtaExpanded]
idx:275 [in MetaCoq.Erasure.EWcbvEval]
idx:276 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
idx:277 [in MetaCoq.PCUIC.PCUICWcbvEval]
idx:278 [in MetaCoq.PCUIC.PCUICParallelReduction]
idx:28 [in MetaCoq.PCUIC.Syntax.PCUICViews]
idx:28 [in MetaCoq.PCUIC.PCUICWcbvEval]
idx:28 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
idx:28 [in MetaCoq.Erasure.ESpineView]
idx:28 [in MetaCoq.Erasure.EWellformed]
idx:282 [in MetaCoq.Template.Typing]
idx:282 [in MetaCoq.PCUIC.PCUICParallelReduction]
idx:283 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
idx:287 [in MetaCoq.Template.EtaExpand]
idx:288 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
idx:290 [in MetaCoq.Template.Typing]
idx:290 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
idx:291 [in MetaCoq.PCUIC.PCUICWcbvEval]
idx:293 [in MetaCoq.Template.EtaExpand]
idx:293 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
idx:294 [in MetaCoq.PCUIC.PCUICWcbvEval]
idx:296 [in MetaCoq.PCUIC.PCUICReduction]
idx:299 [in MetaCoq.PCUIC.PCUICWcbvEval]
idx:299 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
idx:30 [in MetaCoq.PCUIC.PCUICWcbvEval]
idx:30 [in MetaCoq.PCUIC.PCUICReduction]
idx:302 [in MetaCoq.Template.EtaExpand]
idx:302 [in MetaCoq.Template.WcbvEval]
idx:302 [in MetaCoq.PCUIC.PCUICReduction]
idx:303 [in MetaCoq.SafeChecker.PCUICSafeReduce]
idx:306 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
idx:308 [in MetaCoq.PCUIC.PCUICReduction]
idx:31 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
idx:314 [in MetaCoq.PCUIC.PCUICReduction]
idx:318 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
idx:324 [in MetaCoq.PCUIC.PCUICWcbvEval]
idx:325 [in MetaCoq.PCUIC.PCUICNormal]
idx:325 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
idx:328 [in MetaCoq.PCUIC.PCUICWcbvEval]
idx:331 [in MetaCoq.PCUIC.PCUICWcbvEval]
idx:331 [in MetaCoq.SafeChecker.PCUICSafeReduce]
idx:333 [in MetaCoq.Erasure.EWcbvEval]
idx:334 [in MetaCoq.PCUIC.PCUICWcbvEval]
idx:336 [in MetaCoq.PCUIC.PCUICWcbvEval]
idx:337 [in MetaCoq.Erasure.EWcbvEval]
idx:338 [in MetaCoq.PCUIC.PCUICWcbvEval]
idx:339 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
idx:34 [in MetaCoq.Erasure.EEtaExpandedFix]
idx:34 [in MetaCoq.PCUIC.PCUICNormal]
idx:34 [in MetaCoq.Template.TypingWf]
idx:340 [in MetaCoq.Erasure.EArities]
idx:342 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
idx:343 [in MetaCoq.Erasure.EEtaExpandedFix]
idx:345 [in MetaCoq.Erasure.EArities]
idx:354 [in MetaCoq.PCUIC.PCUICWcbvEval]
idx:359 [in MetaCoq.Erasure.EEtaExpandedFix]
idx:362 [in MetaCoq.SafeChecker.PCUICSafeConversion]
idx:363 [in MetaCoq.PCUIC.PCUICSR]
idx:364 [in MetaCoq.Erasure.EEtaExpandedFix]
idx:365 [in MetaCoq.Erasure.EWcbvEval]
idx:367 [in MetaCoq.PCUIC.PCUICProgress]
idx:368 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
idx:37 [in MetaCoq.Erasure.EInlineProjections]
idx:37 [in MetaCoq.PCUIC.PCUICNormal]
idx:37 [in MetaCoq.PCUIC.PCUICReduction]
idx:371 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
idx:371 [in MetaCoq.PCUIC.PCUICSR]
idx:373 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
idx:373 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
idx:375 [in MetaCoq.PCUIC.PCUICNormal]
idx:376 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
idx:377 [in MetaCoq.Erasure.EEtaExpandedFix]
idx:378 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
idx:379 [in MetaCoq.PCUIC.PCUICSR]
idx:382 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
idx:384 [in MetaCoq.Erasure.EEtaExpandedFix]
idx:384 [in MetaCoq.PCUIC.PCUICParallelReduction]
idx:384 [in MetaCoq.Erasure.EWcbvEval]
idx:39 [in MetaCoq.PCUIC.Syntax.PCUICViews]
idx:390 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
idx:397 [in MetaCoq.PCUIC.PCUICParallelReduction]
idx:398 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
idx:40 [in MetaCoq.PCUIC.PCUICInductiveInversion]
idx:409 [in MetaCoq.PCUIC.PCUICNormal]
idx:41 [in MetaCoq.Erasure.EEtaExpandedFix]
idx:41 [in MetaCoq.Erasure.EInlineProjections]
idx:412 [in MetaCoq.PCUIC.PCUICParallelReduction]
idx:419 [in MetaCoq.Template.Typing]
idx:425 [in MetaCoq.Template.Typing]
idx:43 [in MetaCoq.Erasure.EWellformed]
idx:431 [in MetaCoq.Template.Typing]
idx:434 [in MetaCoq.Template.EtaExpand]
idx:437 [in MetaCoq.Template.Typing]
idx:44 [in MetaCoq.Erasure.EEtaExpandedFix]
idx:45 [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
idx:455 [in MetaCoq.Erasure.EEtaExpandedFix]
idx:46 [in MetaCoq.PCUIC.PCUICEtaExpand]
idx:464 [in MetaCoq.Erasure.EEtaExpandedFix]
idx:47 [in MetaCoq.Erasure.EOptimizePropDiscr]
idx:473 [in MetaCoq.Erasure.EEtaExpandedFix]
idx:475 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
idx:476 [in MetaCoq.PCUIC.PCUICSR]
idx:477 [in MetaCoq.PCUIC.PCUICParallelReduction]
idx:481 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
idx:482 [in MetaCoq.PCUIC.PCUICSR]
idx:483 [in MetaCoq.PCUIC.PCUICParallelReduction]
idx:486 [in MetaCoq.SafeChecker.PCUICSafeConversion]
idx:488 [in MetaCoq.PCUIC.PCUICSR]
idx:490 [in MetaCoq.Erasure.EEtaExpandedFix]
idx:494 [in MetaCoq.Erasure.EEtaExpandedFix]
idx:494 [in MetaCoq.PCUIC.PCUICSR]
idx:495 [in MetaCoq.SafeChecker.PCUICSafeConversion]
idx:501 [in MetaCoq.Erasure.EEtaExpandedFix]
idx:504 [in MetaCoq.SafeChecker.PCUICSafeConversion]
idx:506 [in MetaCoq.Template.Typing]
idx:51 [in MetaCoq.Erasure.EOptimizePropDiscr]
idx:513 [in MetaCoq.SafeChecker.PCUICSafeConversion]
idx:514 [in MetaCoq.Erasure.EEtaExpandedFix]
idx:52 [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
idx:522 [in MetaCoq.SafeChecker.PCUICSafeConversion]
idx:529 [in MetaCoq.SafeChecker.PCUICSafeConversion]
idx:53 [in MetaCoq.PCUIC.PCUICEtaExpand]
idx:54 [in MetaCoq.PCUIC.PCUICCanonicity]
idx:542 [in MetaCoq.Template.Typing]
idx:570 [in MetaCoq.SafeChecker.PCUICSafeConversion]
idx:574 [in MetaCoq.SafeChecker.PCUICSafeConversion]
idx:58 [in MetaCoq.PCUIC.PCUICCanonicity]
idx:59 [in MetaCoq.PCUIC.PCUICNormal]
idx:60 [in MetaCoq.PCUIC.Syntax.PCUICViews]
idx:61 [in MetaCoq.Erasure.EWcbvEval]
idx:62 [in MetaCoq.Template.Normal]
idx:64 [in MetaCoq.Template.Normal]
idx:67 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
idx:67 [in MetaCoq.Erasure.EWcbvEvalInd]
idx:673 [in MetaCoq.PCUIC.PCUICConversion]
idx:673 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
idx:676 [in MetaCoq.PCUIC.PCUICConversion]
idx:683 [in MetaCoq.PCUIC.PCUICConversion]
idx:688 [in MetaCoq.PCUIC.PCUICConversion]
idx:691 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
idx:695 [in MetaCoq.PCUIC.PCUICConversion]
idx:7 [in MetaCoq.PCUIC.PCUICGuardCondition]
idx:70 [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
idx:70 [in MetaCoq.Erasure.EWcbvEval]
idx:701 [in MetaCoq.PCUIC.PCUICConversion]
idx:709 [in MetaCoq.PCUIC.PCUICConversion]
idx:722 [in MetaCoq.PCUIC.PCUICConversion]
idx:73 [in MetaCoq.Erasure.Prelim]
idx:731 [in MetaCoq.PCUIC.PCUICConversion]
idx:75 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
idx:769 [in MetaCoq.PCUIC.PCUICConversion]
idx:77 [in MetaCoq.Erasure.EWcbvEvalInd]
idx:775 [in MetaCoq.PCUIC.PCUICConversion]
idx:79 [in MetaCoq.Erasure.EWcbvEval]
idx:80 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
idx:805 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
idx:84 [in MetaCoq.Erasure.EEtaExpandedFix]
idx:84 [in MetaCoq.PCUIC.Syntax.PCUICViews]
idx:86 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
idx:87 [in MetaCoq.Erasure.EWcbvEvalInd]
idx:88 [in MetaCoq.PCUIC.PCUICNormal]
idx:88 [in MetaCoq.Erasure.EWcbvEval]
idx:89 [in MetaCoq.Erasure.EWellformed]
idx:90 [in MetaCoq.SafeChecker.PCUICErrors]
idx:93 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
idx:93 [in MetaCoq.Erasure.EWellformed]
idx:94 [in MetaCoq.PCUIC.PCUICWcbvEval]
idx:94 [in MetaCoq.SafeChecker.PCUICErrors]
idx:95 [in MetaCoq.Erasure.EEtaExpandedFix]
idx:95 [in MetaCoq.Template.WcbvEval]
idx:95 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
idx:97 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
idx:97 [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
idx:97 [in MetaCoq.Erasure.EWcbvEval]
idx:98 [in MetaCoq.Erasure.EWcbvEvalInd]
idx:990 [in MetaCoq.PCUIC.PCUICReduction]
id':104 [in MetaCoq.Translations.translation_utils]
id':120 [in MetaCoq.Translations.translation_utils]
id':129 [in MetaCoq.Translations.translation_utils]
id':13 [in MetaCoq.Template.Pretty]
id':147 [in MetaCoq.Translations.translation_utils]
id':16 [in MetaCoq.PCUIC.utils.PCUICPretty]
id':18 [in MetaCoq.Template.Kernames]
id':23 [in MetaCoq.Erasure.EPretty]
id':25 [in MetaCoq.Template.Pretty]
id':26 [in MetaCoq.PCUIC.utils.PCUICPretty]
id':79 [in MetaCoq.Translations.translation_utils]
id':93 [in MetaCoq.Translations.translation_utils]
id:1004 [in MetaCoq.SafeChecker.PCUICSafeChecker]
id:1018 [in MetaCoq.SafeChecker.PCUICSafeChecker]
id:102 [in MetaCoq.Translations.translation_utils]
id:11 [in MetaCoq.Template.Checker]
id:12 [in MetaCoq.Erasure.EPretty]
id:12 [in MetaCoq.Template.Pretty]
id:125 [in MetaCoq.PCUIC.PCUICEquality]
id:146 [in MetaCoq.Translations.translation_utils]
id:146 [in MetaCoq.PCUIC.PCUICNormal]
id:15 [in MetaCoq.Erasure.EEtaExpandedFix]
id:15 [in MetaCoq.PCUIC.PCUICEtaExpand]
id:15 [in MetaCoq.Template.Kernames]
id:15 [in MetaCoq.PCUIC.utils.PCUICPretty]
id:152 [in MetaCoq.Template.AstUtils]
id:157 [in MetaCoq.Template.AstUtils]
id:158 [in MetaCoq.Template.EtaExpand]
id:159 [in MetaCoq.PCUIC.PCUICNormal]
id:165 [in MetaCoq.SafeChecker.PCUICErrors]
id:180 [in MetaCoq.Template.Ast]
id:186 [in MetaCoq.Erasure.EEtaExpanded]
id:19 [in MetaCoq.Erasure.EPretty]
id:2 [in MetaCoq.Template.EnvironmentTyping]
id:2 [in MetaCoq.Erasure.EGlobalEnv]
id:21 [in MetaCoq.Template.Pretty]
id:219 [in MetaCoq.Erasure.EEtaExpanded]
id:22 [in MetaCoq.PCUIC.utils.PCUICPretty]
id:24 [in MetaCoq.Template.TemplateMonad.Core]
id:249 [in MetaCoq.SafeChecker.PCUICErrors]
id:25 [in MetaCoq.Template.TemplateMonad.Core]
id:274 [in MetaCoq.SafeChecker.PCUICErrors]
id:29 [in MetaCoq.Erasure.EPretty]
id:3 [in MetaCoq.Examples.add_constructor]
id:319 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
id:32 [in MetaCoq.Template.Pretty]
id:33 [in MetaCoq.PCUIC.utils.PCUICPretty]
id:359 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
id:362 [in MetaCoq.PCUIC.PCUICNormal]
id:37 [in MetaCoq.Translations.translation_utils]
id:371 [in MetaCoq.Template.Checker]
id:381 [in MetaCoq.Template.Checker]
id:39 [in MetaCoq.Template.TemplateMonad.Core]
id:395 [in MetaCoq.Template.Checker]
id:398 [in MetaCoq.Template.Checker]
id:400 [in MetaCoq.SafeChecker.PCUICSafeChecker]
id:402 [in MetaCoq.Template.Checker]
id:417 [in MetaCoq.Template.Checker]
id:42 [in MetaCoq.Template.TemplateMonad.Core]
id:46 [in MetaCoq.Template.TemplateMonad.Core]
id:49 [in MetaCoq.Template.TemplateMonad.Core]
id:53 [in MetaCoq.Translations.translation_utils]
id:54 [in MetaCoq.Template.EnvironmentTyping]
id:55 [in MetaCoq.Erasure.EEtaExpandedFix]
id:59 [in MetaCoq.Template.EnvironmentTyping]
id:6 [in MetaCoq.Template.Kernames]
id:6 [in MetaCoq.Erasure.EGlobalEnv]
id:646 [in MetaCoq.SafeChecker.PCUICSafeChecker]
id:66 [in MetaCoq.Template.AstUtils]
id:68 [in MetaCoq.SafeChecker.PCUICSafeChecker]
id:7 [in MetaCoq.Template.WfAst]
id:709 [in MetaCoq.SafeChecker.PCUICSafeChecker]
id:71 [in MetaCoq.Erasure.EGlobalEnv]
id:74 [in MetaCoq.PCUIC.PCUICEtaExpand]
id:75 [in MetaCoq.SafeChecker.PCUICSafeChecker]
id:793 [in MetaCoq.SafeChecker.PCUICSafeChecker]
id:81 [in MetaCoq.Template.TermEquality]
id:88 [in MetaCoq.Translations.translation_utils]
id:9 [in MetaCoq.Template.Kernames]
id:94 [in MetaCoq.Template.EtaExpand]
id:946 [in MetaCoq.SafeChecker.PCUICSafeChecker]
id:95 [in MetaCoq.SafeChecker.PCUICSafeChecker]
id:981 [in MetaCoq.SafeChecker.PCUICSafeChecker]
IH:303 [in MetaCoq.PCUIC.PCUICInductives]
IH:630 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
il:1100 [in MetaCoq.Template.utils.All_Forall]
inapp:122 [in MetaCoq.PCUIC.utils.PCUICPretty]
inapp:41 [in MetaCoq.Erasure.EPretty]
inapp:71 [in MetaCoq.PCUIC.utils.PCUICPretty]
inclre:562 [in MetaCoq.PCUIC.PCUICConfluence]
indargs:125 [in MetaCoq.PCUIC.PCUICCanonicity]
indargs:139 [in MetaCoq.PCUIC.PCUICCanonicity]
indargs:159 [in MetaCoq.PCUIC.PCUICCanonicity]
indargs:202 [in MetaCoq.PCUIC.PCUICCanonicity]
indargs:357 [in MetaCoq.Template.Checker]
indargs:364 [in MetaCoq.Template.Checker]
indb:294 [in MetaCoq.PCUIC.PCUICInductives]
indctx':50 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
indctx':660 [in MetaCoq.PCUIC.PCUICInductiveInversion]
indctx:146 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
indctx:49 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
indctx:659 [in MetaCoq.PCUIC.PCUICInductiveInversion]
inddecl:16 [in MetaCoq.PCUIC.Syntax.PCUICCases]
inddecl:336 [in MetaCoq.Template.Ast]
index_names:41 [in MetaCoq.Template.Pretty]
index_terms:156 [in MetaCoq.Template.AstUtils]
indices:1021 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
indices:104 [in MetaCoq.PCUIC.Syntax.PCUICCases]
indices:1058 [in MetaCoq.Template.Typing]
indices:1085 [in MetaCoq.SafeChecker.PCUICTypeChecker]
indices:114 [in MetaCoq.PCUIC.PCUICInversion]
indices:128 [in MetaCoq.PCUIC.PCUICTyping]
indices:145 [in MetaCoq.PCUIC.PCUICInversion]
indices:159 [in MetaCoq.Template.AstUtils]
indices:163 [in MetaCoq.PCUIC.PCUICProgress]
indices:17 [in MetaCoq.PCUIC.PCUICExpandLets]
indices:17 [in MetaCoq.Examples.add_constructor]
indices:216 [in MetaCoq.PCUIC.PCUICSubstitution]
indices:226 [in MetaCoq.PCUIC.PCUICSubstitution]
indices:23 [in MetaCoq.PCUIC.PCUICExpandLets]
indices:313 [in MetaCoq.PCUIC.PCUICProgress]
indices:396 [in MetaCoq.Template.Ast]
indices:398 [in MetaCoq.PCUIC.PCUICProgress]
indices:424 [in MetaCoq.PCUIC.PCUICInductives]
indices:46 [in MetaCoq.PCUIC.PCUICElimination]
indices:49 [in MetaCoq.PCUIC.PCUICTyping]
indices:493 [in MetaCoq.Template.EnvironmentTyping]
indices:539 [in MetaCoq.Template.EnvironmentTyping]
indices:555 [in MetaCoq.PCUIC.PCUICTyping]
indices:582 [in MetaCoq.SafeChecker.PCUICSafeChecker]
indices:636 [in MetaCoq.SafeChecker.PCUICSafeChecker]
indices:652 [in MetaCoq.Template.Typing]
indices:656 [in MetaCoq.PCUIC.PCUICInductives]
indices:710 [in MetaCoq.SafeChecker.PCUICSafeChecker]
indices:715 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
indices:75 [in MetaCoq.Template.Pretty]
indices:804 [in MetaCoq.SafeChecker.PCUICSafeChecker]
indices:82 [in MetaCoq.PCUIC.utils.PCUICPretty]
indices:826 [in MetaCoq.SafeChecker.PCUICSafeChecker]
indices:832 [in MetaCoq.SafeChecker.PCUICSafeChecker]
indices:878 [in MetaCoq.PCUIC.PCUICTyping]
indices:885 [in MetaCoq.SafeChecker.PCUICSafeChecker]
indices:904 [in MetaCoq.SafeChecker.PCUICSafeChecker]
indices:930 [in MetaCoq.SafeChecker.PCUICSafeChecker]
indices:951 [in MetaCoq.SafeChecker.PCUICSafeChecker]
indn:115 [in MetaCoq.PCUIC.PCUICAst]
indn:162 [in MetaCoq.PCUIC.PCUICEquality]
indn:295 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
indn:454 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
indn:627 [in MetaCoq.PCUIC.PCUICConversion]
indn:642 [in MetaCoq.PCUIC.PCUICConversion]
indn:78 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
indrel:153 [in MetaCoq.Template.AstUtils]
indsubst:122 [in MetaCoq.PCUIC.PCUICInductives]
indsubst:129 [in MetaCoq.PCUIC.PCUICInductives]
indsubst:136 [in MetaCoq.PCUIC.PCUICInductives]
indsubst:185 [in MetaCoq.PCUIC.PCUICInductives]
indsubst:299 [in MetaCoq.PCUIC.PCUICInductives]
indsubst:315 [in MetaCoq.PCUIC.PCUICInductiveInversion]
indsubst:329 [in MetaCoq.PCUIC.PCUICInductives]
indsubst:743 [in MetaCoq.PCUIC.PCUICInductiveInversion]
indsubst:85 [in MetaCoq.PCUIC.PCUICInductives]
inds:10 [in MetaCoq.PCUIC.PCUICSR]
inds:13 [in MetaCoq.PCUIC.PCUICFirstorder]
inds:26 [in MetaCoq.PCUIC.PCUICSR]
inds:27 [in MetaCoq.PCUIC.PCUICSR]
inds:304 [in MetaCoq.PCUIC.PCUICSubstitution]
inds:309 [in MetaCoq.PCUIC.PCUICSubstitution]
inds:638 [in MetaCoq.SafeChecker.PCUICSafeChecker]
inds:806 [in MetaCoq.SafeChecker.PCUICSafeChecker]
inds:9 [in MetaCoq.PCUIC.PCUICSR]
indtys:965 [in MetaCoq.SafeChecker.PCUICSafeChecker]
indty:15 [in MetaCoq.PCUIC.Syntax.PCUICCases]
indty:335 [in MetaCoq.Template.Ast]
indty:40 [in MetaCoq.PCUIC.PCUICCasesContexts]
ind_sort:74 [in MetaCoq.PCUIC.PCUICElimination]
ind_indices:73 [in MetaCoq.PCUIC.PCUICElimination]
ind_type':104 [in MetaCoq.Translations.times_bool_fun]
ind_type':102 [in MetaCoq.Translations.times_bool_fun]
ind_sort:623 [in MetaCoq.Template.EnvironmentTyping]
ind_indices:621 [in MetaCoq.Template.EnvironmentTyping]
ind_ctors_sort:616 [in MetaCoq.Template.EnvironmentTyping]
ind_ctors_sort:614 [in MetaCoq.Template.EnvironmentTyping]
ind_sort:611 [in MetaCoq.Template.EnvironmentTyping]
ind_indices:601 [in MetaCoq.Template.EnvironmentTyping]
ind_indices:577 [in MetaCoq.Template.EnvironmentTyping]
ind_indices:556 [in MetaCoq.Template.EnvironmentTyping]
ind_indices:457 [in MetaCoq.PCUIC.PCUICInductiveInversion]
ind_inst:126 [in MetaCoq.PCUIC.PCUICInversion]
ind_inst:59 [in MetaCoq.PCUIC.PCUICTyping]
ind_sort:933 [in MetaCoq.SafeChecker.PCUICSafeChecker]
ind_sort:922 [in MetaCoq.SafeChecker.PCUICSafeChecker]
ind_sort:915 [in MetaCoq.SafeChecker.PCUICSafeChecker]
ind_ctors:161 [in MetaCoq.Template.AstUtils]
ind_ctor_sort:173 [in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
ind':1075 [in MetaCoq.SafeChecker.PCUICTypeChecker]
ind':1100 [in MetaCoq.SafeChecker.PCUICTypeChecker]
ind':124 [in MetaCoq.PCUIC.Bidirectional.BDUnique]
ind':137 [in MetaCoq.PCUIC.Bidirectional.BDUnique]
ind':170 [in MetaCoq.PCUIC.PCUICCanonicity]
ind':221 [in MetaCoq.PCUIC.PCUICInductiveInversion]
ind':28 [in MetaCoq.PCUIC.Bidirectional.BDUnique]
ind':281 [in MetaCoq.PCUIC.PCUICSafeLemmata]
ind':33 [in MetaCoq.Examples.add_constructor]
ind':352 [in MetaCoq.PCUIC.PCUICCumulProp]
ind':362 [in MetaCoq.PCUIC.PCUICCumulProp]
ind':398 [in MetaCoq.PCUIC.PCUICConversion]
ind':46 [in MetaCoq.PCUIC.PCUICAlpha]
ind':479 [in MetaCoq.PCUIC.PCUICConversion]
ind':95 [in MetaCoq.PCUIC.PCUICInductiveInversion]
ind0:19 [in MetaCoq.Examples.add_constructor]
ind1:359 [in MetaCoq.Template.Checker]
ind2:360 [in MetaCoq.Template.Checker]
ind:1 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
ind:10 [in MetaCoq.Erasure.ESubstitution]
ind:10 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
ind:10 [in MetaCoq.Erasure.ErasureFunction]
ind:10 [in MetaCoq.Erasure.EEtaExpanded]
ind:100 [in MetaCoq.Erasure.EInlineProjections]
ind:100 [in MetaCoq.PCUIC.PCUICEtaExpand]
ind:100 [in MetaCoq.PCUIC.PCUICInversion]
ind:100 [in MetaCoq.Erasure.EGlobalEnv]
ind:1027 [in MetaCoq.Erasure.ErasureFunction]
ind:103 [in MetaCoq.Template.TypingWf]
ind:1034 [in MetaCoq.Template.Typing]
ind:104 [in MetaCoq.PCUIC.PCUICInductives]
ind:104 [in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
ind:1043 [in MetaCoq.Template.Typing]
ind:105 [in MetaCoq.PCUIC.PCUICInductiveInversion]
ind:105 [in MetaCoq.Erasure.EGlobalEnv]
ind:106 [in MetaCoq.Erasure.EInlineProjections]
ind:106 [in MetaCoq.PCUIC.Syntax.PCUICCases]
ind:107 [in MetaCoq.PCUIC.PCUICFirstorder]
ind:108 [in MetaCoq.PCUIC.PCUICWeakeningEnv]
ind:108 [in MetaCoq.Erasure.EArities]
ind:108 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
ind:108 [in MetaCoq.Template.TypingWf]
ind:109 [in MetaCoq.PCUIC.PCUICInductives]
ind:109 [in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
ind:1099 [in MetaCoq.PCUIC.PCUICConversion]
ind:11 [in MetaCoq.PCUIC.Syntax.PCUICCases]
ind:11 [in MetaCoq.Erasure.EExtends]
ind:110 [in MetaCoq.PCUIC.PCUICAst]
ind:110 [in MetaCoq.Template.AstUtils]
ind:110 [in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
ind:1106 [in MetaCoq.PCUIC.PCUICConversion]
ind:111 [in MetaCoq.Erasure.EEtaExpanded]
ind:112 [in MetaCoq.Erasure.EInlineProjections]
ind:112 [in MetaCoq.PCUIC.PCUICInductives]
ind:112 [in MetaCoq.PCUIC.PCUICAst]
ind:113 [in MetaCoq.PCUIC.PCUICWeakeningEnv]
ind:113 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
ind:114 [in MetaCoq.PCUIC.PCUICTyping]
ind:115 [in MetaCoq.Template.EtaExpand]
ind:115 [in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
ind:117 [in MetaCoq.Template.EtaExpand]
ind:117 [in MetaCoq.PCUIC.PCUICAlpha]
ind:117 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
ind:117 [in MetaCoq.Erasure.EOptimizePropDiscr]
ind:118 [in MetaCoq.Template.TermEquality]
ind:118 [in MetaCoq.PCUIC.PCUICInductives]
ind:118 [in MetaCoq.PCUIC.PCUICTyping]
ind:119 [in MetaCoq.PCUIC.PCUICWeakeningEnv]
ind:119 [in MetaCoq.Erasure.EArities]
ind:12 [in MetaCoq.Erasure.EGlobalEnv]
ind:120 [in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
ind:120 [in MetaCoq.Erasure.EOptimizePropDiscr]
ind:120 [in MetaCoq.Template.AstUtils]
ind:121 [in MetaCoq.Erasure.EWellformed]
ind:121 [in MetaCoq.Template.Checker]
ind:121 [in MetaCoq.Erasure.Prelim]
ind:122 [in MetaCoq.PCUIC.PCUICAlpha]
ind:122 [in MetaCoq.Erasure.EWcbvEval]
ind:123 [in MetaCoq.PCUIC.PCUICCanonicity]
ind:123 [in MetaCoq.PCUIC.Bidirectional.BDUnique]
ind:123 [in MetaCoq.Erasure.ERemoveParams]
ind:1233 [in MetaCoq.PCUIC.PCUICConversion]
ind:125 [in MetaCoq.PCUIC.PCUICElimination]
ind:125 [in MetaCoq.PCUIC.PCUICInductives]
ind:126 [in MetaCoq.PCUIC.PCUICWeakeningEnv]
ind:126 [in MetaCoq.PCUIC.PCUICWcbvEval]
ind:126 [in MetaCoq.Erasure.EEtaExpanded]
ind:126 [in MetaCoq.Template.Pretty]
ind:1263 [in MetaCoq.PCUIC.PCUICConfluence]
ind:127 [in MetaCoq.Erasure.EWellformed]
ind:1270 [in MetaCoq.PCUIC.PCUICConfluence]
ind:128 [in MetaCoq.Erasure.Extract]
ind:128 [in MetaCoq.Template.WcbvEval]
ind:13 [in MetaCoq.Template.EtaExpand]
ind:13 [in MetaCoq.PCUIC.PCUICProgram]
ind:130 [in MetaCoq.PCUIC.PCUICAlpha]
ind:130 [in MetaCoq.Template.Checker]
ind:1308 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
ind:131 [in MetaCoq.Erasure.EWcbvEval]
ind:132 [in MetaCoq.PCUIC.PCUICEtaExpand]
ind:132 [in MetaCoq.PCUIC.PCUICInductives]
ind:132 [in MetaCoq.Erasure.EOptimizePropDiscr]
ind:133 [in MetaCoq.Erasure.EWellformed]
ind:133 [in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
ind:134 [in MetaCoq.Template.Checker]
ind:1344 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
ind:135 [in MetaCoq.Erasure.EOptimizePropDiscr]
ind:136 [in MetaCoq.PCUIC.Bidirectional.BDUnique]
ind:137 [in MetaCoq.Translations.param_cheap_packed]
ind:137 [in MetaCoq.PCUIC.PCUICCanonicity]
ind:138 [in MetaCoq.Template.Checker]
ind:138 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
ind:139 [in MetaCoq.PCUIC.PCUICProgress]
ind:14 [in MetaCoq.Template.Pretty]
ind:140 [in MetaCoq.PCUIC.PCUICInductives]
ind:1405 [in MetaCoq.SafeChecker.PCUICSafeReduce]
ind:141 [in MetaCoq.Template.EtaExpand]
ind:141 [in MetaCoq.PCUIC.PCUICElimination]
ind:1412 [in MetaCoq.SafeChecker.PCUICSafeReduce]
ind:142 [in MetaCoq.Erasure.EEtaExpandedFix]
ind:142 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
ind:143 [in MetaCoq.Erasure.EWcbvEvalInd]
ind:143 [in MetaCoq.Translations.param_cheap_packed]
ind:144 [in MetaCoq.PCUIC.PCUICWcbvEval]
ind:144 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
ind:148 [in MetaCoq.PCUIC.PCUICProgress]
ind:148 [in MetaCoq.PCUIC.Bidirectional.BDUnique]
ind:148 [in MetaCoq.Erasure.EWcbvEval]
ind:149 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
ind:149 [in MetaCoq.PCUIC.PCUICAlpha]
ind:15 [in MetaCoq.Erasure.EArities]
ind:15 [in MetaCoq.PCUIC.PCUICCumulProp]
ind:15 [in MetaCoq.Erasure.ErasureFunction]
ind:15 [in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
ind:150 [in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
ind:150 [in MetaCoq.PCUIC.PCUICWcbvEval]
ind:153 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
ind:156 [in MetaCoq.Template.Typing]
ind:157 [in MetaCoq.Erasure.EWcbvEvalInd]
ind:157 [in MetaCoq.PCUIC.PCUICCanonicity]
ind:157 [in MetaCoq.Template.TypingWf]
ind:16 [in MetaCoq.Erasure.EExtends]
ind:162 [in MetaCoq.PCUIC.PCUICElimination]
ind:162 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
ind:162 [in MetaCoq.Erasure.EWcbvEval]
ind:163 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
ind:163 [in MetaCoq.Erasure.ERemoveParams]
ind:164 [in MetaCoq.Template.Typing]
ind:165 [in MetaCoq.Erasure.EEtaExpandedFix]
ind:165 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
ind:165 [in MetaCoq.Erasure.ERemoveParams]
ind:167 [in MetaCoq.PCUIC.PCUICCanonicity]
ind:167 [in MetaCoq.Erasure.EEtaExpanded]
ind:169 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
ind:17 [in MetaCoq.PCUIC.Syntax.PCUICCases]
ind:170 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
ind:171 [in MetaCoq.Template.TypingWf]
ind:173 [in MetaCoq.PCUIC.PCUICContexts]
ind:1733 [in MetaCoq.SafeChecker.PCUICSafeReduce]
ind:174 [in MetaCoq.Template.WcbvEval]
ind:174 [in MetaCoq.Template.TypingWf]
ind:176 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
ind:176 [in MetaCoq.Erasure.EWcbvEval]
ind:177 [in MetaCoq.Template.Typing]
ind:177 [in MetaCoq.PCUIC.PCUICInductives]
ind:177 [in MetaCoq.PCUIC.PCUICCanonicity]
ind:178 [in MetaCoq.PCUIC.PCUICElimination]
ind:178 [in MetaCoq.PCUIC.PCUICArities]
ind:18 [in MetaCoq.PCUIC.PCUICInductives]
ind:180 [in MetaCoq.PCUIC.PCUICAlpha]
ind:180 [in MetaCoq.Template.TypingWf]
ind:181 [in MetaCoq.PCUIC.PCUICInductives]
ind:181 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
ind:181 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
ind:182 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
ind:182 [in MetaCoq.Template.Typing]
ind:186 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
ind:186 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
ind:186 [in MetaCoq.PCUIC.PCUICInductives]
ind:187 [in MetaCoq.PCUIC.PCUICWfUniverses]
ind:187 [in MetaCoq.SafeChecker.PCUICSafeReduce]
ind:187 [in MetaCoq.Template.TypingWf]
ind:188 [in MetaCoq.Template.EtaExpand]
ind:188 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
ind:188 [in MetaCoq.Erasure.EConstructorsAsBlocks]
ind:19 [in MetaCoq.PCUIC.PCUICElimination]
ind:19 [in MetaCoq.PCUIC.TemplateToPCUIC]
ind:190 [in MetaCoq.PCUIC.PCUICAlpha]
ind:190 [in MetaCoq.PCUIC.PCUICSR]
ind:191 [in MetaCoq.Template.EtaExpand]
ind:193 [in MetaCoq.PCUIC.PCUICArities]
ind:194 [in MetaCoq.Erasure.EConstructorsAsBlocks]
ind:196 [in MetaCoq.PCUIC.Syntax.PCUICCases]
ind:196 [in MetaCoq.Erasure.EWcbvEval]
ind:197 [in MetaCoq.Erasure.EEtaExpanded]
ind:197 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
ind:199 [in MetaCoq.Erasure.EConstructorsAsBlocks]
ind:2 [in MetaCoq.Erasure.EPretty]
ind:2 [in MetaCoq.PCUIC.Syntax.PCUICCases]
ind:2 [in MetaCoq.PCUIC.utils.PCUICPretty]
ind:20 [in MetaCoq.PCUIC.PCUICFirstorder]
ind:20 [in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
ind:200 [in MetaCoq.PCUIC.PCUICCanonicity]
ind:200 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
ind:201 [in MetaCoq.Template.Ast]
ind:201 [in MetaCoq.PCUIC.PCUICInductiveInversion]
ind:201 [in MetaCoq.PCUIC.Syntax.PCUICCases]
ind:203 [in MetaCoq.Erasure.Extract]
ind:203 [in MetaCoq.Template.Ast]
ind:203 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
ind:204 [in MetaCoq.Erasure.EWcbvEval]
ind:206 [in MetaCoq.PCUIC.Syntax.PCUICCases]
ind:207 [in MetaCoq.PCUIC.PCUICInductives]
ind:209 [in MetaCoq.Template.TypingWf]
ind:21 [in MetaCoq.PCUIC.PCUICTyping]
ind:210 [in MetaCoq.Erasure.EEtaExpanded]
ind:211 [in MetaCoq.PCUIC.Syntax.PCUICCases]
ind:213 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
ind:214 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
ind:214 [in MetaCoq.PCUIC.PCUICInductives]
ind:216 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
ind:217 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
ind:218 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
ind:218 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
ind:22 [in MetaCoq.Erasure.EArities]
ind:22 [in MetaCoq.Template.TermEquality]
ind:221 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
ind:222 [in MetaCoq.Template.WcbvEval]
ind:223 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
ind:223 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
ind:223 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
ind:225 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
ind:225 [in MetaCoq.PCUIC.Syntax.PCUICCases]
ind:226 [in MetaCoq.Template.EtaExpand]
ind:230 [in MetaCoq.PCUIC.PCUICSubstitution]
ind:230 [in MetaCoq.Erasure.EEtaExpanded]
ind:231 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
ind:231 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
ind:231 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
ind:235 [in MetaCoq.Template.Environment]
ind:235 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
ind:237 [in MetaCoq.Erasure.EConstructorsAsBlocks]
ind:238 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
ind:239 [in MetaCoq.PCUIC.PCUICAst]
ind:24 [in MetaCoq.Template.TermEquality]
ind:24 [in MetaCoq.PCUIC.PCUICPrincipality]
ind:24 [in MetaCoq.PCUIC.Bidirectional.BDUnique]
ind:24 [in MetaCoq.Examples.add_constructor]
ind:244 [in MetaCoq.Erasure.Extract]
ind:245 [in MetaCoq.Template.WcbvEval]
ind:246 [in MetaCoq.Erasure.EEtaExpanded]
ind:25 [in MetaCoq.Erasure.EEtaExpanded]
ind:25 [in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
ind:250 [in MetaCoq.Erasure.Extract]
ind:252 [in MetaCoq.PCUIC.PCUICInductiveInversion]
ind:253 [in MetaCoq.Template.WcbvEval]
ind:254 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
ind:254 [in MetaCoq.PCUIC.PCUICReduction]
ind:256 [in MetaCoq.PCUIC.PCUICWcbvEval]
ind:257 [in MetaCoq.PCUIC.PCUICWfUniverses]
ind:257 [in MetaCoq.Erasure.EWcbvEval]
ind:26 [in MetaCoq.Erasure.EEtaExpandedFix]
ind:26 [in MetaCoq.Erasure.EWcbvEvalInd]
ind:26 [in MetaCoq.PCUIC.PCUICCanonicity]
ind:26 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
ind:262 [in MetaCoq.PCUIC.PCUICWfUniverses]
ind:265 [in MetaCoq.Erasure.EWcbvEval]
ind:266 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
ind:267 [in MetaCoq.Erasure.EEtaExpanded]
ind:27 [in MetaCoq.Template.EnvironmentTyping]
ind:27 [in MetaCoq.PCUIC.TemplateToPCUIC]
ind:270 [in MetaCoq.Template.TypingWf]
ind:271 [in MetaCoq.PCUIC.PCUICWcbvEval]
ind:271 [in MetaCoq.Template.Environment]
ind:272 [in MetaCoq.Erasure.EArities]
ind:274 [in MetaCoq.Erasure.EEtaExpanded]
ind:276 [in MetaCoq.Template.Environment]
ind:28 [in MetaCoq.PCUIC.PCUICInductives]
ind:282 [in MetaCoq.PCUIC.PCUICInductives]
ind:283 [in MetaCoq.PCUIC.PCUICInductiveInversion]
ind:285 [in MetaCoq.Template.Ast]
ind:286 [in MetaCoq.Template.EtaExpand]
ind:288 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
ind:289 [in MetaCoq.PCUIC.PCUICProgress]
ind:289 [in MetaCoq.PCUIC.PCUICInductives]
ind:29 [in MetaCoq.PCUIC.PCUICElimination]
ind:29 [in MetaCoq.Template.EnvironmentTyping]
ind:292 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
ind:293 [in MetaCoq.Erasure.EArities]
ind:297 [in MetaCoq.Erasure.EEtaExpandedFix]
ind:298 [in MetaCoq.PCUIC.PCUICProgress]
ind:298 [in MetaCoq.Template.TypingWf]
ind:299 [in MetaCoq.Erasure.EArities]
ind:299 [in MetaCoq.SafeChecker.PCUICSafeReduce]
ind:30 [in MetaCoq.PCUIC.PCUICGlobalEnv]
ind:30 [in MetaCoq.PCUIC.PCUICCanonicity]
ind:304 [in MetaCoq.Erasure.EArities]
ind:304 [in MetaCoq.Template.TypingWf]
ind:31 [in MetaCoq.PCUIC.PCUICFirstorder]
ind:312 [in MetaCoq.Erasure.EArities]
ind:312 [in MetaCoq.PCUIC.PCUICWcbvEval]
ind:313 [in MetaCoq.PCUIC.PCUICInductives]
ind:314 [in MetaCoq.PCUIC.PCUICCumulProp]
ind:314 [in MetaCoq.Erasure.ERemoveParams]
ind:317 [in MetaCoq.Erasure.EEtaExpandedFix]
ind:318 [in MetaCoq.Erasure.ERemoveParams]
ind:322 [in MetaCoq.Erasure.ERemoveParams]
ind:322 [in MetaCoq.SafeChecker.PCUICSafeChecker]
ind:324 [in MetaCoq.PCUIC.PCUICInductives]
ind:324 [in MetaCoq.Template.Ast]
ind:327 [in MetaCoq.Template.Ast]
ind:328 [in MetaCoq.SafeChecker.PCUICSafeReduce]
ind:33 [in MetaCoq.PCUIC.PCUICEtaExpand]
ind:331 [in MetaCoq.Template.Ast]
ind:333 [in MetaCoq.Template.Typing]
ind:34 [in MetaCoq.PCUIC.PCUICGlobalEnv]
ind:34 [in MetaCoq.Erasure.EWcbvEval]
ind:340 [in MetaCoq.Template.Ast]
ind:341 [in MetaCoq.Erasure.ERemoveParams]
ind:342 [in MetaCoq.SafeChecker.PCUICSafeChecker]
ind:343 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
ind:345 [in MetaCoq.Template.Ast]
ind:345 [in MetaCoq.Erasure.ERemoveParams]
ind:347 [in MetaCoq.SafeChecker.PCUICSafeChecker]
ind:348 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
ind:348 [in MetaCoq.PCUIC.PCUICConversion]
ind:349 [in MetaCoq.PCUIC.PCUICCumulProp]
ind:35 [in MetaCoq.PCUIC.PCUICCasesContexts]
ind:35 [in MetaCoq.PCUIC.TemplateToPCUICExpanded]
ind:351 [in MetaCoq.Template.Ast]
ind:351 [in MetaCoq.Erasure.ERemoveParams]
ind:355 [in MetaCoq.Template.Typing]
ind:355 [in MetaCoq.Template.Ast]
ind:357 [in MetaCoq.Erasure.ERemoveParams]
ind:358 [in MetaCoq.Template.Ast]
ind:359 [in MetaCoq.PCUIC.PCUICCumulProp]
ind:36 [in MetaCoq.PCUIC.PCUICAlpha]
ind:361 [in MetaCoq.Template.Typing]
ind:364 [in MetaCoq.PCUIC.PCUICWcbvEval]
ind:364 [in MetaCoq.Template.Ast]
ind:367 [in MetaCoq.PCUIC.PCUICConversion]
ind:369 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
ind:369 [in MetaCoq.Template.Ast]
ind:37 [in MetaCoq.PCUIC.PCUICArities]
ind:37 [in MetaCoq.PCUIC.PCUICCasesContexts]
ind:37 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
ind:37 [in MetaCoq.Erasure.EGenericMapEnv]
ind:370 [in MetaCoq.PCUIC.PCUICWcbvEval]
ind:374 [in MetaCoq.PCUIC.PCUICProgress]
ind:376 [in MetaCoq.Erasure.EEtaExpandedFix]
ind:377 [in MetaCoq.Template.Ast]
ind:378 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
ind:38 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
ind:38 [in MetaCoq.PCUIC.PCUICEquality]
ind:38 [in MetaCoq.Template.Pretty]
ind:382 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
ind:382 [in MetaCoq.PCUIC.PCUICProgress]
ind:383 [in MetaCoq.Erasure.EEtaExpandedFix]
ind:383 [in MetaCoq.Template.Ast]
ind:387 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
ind:389 [in MetaCoq.PCUIC.PCUICConversion]
ind:39 [in MetaCoq.PCUIC.Syntax.PCUICCases]
ind:39 [in MetaCoq.PCUIC.PCUICGlobalEnv]
ind:39 [in MetaCoq.Erasure.EGenericMapEnv]
ind:39 [in MetaCoq.SafeChecker.PCUICTypeChecker]
ind:390 [in MetaCoq.PCUIC.PCUICProgress]
ind:393 [in MetaCoq.PCUIC.PCUICInductives]
ind:397 [in MetaCoq.PCUIC.PCUICConversion]
ind:398 [in MetaCoq.Template.Ast]
ind:4 [in MetaCoq.PCUIC.Syntax.PCUICCases]
ind:40 [in MetaCoq.Template.EnvironmentTyping]
ind:40 [in MetaCoq.PCUIC.PCUICInductives]
ind:40 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
ind:402 [in MetaCoq.PCUIC.PCUICProgress]
ind:402 [in MetaCoq.PCUIC.PCUICInductives]
ind:403 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
ind:406 [in MetaCoq.SafeChecker.PCUICSafeChecker]
ind:407 [in MetaCoq.Template.EtaExpand]
ind:407 [in MetaCoq.Erasure.EEtaExpandedFix]
ind:409 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
ind:41 [in MetaCoq.PCUIC.PCUICConvCumInversion]
ind:41 [in MetaCoq.PCUIC.PCUICCasesContexts]
ind:41 [in MetaCoq.PCUIC.PCUICContexts]
ind:413 [in MetaCoq.Erasure.ERemoveParams]
ind:416 [in MetaCoq.PCUIC.PCUICInductives]
ind:416 [in MetaCoq.Erasure.ERemoveParams]
ind:417 [in MetaCoq.Template.EtaExpand]
ind:418 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
ind:42 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
ind:42 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
ind:42 [in MetaCoq.Erasure.EWcbvEvalInd]
ind:42 [in MetaCoq.PCUIC.Conversion.PCUICClosedConv]
ind:422 [in MetaCoq.Erasure.ERemoveParams]
ind:424 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
ind:424 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
ind:427 [in MetaCoq.PCUIC.PCUICInductiveInversion]
ind:43 [in MetaCoq.Erasure.EEtaExpandedFix]
ind:43 [in MetaCoq.Template.EnvironmentTyping]
ind:43 [in MetaCoq.PCUIC.PCUICAlpha]
ind:43 [in MetaCoq.Erasure.EWcbvEval]
ind:430 [in MetaCoq.PCUIC.PCUICInductiveInversion]
ind:432 [in MetaCoq.Erasure.EEtaExpandedFix]
ind:434 [in MetaCoq.PCUIC.PCUICSR]
ind:436 [in MetaCoq.Erasure.EWcbvEval]
ind:439 [in MetaCoq.PCUIC.PCUICInductiveInversion]
ind:44 [in MetaCoq.PCUIC.Syntax.PCUICCases]
ind:443 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
ind:448 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
ind:45 [in MetaCoq.Erasure.EGenericMapEnv]
ind:453 [in MetaCoq.PCUIC.PCUICInductiveInversion]
ind:458 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
ind:46 [in MetaCoq.Template.EnvironmentTyping]
ind:466 [in MetaCoq.PCUIC.PCUICInductives]
ind:466 [in MetaCoq.PCUIC.PCUICInductiveInversion]
ind:467 [in MetaCoq.PCUIC.PCUICConversion]
ind:47 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
ind:470 [in MetaCoq.PCUIC.PCUICInductives]
ind:474 [in MetaCoq.PCUIC.PCUICConversion]
ind:478 [in MetaCoq.PCUIC.PCUICConversion]
ind:479 [in MetaCoq.PCUIC.PCUICInductives]
ind:48 [in MetaCoq.PCUIC.PCUICGlobalEnv]
ind:48 [in MetaCoq.Erasure.EEnvMap]
ind:48 [in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
ind:48 [in MetaCoq.SafeChecker.PCUICTypeChecker]
ind:485 [in MetaCoq.PCUIC.PCUICInductives]
ind:486 [in MetaCoq.PCUIC.PCUICConversion]
ind:488 [in MetaCoq.PCUIC.PCUICInductives]
ind:49 [in MetaCoq.PCUIC.PCUICCasesContexts]
ind:49 [in MetaCoq.PCUIC.PCUICContexts]
ind:491 [in MetaCoq.PCUIC.PCUICConversion]
ind:498 [in MetaCoq.Template.EtaExpand]
ind:50 [in MetaCoq.Template.EnvironmentTyping]
ind:50 [in MetaCoq.PCUIC.Syntax.PCUICCases]
ind:50 [in MetaCoq.PCUIC.TemplateToPCUICExpanded]
ind:50 [in MetaCoq.Erasure.EGenericMapEnv]
ind:500 [in MetaCoq.Template.EtaExpand]
ind:513 [in MetaCoq.SafeChecker.PCUICTypeChecker]
ind:52 [in MetaCoq.Erasure.EWcbvEval]
ind:524 [in MetaCoq.PCUIC.PCUICInductives]
ind:531 [in MetaCoq.PCUIC.PCUICTyping]
ind:54 [in MetaCoq.PCUIC.PCUICInductives]
ind:54 [in MetaCoq.PCUIC.PCUICInductiveInversion]
ind:54 [in MetaCoq.PCUIC.Syntax.PCUICCases]
ind:54 [in MetaCoq.PCUIC.PCUICCasesContexts]
ind:54 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
ind:54 [in MetaCoq.Translations.param_original]
ind:54 [in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
ind:540 [in MetaCoq.PCUIC.PCUICTyping]
ind:55 [in MetaCoq.PCUIC.PCUICEtaExpand]
ind:55 [in MetaCoq.Erasure.EEnvMap]
ind:56 [in MetaCoq.PCUIC.Syntax.PCUICViews]
ind:56 [in MetaCoq.Erasure.EGenericMapEnv]
ind:57 [in MetaCoq.Erasure.Extract]
ind:57 [in MetaCoq.PCUIC.Syntax.PCUICCases]
ind:57 [in MetaCoq.PCUIC.PCUICContexts]
ind:58 [in MetaCoq.Translations.param_binary]
ind:58 [in MetaCoq.Erasure.EWcbvEvalInd]
ind:58 [in MetaCoq.Translations.param_original]
ind:582 [in MetaCoq.Template.Typing]
ind:583 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
ind:587 [in MetaCoq.Template.EnvironmentTyping]
ind:590 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
ind:61 [in MetaCoq.Template.Checker]
ind:610 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
ind:610 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
ind:62 [in MetaCoq.Translations.param_binary]
ind:62 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
ind:621 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
ind:63 [in MetaCoq.PCUIC.Syntax.PCUICCases]
ind:63 [in MetaCoq.Template.Checker]
ind:630 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
ind:636 [in MetaCoq.Template.Typing]
ind:64 [in MetaCoq.Erasure.EArities]
ind:64 [in MetaCoq.PCUIC.PCUICInductiveInversion]
ind:64 [in MetaCoq.Erasure.EGlobalEnv]
ind:640 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
ind:641 [in MetaCoq.Template.Typing]
ind:644 [in MetaCoq.PCUIC.PCUICSR]
ind:648 [in MetaCoq.PCUIC.PCUICInductiveInversion]
ind:658 [in MetaCoq.PCUIC.PCUICSR]
ind:66 [in MetaCoq.PCUIC.PCUICInductives]
ind:66 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
ind:667 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
ind:67 [in MetaCoq.Template.Checker]
ind:67 [in MetaCoq.Erasure.EGlobalEnv]
ind:671 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
ind:678 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
ind:68 [in MetaCoq.PCUIC.Syntax.PCUICCases]
ind:697 [in MetaCoq.PCUIC.PCUICSR]
ind:7 [in MetaCoq.PCUIC.Syntax.PCUICCases]
ind:7 [in MetaCoq.Erasure.EExtends]
ind:70 [in MetaCoq.PCUIC.PCUICInductives]
ind:701 [in MetaCoq.SafeChecker.PCUICSafeChecker]
ind:71 [in MetaCoq.PCUIC.PCUICElimination]
ind:727 [in MetaCoq.PCUIC.PCUICInductiveInversion]
ind:73 [in MetaCoq.Erasure.EEtaExpandedFix]
ind:74 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
ind:74 [in MetaCoq.PCUIC.Syntax.PCUICCases]
ind:74 [in MetaCoq.Template.Checker]
ind:74 [in MetaCoq.PCUIC.PCUICCasesContexts]
ind:744 [in MetaCoq.PCUIC.PCUICInductiveInversion]
ind:75 [in MetaCoq.PCUIC.PCUICInductiveInversion]
ind:765 [in MetaCoq.PCUIC.PCUICInductiveInversion]
ind:772 [in MetaCoq.PCUIC.PCUICInductiveInversion]
ind:79 [in MetaCoq.Erasure.EArities]
ind:79 [in MetaCoq.PCUIC.Syntax.PCUICCases]
ind:79 [in MetaCoq.Template.Checker]
ind:79 [in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
ind:790 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
ind:8 [in MetaCoq.Template.EnvironmentTyping]
ind:8 [in MetaCoq.PCUIC.PCUICGlobalEnv]
ind:81 [in MetaCoq.PCUIC.Syntax.PCUICViews]
ind:84 [in MetaCoq.Erasure.EInlineProjections]
ind:84 [in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
ind:844 [in MetaCoq.SafeChecker.PCUICSafeChecker]
ind:85 [in MetaCoq.PCUIC.Syntax.PCUICCases]
ind:85 [in MetaCoq.Template.Checker]
ind:854 [in MetaCoq.PCUIC.PCUICTyping]
ind:863 [in MetaCoq.PCUIC.PCUICTyping]
ind:87 [in MetaCoq.Erasure.EDeps]
ind:87 [in MetaCoq.Erasure.EInlineProjections]
ind:9 [in MetaCoq.PCUIC.PCUICElimination]
ind:9 [in MetaCoq.Erasure.Extract]
ind:90 [in MetaCoq.Erasure.EArities]
ind:90 [in MetaCoq.PCUIC.PCUICInductives]
ind:90 [in MetaCoq.PCUIC.Syntax.PCUICCases]
ind:91 [in MetaCoq.PCUIC.PCUICCanonicity]
ind:91 [in MetaCoq.Erasure.EOptimizePropDiscr]
ind:92 [in MetaCoq.PCUIC.PCUICInductiveInversion]
ind:921 [in MetaCoq.PCUIC.PCUICInductiveInversion]
ind:928 [in MetaCoq.PCUIC.PCUICInductiveInversion]
ind:938 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
ind:94 [in MetaCoq.PCUIC.PCUICInductives]
ind:94 [in MetaCoq.PCUIC.PCUICInversion]
ind:94 [in MetaCoq.Erasure.EGlobalEnv]
ind:946 [in MetaCoq.PCUIC.PCUICInductiveInversion]
ind:95 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
ind:95 [in MetaCoq.Template.TypingWf]
ind:96 [in MetaCoq.Erasure.ESubstitution]
ind:960 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
ind:964 [in MetaCoq.SafeChecker.PCUICSafeChecker]
ind:97 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
ind:97 [in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
ind:98 [in MetaCoq.PCUIC.PCUICSafeLemmata]
ind:98 [in MetaCoq.Erasure.EArities]
ind:98 [in MetaCoq.PCUIC.PCUICInductives]
ind:982 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
ind:99 [in MetaCoq.Erasure.EEtaExpandedFix]
ind:99 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
infering_size:138 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
infer_sort:178 [in MetaCoq.Template.EnvironmentTyping]
infer:709 [in MetaCoq.SafeChecker.PCUICTypeChecker]
infer:784 [in MetaCoq.SafeChecker.PCUICTypeChecker]
inft:1083 [in MetaCoq.SafeChecker.PCUICSafeChecker]
init_edges:208 [in MetaCoq.Template.common.uGraph]
init_global_env:62 [in MetaCoq.PCUIC.TemplateToPCUIC]
init:65 [in MetaCoq.PCUIC.TemplateToPCUIC]
input:29 [in MetaCoq.Template.Transform]
instf:12 [in MetaCoq.Template.Ast]
instp:41 [in MetaCoq.PCUIC.PCUICAst]
instp:44 [in MetaCoq.PCUIC.PCUICAst]
instp:48 [in MetaCoq.PCUIC.PCUICAst]
instp:77 [in MetaCoq.Template.Ast]
instsubst:180 [in MetaCoq.PCUIC.PCUICSpine]
instsubst:99 [in MetaCoq.PCUIC.PCUICInductiveInversion]
insts':220 [in MetaCoq.PCUIC.PCUICSpine]
insts:217 [in MetaCoq.PCUIC.PCUICSpine]
insts:249 [in MetaCoq.PCUIC.PCUICSpine]
insts:687 [in MetaCoq.PCUIC.PCUICSpine]
inst_ctrs:423 [in MetaCoq.Template.Universes]
inst':120 [in MetaCoq.Erasure.Prelim]
inst':216 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
inst':219 [in MetaCoq.PCUIC.PCUICSpine]
inst':223 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
inst':230 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
inst':248 [in MetaCoq.PCUIC.PCUICSpine]
inst':291 [in MetaCoq.PCUIC.PCUICSR]
inst':303 [in MetaCoq.PCUIC.PCUICSR]
inst':686 [in MetaCoq.PCUIC.PCUICSpine]
inst':790 [in MetaCoq.PCUIC.PCUICSpine]
inst':806 [in MetaCoq.PCUIC.PCUICSpine]
inst0:138 [in MetaCoq.PCUIC.PCUICSpine]
inst:100 [in MetaCoq.PCUIC.PCUICSpine]
inst:113 [in MetaCoq.PCUIC.PCUICSR]
inst:120 [in MetaCoq.PCUIC.PCUICSR]
inst:131 [in MetaCoq.PCUIC.PCUICSR]
inst:139 [in MetaCoq.PCUIC.PCUICSR]
inst:141 [in MetaCoq.PCUIC.PCUICSpine]
inst:160 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
inst:175 [in MetaCoq.PCUIC.PCUICInductives]
inst:178 [in MetaCoq.PCUIC.PCUICSpine]
inst:199 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
inst:215 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
inst:216 [in MetaCoq.PCUIC.PCUICSpine]
inst:222 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
inst:229 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
inst:247 [in MetaCoq.PCUIC.PCUICSpine]
inst:249 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
inst:282 [in MetaCoq.PCUIC.PCUICSpine]
inst:290 [in MetaCoq.PCUIC.PCUICSR]
inst:302 [in MetaCoq.PCUIC.PCUICSR]
inst:311 [in MetaCoq.Template.EnvironmentTyping]
inst:316 [in MetaCoq.Template.EnvironmentTyping]
inst:32 [in MetaCoq.SafeChecker.PCUICTypeChecker]
inst:322 [in MetaCoq.Template.EnvironmentTyping]
inst:325 [in MetaCoq.PCUIC.PCUICSpine]
inst:329 [in MetaCoq.PCUIC.PCUICSpine]
inst:33 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
inst:33 [in MetaCoq.SafeChecker.PCUICSafeChecker]
inst:336 [in MetaCoq.PCUIC.PCUICSpine]
inst:36 [in MetaCoq.SafeChecker.PCUICSafeChecker]
inst:38 [in MetaCoq.SafeChecker.PCUICSafeChecker]
inst:40 [in MetaCoq.SafeChecker.PCUICSafeChecker]
inst:494 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
inst:515 [in MetaCoq.Template.EnvironmentTyping]
inst:517 [in MetaCoq.PCUIC.PCUICSpine]
inst:519 [in MetaCoq.PCUIC.PCUICInductiveInversion]
inst:525 [in MetaCoq.PCUIC.PCUICInductiveInversion]
inst:528 [in MetaCoq.Template.EnvironmentTyping]
inst:53 [in MetaCoq.PCUIC.PCUICInductives]
inst:535 [in MetaCoq.PCUIC.PCUICInductiveInversion]
inst:543 [in MetaCoq.PCUIC.PCUICInductiveInversion]
inst:548 [in MetaCoq.PCUIC.PCUICSR]
inst:586 [in MetaCoq.PCUIC.PCUICSpine]
inst:60 [in MetaCoq.PCUIC.PCUICInductiveInversion]
inst:620 [in MetaCoq.PCUIC.PCUICInductives]
inst:675 [in MetaCoq.PCUIC.PCUICSpine]
inst:679 [in MetaCoq.PCUIC.PCUICSpine]
inst:685 [in MetaCoq.PCUIC.PCUICSpine]
inst:72 [in MetaCoq.PCUIC.PCUICInductiveInversion]
inst:789 [in MetaCoq.PCUIC.PCUICSpine]
inst:805 [in MetaCoq.PCUIC.PCUICSpine]
inst:82 [in MetaCoq.PCUIC.PCUICSpine]
inst:83 [in MetaCoq.PCUIC.PCUICInductiveInversion]
inst:9 [in MetaCoq.SafeChecker.PCUICTypeChecker]
inst:93 [in MetaCoq.PCUIC.PCUICSpine]
inst:94 [in MetaCoq.PCUIC.PCUICInductiveInversion]
invG:1161 [in MetaCoq.Template.utils.wGraph]
invG:837 [in MetaCoq.Template.utils.wGraph]
inx:306 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
inx:869 [in MetaCoq.Template.utils.MCList]
inx:888 [in MetaCoq.Template.utils.MCList]
in_str:78 [in MetaCoq.Template.Pretty]
in_args:76 [in MetaCoq.Template.Pretty]
in_str:85 [in MetaCoq.PCUIC.utils.PCUICPretty]
in_args:83 [in MetaCoq.PCUIC.utils.PCUICPretty]
ip:108 [in MetaCoq.PCUIC.PCUICWcbvEval]
ip:110 [in MetaCoq.Template.Typing]
ip:110 [in MetaCoq.Template.WcbvEval]
ip:125 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
ip:194 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
ip:204 [in MetaCoq.Template.WcbvEval]
ip:242 [in MetaCoq.PCUIC.PCUICWcbvEval]
ip:27 [in MetaCoq.PCUIC.PCUICReduction]
ip:278 [in MetaCoq.Erasure.EArities]
ip:279 [in MetaCoq.Template.Typing]
ip:86 [in MetaCoq.Erasure.EWcbvEval]
ip:96 [in MetaCoq.Erasure.EWcbvEvalInd]
ir1:2567 [in MetaCoq.SafeChecker.PCUICSafeConversion]
ir1:5240 [in MetaCoq.SafeChecker.PCUICSafeConversion]
ir2:2568 [in MetaCoq.SafeChecker.PCUICSafeConversion]
ir2:5241 [in MetaCoq.SafeChecker.PCUICSafeConversion]
isconv_stacks:253 [in MetaCoq.Template.Checker]
isdecl':423 [in MetaCoq.Template.EtaExpand]
isdecl':741 [in MetaCoq.SafeChecker.PCUICTypeChecker]
isdecl:102 [in MetaCoq.PCUIC.Typing.PCUICWeakeningTyp]
isdecl:1038 [in MetaCoq.Template.Typing]
isdecl:1049 [in MetaCoq.Template.Typing]
isdecl:106 [in MetaCoq.Erasure.EWcbvEval]
isdecl:1062 [in MetaCoq.Template.Typing]
isdecl:1081 [in MetaCoq.Template.Typing]
isdecl:1081 [in MetaCoq.SafeChecker.PCUICTypeChecker]
isdecl:1224 [in MetaCoq.Template.utils.All_Forall]
isdecl:1258 [in MetaCoq.Template.Typing]
isdecl:127 [in MetaCoq.Template.Typing]
isdecl:1300 [in MetaCoq.Template.Typing]
isdecl:142 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
isdecl:143 [in MetaCoq.PCUIC.PCUICProgress]
isdecl:144 [in MetaCoq.PCUIC.PCUICInversion]
isdecl:154 [in MetaCoq.PCUIC.PCUICProgress]
isdecl:167 [in MetaCoq.PCUIC.PCUICProgress]
isdecl:167 [in MetaCoq.Template.Typing]
isdecl:185 [in MetaCoq.Template.Typing]
isdecl:186 [in MetaCoq.PCUIC.PCUICProgress]
isdecl:204 [in MetaCoq.PCUIC.PCUICWcbvEval]
isdecl:239 [in MetaCoq.PCUIC.PCUICParallelReduction]
isdecl:293 [in MetaCoq.PCUIC.PCUICProgress]
isdecl:304 [in MetaCoq.PCUIC.PCUICProgress]
isdecl:317 [in MetaCoq.PCUIC.PCUICProgress]
isdecl:336 [in MetaCoq.PCUIC.PCUICProgress]
isdecl:345 [in MetaCoq.Template.Typing]
isdecl:361 [in MetaCoq.PCUIC.PCUICContextConversion]
isdecl:364 [in MetaCoq.Template.Typing]
isdecl:41 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
isdecl:44 [in MetaCoq.PCUIC.PCUICReduction]
isdecl:46 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
isdecl:53 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
isdecl:535 [in MetaCoq.PCUIC.PCUICTyping]
isdecl:546 [in MetaCoq.PCUIC.PCUICTyping]
isdecl:559 [in MetaCoq.PCUIC.PCUICTyping]
isdecl:57 [in MetaCoq.Template.utils.MCList]
isdecl:578 [in MetaCoq.PCUIC.PCUICTyping]
isdecl:635 [in MetaCoq.Template.Typing]
isdecl:640 [in MetaCoq.Template.Typing]
isdecl:647 [in MetaCoq.Template.Typing]
isdecl:656 [in MetaCoq.Template.Typing]
isdecl:67 [in MetaCoq.PCUIC.PCUICWcbvEval]
isdecl:67 [in MetaCoq.Template.WcbvEval]
isdecl:670 [in MetaCoq.Template.Typing]
isdecl:722 [in MetaCoq.SafeChecker.PCUICTypeChecker]
isdecl:752 [in MetaCoq.SafeChecker.PCUICTypeChecker]
isdecl:775 [in MetaCoq.PCUIC.PCUICInductiveInversion]
isdecl:858 [in MetaCoq.PCUIC.PCUICTyping]
isdecl:869 [in MetaCoq.PCUIC.PCUICTyping]
isdecl:882 [in MetaCoq.PCUIC.PCUICTyping]
isdecl:901 [in MetaCoq.PCUIC.PCUICTyping]
isdecl:931 [in MetaCoq.PCUIC.PCUICTyping]
isdecl:985 [in MetaCoq.PCUIC.PCUICTyping]
isfresh:1034 [in MetaCoq.SafeChecker.PCUICSafeChecker]
isind:554 [in MetaCoq.SafeChecker.PCUICSafeChecker]
isinvol:1549 [in MetaCoq.Translations.MiniHoTT]
isinvol:1552 [in MetaCoq.Translations.MiniHoTT]
isinvol:1557 [in MetaCoq.Translations.MiniHoTT_paths]
isinvol:1560 [in MetaCoq.Translations.MiniHoTT_paths]
isprod:107 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
isretr:1537 [in MetaCoq.Translations.MiniHoTT]
isretr:1545 [in MetaCoq.Translations.MiniHoTT_paths]
issect:1538 [in MetaCoq.Translations.MiniHoTT]
issect:1546 [in MetaCoq.Translations.MiniHoTT_paths]
isty:1093 [in MetaCoq.SafeChecker.PCUICTypeChecker]
isty:592 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
ist:581 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
is_propositional:675 [in MetaCoq.Erasure.ErasureFunction]
it:516 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
i':1076 [in MetaCoq.Template.utils.All_Forall]
i':1086 [in MetaCoq.Template.utils.All_Forall]
i':1114 [in MetaCoq.PCUIC.PCUICConversion]
i':1118 [in MetaCoq.PCUIC.PCUICConversion]
i':120 [in MetaCoq.PCUIC.PCUICInductiveInversion]
i':129 [in MetaCoq.Erasure.EEtaExpanded]
i':147 [in MetaCoq.PCUIC.PCUICInductiveInversion]
i':15 [in MetaCoq.Erasure.EReflect]
i':163 [in MetaCoq.Erasure.Extract]
i':192 [in MetaCoq.PCUIC.PCUICInductives]
i':194 [in MetaCoq.PCUIC.PCUICInductives]
i':232 [in MetaCoq.PCUIC.PCUICSafeLemmata]
i':233 [in MetaCoq.PCUIC.PCUICInductiveInversion]
i':244 [in MetaCoq.PCUIC.PCUICInductiveInversion]
i':255 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
i':259 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
i':263 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
i':275 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
i':283 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
i':289 [in MetaCoq.PCUIC.PCUICSafeLemmata]
i':291 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
i':300 [in MetaCoq.Erasure.EEtaExpandedFix]
I':357 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
i':41 [in MetaCoq.PCUIC.PCUICEquality]
I':449 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
i':514 [in MetaCoq.PCUIC.PCUICInductiveInversion]
i':565 [in MetaCoq.PCUIC.PCUICInductiveInversion]
i':576 [in MetaCoq.PCUIC.PCUICInductiveInversion]
i':590 [in MetaCoq.PCUIC.PCUICInductiveInversion]
i':645 [in MetaCoq.Template.EnvironmentTyping]
i':73 [in MetaCoq.Template.Kernames]
i':923 [in MetaCoq.Template.utils.All_Forall]
i':96 [in MetaCoq.PCUIC.PCUICInductiveInversion]
I':960 [in MetaCoq.Template.utils.All_Forall]
i0:22 [in MetaCoq.Examples.add_constructor]
i0:300 [in MetaCoq.PCUIC.PCUICInductives]
i1:118 [in MetaCoq.Translations.param_cheap_packed]
i1:120 [in MetaCoq.Translations.param_cheap_packed]
i:1 [in MetaCoq.PCUIC.TemplateToPCUIC]
i:1 [in MetaCoq.PCUIC.PCUICToTemplate]
i:1 [in MetaCoq.Template.AstUtils]
i:10 [in MetaCoq.PCUIC.Syntax.PCUICCases]
i:10 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
i:10 [in MetaCoq.Erasure.EReflect]
i:100 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
i:1000 [in MetaCoq.PCUIC.PCUICInductiveInversion]
i:1000 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
i:1009 [in MetaCoq.SafeChecker.PCUICSafeChecker]
i:101 [in MetaCoq.Template.utils.All_Forall]
i:101 [in MetaCoq.PCUIC.PCUICInversion]
i:1012 [in MetaCoq.Template.utils.All_Forall]
i:1013 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
i:1017 [in MetaCoq.PCUIC.PCUICInductiveInversion]
i:1018 [in MetaCoq.Template.utils.All_Forall]
i:102 [in MetaCoq.PCUIC.PCUICFirstorder]
i:1025 [in MetaCoq.Template.utils.All_Forall]
i:103 [in MetaCoq.PCUIC.Syntax.PCUICViews]
i:103 [in MetaCoq.Translations.param_cheap_packed]
i:103 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
i:103 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
i:1033 [in MetaCoq.Template.utils.All_Forall]
i:104 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
i:104 [in MetaCoq.Erasure.Prelim]
i:1040 [in MetaCoq.Template.utils.All_Forall]
i:1044 [in MetaCoq.Template.Typing]
i:1049 [in MetaCoq.Template.utils.All_Forall]
i:105 [in MetaCoq.Template.Environment]
i:105 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
i:1052 [in MetaCoq.Template.utils.All_Forall]
i:1061 [in MetaCoq.Template.utils.All_Forall]
i:1064 [in MetaCoq.Template.utils.All_Forall]
i:1066 [in MetaCoq.Template.Typing]
i:1069 [in MetaCoq.Template.utils.All_Forall]
I:1074 [in MetaCoq.SafeChecker.PCUICTypeChecker]
i:1076 [in MetaCoq.Template.utils.wGraph]
i:1079 [in MetaCoq.Template.utils.All_Forall]
i:109 [in MetaCoq.Translations.param_cheap_packed]
i:1091 [in MetaCoq.Template.utils.All_Forall]
i:1094 [in MetaCoq.Template.utils.All_Forall]
I:1099 [in MetaCoq.SafeChecker.PCUICTypeChecker]
i:11 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
i:11 [in MetaCoq.PCUIC.Syntax.PCUICInstDef]
i:110 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
i:110 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
i:1103 [in MetaCoq.Template.utils.All_Forall]
i:111 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
i:111 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
i:1113 [in MetaCoq.PCUIC.PCUICConversion]
i:1117 [in MetaCoq.PCUIC.PCUICConversion]
i:112 [in MetaCoq.PCUIC.Syntax.PCUICCases]
i:112 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
i:112 [in MetaCoq.Erasure.EEtaExpanded]
i:113 [in MetaCoq.Erasure.EInduction]
i:114 [in MetaCoq.PCUIC.PCUICAlpha]
i:114 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
i:1143 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
i:1148 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
i:116 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
i:1165 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
i:117 [in MetaCoq.PCUIC.PCUICInductiveInversion]
i:118 [in MetaCoq.Erasure.EDeps]
i:118 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
i:119 [in MetaCoq.PCUIC.PCUICTyping]
i:12 [in MetaCoq.PCUIC.PCUICExpandLets]
i:12 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
i:12 [in MetaCoq.PCUIC.PCUICInductiveInversion]
i:12 [in MetaCoq.Template.utils.MCPred]
i:12 [in MetaCoq.PCUIC.PCUICAlpha]
i:120 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
i:1207 [in MetaCoq.PCUIC.PCUICConversion]
i:121 [in MetaCoq.Translations.times_bool_fun]
i:1210 [in MetaCoq.PCUIC.PCUICConversion]
i:1216 [in MetaCoq.PCUIC.PCUICConversion]
i:123 [in MetaCoq.Translations.times_bool_fun]
i:123 [in MetaCoq.Erasure.EDeps]
i:123 [in MetaCoq.Translations.param_cheap_packed]
i:1240 [in MetaCoq.PCUIC.PCUICConversion]
i:1257 [in MetaCoq.Template.utils.All_Forall]
i:126 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
i:127 [in MetaCoq.PCUIC.PCUICNormal]
i:1274 [in MetaCoq.Template.utils.All_Forall]
i:128 [in MetaCoq.Erasure.EEtaExpanded]
i:129 [in MetaCoq.Translations.param_cheap_packed]
i:13 [in MetaCoq.PCUIC.PCUICReduction]
i:130 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
i:131 [in MetaCoq.PCUIC.PCUICParallelReduction]
i:131 [in MetaCoq.PCUIC.PCUICInversion]
i:133 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
i:133 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
i:1337 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
i:134 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
i:135 [in MetaCoq.Template.EtaExpand]
i:135 [in MetaCoq.PCUIC.PCUICNormal]
i:135 [in MetaCoq.PCUIC.PCUICEquality]
i:135 [in MetaCoq.Template.Checker]
i:135 [in MetaCoq.Translations.param_cheap_packed]
i:1359 [in MetaCoq.Erasure.ErasureFunction]
i:136 [in MetaCoq.PCUIC.PCUICConvCumInversion]
i:1369 [in MetaCoq.Template.utils.All_Forall]
i:137 [in MetaCoq.PCUIC.PCUICParallelReduction]
i:1377 [in MetaCoq.Erasure.ErasureFunction]
i:1378 [in MetaCoq.Template.utils.All_Forall]
i:138 [in MetaCoq.PCUIC.PCUICEquality]
i:138 [in MetaCoq.PCUIC.PCUICConvCumInversion]
i:139 [in MetaCoq.Template.Checker]
i:1392 [in MetaCoq.Template.utils.All_Forall]
i:1399 [in MetaCoq.Erasure.ErasureFunction]
i:14 [in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
i:14 [in MetaCoq.Erasure.EInduction]
i:14 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
i:14 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
i:14 [in MetaCoq.PCUIC.Conversion.PCUICOnFreeVarsConv]
i:14 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
i:14 [in MetaCoq.PCUIC.utils.PCUICPrimitive]
i:140 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
i:140 [in MetaCoq.PCUIC.PCUICNormal]
i:140 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
i:141 [in MetaCoq.Translations.param_cheap_packed]
i:142 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
i:142 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
i:142 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
i:144 [in MetaCoq.PCUIC.PCUICInductives]
i:144 [in MetaCoq.PCUIC.PCUICInductiveInversion]
i:144 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
i:148 [in MetaCoq.PCUIC.PCUICConvCumInversion]
i:148 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
i:149 [in MetaCoq.PCUIC.PCUICProgress]
i:15 [in MetaCoq.PCUIC.PCUICExpandLets]
i:15 [in MetaCoq.Template.Normal]
i:15 [in MetaCoq.Template.Pretty]
i:15 [in MetaCoq.Template.LiftSubst]
i:150 [in MetaCoq.PCUIC.PCUICConvCumInversion]
i:151 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
i:152 [in MetaCoq.Template.LiftSubst]
i:153 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
i:153 [in MetaCoq.Template.Checker]
i:154 [in MetaCoq.Template.LiftSubst]
i:155 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
i:156 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
i:156 [in MetaCoq.Template.LiftSubst]
i:158 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
i:16 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
i:16 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
i:16 [in MetaCoq.PCUIC.PCUICAlpha]
i:161 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
i:161 [in MetaCoq.Erasure.Extract]
i:161 [in MetaCoq.PCUIC.PCUICFirstorder]
i:1619 [in MetaCoq.SafeChecker.PCUICSafeReduce]
i:162 [in MetaCoq.Erasure.Extract]
i:163 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
i:169 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
i:169 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
i:1698 [in MetaCoq.Template.utils.All_Forall]
i:17 [in MetaCoq.Erasure.ESpineView]
i:17 [in MetaCoq.Template.Checker]
i:17 [in MetaCoq.PCUIC.PCUICCasesContexts]
i:17 [in MetaCoq.PCUIC.PCUICContextConversion]
i:17 [in MetaCoq.PCUIC.Conversion.PCUICClosedConv]
i:170 [in MetaCoq.SafeChecker.PCUICErrors]
i:170 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
i:171 [in MetaCoq.PCUIC.PCUICProgress]
i:171 [in MetaCoq.PCUIC.PCUICReduction]
i:172 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
i:1733 [in MetaCoq.Template.utils.All_Forall]
i:175 [in MetaCoq.PCUIC.PCUICCanonicity]
i:175 [in MetaCoq.Template.TypingWf]
i:176 [in MetaCoq.Erasure.EWcbvEvalInd]
i:179 [in MetaCoq.PCUIC.PCUICFirstorder]
i:18 [in MetaCoq.PCUIC.PCUICExpandLets]
i:18 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
i:181 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
i:182 [in MetaCoq.PCUIC.PCUICArities]
i:183 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
i:184 [in MetaCoq.PCUIC.PCUICArities]
i:184 [in MetaCoq.PCUIC.PCUICFirstorder]
i:185 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
i:188 [in MetaCoq.Erasure.Extract]
i:189 [in MetaCoq.PCUIC.PCUICParallelReduction]
i:189 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
i:19 [in MetaCoq.Template.Normal]
i:190 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
i:191 [in MetaCoq.PCUIC.PCUICInductives]
i:191 [in MetaCoq.PCUIC.PCUICParallelReduction]
i:191 [in MetaCoq.SafeChecker.PCUICErrors]
i:192 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
i:193 [in MetaCoq.Erasure.EInduction]
i:1931 [in MetaCoq.SafeChecker.PCUICSafeConversion]
i:1935 [in MetaCoq.SafeChecker.PCUICSafeConversion]
i:1943 [in MetaCoq.Template.utils.All_Forall]
i:195 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
i:196 [in MetaCoq.PCUIC.PCUICNormal]
i:196 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
i:196 [in MetaCoq.PCUIC.PCUICCanonicity]
i:198 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
i:1983 [in MetaCoq.Template.utils.All_Forall]
i:199 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
i:2 [in MetaCoq.PCUIC.TemplateToPCUIC]
i:20 [in MetaCoq.Template.EtaExpand]
i:20 [in MetaCoq.Erasure.EPretty]
i:20 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
i:20 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
i:203 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
i:205 [in MetaCoq.Template.Universes]
i:205 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
i:21 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
i:21 [in MetaCoq.Erasure.Extract]
i:21 [in MetaCoq.Template.EnvMap]
i:21 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
i:210 [in MetaCoq.Erasure.EInduction]
i:213 [in MetaCoq.Template.EtaExpand]
i:213 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
i:2141 [in MetaCoq.Template.utils.All_Forall]
i:215 [in MetaCoq.PCUIC.PCUICInductives]
i:2152 [in MetaCoq.Template.utils.All_Forall]
i:216 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
i:2161 [in MetaCoq.Template.utils.All_Forall]
i:2169 [in MetaCoq.Template.utils.All_Forall]
i:217 [in MetaCoq.Template.EtaExpand]
i:217 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
i:218 [in MetaCoq.PCUIC.PCUICTyping]
i:218 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
i:219 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
i:22 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
i:22 [in MetaCoq.PCUIC.PCUICFirstorder]
i:22 [in MetaCoq.Template.Pretty]
i:220 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
i:220 [in MetaCoq.Template.TypingWf]
i:221 [in MetaCoq.PCUIC.PCUICCanonicity]
i:222 [in MetaCoq.PCUIC.Syntax.PCUICCases]
i:223 [in MetaCoq.PCUIC.PCUICInductiveInversion]
i:223 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
i:224 [in MetaCoq.Template.BasicAst]
i:224 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
i:225 [in MetaCoq.PCUIC.PCUICCanonicity]
i:225 [in MetaCoq.PCUIC.PCUICSpine]
i:229 [in MetaCoq.PCUIC.PCUICInductives]
i:229 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
i:23 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
i:23 [in MetaCoq.PCUIC.Conversion.PCUICClosedConv]
i:23 [in MetaCoq.Examples.add_constructor]
i:23 [in MetaCoq.PCUIC.utils.PCUICPretty]
i:230 [in MetaCoq.Erasure.Extract]
i:231 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
i:231 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
i:231 [in MetaCoq.PCUIC.PCUICSpine]
i:232 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
i:232 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
i:233 [in MetaCoq.Erasure.Extract]
i:237 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
i:237 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
i:24 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
i:24 [in MetaCoq.Template.Induction]
i:240 [in MetaCoq.PCUIC.PCUICTyping]
i:240 [in MetaCoq.PCUIC.PCUICSpine]
i:242 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
i:246 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
i:248 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
i:248 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
i:249 [in MetaCoq.PCUIC.PCUICSubstitution]
i:25 [in MetaCoq.PCUIC.PCUICInductiveInversion]
i:25 [in MetaCoq.Template.LiftSubst]
i:250 [in MetaCoq.SafeChecker.PCUICSafeConversion]
i:252 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
i:253 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
i:254 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
i:258 [in MetaCoq.Template.Typing]
i:258 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
i:258 [in MetaCoq.PCUIC.PCUICSpine]
i:26 [in MetaCoq.Template.EtaExpand]
i:26 [in MetaCoq.PCUIC.PCUICExpandLets]
i:26 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
i:26 [in MetaCoq.PCUIC.PCUICInductiveInversion]
i:26 [in MetaCoq.Template.Normal]
i:26 [in MetaCoq.PCUIC.PCUICNormal]
i:26 [in MetaCoq.Template.Induction]
i:262 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
i:262 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
i:262 [in MetaCoq.PCUIC.PCUICSpine]
i:264 [in MetaCoq.Template.utils.MCList]
i:266 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
i:267 [in MetaCoq.Template.TypingWf]
i:268 [in MetaCoq.Template.utils.All_Forall]
i:27 [in MetaCoq.PCUIC.PCUICCanonicity]
i:27 [in MetaCoq.PCUIC.Conversion.PCUICClosedConv]
i:270 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
i:271 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
i:272 [in MetaCoq.Template.utils.MCList]
i:272 [in MetaCoq.PCUIC.PCUICSpine]
i:273 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
i:274 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
i:274 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
i:274 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
i:275 [in MetaCoq.PCUIC.PCUICNormal]
i:276 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
i:276 [in MetaCoq.PCUIC.PCUICSpine]
i:277 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
i:277 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
i:278 [in MetaCoq.Template.utils.All_Forall]
i:28 [in MetaCoq.Template.WfAst]
i:28 [in MetaCoq.PCUIC.PCUICInversion]
i:28 [in MetaCoq.Template.Checker]
i:28 [in MetaCoq.SafeChecker.PCUICSafeChecker]
i:28 [in MetaCoq.Template.TemplateMonad.Extractable]
i:281 [in MetaCoq.PCUIC.PCUICNormal]
i:281 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
i:282 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
i:283 [in MetaCoq.PCUIC.PCUICSafeLemmata]
i:285 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
i:286 [in MetaCoq.PCUIC.PCUICNormal]
i:287 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
i:288 [in MetaCoq.Template.utils.All_Forall]
i:288 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
i:289 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
i:29 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
i:29 [in MetaCoq.SafeChecker.PCUICSafeChecker]
i:290 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
i:290 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
i:291 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
i:292 [in MetaCoq.PCUIC.PCUICNormal]
i:293 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
i:293 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
i:295 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
i:296 [in MetaCoq.PCUIC.PCUICInductives]
i:297 [in MetaCoq.PCUIC.PCUICCumulProp]
i:298 [in MetaCoq.PCUIC.PCUICInductives]
i:298 [in MetaCoq.PCUIC.PCUICNormal]
i:299 [in MetaCoq.PCUIC.PCUICProgress]
i:299 [in MetaCoq.Erasure.EEtaExpandedFix]
i:3 [in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
i:3 [in MetaCoq.Erasure.EInduction]
i:3 [in MetaCoq.Erasure.EPretty]
i:3 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
i:3 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
i:3 [in MetaCoq.PCUIC.Syntax.PCUICInstDef]
i:3 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
i:3 [in MetaCoq.Template.TemplateMonad.Common]
i:3 [in MetaCoq.PCUIC.utils.PCUICPretty]
i:3 [in MetaCoq.Template.Induction]
i:30 [in MetaCoq.PCUIC.PCUICSafeLemmata]
i:30 [in MetaCoq.Template.Typing]
i:30 [in MetaCoq.Template.WfAst]
i:30 [in MetaCoq.PCUIC.PCUICNormal]
i:302 [in MetaCoq.PCUIC.PCUICInductiveInversion]
i:304 [in MetaCoq.PCUIC.PCUICNormal]
i:306 [in MetaCoq.Template.Environment]
i:308 [in MetaCoq.PCUIC.PCUICInductiveInversion]
i:308 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
i:31 [in MetaCoq.PCUIC.PCUICCanonicity]
i:31 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
i:31 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
i:310 [in MetaCoq.Template.EnvironmentTyping]
i:313 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
i:313 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
i:314 [in MetaCoq.PCUIC.PCUICNormal]
i:316 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
i:317 [in MetaCoq.PCUIC.PCUICInductiveInversion]
i:317 [in MetaCoq.PCUIC.PCUICSR]
i:318 [in MetaCoq.Erasure.EEtaExpandedFix]
i:318 [in MetaCoq.PCUIC.PCUICInductives]
i:32 [in MetaCoq.Template.TemplateMonad.Extractable]
i:321 [in MetaCoq.PCUIC.PCUICProgress]
i:321 [in MetaCoq.Template.BasicAst]
i:324 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
i:326 [in MetaCoq.Template.BasicAst]
i:330 [in MetaCoq.Template.Ast]
i:330 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
i:330 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
i:331 [in MetaCoq.PCUIC.PCUICInductives]
i:333 [in MetaCoq.Template.BasicAst]
i:335 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
i:335 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
i:337 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
i:339 [in MetaCoq.PCUIC.PCUICInductiveInversion]
i:34 [in MetaCoq.PCUIC.PCUICInductiveInversion]
i:34 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
i:34 [in MetaCoq.Template.Pretty]
i:341 [in MetaCoq.Template.BasicAst]
i:341 [in MetaCoq.PCUIC.PCUICAst]
i:344 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
i:345 [in MetaCoq.Template.BasicAst]
i:345 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
i:348 [in MetaCoq.PCUIC.PCUICWcbvEval]
i:349 [in MetaCoq.Template.BasicAst]
i:349 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
i:35 [in MetaCoq.Template.EtaExpand]
i:35 [in MetaCoq.PCUIC.PCUICInductiveInversion]
i:35 [in MetaCoq.Template.Normal]
i:350 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
i:350 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
i:351 [in MetaCoq.PCUIC.PCUICSR]
i:354 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
i:355 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
I:356 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
i:357 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
i:359 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
i:36 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
i:36 [in MetaCoq.PCUIC.PCUICCanonicity]
i:361 [in MetaCoq.PCUIC.PCUICParallelReduction]
i:361 [in MetaCoq.PCUIC.PCUICNormal]
i:363 [in MetaCoq.Template.BasicAst]
i:364 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
i:364 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
i:365 [in MetaCoq.PCUIC.PCUICParallelReduction]
i:368 [in MetaCoq.Template.BasicAst]
i:37 [in MetaCoq.PCUIC.PCUICFirstorder]
i:37 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
i:37 [in MetaCoq.PCUIC.PCUICConvCumInversion]
i:37 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
i:37 [in MetaCoq.Template.TemplateMonad.Extractable]
i:370 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
i:371 [in MetaCoq.PCUIC.PCUICAst]
i:372 [in MetaCoq.Template.BasicAst]
i:372 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
i:376 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
i:377 [in MetaCoq.PCUIC.PCUICAst]
i:379 [in MetaCoq.PCUIC.PCUICSpine]
i:38 [in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
i:384 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
i:387 [in MetaCoq.Template.utils.MCList]
i:387 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
i:388 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
i:388 [in MetaCoq.Template.Ast]
i:39 [in MetaCoq.PCUIC.PCUICNormal]
i:39 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
i:39 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
i:4 [in MetaCoq.Template.utils.MCPred]
i:40 [in MetaCoq.PCUIC.PCUICNormal]
i:40 [in MetaCoq.PCUIC.PCUICEquality]
i:402 [in MetaCoq.Template.Ast]
i:402 [in MetaCoq.PCUIC.PCUICNormal]
i:403 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
i:405 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
i:405 [in MetaCoq.PCUIC.PCUICNormal]
i:406 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
i:41 [in MetaCoq.PCUIC.PCUICArities]
i:414 [in MetaCoq.Template.BasicAst]
i:415 [in MetaCoq.Template.Universes]
i:415 [in MetaCoq.Template.BasicAst]
i:416 [in MetaCoq.PCUIC.PCUICSpine]
i:417 [in MetaCoq.Template.Universes]
i:417 [in MetaCoq.Template.utils.All_Forall]
i:418 [in MetaCoq.Template.EtaExpand]
i:42 [in MetaCoq.Erasure.ELiftSubst]
i:42 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
i:42 [in MetaCoq.Template.LiftSubst]
i:42 [in MetaCoq.Template.Induction]
i:420 [in MetaCoq.Template.Universes]
i:427 [in MetaCoq.Template.utils.All_Forall]
i:428 [in MetaCoq.SafeChecker.PCUICSafeChecker]
i:43 [in MetaCoq.Template.EtaExpand]
i:43 [in MetaCoq.PCUIC.PCUICArities]
i:43 [in MetaCoq.Erasure.EDeps]
i:43 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
i:43 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
i:43 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
i:432 [in MetaCoq.Template.Universes]
i:438 [in MetaCoq.Template.Universes]
i:44 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
I:448 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
i:45 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
i:45 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
i:45 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
i:451 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
i:451 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
i:452 [in MetaCoq.PCUIC.PCUICInductiveInversion]
i:456 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
i:46 [in MetaCoq.PCUIC.PCUICFirstorder]
i:46 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
i:468 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
i:469 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
i:474 [in MetaCoq.PCUIC.PCUICProgress]
i:474 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
i:477 [in MetaCoq.Template.utils.All_Forall]
i:48 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
i:48 [in MetaCoq.Erasure.EArities]
i:48 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
i:480 [in MetaCoq.Template.EnvironmentTyping]
i:480 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
i:482 [in MetaCoq.PCUIC.PCUICProgress]
i:485 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
i:489 [in MetaCoq.Template.EnvironmentTyping]
i:49 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
i:49 [in MetaCoq.PCUIC.PCUICInductiveInversion]
i:49 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
i:491 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
i:491 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
i:495 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
i:5 [in MetaCoq.PCUIC.PCUICInductives]
i:5 [in MetaCoq.SafeChecker.PCUICTypeChecker]
i:50 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
i:50 [in MetaCoq.Erasure.EDeps]
i:502 [in MetaCoq.Template.utils.All_Forall]
i:505 [in MetaCoq.PCUIC.PCUICInductiveInversion]
i:507 [in MetaCoq.Template.utils.All_Forall]
i:507 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
i:507 [in MetaCoq.PCUIC.PCUICInductiveInversion]
i:508 [in MetaCoq.Template.utils.MCList]
i:51 [in MetaCoq.Erasure.ELiftSubst]
i:512 [in MetaCoq.PCUIC.PCUICAst]
i:513 [in MetaCoq.Template.utils.All_Forall]
i:513 [in MetaCoq.PCUIC.PCUICInductiveInversion]
i:515 [in MetaCoq.Template.utils.MCList]
i:516 [in MetaCoq.Template.EnvironmentTyping]
i:52 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
i:520 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
i:521 [in MetaCoq.PCUIC.PCUICAst]
i:53 [in MetaCoq.Erasure.EArities]
i:53 [in MetaCoq.Translations.param_original]
i:531 [in MetaCoq.Template.utils.MCList]
i:531 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
i:534 [in MetaCoq.Template.utils.MCList]
i:539 [in MetaCoq.Template.utils.MCList]
i:54 [in MetaCoq.Template.Normal]
i:54 [in MetaCoq.PCUIC.PCUICFirstorder]
i:54 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
i:541 [in MetaCoq.PCUIC.PCUICTyping]
i:547 [in MetaCoq.Template.EnvironmentTyping]
i:548 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
i:55 [in MetaCoq.Template.TypingWf]
i:550 [in MetaCoq.Template.EnvironmentTyping]
i:550 [in MetaCoq.PCUIC.PCUICEquality]
i:554 [in MetaCoq.Template.EnvironmentTyping]
i:56 [in MetaCoq.Template.utils.All_Forall]
i:56 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
i:563 [in MetaCoq.PCUIC.PCUICTyping]
i:564 [in MetaCoq.PCUIC.PCUICInductiveInversion]
i:566 [in MetaCoq.Template.utils.MCList]
i:566 [in MetaCoq.PCUIC.PCUICSR]
i:57 [in MetaCoq.Translations.param_binary]
i:57 [in MetaCoq.Translations.param_original]
i:570 [in MetaCoq.Template.utils.MCList]
i:573 [in MetaCoq.PCUIC.PCUICSR]
i:575 [in MetaCoq.Template.EnvironmentTyping]
i:575 [in MetaCoq.PCUIC.PCUICInductiveInversion]
i:578 [in MetaCoq.Template.utils.MCList]
i:578 [in MetaCoq.PCUIC.PCUICAst]
i:58 [in MetaCoq.PCUIC.Syntax.PCUICViews]
i:58 [in MetaCoq.PCUIC.PCUICValidity]
i:58 [in MetaCoq.Template.Normal]
i:58 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
i:580 [in MetaCoq.Template.EnvironmentTyping]
i:582 [in MetaCoq.Template.utils.MCList]
i:583 [in MetaCoq.PCUIC.PCUICSR]
i:589 [in MetaCoq.PCUIC.PCUICInductiveInversion]
i:589 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
i:592 [in MetaCoq.Template.EnvironmentTyping]
i:593 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
i:599 [in MetaCoq.Template.EnvironmentTyping]
i:6 [in MetaCoq.PCUIC.Syntax.PCUICRenameDef]
i:608 [in MetaCoq.Template.utils.MCList]
i:61 [in MetaCoq.Translations.param_binary]
i:61 [in MetaCoq.PCUIC.PCUICInductives]
i:61 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
i:610 [in MetaCoq.Template.utils.MCList]
i:616 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
i:619 [in MetaCoq.Template.utils.MCList]
i:62 [in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
i:62 [in MetaCoq.Template.Checker]
i:621 [in MetaCoq.Template.utils.MCList]
i:623 [in MetaCoq.Template.utils.MCList]
i:625 [in MetaCoq.Template.utils.MCList]
i:627 [in MetaCoq.Template.utils.MCList]
i:627 [in MetaCoq.Template.EnvironmentTyping]
i:629 [in MetaCoq.Template.utils.MCList]
i:63 [in MetaCoq.Template.utils.All_Forall]
i:63 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
i:63 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
i:63 [in MetaCoq.Template.Induction]
i:631 [in MetaCoq.Template.utils.MCList]
i:633 [in MetaCoq.Template.utils.MCList]
i:64 [in MetaCoq.Erasure.EDeps]
i:64 [in MetaCoq.Template.Checker]
i:642 [in MetaCoq.Template.Typing]
i:644 [in MetaCoq.Template.EnvironmentTyping]
i:647 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
i:65 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
i:65 [in MetaCoq.Template.Normal]
i:65 [in MetaCoq.PCUIC.PCUICNormal]
i:65 [in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
i:65 [in MetaCoq.Template.Induction]
i:650 [in MetaCoq.Template.utils.MCList]
i:651 [in MetaCoq.Template.utils.MCList]
i:656 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
i:657 [in MetaCoq.PCUIC.PCUICParallelReduction]
i:658 [in MetaCoq.PCUIC.PCUICParallelReduction]
i:659 [in MetaCoq.Template.Typing]
i:66 [in MetaCoq.PCUIC.PCUICNormal]
i:66 [in MetaCoq.Translations.param_original]
i:663 [in MetaCoq.Template.utils.MCList]
i:664 [in MetaCoq.Template.utils.MCList]
i:669 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
i:67 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
i:67 [in MetaCoq.PCUIC.PCUICFirstorder]
i:672 [in MetaCoq.PCUIC.PCUICInductiveInversion]
i:673 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
i:677 [in MetaCoq.Template.utils.MCList]
i:679 [in MetaCoq.PCUIC.PCUICInductiveInversion]
i:68 [in MetaCoq.Template.Checker]
i:69 [in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
i:69 [in MetaCoq.Translations.param_original]
i:697 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
i:697 [in MetaCoq.SafeChecker.PCUICTypeChecker]
i:7 [in MetaCoq.PCUIC.Syntax.PCUICViews]
i:7 [in MetaCoq.Template.Kernames]
i:70 [in MetaCoq.Translations.param_binary]
i:70 [in MetaCoq.Template.utils.All_Forall]
i:70 [in MetaCoq.PCUIC.PCUICNormal]
i:705 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
i:71 [in MetaCoq.Template.Kernames]
i:71 [in MetaCoq.Translations.param_original]
i:710 [in MetaCoq.Template.utils.MCList]
i:719 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
i:72 [in MetaCoq.Template.WfAst]
i:72 [in MetaCoq.Erasure.Extract]
i:72 [in MetaCoq.Template.Kernames]
i:72 [in MetaCoq.Erasure.ELiftSubst]
i:72 [in MetaCoq.Template.utils.MCOption]
i:72 [in MetaCoq.Translations.param_original]
i:726 [in MetaCoq.PCUIC.PCUICParallelReduction]
i:728 [in MetaCoq.Template.utils.MCList]
i:729 [in MetaCoq.Template.utils.All_Forall]
i:73 [in MetaCoq.Translations.param_binary]
i:73 [in MetaCoq.Translations.times_bool_fun]
i:730 [in MetaCoq.PCUIC.PCUICParallelReduction]
i:733 [in MetaCoq.Template.utils.All_Forall]
i:735 [in MetaCoq.PCUIC.PCUICInductiveInversion]
i:735 [in MetaCoq.Template.utils.wGraph]
i:739 [in MetaCoq.SafeChecker.PCUICTypeChecker]
i:74 [in MetaCoq.Template.Normal]
i:740 [in MetaCoq.Template.utils.All_Forall]
i:740 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
i:741 [in MetaCoq.Template.utils.MCList]
i:743 [in MetaCoq.Template.utils.All_Forall]
i:744 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
i:746 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
i:746 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
i:748 [in MetaCoq.Template.utils.All_Forall]
i:75 [in MetaCoq.Translations.param_binary]
i:75 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
i:75 [in MetaCoq.Template.Checker]
i:75 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
i:750 [in MetaCoq.SafeChecker.PCUICTypeChecker]
i:751 [in MetaCoq.Template.utils.MCList]
i:754 [in MetaCoq.Template.utils.All_Forall]
i:76 [in MetaCoq.Translations.param_binary]
i:76 [in MetaCoq.Translations.times_bool_fun]
i:76 [in MetaCoq.Template.Kernames]
i:76 [in MetaCoq.PCUIC.PCUICTyping]
i:76 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
i:760 [in MetaCoq.Template.utils.All_Forall]
i:766 [in MetaCoq.Template.utils.All_Forall]
i:766 [in MetaCoq.PCUIC.PCUICSpine]
i:769 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
i:77 [in MetaCoq.PCUIC.PCUICInductives]
i:77 [in MetaCoq.PCUIC.PCUICSpine]
i:770 [in MetaCoq.Template.utils.All_Forall]
i:773 [in MetaCoq.PCUIC.PCUICSpine]
i:774 [in MetaCoq.Template.utils.All_Forall]
i:776 [in MetaCoq.PCUIC.PCUICSpine]
i:778 [in MetaCoq.Template.utils.All_Forall]
i:78 [in MetaCoq.PCUIC.PCUICFirstorder]
i:781 [in MetaCoq.Template.utils.All_Forall]
i:784 [in MetaCoq.Template.utils.All_Forall]
i:79 [in MetaCoq.Erasure.ELiftSubst]
i:790 [in MetaCoq.Template.utils.All_Forall]
i:793 [in MetaCoq.Template.utils.All_Forall]
i:8 [in MetaCoq.PCUIC.Conversion.PCUICOnFreeVarsConv]
i:8 [in MetaCoq.PCUIC.PCUICAlpha]
i:8 [in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
i:80 [in MetaCoq.Template.Checker]
i:801 [in MetaCoq.Template.utils.All_Forall]
i:806 [in MetaCoq.Template.utils.All_Forall]
i:81 [in MetaCoq.Template.utils.All_Forall]
i:812 [in MetaCoq.Template.utils.All_Forall]
i:817 [in MetaCoq.Template.utils.All_Forall]
i:82 [in MetaCoq.PCUIC.Syntax.PCUICViews]
i:82 [in MetaCoq.PCUIC.PCUICSubstitution]
i:822 [in MetaCoq.Template.utils.All_Forall]
i:822 [in MetaCoq.PCUIC.PCUICInductiveInversion]
i:824 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
i:824 [in MetaCoq.SafeChecker.PCUICSafeChecker]
i:829 [in MetaCoq.Template.utils.All_Forall]
i:83 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
i:83 [in MetaCoq.Template.Kernames]
i:830 [in MetaCoq.SafeChecker.PCUICSafeChecker]
i:836 [in MetaCoq.Template.utils.All_Forall]
i:84 [in MetaCoq.PCUIC.PCUICSubstitution]
i:843 [in MetaCoq.Template.utils.All_Forall]
i:845 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
i:851 [in MetaCoq.Template.utils.All_Forall]
i:854 [in MetaCoq.Template.utils.All_Forall]
i:86 [in MetaCoq.PCUIC.PCUICSubstitution]
i:86 [in MetaCoq.Template.Checker]
i:862 [in MetaCoq.Template.utils.All_Forall]
i:864 [in MetaCoq.PCUIC.PCUICTyping]
i:865 [in MetaCoq.Template.utils.All_Forall]
i:87 [in MetaCoq.PCUIC.PCUICInductives]
i:87 [in MetaCoq.PCUIC.PCUICFirstorder]
i:871 [in MetaCoq.Template.utils.All_Forall]
i:877 [in MetaCoq.Template.utils.All_Forall]
i:879 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
i:883 [in MetaCoq.SafeChecker.PCUICSafeChecker]
i:886 [in MetaCoq.PCUIC.PCUICTyping]
i:888 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
i:89 [in MetaCoq.Template.utils.All_Forall]
i:89 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
i:890 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
i:9 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
i:902 [in MetaCoq.SafeChecker.PCUICSafeChecker]
i:903 [in MetaCoq.Template.utils.All_Forall]
i:906 [in MetaCoq.Template.utils.All_Forall]
i:91 [in MetaCoq.Template.TermEquality]
i:913 [in MetaCoq.Template.utils.All_Forall]
i:916 [in MetaCoq.Template.utils.All_Forall]
i:92 [in MetaCoq.Template.Typing]
i:92 [in MetaCoq.PCUIC.PCUICAst]
i:922 [in MetaCoq.Template.utils.All_Forall]
i:927 [in MetaCoq.Erasure.ErasureFunction]
i:929 [in MetaCoq.Erasure.ErasureFunction]
i:93 [in MetaCoq.Template.WfAst]
i:93 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
i:93 [in MetaCoq.PCUIC.PCUICInductiveInversion]
i:930 [in MetaCoq.Template.utils.All_Forall]
i:936 [in MetaCoq.Template.utils.All_Forall]
i:94 [in MetaCoq.Template.utils.All_Forall]
i:94 [in MetaCoq.Template.TermEquality]
i:94 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
i:94 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
I:941 [in MetaCoq.Template.utils.All_Forall]
i:943 [in MetaCoq.Template.utils.All_Forall]
i:947 [in MetaCoq.Template.utils.All_Forall]
I:949 [in MetaCoq.Template.utils.All_Forall]
i:95 [in MetaCoq.Template.WfAst]
i:951 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
i:952 [in MetaCoq.Template.utils.All_Forall]
i:956 [in MetaCoq.Template.utils.All_Forall]
I:959 [in MetaCoq.Template.utils.All_Forall]
i:96 [in MetaCoq.Erasure.EInduction]
i:96 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
i:96 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
i:962 [in MetaCoq.Template.utils.All_Forall]
i:965 [in MetaCoq.PCUIC.PCUICInductiveInversion]
i:967 [in MetaCoq.Template.utils.All_Forall]
i:97 [in MetaCoq.PCUIC.Syntax.PCUICCases]
i:971 [in MetaCoq.Template.utils.All_Forall]
i:974 [in MetaCoq.Template.utils.All_Forall]
i:977 [in MetaCoq.SafeChecker.PCUICSafeChecker]
i:98 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
i:98 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
i:981 [in MetaCoq.Template.utils.All_Forall]
i:983 [in MetaCoq.PCUIC.PCUICInductiveInversion]
i:983 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
i:984 [in MetaCoq.Template.utils.All_Forall]
i:993 [in MetaCoq.Template.utils.All_Forall]
| 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) |