| 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) |
M (binder)
max:7 [in MetaCoq.Template.utils.MCArith]mdeclvar:712 [in MetaCoq.SafeChecker.PCUICSafeChecker]
mdeclvar:801 [in MetaCoq.SafeChecker.PCUICSafeChecker]
mdeclvar:950 [in MetaCoq.SafeChecker.PCUICSafeChecker]
mdeclvar:976 [in MetaCoq.SafeChecker.PCUICSafeChecker]
mdecl':111 [in MetaCoq.Erasure.EDeps]
mdecl':125 [in MetaCoq.PCUIC.PCUICConvCumInversion]
mdecl':13 [in MetaCoq.PCUIC.PCUICGlobalEnv]
mdecl':143 [in MetaCoq.Erasure.EDeps]
mdecl':208 [in MetaCoq.Erasure.Extract]
mdecl':21 [in MetaCoq.PCUIC.PCUICGlobalEnv]
mdecl':213 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mdecl':214 [in MetaCoq.Erasure.Extract]
mdecl':224 [in MetaCoq.Erasure.Extract]
mdecl':307 [in MetaCoq.Erasure.EArities]
mdecl':317 [in MetaCoq.Erasure.EArities]
mdecl':346 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mdecl':358 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mdecl':41 [in MetaCoq.PCUIC.PCUICSR]
mdecl':444 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mdecl':451 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mdecl':461 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mdecl':473 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mdecl':484 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mdecl':497 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mdecl':7 [in MetaCoq.PCUIC.PCUICGlobalEnv]
mdecl':752 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mdecl':832 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mdecl':839 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mdecl':848 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mdecl':868 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mdecl':92 [in MetaCoq.Erasure.EDeps]
mdecl':99 [in MetaCoq.Erasure.EDeps]
mdecl:1 [in MetaCoq.PCUIC.Syntax.PCUICCases]
mdecl:1 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
mdecl:10 [in MetaCoq.PCUIC.PCUICElimination]
mdecl:10 [in MetaCoq.PCUIC.PCUICInductives]
mdecl:10 [in MetaCoq.PCUIC.PCUICInductiveInversion]
mdecl:10 [in MetaCoq.PCUIC.TemplateToPCUICExpanded]
mdecl:100 [in MetaCoq.Erasure.EArities]
mdecl:100 [in MetaCoq.Template.WfAst]
mdecl:1000 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
mdecl:1008 [in MetaCoq.PCUIC.PCUICInductiveInversion]
mdecl:102 [in MetaCoq.Erasure.EGlobalEnv]
mdecl:1029 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
mdecl:103 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
mdecl:1036 [in MetaCoq.Template.Typing]
mdecl:104 [in MetaCoq.PCUIC.PCUICInversion]
mdecl:104 [in MetaCoq.PCUIC.PCUICSR]
mdecl:104 [in MetaCoq.Template.TypingWf]
mdecl:1046 [in MetaCoq.Template.Typing]
mdecl:105 [in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
mdecl:1060 [in MetaCoq.Template.Typing]
mdecl:107 [in MetaCoq.Erasure.EDeps]
mdecl:107 [in MetaCoq.PCUIC.Syntax.PCUICCases]
mdecl:1077 [in MetaCoq.Template.Typing]
mdecl:1079 [in MetaCoq.SafeChecker.PCUICTypeChecker]
mdecl:109 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
mdecl:109 [in MetaCoq.Erasure.EGlobalEnv]
mdecl:109 [in MetaCoq.Template.TypingWf]
mdecl:11 [in MetaCoq.Erasure.ESubstitution]
mdecl:11 [in MetaCoq.PCUIC.PCUICExpandLets]
mdecl:11 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
mdecl:11 [in MetaCoq.Erasure.ErasureFunction]
mdecl:110 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
mdecl:110 [in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
mdecl:1100 [in MetaCoq.PCUIC.PCUICConversion]
mdecl:1107 [in MetaCoq.PCUIC.PCUICConversion]
mdecl:112 [in MetaCoq.PCUIC.PCUICInversion]
mdecl:113 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
mdecl:114 [in MetaCoq.PCUIC.PCUICWeakeningEnv]
mdecl:114 [in MetaCoq.Erasure.EInlineProjections]
mdecl:114 [in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
mdecl:115 [in MetaCoq.PCUIC.Syntax.PCUICCases]
mdecl:115 [in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
mdecl:116 [in MetaCoq.PCUIC.PCUICTyping]
mdecl:117 [in MetaCoq.PCUIC.PCUICInductives]
mdecl:117 [in MetaCoq.Template.TypingWf]
mdecl:118 [in MetaCoq.PCUIC.PCUICAlpha]
mdecl:119 [in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
mdecl:12 [in MetaCoq.PCUIC.Syntax.PCUICCases]
mdecl:12 [in MetaCoq.PCUIC.PCUICGlobalEnv]
mdecl:12 [in MetaCoq.Erasure.EExtends]
mdecl:120 [in MetaCoq.PCUIC.PCUICWeakeningEnv]
mdecl:121 [in MetaCoq.PCUIC.PCUICTyping]
mdecl:123 [in MetaCoq.PCUIC.PCUICInductiveInversion]
mdecl:123 [in MetaCoq.PCUIC.PCUICAlpha]
mdecl:123 [in MetaCoq.PCUIC.PCUICConvCumInversion]
mdecl:123 [in MetaCoq.Erasure.Prelim]
mdecl:124 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
mdecl:124 [in MetaCoq.PCUIC.PCUICInductives]
mdecl:124 [in MetaCoq.Erasure.EWcbvEval]
mdecl:127 [in MetaCoq.PCUIC.PCUICWeakeningEnv]
mdecl:1270 [in MetaCoq.SafeChecker.PCUICSafeConversion]
mdecl:1286 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
mdecl:129 [in MetaCoq.PCUIC.PCUICWcbvEval]
mdecl:129 [in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
mdecl:13 [in MetaCoq.Template.EnvironmentTyping]
mdecl:13 [in MetaCoq.Erasure.EGlobalEnv]
mdecl:13 [in MetaCoq.Examples.add_constructor]
mdecl:130 [in MetaCoq.PCUIC.PCUICTyping]
mdecl:130 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
mdecl:131 [in MetaCoq.PCUIC.PCUICInductives]
mdecl:131 [in MetaCoq.PCUIC.PCUICAlpha]
mdecl:131 [in MetaCoq.PCUIC.Syntax.PCUICCases]
mdecl:131 [in MetaCoq.Template.WcbvEval]
mdecl:132 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
mdecl:133 [in MetaCoq.Erasure.EWcbvEval]
mdecl:1336 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
mdecl:134 [in MetaCoq.PCUIC.PCUICElimination]
mdecl:135 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
mdecl:138 [in MetaCoq.PCUIC.Syntax.PCUICCases]
mdecl:139 [in MetaCoq.PCUIC.PCUICElimination]
mdecl:139 [in MetaCoq.PCUIC.PCUICInductives]
mdecl:139 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
mdecl:139 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
mdecl:14 [in MetaCoq.PCUIC.PCUICExpandLets]
mdecl:14 [in MetaCoq.Erasure.ErasureFunction]
mdecl:14 [in MetaCoq.PCUIC.TemplateToPCUICExpanded]
mdecl:141 [in MetaCoq.PCUIC.PCUICProgress]
mdecl:141 [in MetaCoq.Erasure.EDeps]
mdecl:141 [in MetaCoq.PCUIC.Syntax.PCUICCases]
mdecl:141 [in MetaCoq.PCUIC.PCUICTyping]
mdecl:142 [in MetaCoq.PCUIC.PCUICInversion]
mdecl:143 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
mdecl:143 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
mdecl:144 [in MetaCoq.Erasure.ErasureProperties]
mdecl:145 [in MetaCoq.PCUIC.PCUICWfUniverses]
mdecl:145 [in MetaCoq.Erasure.EWcbvEvalInd]
mdecl:145 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
mdecl:146 [in MetaCoq.PCUIC.PCUICEtaExpand]
mdecl:147 [in MetaCoq.PCUIC.PCUICWcbvEval]
mdecl:147 [in MetaCoq.PCUIC.Syntax.PCUICCases]
mdecl:147 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
mdecl:150 [in MetaCoq.PCUIC.PCUICInductiveInversion]
mdecl:150 [in MetaCoq.PCUIC.PCUICAlpha]
mdecl:150 [in MetaCoq.Erasure.EWcbvEval]
mdecl:151 [in MetaCoq.PCUIC.PCUICProgress]
mdecl:151 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
mdecl:151 [in MetaCoq.PCUIC.PCUICEtaExpand]
mdecl:151 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
mdecl:153 [in MetaCoq.PCUIC.PCUICInversion]
mdecl:155 [in MetaCoq.PCUIC.PCUICSR]
mdecl:156 [in MetaCoq.PCUIC.PCUICEtaExpand]
mdecl:158 [in MetaCoq.Template.TypingWf]
mdecl:159 [in MetaCoq.Erasure.EWcbvEvalInd]
mdecl:161 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
mdecl:162 [in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
mdecl:163 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mdecl:163 [in MetaCoq.Template.WcbvEval]
mdecl:164 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
mdecl:164 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mdecl:164 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
mdecl:164 [in MetaCoq.Erasure.EWcbvEval]
mdecl:165 [in MetaCoq.PCUIC.PCUICProgress]
mdecl:165 [in MetaCoq.PCUIC.PCUICElimination]
mdecl:165 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mdecl:165 [in MetaCoq.Template.Typing]
mdecl:165 [in MetaCoq.PCUIC.PCUICSR]
mdecl:166 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mdecl:166 [in MetaCoq.Template.TypingWf]
mdecl:167 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mdecl:168 [in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
mdecl:169 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
mdecl:169 [in MetaCoq.Template.TypingWf]
mdecl:17 [in MetaCoq.PCUIC.PCUICInductives]
mdecl:17 [in MetaCoq.Erasure.EGlobalEnv]
mdecl:17 [in MetaCoq.Erasure.EExtends]
mdecl:172 [in MetaCoq.Template.TypingWf]
mdecl:173 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
mdecl:175 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
mdecl:177 [in MetaCoq.Template.TypingWf]
mdecl:178 [in MetaCoq.PCUIC.PCUICInductives]
mdecl:178 [in MetaCoq.Erasure.EWcbvEval]
mdecl:179 [in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
mdecl:18 [in MetaCoq.Template.EnvironmentTyping]
mdecl:18 [in MetaCoq.PCUIC.Syntax.PCUICCases]
mdecl:180 [in MetaCoq.PCUIC.PCUICArities]
mdecl:180 [in MetaCoq.Erasure.EConstructorsAsBlocks]
mdecl:181 [in MetaCoq.PCUIC.PCUICAlpha]
mdecl:181 [in MetaCoq.PCUIC.Syntax.PCUICCases]
mdecl:181 [in MetaCoq.Template.TypingWf]
mdecl:182 [in MetaCoq.PCUIC.PCUICProgress]
mdecl:182 [in MetaCoq.PCUIC.PCUICInductives]
mdecl:182 [in MetaCoq.Template.WcbvEval]
mdecl:183 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
mdecl:183 [in MetaCoq.Template.Typing]
mdecl:184 [in MetaCoq.Erasure.EConstructorsAsBlocks]
mdecl:185 [in MetaCoq.PCUIC.Syntax.PCUICCases]
mdecl:187 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mdecl:187 [in MetaCoq.PCUIC.PCUICInductives]
mdecl:188 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
mdecl:188 [in MetaCoq.PCUIC.Syntax.PCUICCases]
mdecl:188 [in MetaCoq.Template.TypingWf]
mdecl:189 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
mdecl:19 [in MetaCoq.PCUIC.PCUICExpandLets]
mdecl:190 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
mdecl:190 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mdecl:190 [in MetaCoq.Erasure.EConstructorsAsBlocks]
mdecl:191 [in MetaCoq.PCUIC.PCUICAlpha]
mdecl:191 [in MetaCoq.PCUIC.Syntax.PCUICCases]
mdecl:192 [in MetaCoq.PCUIC.PCUICSR]
mdecl:193 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
mdecl:193 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
mdecl:194 [in MetaCoq.PCUIC.PCUICElimination]
mdecl:194 [in MetaCoq.PCUIC.PCUICArities]
mdecl:194 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mdecl:194 [in MetaCoq.PCUIC.PCUICInductiveInversion]
mdecl:197 [in MetaCoq.PCUIC.Syntax.PCUICCases]
mdecl:198 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
mdecl:198 [in MetaCoq.Erasure.EWcbvEval]
mdecl:2 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mdecl:20 [in MetaCoq.PCUIC.PCUICElimination]
mdecl:20 [in MetaCoq.PCUIC.PCUICInductives]
mdecl:20 [in MetaCoq.PCUIC.TemplateToPCUIC]
mdecl:20 [in MetaCoq.PCUIC.PCUICGlobalEnv]
mdecl:20 [in MetaCoq.Erasure.EEnvMap]
mdecl:200 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
mdecl:201 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
mdecl:202 [in MetaCoq.PCUIC.Syntax.PCUICCases]
mdecl:204 [in MetaCoq.PCUIC.PCUICSubstitution]
mdecl:204 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
mdecl:205 [in MetaCoq.Erasure.Extract]
mdecl:206 [in MetaCoq.PCUIC.PCUICInductives]
mdecl:207 [in MetaCoq.PCUIC.Syntax.PCUICCases]
mdecl:208 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
mdecl:209 [in MetaCoq.PCUIC.PCUICSubstitution]
mdecl:21 [in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
mdecl:210 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
mdecl:210 [in MetaCoq.PCUIC.PCUICTyping]
mdecl:210 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
mdecl:212 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mdecl:212 [in MetaCoq.PCUIC.PCUICWcbvEval]
mdecl:212 [in MetaCoq.Erasure.Extract]
mdecl:212 [in MetaCoq.PCUIC.Syntax.PCUICCases]
mdecl:213 [in MetaCoq.Template.TypingWf]
mdecl:214 [in MetaCoq.PCUIC.PCUICSubstitution]
mdecl:214 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
mdecl:215 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
mdecl:216 [in MetaCoq.PCUIC.PCUICInductives]
mdecl:217 [in MetaCoq.PCUIC.Syntax.PCUICCases]
mdecl:218 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
mdecl:218 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
mdecl:219 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mdecl:219 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
mdecl:22 [in MetaCoq.PCUIC.PCUICSafeLemmata]
mdecl:22 [in MetaCoq.Erasure.EGlobalEnv]
mdecl:220 [in MetaCoq.Erasure.Extract]
mdecl:222 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
mdecl:223 [in MetaCoq.PCUIC.PCUICSubstitution]
mdecl:224 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
mdecl:225 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
mdecl:225 [in MetaCoq.Erasure.EConstructorsAsBlocks]
mdecl:225 [in MetaCoq.Template.WcbvEval]
mdecl:225 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
mdecl:226 [in MetaCoq.PCUIC.Syntax.PCUICCases]
mdecl:226 [in MetaCoq.PCUIC.PCUICTyping]
mdecl:227 [in MetaCoq.PCUIC.PCUICWcbvEval]
mdecl:231 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
mdecl:232 [in MetaCoq.PCUIC.PCUICSubstitution]
mdecl:232 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
mdecl:233 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
mdecl:233 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
mdecl:2353 [in MetaCoq.SafeChecker.PCUICSafeConversion]
mdecl:236 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
mdecl:238 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
mdecl:238 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
mdecl:238 [in MetaCoq.Template.TypingWf]
mdecl:239 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
mdecl:239 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
mdecl:240 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
mdecl:243 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
mdecl:244 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
mdecl:245 [in MetaCoq.Template.EtaExpand]
mdecl:248 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
mdecl:248 [in MetaCoq.Template.WcbvEval]
mdecl:25 [in MetaCoq.PCUIC.PCUICExpandLets]
mdecl:251 [in MetaCoq.Template.EtaExpand]
mdecl:252 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
mdecl:256 [in MetaCoq.Template.EtaExpand]
mdecl:257 [in MetaCoq.PCUIC.PCUICInductiveInversion]
mdecl:258 [in MetaCoq.PCUIC.PCUICWfUniverses]
mdecl:259 [in MetaCoq.PCUIC.PCUICWcbvEval]
mdecl:259 [in MetaCoq.Erasure.EWcbvEval]
mdecl:26 [in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
mdecl:262 [in MetaCoq.Template.Typing]
mdecl:263 [in MetaCoq.PCUIC.PCUICWfUniverses]
mdecl:267 [in MetaCoq.Erasure.EWcbvEval]
mdecl:27 [in MetaCoq.PCUIC.PCUICInductives]
mdecl:271 [in MetaCoq.Template.TypingWf]
mdecl:278 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
mdecl:28 [in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
mdecl:28 [in MetaCoq.Erasure.ErasureCorrectness]
mdecl:28 [in MetaCoq.PCUIC.TemplateToPCUIC]
mdecl:28 [in MetaCoq.Erasure.EEnvMap]
mdecl:281 [in MetaCoq.PCUIC.PCUICInductives]
mdecl:281 [in MetaCoq.PCUIC.PCUICInductiveInversion]
mdecl:283 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
mdecl:288 [in MetaCoq.PCUIC.PCUICInductives]
mdecl:291 [in MetaCoq.PCUIC.PCUICProgress]
mdecl:294 [in MetaCoq.Template.TypingWf]
mdecl:296 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
mdecl:299 [in MetaCoq.Template.TypingWf]
mdecl:30 [in MetaCoq.PCUIC.PCUICElimination]
mdecl:301 [in MetaCoq.PCUIC.PCUICProgress]
mdecl:301 [in MetaCoq.PCUIC.PCUICInductiveInversion]
mdecl:305 [in MetaCoq.Erasure.EArities]
mdecl:305 [in MetaCoq.Template.TypingWf]
mdecl:309 [in MetaCoq.PCUIC.PCUICInductiveInversion]
mdecl:31 [in MetaCoq.PCUIC.PCUICGlobalEnv]
mdecl:312 [in MetaCoq.PCUIC.PCUICInductives]
mdecl:312 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
mdecl:314 [in MetaCoq.Erasure.EArities]
mdecl:315 [in MetaCoq.PCUIC.PCUICProgress]
mdecl:316 [in MetaCoq.PCUIC.PCUICInductiveInversion]
mdecl:317 [in MetaCoq.PCUIC.PCUICCumulProp]
mdecl:323 [in MetaCoq.PCUIC.PCUICInductives]
mdecl:323 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
mdecl:323 [in MetaCoq.SafeChecker.PCUICSafeChecker]
mdecl:327 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
mdecl:328 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
mdecl:329 [in MetaCoq.SafeChecker.PCUICSafeChecker]
mdecl:33 [in MetaCoq.PCUIC.PCUICCasesContexts]
mdecl:332 [in MetaCoq.PCUIC.PCUICProgress]
mdecl:332 [in MetaCoq.Template.Ast]
mdecl:332 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
mdecl:334 [in MetaCoq.PCUIC.PCUICInductives]
mdecl:337 [in MetaCoq.Erasure.EArities]
mdecl:34 [in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
mdecl:340 [in MetaCoq.PCUIC.PCUICInductiveInversion]
mdecl:341 [in MetaCoq.Template.Ast]
mdecl:341 [in MetaCoq.SafeChecker.PCUICSafeChecker]
mdecl:343 [in MetaCoq.PCUIC.PCUICInductiveInversion]
mdecl:344 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mdecl:344 [in MetaCoq.Template.Typing]
mdecl:344 [in MetaCoq.PCUIC.PCUICInductives]
mdecl:345 [in MetaCoq.SafeChecker.PCUICSafeChecker]
mdecl:346 [in MetaCoq.Template.Ast]
mdecl:348 [in MetaCoq.SafeChecker.PCUICSafeChecker]
mdecl:349 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mdecl:35 [in MetaCoq.PCUIC.PCUICGlobalEnv]
mdecl:352 [in MetaCoq.Template.Ast]
mdecl:356 [in MetaCoq.Template.Ast]
mdecl:359 [in MetaCoq.Template.Ast]
mdecl:359 [in MetaCoq.Erasure.ERemoveParams]
mdecl:36 [in MetaCoq.PCUIC.PCUICWcbvEval]
mdecl:362 [in MetaCoq.Template.Typing]
mdecl:365 [in MetaCoq.PCUIC.PCUICWcbvEval]
mdecl:365 [in MetaCoq.Template.Ast]
mdecl:37 [in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
mdecl:37 [in MetaCoq.Template.WfAst]
mdecl:37 [in MetaCoq.Erasure.EEnvMap]
mdecl:370 [in MetaCoq.Template.Ast]
mdecl:371 [in MetaCoq.PCUIC.PCUICWcbvEval]
mdecl:378 [in MetaCoq.Template.Ast]
mdecl:38 [in MetaCoq.PCUIC.PCUICArities]
mdecl:38 [in MetaCoq.Erasure.EGlobalEnv]
mdecl:384 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
mdecl:384 [in MetaCoq.PCUIC.PCUICProgress]
mdecl:384 [in MetaCoq.PCUIC.PCUICInductives]
mdecl:384 [in MetaCoq.Template.Ast]
mdecl:385 [in MetaCoq.Erasure.ERemoveParams]
mdecl:39 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
mdecl:39 [in MetaCoq.PCUIC.PCUICInductives]
mdecl:390 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
mdecl:390 [in MetaCoq.Erasure.ERemoveParams]
mdecl:395 [in MetaCoq.PCUIC.PCUICProgress]
mdecl:397 [in MetaCoq.PCUIC.PCUICInductives]
mdecl:399 [in MetaCoq.Template.Ast]
mdecl:4 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
mdecl:4 [in MetaCoq.PCUIC.PCUICTyping]
mdecl:40 [in MetaCoq.PCUIC.Syntax.PCUICCases]
mdecl:40 [in MetaCoq.PCUIC.PCUICGlobalEnv]
mdecl:40 [in MetaCoq.PCUIC.PCUICSR]
mdecl:40 [in MetaCoq.SafeChecker.PCUICTypeChecker]
mdecl:401 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
mdecl:401 [in MetaCoq.SafeChecker.PCUICSafeChecker]
mdecl:404 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
mdecl:406 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mdecl:406 [in MetaCoq.PCUIC.PCUICInductives]
mdecl:407 [in MetaCoq.PCUIC.PCUICProgress]
mdecl:409 [in MetaCoq.Template.EtaExpand]
mdecl:409 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mdecl:41 [in MetaCoq.Template.EnvironmentTyping]
mdecl:41 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
mdecl:41 [in MetaCoq.Erasure.EGlobalEnv]
mdecl:410 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
mdecl:413 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
mdecl:414 [in MetaCoq.Erasure.ERemoveParams]
mdecl:417 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
mdecl:417 [in MetaCoq.Erasure.ERemoveParams]
mdecl:419 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
mdecl:42 [in MetaCoq.PCUIC.PCUICElimination]
mdecl:42 [in MetaCoq.PCUIC.PCUICConvCumInversion]
mdecl:42 [in MetaCoq.PCUIC.PCUICCasesContexts]
mdecl:42 [in MetaCoq.PCUIC.PCUICContexts]
mdecl:420 [in MetaCoq.Template.EtaExpand]
mdecl:420 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mdecl:420 [in MetaCoq.PCUIC.PCUICInductives]
mdecl:425 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mdecl:425 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
mdecl:427 [in MetaCoq.SafeChecker.PCUICSafeChecker]
mdecl:428 [in MetaCoq.PCUIC.PCUICInductiveInversion]
mdecl:43 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
mdecl:43 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
mdecl:43 [in MetaCoq.PCUIC.Conversion.PCUICClosedConv]
mdecl:432 [in MetaCoq.PCUIC.PCUICInductives]
mdecl:439 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mdecl:44 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
mdecl:44 [in MetaCoq.Template.EnvironmentTyping]
mdecl:44 [in MetaCoq.Erasure.EEnvMap]
mdecl:440 [in MetaCoq.PCUIC.PCUICInductiveInversion]
mdecl:441 [in MetaCoq.PCUIC.PCUICProgress]
mdecl:446 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
mdecl:449 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mdecl:45 [in MetaCoq.PCUIC.Syntax.PCUICCases]
mdecl:45 [in MetaCoq.Template.WcbvEval]
mdecl:45 [in MetaCoq.Erasure.EGlobalEnv]
mdecl:454 [in MetaCoq.PCUIC.PCUICInductiveInversion]
mdecl:457 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
mdecl:459 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mdecl:467 [in MetaCoq.PCUIC.PCUICInductiveInversion]
mdecl:468 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mdecl:47 [in MetaCoq.Template.EnvironmentTyping]
mdecl:47 [in MetaCoq.Erasure.EWellformed]
mdecl:47 [in MetaCoq.PCUIC.PCUICGlobalEnv]
mdecl:47 [in MetaCoq.PCUIC.PCUICTyping]
mdecl:473 [in MetaCoq.Template.EnvironmentTyping]
mdecl:473 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
mdecl:477 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mdecl:488 [in MetaCoq.Template.EnvironmentTyping]
mdecl:490 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mdecl:50 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
mdecl:50 [in MetaCoq.Erasure.EEnvMap]
mdecl:50 [in MetaCoq.PCUIC.PCUICCasesContexts]
mdecl:50 [in MetaCoq.PCUIC.Conversion.PCUICClosedConv]
mdecl:50 [in MetaCoq.PCUIC.PCUICContexts]
mdecl:501 [in MetaCoq.Template.EtaExpand]
mdecl:51 [in MetaCoq.Template.EnvironmentTyping]
mdecl:51 [in MetaCoq.PCUIC.Syntax.PCUICCases]
mdecl:510 [in MetaCoq.PCUIC.PCUICInductiveInversion]
mdecl:52 [in MetaCoq.Template.WfAst]
mdecl:52 [in MetaCoq.Erasure.EGlobalEnv]
mdecl:52 [in MetaCoq.PCUIC.TemplateToPCUICExpanded]
mdecl:52 [in MetaCoq.SafeChecker.PCUICTypeChecker]
mdecl:533 [in MetaCoq.PCUIC.PCUICTyping]
mdecl:535 [in MetaCoq.Template.EnvironmentTyping]
mdecl:537 [in MetaCoq.Template.EnvironmentTyping]
mdecl:539 [in MetaCoq.SafeChecker.PCUICSafeChecker]
mdecl:54 [in MetaCoq.PCUIC.PCUICElimination]
mdecl:542 [in MetaCoq.Template.EnvironmentTyping]
mdecl:543 [in MetaCoq.PCUIC.PCUICTyping]
mdecl:546 [in MetaCoq.Template.EnvironmentTyping]
mdecl:549 [in MetaCoq.Template.EnvironmentTyping]
mdecl:55 [in MetaCoq.Template.EnvironmentTyping]
mdecl:55 [in MetaCoq.PCUIC.PCUICInductiveInversion]
mdecl:55 [in MetaCoq.PCUIC.Syntax.PCUICCases]
mdecl:55 [in MetaCoq.PCUIC.PCUICCasesContexts]
mdecl:553 [in MetaCoq.Template.EnvironmentTyping]
mdecl:556 [in MetaCoq.SafeChecker.PCUICSafeChecker]
mdecl:557 [in MetaCoq.PCUIC.PCUICTyping]
mdecl:559 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
mdecl:561 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
mdecl:564 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
mdecl:567 [in MetaCoq.PCUIC.PCUICSR]
mdecl:57 [in MetaCoq.Erasure.EGlobalEnv]
mdecl:572 [in MetaCoq.PCUIC.PCUICInductiveInversion]
mdecl:574 [in MetaCoq.Template.EnvironmentTyping]
mdecl:574 [in MetaCoq.PCUIC.PCUICTyping]
mdecl:574 [in MetaCoq.PCUIC.PCUICSR]
mdecl:578 [in MetaCoq.Template.EnvironmentTyping]
mdecl:58 [in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
mdecl:58 [in MetaCoq.PCUIC.Syntax.PCUICCases]
mdecl:58 [in MetaCoq.PCUIC.PCUICContexts]
mdecl:58 [in MetaCoq.Erasure.EGenericMapEnv]
mdecl:581 [in MetaCoq.SafeChecker.PCUICSafeChecker]
mdecl:584 [in MetaCoq.PCUIC.PCUICSR]
mdecl:586 [in MetaCoq.PCUIC.PCUICInductiveInversion]
mdecl:59 [in MetaCoq.Erasure.EEnvMap]
mdecl:590 [in MetaCoq.Template.EnvironmentTyping]
mdecl:597 [in MetaCoq.Template.EnvironmentTyping]
mdecl:6 [in MetaCoq.PCUIC.PCUICSafeLemmata]
mdecl:6 [in MetaCoq.Template.Typing]
mdecl:6 [in MetaCoq.PCUIC.PCUICGlobalEnv]
mdecl:60 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
mdecl:60 [in MetaCoq.Template.EnvironmentTyping]
mdecl:61 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
mdecl:61 [in MetaCoq.PCUIC.Syntax.PCUICCases]
mdecl:611 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
mdecl:617 [in MetaCoq.SafeChecker.PCUICSafeChecker]
mdecl:622 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
mdecl:626 [in MetaCoq.Template.EnvironmentTyping]
mdecl:626 [in MetaCoq.SafeChecker.PCUICSafeChecker]
mdecl:634 [in MetaCoq.PCUIC.PCUICInductives]
mdecl:638 [in MetaCoq.Template.Typing]
mdecl:64 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
mdecl:64 [in MetaCoq.PCUIC.Syntax.PCUICCases]
mdecl:641 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
mdecl:642 [in MetaCoq.PCUIC.PCUICInductives]
mdecl:644 [in MetaCoq.Template.Typing]
mdecl:645 [in MetaCoq.PCUIC.PCUICSR]
mdecl:648 [in MetaCoq.Template.EnvironmentTyping]
mdecl:649 [in MetaCoq.PCUIC.PCUICInductiveInversion]
mdecl:65 [in MetaCoq.Template.EnvironmentTyping]
mdecl:65 [in MetaCoq.PCUIC.PCUICInductiveInversion]
mdecl:65 [in MetaCoq.Erasure.EGlobalEnv]
mdecl:652 [in MetaCoq.PCUIC.PCUICInductives]
mdecl:654 [in MetaCoq.Template.Typing]
mdecl:659 [in MetaCoq.PCUIC.PCUICSR]
mdecl:66 [in MetaCoq.Template.EtaExpand]
mdecl:66 [in MetaCoq.PCUIC.PCUICElimination]
mdecl:66 [in MetaCoq.Erasure.EArities]
mdecl:66 [in MetaCoq.PCUIC.PCUICValidity]
mdecl:666 [in MetaCoq.Template.Typing]
mdecl:668 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mdecl:669 [in MetaCoq.PCUIC.PCUICSR]
mdecl:67 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
mdecl:670 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
mdecl:672 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mdecl:673 [in MetaCoq.PCUIC.PCUICInductiveInversion]
mdecl:68 [in MetaCoq.Erasure.EGlobalEnv]
mdecl:680 [in MetaCoq.PCUIC.PCUICInductiveInversion]
mdecl:682 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mdecl:69 [in MetaCoq.Template.EtaExpand]
mdecl:69 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
mdecl:69 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
mdecl:69 [in MetaCoq.PCUIC.Syntax.PCUICCases]
mdecl:69 [in MetaCoq.PCUIC.PCUICTyping]
mdecl:698 [in MetaCoq.PCUIC.PCUICInductiveInversion]
mdecl:698 [in MetaCoq.PCUIC.PCUICSR]
mdecl:70 [in MetaCoq.PCUIC.PCUICElimination]
mdecl:702 [in MetaCoq.SafeChecker.PCUICSafeChecker]
mdecl:708 [in MetaCoq.SafeChecker.PCUICSafeChecker]
mdecl:71 [in MetaCoq.Template.EnvironmentTyping]
mdecl:71 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
mdecl:71 [in MetaCoq.Template.WcbvEval]
mdecl:713 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mdecl:716 [in MetaCoq.SafeChecker.PCUICTypeChecker]
mdecl:72 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
mdecl:72 [in MetaCoq.Template.EtaExpand]
mdecl:72 [in MetaCoq.Erasure.EGlobalEnv]
mdecl:726 [in MetaCoq.PCUIC.PCUICInductiveInversion]
mdecl:728 [in MetaCoq.PCUIC.PCUICSR]
mdecl:73 [in MetaCoq.PCUIC.PCUICWcbvEval]
mdecl:736 [in MetaCoq.PCUIC.PCUICInductiveInversion]
mdecl:743 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mdecl:75 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
mdecl:75 [in MetaCoq.PCUIC.Syntax.PCUICCases]
mdecl:75 [in MetaCoq.PCUIC.PCUICCasesContexts]
mdecl:750 [in MetaCoq.PCUIC.PCUICInductiveInversion]
mdecl:76 [in MetaCoq.Erasure.EAst]
mdecl:768 [in MetaCoq.PCUIC.PCUICInductiveInversion]
mdecl:77 [in MetaCoq.PCUIC.PCUICInductiveInversion]
mdecl:77 [in MetaCoq.Erasure.EGlobalEnv]
mdecl:770 [in MetaCoq.SafeChecker.PCUICTypeChecker]
mdecl:773 [in MetaCoq.PCUIC.PCUICInductiveInversion]
mdecl:773 [in MetaCoq.SafeChecker.PCUICTypeChecker]
mdecl:78 [in MetaCoq.PCUIC.PCUICInductives]
mdecl:791 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mdecl:794 [in MetaCoq.SafeChecker.PCUICSafeChecker]
mdecl:80 [in MetaCoq.PCUIC.Syntax.PCUICCases]
mdecl:80 [in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
mdecl:806 [in MetaCoq.PCUIC.PCUICInductiveInversion]
mdecl:819 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mdecl:823 [in MetaCoq.SafeChecker.PCUICSafeChecker]
mdecl:829 [in MetaCoq.SafeChecker.PCUICSafeChecker]
mdecl:83 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
mdecl:83 [in MetaCoq.Erasure.EGlobalEnv]
mdecl:830 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mdecl:835 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mdecl:84 [in MetaCoq.Erasure.Prelim]
mdecl:844 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mdecl:85 [in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
mdecl:856 [in MetaCoq.PCUIC.PCUICTyping]
mdecl:86 [in MetaCoq.PCUIC.Syntax.PCUICCases]
mdecl:864 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mdecl:866 [in MetaCoq.PCUIC.PCUICTyping]
mdecl:88 [in MetaCoq.PCUIC.PCUICWcbvEval]
mdecl:880 [in MetaCoq.PCUIC.PCUICTyping]
mdecl:882 [in MetaCoq.SafeChecker.PCUICSafeChecker]
mdecl:89 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
mdecl:89 [in MetaCoq.Erasure.EDeps]
mdecl:89 [in MetaCoq.Template.WcbvEval]
mdecl:891 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mdecl:897 [in MetaCoq.PCUIC.PCUICTyping]
mdecl:9 [in MetaCoq.Erasure.EInlineProjections]
mdecl:9 [in MetaCoq.Template.EnvironmentTyping]
mdecl:90 [in MetaCoq.Erasure.EGlobalEnv]
mdecl:90 [in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
mdecl:901 [in MetaCoq.SafeChecker.PCUICSafeChecker]
mdecl:907 [in MetaCoq.PCUIC.PCUICInductiveInversion]
mdecl:91 [in MetaCoq.PCUIC.Syntax.PCUICCases]
mdecl:914 [in MetaCoq.PCUIC.PCUICInductiveInversion]
mdecl:92 [in MetaCoq.Erasure.Prelim]
mdecl:922 [in MetaCoq.PCUIC.PCUICInductiveInversion]
mdecl:925 [in MetaCoq.Erasure.ErasureFunction]
mdecl:929 [in MetaCoq.PCUIC.PCUICInductiveInversion]
mdecl:939 [in MetaCoq.PCUIC.PCUICInductiveInversion]
mdecl:939 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
mdecl:945 [in MetaCoq.SafeChecker.PCUICSafeChecker]
mdecl:947 [in MetaCoq.PCUIC.PCUICInductiveInversion]
mdecl:948 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
mdecl:95 [in MetaCoq.Template.Typing]
mdecl:957 [in MetaCoq.PCUIC.PCUICInductiveInversion]
mdecl:96 [in MetaCoq.Erasure.EGlobalEnv]
mdecl:96 [in MetaCoq.Template.TypingWf]
mdecl:962 [in MetaCoq.SafeChecker.PCUICSafeChecker]
mdecl:963 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
mdecl:969 [in MetaCoq.SafeChecker.PCUICSafeChecker]
mdecl:97 [in MetaCoq.Erasure.EDeps]
mdecl:97 [in MetaCoq.PCUIC.PCUICInversion]
mdecl:97 [in MetaCoq.Erasure.Prelim]
mdecl:975 [in MetaCoq.PCUIC.PCUICInductiveInversion]
mdecl:979 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
mdecl:98 [in MetaCoq.Erasure.ESubstitution]
mdecl:988 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
mdecl:991 [in MetaCoq.PCUIC.PCUICInductiveInversion]
md:1023 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
md:17 [in MetaCoq.PCUIC.PCUICToTemplate]
md:28 [in MetaCoq.PCUIC.PCUICExpandLets]
md:51 [in MetaCoq.PCUIC.TemplateToPCUIC]
ME:19 [in MetaCoq.SafeChecker.PCUICSafeChecker]
ME:71 [in MetaCoq.Template.monad_utils]
mfixctx:125 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
mfixctx:585 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
mfixctx:608 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
mfixctx:617 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
mfixctx:622 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
mfixctx:629 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
mfixctx:639 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
mfixi:1050 [in MetaCoq.PCUIC.PCUICReduction]
mfixi:1055 [in MetaCoq.PCUIC.PCUICReduction]
mfixi:1121 [in MetaCoq.PCUIC.PCUICReduction]
mfixi:1126 [in MetaCoq.PCUIC.PCUICReduction]
mfix'':734 [in MetaCoq.PCUIC.PCUICConversion]
mfix'':739 [in MetaCoq.PCUIC.PCUICConversion]
mfix'':756 [in MetaCoq.PCUIC.PCUICConversion]
mfix'':761 [in MetaCoq.PCUIC.PCUICConversion]
mfix':10 [in MetaCoq.PCUIC.PCUICToTemplate]
mfix':100 [in MetaCoq.Erasure.EConstructorsAsBlocks]
mfix':101 [in MetaCoq.Erasure.ERemoveParams]
mfix':1012 [in MetaCoq.PCUIC.PCUICReduction]
mfix':1017 [in MetaCoq.PCUIC.PCUICReduction]
mfix':103 [in MetaCoq.Erasure.EConstructorsAsBlocks]
mfix':1038 [in MetaCoq.PCUIC.PCUICReduction]
mfix':1046 [in MetaCoq.PCUIC.PCUICReduction]
mfix':1062 [in MetaCoq.PCUIC.PCUICReduction]
mfix':107 [in MetaCoq.SafeChecker.PCUICErrors]
mfix':1083 [in MetaCoq.PCUIC.PCUICReduction]
mfix':1088 [in MetaCoq.PCUIC.PCUICReduction]
mfix':11 [in MetaCoq.PCUIC.PCUICCSubst]
mfix':11 [in MetaCoq.Erasure.ELiftSubst]
mfix':11 [in MetaCoq.Template.WcbvEval]
mfix':11 [in MetaCoq.PCUIC.PCUICToTemplate]
mfix':11 [in MetaCoq.Erasure.ECSubst]
mfix':1109 [in MetaCoq.PCUIC.PCUICReduction]
mfix':1117 [in MetaCoq.PCUIC.PCUICReduction]
mfix':112 [in MetaCoq.SafeChecker.PCUICErrors]
mfix':127 [in MetaCoq.SafeChecker.PCUICErrors]
mfix':13 [in MetaCoq.PCUIC.PCUICGuardCondition]
mfix':131 [in MetaCoq.Template.TermEquality]
mfix':131 [in MetaCoq.PCUIC.PCUICConvCumInversion]
mfix':133 [in MetaCoq.Erasure.Extract]
mfix':136 [in MetaCoq.Template.TermEquality]
mfix':142 [in MetaCoq.Erasure.Extract]
mfix':143 [in MetaCoq.PCUIC.PCUICConvCumInversion]
mfix':150 [in MetaCoq.PCUIC.PCUICNormal]
mfix':153 [in MetaCoq.PCUIC.PCUICNormal]
mfix':157 [in MetaCoq.Template.Checker]
mfix':159 [in MetaCoq.Template.Checker]
mfix':163 [in MetaCoq.PCUIC.PCUICNormal]
mfix':166 [in MetaCoq.PCUIC.PCUICNormal]
mfix':166 [in MetaCoq.PCUIC.PCUICConfluence]
mfix':171 [in MetaCoq.PCUIC.PCUICConfluence]
mfix':172 [in MetaCoq.PCUIC.PCUICAst]
mfix':174 [in MetaCoq.PCUIC.PCUICAst]
mfix':175 [in MetaCoq.PCUIC.PCUICEquality]
mfix':176 [in MetaCoq.PCUIC.PCUICConfluence]
mfix':18 [in MetaCoq.Erasure.EInlineProjections]
mfix':180 [in MetaCoq.PCUIC.PCUICEquality]
mfix':181 [in MetaCoq.PCUIC.PCUICConfluence]
mfix':183 [in MetaCoq.PCUIC.PCUICAst]
mfix':185 [in MetaCoq.PCUIC.PCUICAst]
mfix':19 [in MetaCoq.Erasure.EInlineProjections]
mfix':1945 [in MetaCoq.SafeChecker.PCUICSafeConversion]
mfix':20 [in MetaCoq.Erasure.ELiftSubst]
mfix':200 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
mfix':201 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
mfix':205 [in MetaCoq.PCUIC.PCUICConfluence]
mfix':2126 [in MetaCoq.SafeChecker.PCUICSafeConversion]
mfix':2140 [in MetaCoq.SafeChecker.PCUICSafeConversion]
mfix':219 [in MetaCoq.PCUIC.PCUICConfluence]
mfix':22 [in MetaCoq.Erasure.ELiftSubst]
mfix':224 [in MetaCoq.PCUIC.PCUICConfluence]
mfix':227 [in MetaCoq.PCUIC.PCUICAst]
mfix':228 [in MetaCoq.PCUIC.PCUICAst]
mfix':229 [in MetaCoq.Template.Ast]
mfix':229 [in MetaCoq.PCUIC.PCUICConfluence]
mfix':231 [in MetaCoq.Template.Ast]
mfix':234 [in MetaCoq.PCUIC.PCUICConfluence]
mfix':239 [in MetaCoq.PCUIC.PCUICConfluence]
mfix':241 [in MetaCoq.Template.Ast]
mfix':243 [in MetaCoq.Template.Ast]
mfix':263 [in MetaCoq.PCUIC.PCUICConfluence]
mfix':267 [in MetaCoq.Erasure.ERemoveParams]
mfix':268 [in MetaCoq.Erasure.ERemoveParams]
mfix':273 [in MetaCoq.Template.Ast]
mfix':274 [in MetaCoq.Template.Ast]
mfix':277 [in MetaCoq.PCUIC.PCUICConfluence]
mfix':30 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
mfix':31 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
mfix':317 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
mfix':324 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
mfix':33 [in MetaCoq.PCUIC.PCUICGuardCondition]
mfix':35 [in MetaCoq.PCUIC.PCUICRedTypeIrrelevance]
mfix':374 [in MetaCoq.PCUIC.PCUICNormal]
mfix':404 [in MetaCoq.PCUIC.PCUICConfluence]
mfix':408 [in MetaCoq.PCUIC.PCUICNormal]
mfix':417 [in MetaCoq.Erasure.ErasureFunction]
mfix':419 [in MetaCoq.Erasure.ErasureFunction]
mfix':42 [in MetaCoq.PCUIC.PCUICGuardCondition]
mfix':425 [in MetaCoq.PCUIC.PCUICConfluence]
mfix':43 [in MetaCoq.PCUIC.TemplateToPCUIC]
mfix':44 [in MetaCoq.PCUIC.TemplateToPCUIC]
mfix':474 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
mfix':476 [in MetaCoq.PCUIC.PCUICConfluence]
mfix':480 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
mfix':49 [in MetaCoq.PCUIC.PCUICAlpha]
mfix':497 [in MetaCoq.PCUIC.PCUICConfluence]
mfix':505 [in MetaCoq.Template.Typing]
mfix':51 [in MetaCoq.PCUIC.PCUICGuardCondition]
mfix':514 [in MetaCoq.Template.Typing]
mfix':524 [in MetaCoq.Template.Typing]
mfix':53 [in MetaCoq.PCUIC.PCUICAlpha]
mfix':541 [in MetaCoq.Template.Typing]
mfix':550 [in MetaCoq.Template.Typing]
mfix':560 [in MetaCoq.Template.Typing]
mfix':571 [in MetaCoq.SafeChecker.PCUICSafeConversion]
mfix':575 [in MetaCoq.SafeChecker.PCUICSafeConversion]
mfix':589 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
mfix':6 [in MetaCoq.PCUIC.PCUICGuardCondition]
mfix':60 [in MetaCoq.Erasure.Extract]
mfix':60 [in MetaCoq.PCUIC.PCUICGuardCondition]
mfix':609 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
mfix':618 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
mfix':65 [in MetaCoq.Erasure.Extract]
mfix':677 [in MetaCoq.PCUIC.PCUICConversion]
mfix':687 [in MetaCoq.PCUIC.PCUICConversion]
mfix':694 [in MetaCoq.PCUIC.PCUICConversion]
mfix':7 [in MetaCoq.Erasure.EOptimizePropDiscr]
mfix':702 [in MetaCoq.PCUIC.PCUICConversion]
mfix':708 [in MetaCoq.PCUIC.PCUICConversion]
mfix':715 [in MetaCoq.PCUIC.PCUICConversion]
mfix':721 [in MetaCoq.PCUIC.PCUICConversion]
mfix':730 [in MetaCoq.PCUIC.PCUICConversion]
mfix':74 [in MetaCoq.Translations.param_cheap_packed]
mfix':76 [in MetaCoq.Translations.param_cheap_packed]
mfix':768 [in MetaCoq.PCUIC.PCUICConversion]
mfix':774 [in MetaCoq.PCUIC.PCUICConversion]
mfix':8 [in MetaCoq.PCUIC.PCUICExpandLets]
mfix':8 [in MetaCoq.Erasure.EOptimizePropDiscr]
mfix':86 [in MetaCoq.Template.AstUtils]
mfix':87 [in MetaCoq.Template.AstUtils]
mfix':9 [in MetaCoq.PCUIC.PCUICExpandLets]
mfix':9 [in MetaCoq.PCUIC.PCUICCSubst]
mfix':9 [in MetaCoq.Erasure.ELiftSubst]
mfix':9 [in MetaCoq.Template.WcbvEval]
mfix':9 [in MetaCoq.Erasure.ECSubst]
mfix':92 [in MetaCoq.SafeChecker.PCUICErrors]
mfix':94 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
mfix':98 [in MetaCoq.Erasure.ERemoveParams]
mfix':99 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
mfix':991 [in MetaCoq.PCUIC.PCUICReduction]
mfix0:101 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
mfix0:1055 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
mfix0:111 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
mfix0:1125 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
mfix0:1140 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
mfix0:1151 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
mfix0:121 [in MetaCoq.PCUIC.PCUICReduction]
mfix0:128 [in MetaCoq.PCUIC.PCUICReduction]
mfix0:135 [in MetaCoq.PCUIC.PCUICReduction]
mfix0:142 [in MetaCoq.PCUIC.PCUICReduction]
mfix0:202 [in MetaCoq.PCUIC.PCUICConfluence]
mfix0:204 [in MetaCoq.PCUIC.PCUICParallelReduction]
mfix0:215 [in MetaCoq.PCUIC.PCUICParallelReduction]
mfix0:216 [in MetaCoq.PCUIC.PCUICConfluence]
mfix0:224 [in MetaCoq.Template.Typing]
mfix0:228 [in MetaCoq.PCUIC.PCUICParallelReduction]
mfix0:229 [in MetaCoq.Template.Typing]
mfix0:234 [in MetaCoq.Template.Typing]
mfix0:239 [in MetaCoq.Template.Typing]
mfix0:260 [in MetaCoq.PCUIC.PCUICConfluence]
mfix0:274 [in MetaCoq.PCUIC.PCUICConfluence]
mfix0:276 [in MetaCoq.PCUIC.PCUICParallelReduction]
mfix0:280 [in MetaCoq.PCUIC.PCUICParallelReduction]
mfix0:294 [in MetaCoq.PCUIC.PCUICReduction]
mfix0:300 [in MetaCoq.PCUIC.PCUICReduction]
mfix0:306 [in MetaCoq.PCUIC.PCUICReduction]
mfix0:312 [in MetaCoq.PCUIC.PCUICReduction]
mfix0:382 [in MetaCoq.PCUIC.PCUICParallelReduction]
mfix0:395 [in MetaCoq.PCUIC.PCUICParallelReduction]
mfix0:401 [in MetaCoq.PCUIC.PCUICConfluence]
mfix0:410 [in MetaCoq.PCUIC.PCUICParallelReduction]
mfix0:417 [in MetaCoq.Template.Typing]
mfix0:422 [in MetaCoq.PCUIC.PCUICConfluence]
mfix0:423 [in MetaCoq.Template.Typing]
mfix0:429 [in MetaCoq.Template.Typing]
mfix0:435 [in MetaCoq.Template.Typing]
mfix0:473 [in MetaCoq.PCUIC.PCUICConfluence]
mfix0:474 [in MetaCoq.PCUIC.PCUICSR]
mfix0:475 [in MetaCoq.PCUIC.PCUICParallelReduction]
mfix0:480 [in MetaCoq.PCUIC.PCUICSR]
mfix0:481 [in MetaCoq.PCUIC.PCUICParallelReduction]
mfix0:486 [in MetaCoq.PCUIC.PCUICSR]
mfix0:492 [in MetaCoq.PCUIC.PCUICSR]
mfix0:494 [in MetaCoq.PCUIC.PCUICConfluence]
mfix0:79 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
mfix0:90 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
mfix1':101 [in MetaCoq.SafeChecker.PCUICErrors]
mfix1':121 [in MetaCoq.SafeChecker.PCUICErrors]
mfix1':1517 [in MetaCoq.SafeChecker.PCUICSafeConversion]
mfix1':1776 [in MetaCoq.SafeChecker.PCUICSafeConversion]
mfix1:1028 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
mfix1:1030 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
mfix1:105 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
mfix1:1056 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
mfix1:112 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
mfix1:1126 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
mfix1:1141 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
mfix1:1152 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
mfix1:117 [in MetaCoq.SafeChecker.PCUICErrors]
mfix1:122 [in MetaCoq.PCUIC.PCUICReduction]
mfix1:129 [in MetaCoq.PCUIC.PCUICReduction]
mfix1:136 [in MetaCoq.PCUIC.PCUICReduction]
mfix1:143 [in MetaCoq.PCUIC.PCUICReduction]
mfix1:1513 [in MetaCoq.SafeChecker.PCUICSafeConversion]
mfix1:16 [in MetaCoq.PCUIC.PCUICSR]
mfix1:170 [in MetaCoq.PCUIC.PCUICInductiveInversion]
mfix1:1766 [in MetaCoq.SafeChecker.PCUICSafeConversion]
mfix1:1772 [in MetaCoq.SafeChecker.PCUICSafeConversion]
mfix1:184 [in MetaCoq.PCUIC.PCUICInductiveInversion]
mfix1:203 [in MetaCoq.PCUIC.PCUICConfluence]
mfix1:205 [in MetaCoq.PCUIC.PCUICParallelReduction]
mfix1:216 [in MetaCoq.PCUIC.PCUICParallelReduction]
mfix1:217 [in MetaCoq.PCUIC.PCUICConfluence]
mfix1:225 [in MetaCoq.Template.Typing]
mfix1:229 [in MetaCoq.PCUIC.PCUICParallelReduction]
mfix1:23 [in MetaCoq.PCUIC.PCUICSR]
mfix1:230 [in MetaCoq.Template.Typing]
mfix1:235 [in MetaCoq.Template.Typing]
mfix1:240 [in MetaCoq.Template.Typing]
mfix1:261 [in MetaCoq.PCUIC.PCUICConfluence]
mfix1:275 [in MetaCoq.PCUIC.PCUICConfluence]
mfix1:276 [in MetaCoq.PCUIC.PCUICNormal]
mfix1:277 [in MetaCoq.PCUIC.PCUICParallelReduction]
mfix1:281 [in MetaCoq.PCUIC.PCUICParallelReduction]
mfix1:282 [in MetaCoq.PCUIC.PCUICNormal]
mfix1:295 [in MetaCoq.PCUIC.PCUICReduction]
mfix1:301 [in MetaCoq.PCUIC.PCUICReduction]
mfix1:307 [in MetaCoq.PCUIC.PCUICReduction]
mfix1:313 [in MetaCoq.PCUIC.PCUICReduction]
mfix1:32 [in MetaCoq.PCUIC.PCUICSR]
mfix1:383 [in MetaCoq.PCUIC.PCUICParallelReduction]
mfix1:396 [in MetaCoq.PCUIC.PCUICParallelReduction]
mfix1:402 [in MetaCoq.PCUIC.PCUICConfluence]
mfix1:409 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
mfix1:411 [in MetaCoq.PCUIC.PCUICParallelReduction]
mfix1:418 [in MetaCoq.Template.Typing]
mfix1:423 [in MetaCoq.PCUIC.PCUICConfluence]
mfix1:424 [in MetaCoq.Template.Typing]
mfix1:430 [in MetaCoq.Template.Typing]
mfix1:436 [in MetaCoq.Template.Typing]
mfix1:474 [in MetaCoq.PCUIC.PCUICConfluence]
mfix1:475 [in MetaCoq.PCUIC.PCUICSR]
mfix1:476 [in MetaCoq.PCUIC.PCUICParallelReduction]
mfix1:480 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
mfix1:481 [in MetaCoq.PCUIC.PCUICSR]
mfix1:482 [in MetaCoq.PCUIC.PCUICParallelReduction]
mfix1:487 [in MetaCoq.PCUIC.PCUICSR]
mfix1:493 [in MetaCoq.PCUIC.PCUICSR]
mfix1:495 [in MetaCoq.PCUIC.PCUICConfluence]
mfix1:502 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
mfix1:55 [in MetaCoq.Erasure.Prelim]
mfix1:6 [in MetaCoq.PCUIC.PCUICSR]
mfix1:66 [in MetaCoq.Erasure.Prelim]
mfix1:84 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
mfix1:91 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
mfix1:97 [in MetaCoq.SafeChecker.PCUICErrors]
mfix2':102 [in MetaCoq.SafeChecker.PCUICErrors]
mfix2':122 [in MetaCoq.SafeChecker.PCUICErrors]
mfix2':1518 [in MetaCoq.SafeChecker.PCUICSafeConversion]
mfix2':1777 [in MetaCoq.SafeChecker.PCUICSafeConversion]
mfix2:118 [in MetaCoq.SafeChecker.PCUICErrors]
mfix2:1514 [in MetaCoq.SafeChecker.PCUICSafeConversion]
mfix2:1767 [in MetaCoq.SafeChecker.PCUICSafeConversion]
mfix2:1773 [in MetaCoq.SafeChecker.PCUICSafeConversion]
mfix2:407 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
mfix2:478 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
mfix2:500 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
mfix2:98 [in MetaCoq.SafeChecker.PCUICErrors]
mfix:10 [in MetaCoq.Erasure.Erasure]
mfix:100 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
mfix:100 [in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
mfix:101 [in MetaCoq.PCUIC.PCUICWcbvEval]
mfix:1010 [in MetaCoq.PCUIC.PCUICReduction]
mfix:1014 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
mfix:1015 [in MetaCoq.PCUIC.PCUICReduction]
mfix:1017 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
mfix:102 [in MetaCoq.PCUIC.Syntax.PCUICViews]
mfix:102 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
mfix:102 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
mfix:1020 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
mfix:1021 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
mfix:1024 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
mfix:103 [in MetaCoq.Template.WcbvEval]
mfix:103 [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
mfix:1036 [in MetaCoq.PCUIC.PCUICReduction]
mfix:104 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
mfix:104 [in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
mfix:1045 [in MetaCoq.PCUIC.PCUICReduction]
mfix:105 [in MetaCoq.Template.Typing]
mfix:105 [in MetaCoq.PCUIC.PCUICNormal]
mfix:105 [in MetaCoq.SafeChecker.PCUICErrors]
mfix:106 [in MetaCoq.Erasure.EWcbvEvalInd]
mfix:1060 [in MetaCoq.PCUIC.PCUICReduction]
mfix:107 [in MetaCoq.PCUIC.PCUICInductiveInversion]
mfix:1081 [in MetaCoq.PCUIC.PCUICReduction]
mfix:1086 [in MetaCoq.PCUIC.PCUICReduction]
mfix:1087 [in MetaCoq.Template.Typing]
mfix:109 [in MetaCoq.PCUIC.PCUICWcbvEval]
mfix:109 [in MetaCoq.SafeChecker.PCUICErrors]
mfix:109 [in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
mfix:1095 [in MetaCoq.Template.Typing]
mfix:11 [in MetaCoq.PCUIC.Typing.PCUICNamelessTyp]
mfix:110 [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
mfix:1107 [in MetaCoq.PCUIC.PCUICReduction]
mfix:111 [in MetaCoq.Template.WcbvEval]
mfix:1116 [in MetaCoq.PCUIC.PCUICReduction]
mfix:1116 [in MetaCoq.SafeChecker.PCUICTypeChecker]
mfix:1119 [in MetaCoq.SafeChecker.PCUICTypeChecker]
mfix:112 [in MetaCoq.Template.Typing]
mfix:112 [in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
mfix:116 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
mfix:116 [in MetaCoq.PCUIC.PCUICEtaExpand]
mfix:117 [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
mfix:118 [in MetaCoq.PCUIC.PCUICCanonicity]
mfix:119 [in MetaCoq.Template.Typing]
mfix:119 [in MetaCoq.PCUIC.PCUICWcbvEval]
mfix:12 [in MetaCoq.PCUIC.PCUICGuardCondition]
mfix:120 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
mfix:121 [in MetaCoq.PCUIC.PCUICAst]
mfix:121 [in MetaCoq.Template.WcbvEval]
mfix:123 [in MetaCoq.PCUIC.PCUICAst]
mfix:125 [in MetaCoq.Erasure.EArities]
mfix:125 [in MetaCoq.SafeChecker.PCUICErrors]
mfix:126 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
mfix:127 [in MetaCoq.PCUIC.PCUICEtaExpand]
mfix:127 [in MetaCoq.SafeChecker.PCUICWfEnv]
mfix:127 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
mfix:128 [in MetaCoq.Erasure.EGlobalEnv]
mfix:129 [in MetaCoq.PCUIC.PCUICConvCumInversion]
mfix:129 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
mfix:130 [in MetaCoq.Template.EtaExpand]
mfix:130 [in MetaCoq.Template.TermEquality]
mfix:130 [in MetaCoq.PCUIC.PCUICCanonicity]
mfix:130 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
mfix:131 [in MetaCoq.Erasure.Extract]
mfix:134 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
mfix:134 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
mfix:135 [in MetaCoq.Template.TermEquality]
mfix:135 [in MetaCoq.Erasure.EGlobalEnv]
mfix:135 [in MetaCoq.Erasure.ERemoveParams]
mfix:136 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
mfix:136 [in MetaCoq.Erasure.ERemoveParams]
mfix:137 [in MetaCoq.Erasure.EGlobalEnv]
mfix:137 [in MetaCoq.Erasure.ERemoveParams]
mfix:138 [in MetaCoq.Template.EtaExpand]
mfix:139 [in MetaCoq.PCUIC.PCUICSubstitution]
mfix:139 [in MetaCoq.Erasure.EGlobalEnv]
mfix:14 [in MetaCoq.PCUIC.Typing.PCUICNamelessTyp]
mfix:140 [in MetaCoq.Erasure.Extract]
mfix:140 [in MetaCoq.Erasure.EEtaExpanded]
mfix:141 [in MetaCoq.PCUIC.PCUICConvCumInversion]
mfix:141 [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
mfix:1415 [in MetaCoq.SafeChecker.PCUICSafeReduce]
mfix:142 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
mfix:142 [in MetaCoq.Erasure.EEtaExpanded]
mfix:142 [in MetaCoq.Erasure.ERemoveParams]
mfix:143 [in MetaCoq.Erasure.EEtaExpanded]
mfix:145 [in MetaCoq.Erasure.EEtaExpandedFix]
mfix:145 [in MetaCoq.PCUIC.PCUICSubstitution]
mfix:145 [in MetaCoq.PCUIC.PCUICNormal]
mfix:146 [in MetaCoq.PCUIC.PCUICTyping]
mfix:147 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
mfix:147 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
mfix:148 [in MetaCoq.Erasure.EGlobalEnv]
mfix:148 [in MetaCoq.Erasure.EEtaExpanded]
mfix:149 [in MetaCoq.Erasure.EGlobalEnv]
mfix:15 [in MetaCoq.PCUIC.PCUICSR]
mfix:152 [in MetaCoq.PCUIC.PCUICWcbvEval]
mfix:152 [in MetaCoq.PCUIC.PCUICTyping]
mfix:153 [in MetaCoq.Erasure.EConstructorsAsBlocks]
mfix:153 [in MetaCoq.Erasure.EWcbvEval]
mfix:154 [in MetaCoq.PCUIC.PCUICWcbvEval]
mfix:154 [in MetaCoq.Erasure.EConstructorsAsBlocks]
mfix:154 [in MetaCoq.PCUIC.PCUICCanonicity]
mfix:155 [in MetaCoq.Erasure.EConstructorsAsBlocks]
mfix:155 [in MetaCoq.Erasure.EWcbvEval]
mfix:158 [in MetaCoq.PCUIC.PCUICNormal]
mfix:159 [in MetaCoq.PCUIC.PCUICInversion]
mfix:16 [in MetaCoq.Template.Typing]
mfix:16 [in MetaCoq.Template.WcbvEval]
mfix:160 [in MetaCoq.Erasure.EConstructorsAsBlocks]
mfix:167 [in MetaCoq.PCUIC.PCUICInversion]
mfix:168 [in MetaCoq.Erasure.EEtaExpandedFix]
mfix:168 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
mfix:169 [in MetaCoq.PCUIC.PCUICInductiveInversion]
mfix:169 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
mfix:171 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
mfix:172 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
mfix:174 [in MetaCoq.PCUIC.PCUICEquality]
mfix:174 [in MetaCoq.PCUIC.PCUICCanonicity]
mfix:179 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
mfix:179 [in MetaCoq.PCUIC.PCUICEquality]
mfix:18 [in MetaCoq.Template.WcbvEval]
mfix:181 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
mfix:182 [in MetaCoq.PCUIC.PCUICReduction]
mfix:183 [in MetaCoq.PCUIC.PCUICInductiveInversion]
mfix:185 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
mfix:187 [in MetaCoq.PCUIC.PCUICSubstitution]
mfix:187 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
mfix:188 [in MetaCoq.Template.WcbvEval]
mfix:19 [in MetaCoq.PCUIC.PCUICInductiveInversion]
mfix:19 [in MetaCoq.PCUIC.PCUICGuardCondition]
mfix:190 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
mfix:190 [in MetaCoq.PCUIC.PCUICReduction]
mfix:192 [in MetaCoq.PCUIC.PCUICProgress]
mfix:1941 [in MetaCoq.SafeChecker.PCUICSafeConversion]
mfix:195 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
mfix:197 [in MetaCoq.Template.WcbvEval]
mfix:198 [in MetaCoq.PCUIC.PCUICReduction]
mfix:200 [in MetaCoq.PCUIC.PCUICProgress]
mfix:203 [in MetaCoq.PCUIC.PCUICCanonicity]
mfix:204 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
mfix:204 [in MetaCoq.Erasure.EEtaExpanded]
mfix:205 [in MetaCoq.Template.WcbvEval]
mfix:207 [in MetaCoq.Template.Checker]
mfix:207 [in MetaCoq.Erasure.EEtaExpanded]
mfix:208 [in MetaCoq.Template.EtaExpand]
mfix:209 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
mfix:21 [in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
mfix:212 [in MetaCoq.Template.Ast]
mfix:2123 [in MetaCoq.SafeChecker.PCUICSafeConversion]
mfix:2137 [in MetaCoq.SafeChecker.PCUICSafeConversion]
mfix:214 [in MetaCoq.Template.Ast]
mfix:215 [in MetaCoq.Template.WcbvEval]
mfix:217 [in MetaCoq.Erasure.EWcbvEval]
mfix:218 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
mfix:22 [in MetaCoq.Template.Normal]
mfix:22 [in MetaCoq.PCUIC.PCUICSR]
mfix:22 [in MetaCoq.PCUIC.PCUICReduction]
mfix:220 [in MetaCoq.Erasure.EWcbvEval]
mfix:221 [in MetaCoq.Template.EtaExpand]
mfix:222 [in MetaCoq.Erasure.EWcbvEval]
mfix:223 [in MetaCoq.Erasure.ErasureFunction]
mfix:225 [in MetaCoq.Erasure.EWcbvEval]
mfix:227 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
mfix:227 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
mfix:227 [in MetaCoq.Erasure.EWcbvEval]
mfix:228 [in MetaCoq.Erasure.ErasureFunction]
mfix:228 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
mfix:229 [in MetaCoq.PCUIC.PCUICNormal]
mfix:23 [in MetaCoq.Template.Typing]
mfix:231 [in MetaCoq.PCUIC.PCUICWcbvEval]
mfix:231 [in MetaCoq.SafeChecker.PCUICSafeReduce]
mfix:232 [in MetaCoq.Erasure.EWcbvEval]
mfix:233 [in MetaCoq.PCUIC.Syntax.PCUICCases]
mfix:237 [in MetaCoq.PCUIC.PCUICWcbvEval]
mfix:238 [in MetaCoq.Erasure.EEtaExpanded]
mfix:24 [in MetaCoq.Template.Normal]
mfix:240 [in MetaCoq.PCUIC.Syntax.PCUICCases]
mfix:242 [in MetaCoq.PCUIC.Syntax.PCUICCases]
mfix:242 [in MetaCoq.Erasure.EEtaExpanded]
mfix:243 [in MetaCoq.PCUIC.PCUICWcbvEval]
mfix:243 [in MetaCoq.PCUIC.PCUICNormal]
mfix:243 [in MetaCoq.PCUIC.Syntax.PCUICCases]
mfix:243 [in MetaCoq.Erasure.EWcbvEval]
mfix:244 [in MetaCoq.PCUIC.Syntax.PCUICCases]
mfix:244 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
mfix:245 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
mfix:247 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
mfix:248 [in MetaCoq.Erasure.EWcbvEval]
mfix:25 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
mfix:25 [in MetaCoq.Erasure.ESpineView]
mfix:25 [in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
mfix:250 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
mfix:250 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
mfix:251 [in MetaCoq.Template.WcbvEval]
mfix:253 [in MetaCoq.Erasure.EWcbvEval]
mfix:254 [in MetaCoq.PCUIC.PCUICNormal]
mfix:255 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
mfix:255 [in MetaCoq.Template.WcbvEval]
mfix:257 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
mfix:258 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
mfix:26 [in MetaCoq.Template.TypingWf]
mfix:264 [in MetaCoq.PCUIC.PCUICNormal]
mfix:266 [in MetaCoq.PCUIC.PCUICWcbvEval]
mfix:266 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
mfix:267 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
mfix:27 [in MetaCoq.PCUIC.Syntax.PCUICViews]
mfix:27 [in MetaCoq.Template.Typing]
mfix:27 [in MetaCoq.PCUIC.PCUICWcbvEval]
mfix:27 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
mfix:27 [in MetaCoq.Erasure.ESpineView]
mfix:27 [in MetaCoq.Erasure.EWellformed]
mfix:27 [in MetaCoq.PCUIC.PCUICGuardCondition]
mfix:271 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
mfix:273 [in MetaCoq.Template.Typing]
mfix:273 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
mfix:274 [in MetaCoq.Erasure.EWcbvEval]
mfix:275 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
mfix:276 [in MetaCoq.PCUIC.PCUICWcbvEval]
mfix:276 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
mfix:279 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
mfix:28 [in MetaCoq.Template.Typing]
mfix:28 [in MetaCoq.PCUIC.PCUICTyping]
mfix:28 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
mfix:281 [in MetaCoq.Template.Typing]
mfix:282 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
mfix:286 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
mfix:287 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
mfix:289 [in MetaCoq.Template.Typing]
mfix:289 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
mfix:29 [in MetaCoq.PCUIC.PCUICWcbvEval]
mfix:29 [in MetaCoq.PCUIC.PCUICReduction]
mfix:290 [in MetaCoq.PCUIC.PCUICWcbvEval]
mfix:292 [in MetaCoq.Template.EtaExpand]
mfix:292 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
mfix:293 [in MetaCoq.PCUIC.PCUICWcbvEval]
mfix:298 [in MetaCoq.PCUIC.PCUICWcbvEval]
mfix:298 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
mfix:30 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
mfix:30 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
mfix:30 [in MetaCoq.PCUIC.PCUICInductiveInversion]
mfix:30 [in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
mfix:30 [in MetaCoq.Erasure.ESpineView]
mfix:30 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
mfix:301 [in MetaCoq.Template.EtaExpand]
mfix:301 [in MetaCoq.Template.WcbvEval]
mfix:302 [in MetaCoq.SafeChecker.PCUICSafeReduce]
mfix:303 [in MetaCoq.PCUIC.PCUICSubstitution]
mfix:305 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
mfix:308 [in MetaCoq.PCUIC.PCUICSubstitution]
mfix:31 [in MetaCoq.PCUIC.PCUICSR]
mfix:316 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
mfix:32 [in MetaCoq.Template.Typing]
mfix:32 [in MetaCoq.Erasure.ESpineView]
mfix:32 [in MetaCoq.PCUIC.PCUICGuardCondition]
mfix:323 [in MetaCoq.PCUIC.PCUICWcbvEval]
mfix:323 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
mfix:324 [in MetaCoq.PCUIC.PCUICNormal]
mfix:327 [in MetaCoq.PCUIC.PCUICWcbvEval]
mfix:33 [in MetaCoq.Erasure.EEtaExpandedFix]
mfix:33 [in MetaCoq.PCUIC.PCUICNormal]
mfix:33 [in MetaCoq.Template.TypingWf]
mfix:330 [in MetaCoq.PCUIC.PCUICWcbvEval]
mfix:330 [in MetaCoq.SafeChecker.PCUICSafeReduce]
mfix:330 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
mfix:330 [in MetaCoq.Erasure.EWcbvEval]
mfix:331 [in MetaCoq.Erasure.EWcbvEval]
mfix:332 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
mfix:332 [in MetaCoq.Erasure.EWcbvEval]
mfix:333 [in MetaCoq.PCUIC.PCUICWcbvEval]
mfix:335 [in MetaCoq.PCUIC.PCUICWcbvEval]
mfix:336 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
mfix:336 [in MetaCoq.Erasure.EWcbvEval]
mfix:337 [in MetaCoq.PCUIC.PCUICWcbvEval]
mfix:338 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
mfix:339 [in MetaCoq.Erasure.EArities]
mfix:34 [in MetaCoq.PCUIC.PCUICRedTypeIrrelevance]
mfix:34 [in MetaCoq.Erasure.EInlineProjections]
mfix:341 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
mfix:342 [in MetaCoq.PCUIC.PCUICProgress]
mfix:342 [in MetaCoq.Erasure.EEtaExpandedFix]
mfix:344 [in MetaCoq.Erasure.EArities]
mfix:35 [in MetaCoq.Erasure.EInlineProjections]
mfix:350 [in MetaCoq.PCUIC.PCUICProgress]
mfix:351 [in MetaCoq.Erasure.EEtaExpandedFix]
mfix:353 [in MetaCoq.PCUIC.PCUICWcbvEval]
mfix:357 [in MetaCoq.Erasure.EEtaExpandedFix]
mfix:358 [in MetaCoq.Erasure.EEtaExpandedFix]
mfix:36 [in MetaCoq.Erasure.EInlineProjections]
mfix:36 [in MetaCoq.PCUIC.PCUICNormal]
mfix:36 [in MetaCoq.PCUIC.PCUICTyping]
mfix:36 [in MetaCoq.PCUIC.PCUICReduction]
mfix:361 [in MetaCoq.SafeChecker.PCUICSafeConversion]
mfix:362 [in MetaCoq.PCUIC.PCUICSR]
mfix:363 [in MetaCoq.Erasure.EEtaExpandedFix]
mfix:364 [in MetaCoq.Erasure.EWcbvEval]
mfix:366 [in MetaCoq.PCUIC.PCUICProgress]
mfix:367 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
mfix:370 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
mfix:370 [in MetaCoq.PCUIC.PCUICSR]
mfix:371 [in MetaCoq.PCUIC.PCUICConfluence]
mfix:372 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mfix:372 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
mfix:373 [in MetaCoq.PCUIC.PCUICNormal]
mfix:375 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
mfix:376 [in MetaCoq.PCUIC.PCUICConfluence]
mfix:377 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mfix:378 [in MetaCoq.PCUIC.PCUICSR]
mfix:38 [in MetaCoq.PCUIC.Syntax.PCUICViews]
mfix:381 [in MetaCoq.PCUIC.PCUICConfluence]
mfix:381 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
mfix:383 [in MetaCoq.Erasure.EWcbvEval]
mfix:386 [in MetaCoq.PCUIC.PCUICConfluence]
mfix:389 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
mfix:39 [in MetaCoq.PCUIC.PCUICInductiveInversion]
mfix:39 [in MetaCoq.PCUIC.PCUICGuardCondition]
mfix:397 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
mfix:4 [in MetaCoq.SafeChecker.Extraction]
mfix:40 [in MetaCoq.Erasure.EEtaExpandedFix]
mfix:40 [in MetaCoq.Erasure.EInlineProjections]
mfix:407 [in MetaCoq.PCUIC.PCUICNormal]
mfix:407 [in MetaCoq.PCUIC.PCUICConfluence]
mfix:419 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
mfix:42 [in MetaCoq.Erasure.EWellformed]
mfix:426 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
mfix:427 [in MetaCoq.Template.EtaExpand]
mfix:428 [in MetaCoq.PCUIC.PCUICConfluence]
mfix:43 [in MetaCoq.Template.WfAst]
mfix:433 [in MetaCoq.Template.EtaExpand]
mfix:433 [in MetaCoq.PCUIC.PCUICConfluence]
mfix:438 [in MetaCoq.PCUIC.PCUICConfluence]
mfix:44 [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
mfix:44 [in MetaCoq.Erasure.EOptimizePropDiscr]
mfix:443 [in MetaCoq.PCUIC.PCUICConfluence]
mfix:445 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
mfix:448 [in MetaCoq.PCUIC.PCUICConfluence]
mfix:449 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
mfix:45 [in MetaCoq.PCUIC.PCUICEtaExpand]
mfix:45 [in MetaCoq.PCUIC.PCUICInductiveInversion]
mfix:45 [in MetaCoq.Erasure.EOptimizePropDiscr]
mfix:453 [in MetaCoq.PCUIC.PCUICConfluence]
mfix:454 [in MetaCoq.Erasure.EEtaExpandedFix]
mfix:458 [in MetaCoq.PCUIC.PCUICConfluence]
mfix:46 [in MetaCoq.Template.WfAst]
mfix:46 [in MetaCoq.Erasure.EOptimizePropDiscr]
mfix:463 [in MetaCoq.Erasure.EEtaExpandedFix]
mfix:469 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
mfix:472 [in MetaCoq.Erasure.EEtaExpandedFix]
mfix:473 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
mfix:477 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
mfix:479 [in MetaCoq.PCUIC.PCUICConfluence]
mfix:479 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
mfix:48 [in MetaCoq.PCUIC.PCUICAlpha]
mfix:485 [in MetaCoq.SafeChecker.PCUICSafeConversion]
mfix:489 [in MetaCoq.Erasure.EEtaExpandedFix]
mfix:49 [in MetaCoq.PCUIC.PCUICGuardCondition]
mfix:49 [in MetaCoq.Erasure.Prelim]
mfix:493 [in MetaCoq.Erasure.EEtaExpandedFix]
mfix:494 [in MetaCoq.SafeChecker.PCUICSafeConversion]
mfix:5 [in MetaCoq.PCUIC.PCUICSR]
mfix:5 [in MetaCoq.PCUIC.PCUICGuardCondition]
mfix:50 [in MetaCoq.Erasure.EOptimizePropDiscr]
mfix:500 [in MetaCoq.Erasure.EEtaExpandedFix]
mfix:500 [in MetaCoq.PCUIC.PCUICConfluence]
mfix:503 [in MetaCoq.SafeChecker.PCUICSafeConversion]
mfix:504 [in MetaCoq.Template.Typing]
mfix:505 [in MetaCoq.PCUIC.PCUICConfluence]
mfix:51 [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
mfix:51 [in MetaCoq.Erasure.Prelim]
mfix:510 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
mfix:510 [in MetaCoq.PCUIC.PCUICConfluence]
mfix:511 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
mfix:512 [in MetaCoq.Template.Typing]
mfix:512 [in MetaCoq.SafeChecker.PCUICSafeConversion]
mfix:513 [in MetaCoq.Erasure.EEtaExpandedFix]
mfix:513 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
mfix:514 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
mfix:52 [in MetaCoq.PCUIC.PCUICEtaExpand]
mfix:52 [in MetaCoq.PCUIC.PCUICAlpha]
mfix:520 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
mfix:520 [in MetaCoq.Template.Typing]
mfix:521 [in MetaCoq.SafeChecker.PCUICSafeConversion]
mfix:522 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
mfix:523 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
mfix:526 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
mfix:528 [in MetaCoq.SafeChecker.PCUICSafeConversion]
mfix:529 [in MetaCoq.Template.Typing]
mfix:53 [in MetaCoq.PCUIC.PCUICCanonicity]
mfix:532 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
mfix:535 [in MetaCoq.Template.Typing]
mfix:536 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
mfix:540 [in MetaCoq.Template.Typing]
mfix:548 [in MetaCoq.Template.Typing]
mfix:556 [in MetaCoq.Template.Typing]
mfix:565 [in MetaCoq.Template.Typing]
mfix:569 [in MetaCoq.SafeChecker.PCUICSafeConversion]
mfix:57 [in MetaCoq.PCUIC.PCUICCanonicity]
mfix:571 [in MetaCoq.Template.Typing]
mfix:573 [in MetaCoq.SafeChecker.PCUICSafeConversion]
mfix:58 [in MetaCoq.Erasure.Extract]
mfix:58 [in MetaCoq.PCUIC.PCUICNormal]
mfix:58 [in MetaCoq.PCUIC.PCUICGuardCondition]
mfix:580 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mfix:584 [in MetaCoq.PCUIC.PCUICTyping]
mfix:585 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mfix:589 [in MetaCoq.Template.Typing]
mfix:59 [in MetaCoq.PCUIC.Syntax.PCUICViews]
mfix:592 [in MetaCoq.PCUIC.PCUICTyping]
mfix:596 [in MetaCoq.Template.Typing]
mfix:6 [in MetaCoq.PCUIC.Syntax.PCUICViews]
mfix:60 [in MetaCoq.Erasure.EWcbvEval]
mfix:60 [in MetaCoq.Erasure.Prelim]
mfix:606 [in MetaCoq.PCUIC.PCUICParallelReduction]
mfix:609 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mfix:609 [in MetaCoq.PCUIC.PCUICParallelReduction]
mfix:61 [in MetaCoq.Template.Normal]
mfix:61 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
mfix:62 [in MetaCoq.Erasure.Prelim]
mfix:622 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mfix:629 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mfix:63 [in MetaCoq.Erasure.Extract]
mfix:63 [in MetaCoq.Template.Normal]
mfix:633 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mfix:634 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
mfix:636 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
mfix:640 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
mfix:643 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
mfix:648 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mfix:649 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
mfix:652 [in MetaCoq.PCUIC.PCUICConfluence]
mfix:654 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mfix:655 [in MetaCoq.PCUIC.PCUICConfluence]
mfix:66 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
mfix:66 [in MetaCoq.Erasure.EWcbvEvalInd]
mfix:672 [in MetaCoq.Template.Typing]
mfix:672 [in MetaCoq.PCUIC.PCUICConversion]
mfix:672 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
mfix:675 [in MetaCoq.PCUIC.PCUICConversion]
mfix:677 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
mfix:678 [in MetaCoq.Template.Typing]
mfix:682 [in MetaCoq.PCUIC.PCUICConversion]
mfix:683 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
mfix:686 [in MetaCoq.PCUIC.PCUICConversion]
mfix:687 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
mfix:69 [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
mfix:69 [in MetaCoq.Erasure.EWcbvEval]
mfix:690 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
mfix:693 [in MetaCoq.PCUIC.PCUICConversion]
mfix:696 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
mfix:700 [in MetaCoq.PCUIC.PCUICConversion]
mfix:704 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
mfix:707 [in MetaCoq.PCUIC.PCUICConversion]
mfix:714 [in MetaCoq.PCUIC.PCUICConversion]
mfix:72 [in MetaCoq.Erasure.Prelim]
mfix:720 [in MetaCoq.PCUIC.PCUICConversion]
mfix:729 [in MetaCoq.PCUIC.PCUICConversion]
mfix:74 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
mfix:76 [in MetaCoq.Erasure.EWcbvEvalInd]
mfix:76 [in MetaCoq.Erasure.ErasureProperties]
mfix:767 [in MetaCoq.PCUIC.PCUICConversion]
mfix:77 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
mfix:773 [in MetaCoq.PCUIC.PCUICConversion]
mfix:78 [in MetaCoq.Erasure.EWcbvEval]
mfix:789 [in MetaCoq.SafeChecker.PCUICTypeChecker]
mfix:801 [in MetaCoq.SafeChecker.PCUICTypeChecker]
mfix:804 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
mfix:83 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
mfix:83 [in MetaCoq.Erasure.EEtaExpandedFix]
mfix:83 [in MetaCoq.PCUIC.Syntax.PCUICViews]
mfix:835 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
mfix:838 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
mfix:84 [in MetaCoq.Erasure.EWellformed]
mfix:840 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
mfix:840 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
mfix:841 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
mfix:844 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
mfix:849 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
mfix:85 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
mfix:85 [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
mfix:851 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
mfix:86 [in MetaCoq.Erasure.EWcbvEvalInd]
mfix:86 [in MetaCoq.Erasure.EWellformed]
mfix:862 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
mfix:866 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
mfix:87 [in MetaCoq.PCUIC.PCUICNormal]
mfix:87 [in MetaCoq.Erasure.EWcbvEval]
mfix:88 [in MetaCoq.Erasure.EWellformed]
mfix:88 [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
mfix:89 [in MetaCoq.SafeChecker.PCUICErrors]
mfix:907 [in MetaCoq.PCUIC.PCUICTyping]
mfix:91 [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
mfix:915 [in MetaCoq.PCUIC.PCUICTyping]
mfix:92 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
mfix:92 [in MetaCoq.Erasure.EWellformed]
mfix:93 [in MetaCoq.PCUIC.PCUICWcbvEval]
mfix:93 [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
mfix:93 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
mfix:94 [in MetaCoq.Erasure.EEtaExpandedFix]
mfix:94 [in MetaCoq.Template.WcbvEval]
mfix:95 [in MetaCoq.PCUIC.Typing.PCUICWeakeningTyp]
mfix:96 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
mfix:96 [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
mfix:96 [in MetaCoq.Erasure.EWcbvEval]
mfix:97 [in MetaCoq.Erasure.EWcbvEvalInd]
mfix:98 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
mfix:98 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
mfix:989 [in MetaCoq.PCUIC.PCUICReduction]
mib':1439 [in MetaCoq.Erasure.ErasureFunction]
mib':165 [in MetaCoq.Erasure.Extract]
mib':178 [in MetaCoq.Erasure.Extract]
mib':204 [in MetaCoq.PCUIC.PCUICInductiveInversion]
mib':21 [in MetaCoq.Erasure.ErasureCorrectness]
mib':792 [in MetaCoq.Erasure.ErasureFunction]
mib':831 [in MetaCoq.Erasure.ErasureFunction]
mib:100 [in MetaCoq.PCUIC.utils.PCUICPretty]
mib:104 [in MetaCoq.Template.Pretty]
mib:108 [in MetaCoq.Template.Pretty]
mib:122 [in MetaCoq.Template.Pretty]
mib:131 [in MetaCoq.Template.AstUtils]
mib:164 [in MetaCoq.Erasure.Extract]
mib:177 [in MetaCoq.Erasure.Extract]
mib:20 [in MetaCoq.Erasure.ErasureCorrectness]
mib:202 [in MetaCoq.PCUIC.PCUICInductiveInversion]
mib:246 [in MetaCoq.Erasure.Extract]
mib:354 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
mib:676 [in MetaCoq.Erasure.ErasureFunction]
mib:817 [in MetaCoq.SafeChecker.PCUICSafeConversion]
mib:830 [in MetaCoq.Erasure.ErasureFunction]
mib:96 [in MetaCoq.PCUIC.utils.PCUICPretty]
mie:111 [in MetaCoq.Template.Pretty]
mie:115 [in MetaCoq.Template.Pretty]
mie:125 [in MetaCoq.Template.Pretty]
mie:130 [in MetaCoq.Template.Pretty]
mind':152 [in MetaCoq.Erasure.EDeps]
mind:10 [in MetaCoq.Template.Typing]
mind:101 [in MetaCoq.Erasure.EEtaExpandedFix]
mind:1029 [in MetaCoq.Erasure.ErasureFunction]
mind:109 [in MetaCoq.PCUIC.PCUICFirstorder]
mind:11 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mind:11 [in MetaCoq.PCUIC.PCUICFirstorder]
mind:11 [in MetaCoq.PCUIC.PCUICProgram]
mind:118 [in MetaCoq.Template.AstUtils]
mind:120 [in MetaCoq.Template.EtaExpand]
mind:126 [in MetaCoq.PCUIC.PCUICWfUniverses]
mind:1335 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
mind:135 [in MetaCoq.PCUIC.PCUICEtaExpand]
mind:1362 [in MetaCoq.Erasure.ErasureFunction]
mind:1380 [in MetaCoq.Erasure.ErasureFunction]
mind:14 [in MetaCoq.Erasure.EArities]
mind:14 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
mind:1402 [in MetaCoq.Erasure.ErasureFunction]
mind:144 [in MetaCoq.Template.EtaExpand]
mind:149 [in MetaCoq.Erasure.EDeps]
mind:159 [in MetaCoq.PCUIC.PCUICFirstorder]
mind:16 [in MetaCoq.PCUIC.PCUICInductives]
mind:160 [in MetaCoq.PCUIC.PCUICCanonicity]
mind:164 [in MetaCoq.Template.TypingWf]
mind:179 [in MetaCoq.PCUIC.PCUICElimination]
mind:18 [in MetaCoq.Examples.add_constructor]
mind:187 [in MetaCoq.PCUIC.PCUICFirstorder]
mind:189 [in MetaCoq.PCUIC.PCUICElimination]
mind:19 [in MetaCoq.PCUIC.PCUICFirstorder]
mind:194 [in MetaCoq.Template.EtaExpand]
mind:20 [in MetaCoq.Template.TermEquality]
mind:203 [in MetaCoq.PCUIC.PCUICSubstitution]
mind:204 [in MetaCoq.PCUIC.PCUICElimination]
mind:208 [in MetaCoq.PCUIC.PCUICSubstitution]
mind:21 [in MetaCoq.PCUIC.PCUICFirstorder]
mind:211 [in MetaCoq.PCUIC.PCUICElimination]
mind:212 [in MetaCoq.Erasure.EEtaExpanded]
mind:213 [in MetaCoq.PCUIC.PCUICSubstitution]
mind:222 [in MetaCoq.PCUIC.PCUICSubstitution]
mind:229 [in MetaCoq.Template.EtaExpand]
mind:23 [in MetaCoq.Template.TemplateMonad.Core]
mind:248 [in MetaCoq.Erasure.EEtaExpanded]
mind:25 [in MetaCoq.Template.EnvironmentTyping]
mind:27 [in MetaCoq.Template.TemplateMonad.Extractable]
mind:270 [in MetaCoq.Erasure.EEtaExpanded]
mind:277 [in MetaCoq.Erasure.EEtaExpanded]
mind:283 [in MetaCoq.Template.EtaExpand]
mind:293 [in MetaCoq.Template.TypingWf]
mind:379 [in MetaCoq.Erasure.EEtaExpandedFix]
mind:386 [in MetaCoq.Erasure.EEtaExpandedFix]
mind:389 [in MetaCoq.Erasure.ERemoveParams]
mind:44 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
mind:45 [in MetaCoq.Erasure.EEtaExpandedFix]
mind:46 [in MetaCoq.PCUIC.PCUICInductiveInversion]
mind:477 [in MetaCoq.PCUIC.PCUICProgress]
mind:485 [in MetaCoq.PCUIC.PCUICProgress]
mind:5 [in MetaCoq.Template.EnvironmentTyping]
mind:50 [in MetaCoq.Translations.param_original]
mind:54 [in MetaCoq.Translations.param_binary]
mind:55 [in MetaCoq.PCUIC.PCUICFirstorder]
mind:56 [in MetaCoq.PCUIC.PCUICCanonicity]
mind:562 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
mind:565 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
mind:579 [in MetaCoq.Template.EnvironmentTyping]
mind:58 [in MetaCoq.PCUIC.PCUICEtaExpand]
mind:591 [in MetaCoq.Template.EnvironmentTyping]
mind:598 [in MetaCoq.Template.EnvironmentTyping]
mind:60 [in MetaCoq.PCUIC.PCUICCanonicity]
mind:625 [in MetaCoq.Template.EnvironmentTyping]
mind:647 [in MetaCoq.Template.EnvironmentTyping]
mind:65 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
mind:70 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
mind:72 [in MetaCoq.PCUIC.PCUICFirstorder]
mind:8 [in MetaCoq.PCUIC.PCUICTyping]
mind:80 [in MetaCoq.Translations.param_cheap_packed]
mind:82 [in MetaCoq.Translations.param_binary]
mind:822 [in MetaCoq.SafeChecker.PCUICSafeChecker]
mind:828 [in MetaCoq.SafeChecker.PCUICSafeChecker]
mind:84 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
mind:85 [in MetaCoq.Translations.param_original]
mind:881 [in MetaCoq.SafeChecker.PCUICSafeChecker]
mind:9 [in MetaCoq.PCUIC.PCUICInductives]
mind:9 [in MetaCoq.Erasure.EGlobalEnv]
mind:900 [in MetaCoq.SafeChecker.PCUICSafeChecker]
mind:91 [in MetaCoq.Translations.times_bool_fun]
mind:968 [in MetaCoq.SafeChecker.PCUICSafeChecker]
mm:109 [in MetaCoq.Template.utils.MCRelations]
mm:111 [in MetaCoq.Template.utils.MCRelations]
motivepars:380 [in MetaCoq.PCUIC.PCUICNormal]
motiveret:381 [in MetaCoq.PCUIC.PCUICNormal]
motive:379 [in MetaCoq.PCUIC.PCUICNormal]
motive:484 [in MetaCoq.PCUIC.PCUICNormal]
motive:491 [in MetaCoq.PCUIC.PCUICNormal]
motive:813 [in MetaCoq.SafeChecker.PCUICSafeConversion]
Mphi:512 [in MetaCoq.Examples.tauto]
Mphi:523 [in MetaCoq.Examples.tauto]
mp':21 [in MetaCoq.Template.Kernames]
mp:10 [in MetaCoq.Template.Kernames]
mp:105 [in MetaCoq.Translations.translation_utils]
mp:153 [in MetaCoq.Translations.translation_utils]
mp:20 [in MetaCoq.Template.Kernames]
mp:48 [in MetaCoq.Translations.param_original]
mp:52 [in MetaCoq.Translations.param_binary]
mp:56 [in MetaCoq.Translations.translation_utils]
mp:65 [in MetaCoq.Translations.translation_utils]
mp:78 [in MetaCoq.Translations.param_cheap_packed]
mp:8 [in MetaCoq.Template.Kernames]
mp:80 [in MetaCoq.Translations.param_binary]
mp:83 [in MetaCoq.Translations.param_original]
mp:89 [in MetaCoq.Translations.times_bool_fun]
msg:1 [in MetaCoq.Translations.param_binary]
msg:1 [in MetaCoq.Translations.standard_model]
msg:1 [in MetaCoq.Translations.param_original]
msg:20 [in MetaCoq.Template.TemplateMonad.Core]
msg:22 [in MetaCoq.Template.TemplateMonad.Core]
M':103 [in MetaCoq.Template.monad_utils]
M':1032 [in MetaCoq.PCUIC.PCUICParallelReduction]
M':1045 [in MetaCoq.PCUIC.PCUICParallelReduction]
m':1219 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
m':1231 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
m':1247 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
m':1257 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
m':1264 [in MetaCoq.Erasure.ErasureFunction]
m':1275 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
M':129 [in MetaCoq.Template.monad_utils]
m':1298 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
M':135 [in MetaCoq.Template.Typing]
M':137 [in MetaCoq.Template.monad_utils]
M':139 [in MetaCoq.Template.Typing]
M':144 [in MetaCoq.Template.monad_utils]
M':202 [in MetaCoq.PCUIC.PCUICNormal]
M':207 [in MetaCoq.PCUIC.PCUICNormal]
M':216 [in MetaCoq.PCUIC.PCUICReduction]
M':221 [in MetaCoq.PCUIC.PCUICReduction]
m':24 [in MetaCoq.Erasure.Extract]
M':250 [in MetaCoq.PCUIC.PCUICParallelReduction]
M':307 [in MetaCoq.Template.Typing]
M':312 [in MetaCoq.Template.Typing]
m':333 [in MetaCoq.Template.EtaExpand]
M':375 [in MetaCoq.PCUIC.PCUICSubstitution]
M':396 [in MetaCoq.PCUIC.PCUICSR]
M':401 [in MetaCoq.PCUIC.PCUICSR]
M':439 [in MetaCoq.PCUIC.PCUICParallelReduction]
M':52 [in MetaCoq.PCUIC.PCUICReduction]
M':56 [in MetaCoq.PCUIC.PCUICReduction]
m':584 [in MetaCoq.PCUIC.PCUICConfluence]
m':596 [in MetaCoq.PCUIC.PCUICConfluence]
m':608 [in MetaCoq.PCUIC.PCUICConfluence]
M':7 [in MetaCoq.PCUIC.PCUICContextReduction]
M':702 [in MetaCoq.PCUIC.PCUICReduction]
m':79 [in MetaCoq.Erasure.Extract]
M':839 [in MetaCoq.PCUIC.PCUICReduction]
M0:253 [in MetaCoq.PCUIC.PCUICParallelReduction]
M0:285 [in MetaCoq.PCUIC.PCUICParallelReduction]
M0:30 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
M0:444 [in MetaCoq.PCUIC.PCUICParallelReduction]
M0:488 [in MetaCoq.PCUIC.PCUICParallelReduction]
M0:845 [in MetaCoq.PCUIC.PCUICReduction]
M0:865 [in MetaCoq.PCUIC.PCUICReduction]
M1:102 [in MetaCoq.PCUIC.PCUICReduction]
M1:103 [in MetaCoq.PCUIC.PCUICConversion]
M1:107 [in MetaCoq.PCUIC.PCUICReduction]
M1:109 [in MetaCoq.PCUIC.PCUICReduction]
M1:115 [in MetaCoq.PCUIC.PCUICReduction]
M1:13 [in MetaCoq.Template.Reduction]
M1:18 [in MetaCoq.Template.Reduction]
M1:196 [in MetaCoq.Template.Typing]
M1:201 [in MetaCoq.Template.Typing]
M1:203 [in MetaCoq.Template.Typing]
M1:209 [in MetaCoq.Template.Typing]
M1:213 [in MetaCoq.Template.Typing]
M1:220 [in MetaCoq.Template.Typing]
M1:221 [in MetaCoq.Template.Typing]
M1:23 [in MetaCoq.Template.Reduction]
M1:254 [in MetaCoq.PCUIC.PCUICParallelReduction]
M1:272 [in MetaCoq.PCUIC.PCUICReduction]
M1:278 [in MetaCoq.PCUIC.PCUICReduction]
M1:281 [in MetaCoq.PCUIC.PCUICReduction]
M1:286 [in MetaCoq.PCUIC.PCUICParallelReduction]
M1:288 [in MetaCoq.PCUIC.PCUICReduction]
M1:3 [in MetaCoq.Template.Reduction]
M1:31 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
M1:377 [in MetaCoq.Template.Typing]
M1:383 [in MetaCoq.Template.Typing]
M1:388 [in MetaCoq.Template.Typing]
M1:395 [in MetaCoq.Template.Typing]
M1:403 [in MetaCoq.Template.Typing]
M1:411 [in MetaCoq.Template.Typing]
M1:413 [in MetaCoq.Template.Typing]
M1:445 [in MetaCoq.PCUIC.PCUICParallelReduction]
M1:452 [in MetaCoq.PCUIC.PCUICSR]
M1:458 [in MetaCoq.PCUIC.PCUICSR]
M1:461 [in MetaCoq.PCUIC.PCUICSR]
M1:468 [in MetaCoq.PCUIC.PCUICSR]
M1:489 [in MetaCoq.PCUIC.PCUICParallelReduction]
M1:73 [in MetaCoq.PCUIC.PCUICConversion]
M1:77 [in MetaCoq.PCUIC.PCUICConversion]
M1:8 [in MetaCoq.Template.Reduction]
M1:81 [in MetaCoq.PCUIC.PCUICConversion]
M1:846 [in MetaCoq.PCUIC.PCUICReduction]
M1:859 [in MetaCoq.PCUIC.PCUICReduction]
M1:866 [in MetaCoq.PCUIC.PCUICReduction]
M1:96 [in MetaCoq.PCUIC.PCUICConversion]
M2:10 [in MetaCoq.Template.Reduction]
M2:104 [in MetaCoq.PCUIC.PCUICConversion]
M2:104 [in MetaCoq.PCUIC.PCUICReduction]
M2:105 [in MetaCoq.PCUIC.PCUICReduction]
M2:110 [in MetaCoq.PCUIC.PCUICReduction]
M2:113 [in MetaCoq.PCUIC.PCUICReduction]
M2:15 [in MetaCoq.Template.Reduction]
M2:198 [in MetaCoq.Template.Typing]
M2:199 [in MetaCoq.Template.Typing]
M2:20 [in MetaCoq.Template.Reduction]
M2:204 [in MetaCoq.Template.Typing]
M2:207 [in MetaCoq.Template.Typing]
M2:215 [in MetaCoq.Template.Typing]
M2:217 [in MetaCoq.Template.Typing]
M2:223 [in MetaCoq.Template.Typing]
M2:24 [in MetaCoq.Template.Reduction]
M2:274 [in MetaCoq.PCUIC.PCUICReduction]
M2:276 [in MetaCoq.PCUIC.PCUICReduction]
M2:282 [in MetaCoq.PCUIC.PCUICReduction]
M2:286 [in MetaCoq.PCUIC.PCUICReduction]
M2:379 [in MetaCoq.Template.Typing]
M2:381 [in MetaCoq.Template.Typing]
M2:389 [in MetaCoq.Template.Typing]
M2:393 [in MetaCoq.Template.Typing]
M2:405 [in MetaCoq.Template.Typing]
M2:408 [in MetaCoq.Template.Typing]
M2:415 [in MetaCoq.Template.Typing]
M2:454 [in MetaCoq.PCUIC.PCUICSR]
M2:456 [in MetaCoq.PCUIC.PCUICSR]
M2:462 [in MetaCoq.PCUIC.PCUICSR]
M2:466 [in MetaCoq.PCUIC.PCUICSR]
M2:5 [in MetaCoq.Template.Reduction]
M2:74 [in MetaCoq.PCUIC.PCUICConversion]
M2:78 [in MetaCoq.PCUIC.PCUICConversion]
M2:82 [in MetaCoq.PCUIC.PCUICConversion]
M2:860 [in MetaCoq.PCUIC.PCUICReduction]
M2:97 [in MetaCoq.PCUIC.PCUICConversion]
M3:83 [in MetaCoq.PCUIC.PCUICConversion]
m:1 [in MetaCoq.Template.monad_utils]
m:10 [in MetaCoq.Template.utils.wGraph]
m:10 [in MetaCoq.PCUIC.Syntax.PCUICInstDef]
m:10 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
M:100 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
m:1004 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
m:1006 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
M:101 [in MetaCoq.Erasure.ELiftSubst]
m:1011 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
M:1015 [in MetaCoq.PCUIC.PCUICConversion]
M:102 [in MetaCoq.Template.utils.MCRelations]
M:102 [in MetaCoq.Template.monad_utils]
M:1020 [in MetaCoq.PCUIC.PCUICConversion]
M:1026 [in MetaCoq.PCUIC.PCUICParallelReduction]
m:103 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
M:1031 [in MetaCoq.PCUIC.PCUICParallelReduction]
m:104 [in MetaCoq.Template.utils.MCRelations]
M:104 [in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
m:104 [in MetaCoq.Template.Environment]
M:104 [in MetaCoq.Template.LiftSubst]
M:1044 [in MetaCoq.PCUIC.PCUICParallelReduction]
m:105 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
m:107 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
m:108 [in MetaCoq.Template.WfAst]
M:108 [in MetaCoq.Erasure.ELiftSubst]
m:108 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
m:11 [in MetaCoq.PCUIC.PCUICAlpha]
M:11 [in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
m:110 [in MetaCoq.Template.WfAst]
m:1121 [in MetaCoq.PCUIC.PCUICConfluence]
m:1126 [in MetaCoq.PCUIC.PCUICConfluence]
M:113 [in MetaCoq.Erasure.ELiftSubst]
M:114 [in MetaCoq.Template.LiftSubst]
m:1150 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
m:1153 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
M:116 [in MetaCoq.Erasure.ELiftSubst]
m:1163 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
m:1166 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
M:117 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
m:1170 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
M:119 [in MetaCoq.Template.monad_utils]
m:12 [in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
m:12 [in MetaCoq.PCUIC.PCUICEtaExpand]
m:12 [in MetaCoq.Template.Checker]
M:121 [in MetaCoq.Erasure.ELiftSubst]
m:1218 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
m:1230 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
m:1246 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
m:125 [in MetaCoq.Erasure.EInduction]
M:125 [in MetaCoq.Erasure.ELiftSubst]
M:1255 [in MetaCoq.PCUIC.PCUICConversion]
m:1256 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
M:1258 [in MetaCoq.PCUIC.PCUICConversion]
m:1261 [in MetaCoq.Erasure.ErasureFunction]
M:1261 [in MetaCoq.PCUIC.PCUICConversion]
M:1264 [in MetaCoq.PCUIC.PCUICConversion]
m:1274 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
M:128 [in MetaCoq.Template.monad_utils]
m:129 [in MetaCoq.Erasure.EInduction]
m:1297 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
m:13 [in MetaCoq.Erasure.EEtaExpandedFix]
m:13 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
M:132 [in MetaCoq.Template.LiftSubst]
M:134 [in MetaCoq.Template.Typing]
M:136 [in MetaCoq.Template.monad_utils]
M:137 [in MetaCoq.Erasure.ELiftSubst]
m:137 [in MetaCoq.Template.Environment]
M:138 [in MetaCoq.Template.Typing]
m:14 [in MetaCoq.Template.utils.wGraph]
M:143 [in MetaCoq.Template.monad_utils]
M:144 [in MetaCoq.Erasure.ELiftSubst]
M:145 [in MetaCoq.PCUIC.utils.PCUICUtils]
m:145 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
m:146 [in MetaCoq.Template.monad_utils]
m:147 [in MetaCoq.PCUIC.utils.PCUICUtils]
M:149 [in MetaCoq.Template.monad_utils]
M:15 [in MetaCoq.PCUIC.PCUICConversion]
m:150 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
m:155 [in MetaCoq.Template.EtaExpand]
m:156 [in MetaCoq.PCUIC.PCUICFirstorder]
m:16 [in MetaCoq.Template.utils.MCArith]
M:160 [in MetaCoq.Erasure.ELiftSubst]
M:162 [in MetaCoq.Template.monad_utils]
m:169 [in MetaCoq.Template.AstUtils]
m:17 [in MetaCoq.Template.utils.wGraph]
M:171 [in MetaCoq.PCUIC.PCUICConversion]
M:176 [in MetaCoq.PCUIC.PCUICConversion]
M:177 [in MetaCoq.Template.monad_utils]
m:178 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
m:18 [in MetaCoq.Template.utils.MCArith]
M:18 [in MetaCoq.SafeChecker.PCUICSafeChecker]
M:18 [in MetaCoq.Template.LiftSubst]
m:180 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
m:182 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
m:184 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
m:185 [in MetaCoq.PCUIC.PCUICSubstitution]
M:187 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
m:19 [in MetaCoq.Template.utils.MCArith]
m:190 [in MetaCoq.Erasure.Extract]
m:190 [in MetaCoq.SafeChecker.PCUICErrors]
M:198 [in MetaCoq.Template.monad_utils]
m:2 [in MetaCoq.Template.utils.wGraph]
M:20 [in MetaCoq.Template.LiftSubst]
m:2035 [in MetaCoq.Template.utils.All_Forall]
m:204 [in MetaCoq.Erasure.EConstructorsAsBlocks]
m:204 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
m:209 [in MetaCoq.Erasure.EConstructorsAsBlocks]
m:209 [in MetaCoq.PCUIC.PCUICInductiveInversion]
m:209 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
m:21 [in MetaCoq.Translations.translation_utils]
m:21 [in MetaCoq.Template.utils.wGraph]
M:21 [in MetaCoq.Template.LiftSubst]
M:215 [in MetaCoq.PCUIC.PCUICReduction]
M:22 [in MetaCoq.PCUIC.PCUICSpine]
M:220 [in MetaCoq.PCUIC.PCUICReduction]
m:221 [in MetaCoq.Erasure.EInduction]
M:223 [in MetaCoq.PCUIC.PCUICCumulProp]
m:224 [in MetaCoq.Erasure.EInduction]
m:229 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
m:23 [in MetaCoq.Erasure.EInduction]
m:23 [in MetaCoq.Erasure.Extract]
M:23 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
M:231 [in MetaCoq.PCUIC.PCUICCumulProp]
m:231 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
M:232 [in MetaCoq.Template.TypingWf]
m:236 [in MetaCoq.SafeChecker.PCUICErrors]
m:237 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
m:239 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
M:240 [in MetaCoq.PCUIC.PCUICCumulProp]
m:241 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
m:242 [in MetaCoq.SafeChecker.PCUICErrors]
m:243 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
M:2432 [in MetaCoq.Translations.MiniHoTT]
M:2440 [in MetaCoq.Translations.MiniHoTT_paths]
M:249 [in MetaCoq.PCUIC.PCUICParallelReduction]
m:25 [in MetaCoq.Template.utils.wGraph]
m:25 [in MetaCoq.Template.monad_utils]
m:252 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
m:253 [in MetaCoq.Template.Environment]
m:254 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
m:256 [in MetaCoq.PCUIC.PCUICInductives]
m:256 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
m:258 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
m:26 [in MetaCoq.Erasure.EInduction]
M:26 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
M:26 [in MetaCoq.Template.LiftSubst]
m:261 [in MetaCoq.SafeChecker.PCUICErrors]
M:262 [in MetaCoq.PCUIC.PCUICCumulProp]
m:263 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
m:266 [in MetaCoq.Template.Environment]
M:267 [in MetaCoq.PCUIC.PCUICCumulProp]
m:269 [in MetaCoq.SafeChecker.PCUICErrors]
M:269 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
m:27 [in MetaCoq.Translations.translation_utils]
m:27 [in MetaCoq.Template.utils.bytestring]
m:27 [in MetaCoq.Template.Checker]
M:27 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
m:274 [in MetaCoq.Erasure.EEtaExpandedFix]
M:276 [in MetaCoq.PCUIC.PCUICCumulProp]
m:28 [in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
m:282 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
M:283 [in MetaCoq.PCUIC.PCUICCumulProp]
m:284 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
m:29 [in MetaCoq.Template.Typing]
m:29 [in MetaCoq.Template.utils.wGraph]
m:294 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
m:297 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
m:299 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
m:30 [in MetaCoq.Template.monad_utils]
m:301 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
m:303 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
m:303 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
m:305 [in MetaCoq.Erasure.EEtaExpandedFix]
m:306 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
M:306 [in MetaCoq.Template.Typing]
M:310 [in MetaCoq.SafeChecker.PCUICSafeChecker]
M:311 [in MetaCoq.Template.Typing]
m:314 [in MetaCoq.Erasure.EEtaExpandedFix]
m:32 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
M:32 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
m:32 [in MetaCoq.PCUIC.Syntax.PCUICNamelessDef]
M:321 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
M:325 [in MetaCoq.PCUIC.PCUICSR]
m:33 [in MetaCoq.Template.utils.wGraph]
m:33 [in MetaCoq.Template.Pretty]
m:331 [in MetaCoq.Template.EtaExpand]
m:332 [in MetaCoq.PCUIC.PCUICSubstitution]
m:333 [in MetaCoq.PCUIC.PCUICSubstitution]
m:337 [in MetaCoq.Template.EtaExpand]
m:34 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
m:34 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
m:342 [in MetaCoq.Template.EtaExpand]
m:345 [in MetaCoq.Template.EtaExpand]
m:35 [in MetaCoq.Template.Induction]
M:356 [in MetaCoq.PCUIC.PCUICReduction]
m:357 [in MetaCoq.Template.Universes]
m:359 [in MetaCoq.PCUIC.PCUICWcbvEval]
m:36 [in MetaCoq.PCUIC.PCUICConvCumInversion]
M:361 [in MetaCoq.PCUIC.PCUICReduction]
m:363 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
m:368 [in MetaCoq.Template.EtaExpand]
m:37 [in MetaCoq.Template.Induction]
m:371 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
m:373 [in MetaCoq.Erasure.EEtaExpandedFix]
M:374 [in MetaCoq.PCUIC.PCUICSubstitution]
m:375 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
m:376 [in MetaCoq.PCUIC.PCUICContextConversion]
M:38 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
M:38 [in MetaCoq.Template.LiftSubst]
m:387 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
m:39 [in MetaCoq.Template.utils.wGraph]
m:391 [in MetaCoq.Template.Checker]
M:395 [in MetaCoq.PCUIC.PCUICSR]
M:4 [in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
m:4 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
M:400 [in MetaCoq.PCUIC.PCUICSR]
m:402 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
m:405 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
m:408 [in MetaCoq.Template.utils.MCList]
m:408 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
M:41 [in MetaCoq.Template.monad_utils]
m:419 [in MetaCoq.Erasure.EEtaExpandedFix]
M:421 [in MetaCoq.PCUIC.PCUICContextConversion]
M:43 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
M:43 [in MetaCoq.Template.LiftSubst]
M:438 [in MetaCoq.PCUIC.PCUICParallelReduction]
m:44 [in MetaCoq.Template.Checker]
M:44 [in MetaCoq.PCUIC.PCUICConversion]
M:445 [in MetaCoq.Template.Typing]
M:45 [in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
m:4563 [in MetaCoq.SafeChecker.PCUICSafeConversion]
m:4565 [in MetaCoq.SafeChecker.PCUICSafeConversion]
m:457 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
m:47 [in MetaCoq.Template.utils.wGraph]
M:471 [in MetaCoq.PCUIC.PCUICSubstitution]
M:477 [in MetaCoq.PCUIC.PCUICSubstitution]
m:477 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
M:48 [in MetaCoq.PCUIC.PCUICConversion]
M:483 [in MetaCoq.PCUIC.PCUICSubstitution]
M:489 [in MetaCoq.PCUIC.PCUICSubstitution]
M:495 [in MetaCoq.PCUIC.PCUICSubstitution]
m:50 [in MetaCoq.Template.utils.wGraph]
m:50 [in MetaCoq.Template.Checker]
m:501 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
M:51 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
M:51 [in MetaCoq.PCUIC.PCUICReduction]
m:511 [in MetaCoq.Template.utils.MCList]
M:524 [in MetaCoq.PCUIC.PCUICSubstitution]
m:53 [in MetaCoq.Template.utils.wGraph]
M:530 [in MetaCoq.PCUIC.PCUICSubstitution]
M:539 [in MetaCoq.PCUIC.PCUICSpine]
m:54 [in MetaCoq.Erasure.EEtaExpandedFix]
M:54 [in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
M:54 [in MetaCoq.PCUIC.PCUICConversion]
M:546 [in MetaCoq.PCUIC.PCUICSpine]
M:55 [in MetaCoq.Template.LiftSubst]
M:55 [in MetaCoq.PCUIC.PCUICReduction]
m:56 [in MetaCoq.Template.utils.wGraph]
M:57 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
m:572 [in MetaCoq.Template.common.uGraph]
m:575 [in MetaCoq.Template.common.uGraph]
m:577 [in MetaCoq.Template.common.uGraph]
m:579 [in MetaCoq.Template.common.uGraph]
m:583 [in MetaCoq.PCUIC.PCUICConfluence]
m:59 [in MetaCoq.Template.utils.wGraph]
m:590 [in MetaCoq.Template.utils.wGraph]
m:592 [in MetaCoq.Template.utils.wGraph]
m:595 [in MetaCoq.PCUIC.PCUICConfluence]
m:6 [in MetaCoq.Template.utils.wGraph]
M:6 [in MetaCoq.PCUIC.PCUICContextReduction]
M:60 [in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
M:60 [in MetaCoq.PCUIC.PCUICConversion]
m:60 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
m:607 [in MetaCoq.PCUIC.PCUICConfluence]
M:63 [in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
M:63 [in MetaCoq.Template.LiftSubst]
M:632 [in MetaCoq.PCUIC.PCUICSubstitution]
M:636 [in MetaCoq.PCUIC.PCUICSR]
m:637 [in MetaCoq.Template.utils.MCList]
m:64 [in MetaCoq.Template.utils.wGraph]
M:64 [in MetaCoq.PCUIC.PCUICConversion]
M:64 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
m:640 [in MetaCoq.Template.utils.MCList]
M:641 [in MetaCoq.PCUIC.PCUICSubstitution]
m:644 [in MetaCoq.Template.utils.MCList]
M:65 [in MetaCoq.Erasure.ELiftSubst]
M:650 [in MetaCoq.PCUIC.PCUICSubstitution]
M:67 [in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
M:67 [in MetaCoq.Erasure.ELiftSubst]
m:68 [in MetaCoq.Erasure.EDeps]
m:68 [in MetaCoq.Template.utils.wGraph]
M:68 [in MetaCoq.Erasure.ELiftSubst]
m:688 [in MetaCoq.PCUIC.PCUICParallelReduction]
m:689 [in MetaCoq.PCUIC.PCUICParallelReduction]
M:69 [in MetaCoq.Template.monad_utils]
M:69 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
M:692 [in MetaCoq.PCUIC.PCUICConfluence]
M:697 [in MetaCoq.PCUIC.PCUICConfluence]
M:699 [in MetaCoq.PCUIC.PCUICParallelReduction]
M:701 [in MetaCoq.PCUIC.PCUICReduction]
M:704 [in MetaCoq.PCUIC.PCUICConfluence]
M:708 [in MetaCoq.PCUIC.PCUICParallelReduction]
M:708 [in MetaCoq.PCUIC.PCUICConfluence]
m:71 [in MetaCoq.PCUIC.PCUICEtaExpand]
M:71 [in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
M:714 [in MetaCoq.PCUIC.PCUICConfluence]
M:716 [in MetaCoq.PCUIC.PCUICParallelReduction]
m:72 [in MetaCoq.Template.utils.wGraph]
M:72 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
M:722 [in MetaCoq.PCUIC.PCUICConfluence]
M:726 [in MetaCoq.PCUIC.PCUICConfluence]
M:73 [in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
M:73 [in MetaCoq.Erasure.ELiftSubst]
M:732 [in MetaCoq.PCUIC.PCUICConfluence]
m:739 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
m:74 [in MetaCoq.Template.BasicAst]
M:74 [in MetaCoq.Template.LiftSubst]
m:74 [in MetaCoq.Template.Induction]
M:740 [in MetaCoq.PCUIC.PCUICConfluence]
m:743 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
M:744 [in MetaCoq.SafeChecker.PCUICSafeChecker]
M:747 [in MetaCoq.PCUIC.PCUICConfluence]
M:75 [in MetaCoq.Erasure.ELiftSubst]
m:750 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
M:754 [in MetaCoq.PCUIC.PCUICConfluence]
M:759 [in MetaCoq.PCUIC.PCUICConfluence]
m:76 [in MetaCoq.Template.utils.wGraph]
m:76 [in MetaCoq.Template.Induction]
M:764 [in MetaCoq.PCUIC.PCUICConfluence]
M:769 [in MetaCoq.PCUIC.PCUICConfluence]
M:77 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
M:778 [in MetaCoq.SafeChecker.PCUICSafeChecker]
m:78 [in MetaCoq.Erasure.Extract]
m:781 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
M:79 [in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
M:79 [in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
M:79 [in MetaCoq.Template.LiftSubst]
m:80 [in MetaCoq.Template.utils.wGraph]
M:80 [in MetaCoq.Erasure.ELiftSubst]
M:81 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
m:82 [in MetaCoq.Template.utils.wGraph]
M:82 [in MetaCoq.Template.LiftSubst]
M:838 [in MetaCoq.PCUIC.PCUICReduction]
m:84 [in MetaCoq.Template.utils.wGraph]
M:85 [in MetaCoq.Template.monad_utils]
M:851 [in MetaCoq.SafeChecker.PCUICSafeChecker]
M:854 [in MetaCoq.PCUIC.PCUICReduction]
M:86 [in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
M:86 [in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
m:86 [in MetaCoq.Template.utils.wGraph]
M:87 [in MetaCoq.Template.LiftSubst]
m:89 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
m:894 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
M:895 [in MetaCoq.PCUIC.PCUICConversion]
m:9 [in MetaCoq.Template.monad_utils]
M:90 [in MetaCoq.Template.monad_utils]
M:901 [in MetaCoq.PCUIC.PCUICConversion]
M:908 [in MetaCoq.PCUIC.PCUICConversion]
M:91 [in MetaCoq.Template.LiftSubst]
M:915 [in MetaCoq.PCUIC.PCUICConversion]
M:92 [in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
M:922 [in MetaCoq.PCUIC.PCUICConversion]
m:926 [in MetaCoq.Erasure.ErasureFunction]
m:93 [in MetaCoq.Template.EtaExpand]
M:93 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
M:95 [in MetaCoq.Erasure.ELiftSubst]
M:973 [in MetaCoq.PCUIC.PCUICConfluence]
M:98 [in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
m:998 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
| 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) |