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)

C (binder)

cargs:140 [in MetaCoq.Erasure.EConstructorsAsBlocks]
cargs:217 [in MetaCoq.Erasure.EConstructorsAsBlocks]
case1:41 [in MetaCoq.Translations.param_original]
case:11 [in MetaCoq.Translations.param_original]
case:25 [in MetaCoq.Translations.param_binary]
ca1:4407 [in MetaCoq.SafeChecker.PCUICSafeConversion]
cbctx:957 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cbody:160 [in MetaCoq.PCUIC.PCUICFirstorder]
cbt':958 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cb':1436 [in MetaCoq.Erasure.ErasureFunction]
cb':156 [in MetaCoq.Erasure.Extract]
cb':173 [in MetaCoq.Erasure.Extract]
cb':201 [in MetaCoq.Erasure.Extract]
cb':652 [in MetaCoq.PCUIC.PCUICSR]
cb':788 [in MetaCoq.Erasure.ErasureFunction]
cb':83 [in MetaCoq.Erasure.EDeps]
cb:109 [in MetaCoq.Erasure.EEtaExpandedFix]
cb:1232 [in MetaCoq.Erasure.ErasureFunction]
cb:1250 [in MetaCoq.Erasure.ErasureFunction]
cb:1285 [in MetaCoq.PCUIC.PCUICConfluence]
cb:142 [in MetaCoq.PCUIC.PCUICEtaExpand]
cb:15 [in MetaCoq.SafeChecker.PCUICSafeConversion]
cb:150 [in MetaCoq.Erasure.ERemoveParams]
cb:153 [in MetaCoq.Erasure.EEtaExpanded]
cb:155 [in MetaCoq.Erasure.Extract]
cb:166 [in MetaCoq.PCUIC.PCUICSafeLemmata]
cb:169 [in MetaCoq.Erasure.EConstructorsAsBlocks]
cb:172 [in MetaCoq.Erasure.Extract]
cb:173 [in MetaCoq.PCUIC.PCUICSafeLemmata]
cb:200 [in MetaCoq.Erasure.Extract]
cb:236 [in MetaCoq.Template.EtaExpand]
cb:254 [in MetaCoq.Erasure.EEtaExpanded]
cb:3 [in MetaCoq.Erasure.EGenericMapEnv]
cb:301 [in MetaCoq.Erasure.ERemoveParams]
cb:396 [in MetaCoq.Erasure.EEtaExpandedFix]
cb:45 [in MetaCoq.Erasure.EInlineProjections]
cb:48 [in MetaCoq.Template.EtaExpand]
cb:651 [in MetaCoq.PCUIC.PCUICSR]
cb:666 [in MetaCoq.Erasure.ErasureFunction]
cb:73 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
cb:773 [in MetaCoq.Erasure.ErasureFunction]
cb:78 [in MetaCoq.Erasure.EOptimizePropDiscr]
cb:82 [in MetaCoq.Erasure.EDeps]
cb:90 [in MetaCoq.Template.Pretty]
cb:910 [in MetaCoq.Erasure.ErasureFunction]
cb:917 [in MetaCoq.Erasure.ErasureFunction]
ccs:911 [in MetaCoq.SafeChecker.PCUICSafeChecker]
cctx:262 [in MetaCoq.SafeChecker.PCUICSafeChecker]
cctx:282 [in MetaCoq.SafeChecker.PCUICSafeChecker]
cc:1234 [in MetaCoq.SafeChecker.PCUICSafeConversion]
cc:825 [in MetaCoq.SafeChecker.PCUICSafeConversion]
cdecls:622 [in MetaCoq.Template.EnvironmentTyping]
cdecls:75 [in MetaCoq.PCUIC.PCUICElimination]
cdecl_sorts:77 [in MetaCoq.PCUIC.PCUICElimination]
cdecl':113 [in MetaCoq.Erasure.EDeps]
cdecl':17 [in MetaCoq.PCUIC.PCUICGlobalEnv]
cdecl':210 [in MetaCoq.Erasure.Extract]
cdecl':226 [in MetaCoq.Erasure.Extract]
cdecl':25 [in MetaCoq.PCUIC.PCUICGlobalEnv]
cdecl':347 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
cdecl':360 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
cdecl':46 [in MetaCoq.PCUIC.PCUICSR]
cdecl':462 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
cdecl':486 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
cdecl':499 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
cdecl':754 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
cdecl':840 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
cdecl':94 [in MetaCoq.Erasure.EDeps]
cdecl:1001 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cdecl:1018 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cdecl:102 [in MetaCoq.Erasure.ESubstitution]
cdecl:102 [in MetaCoq.Erasure.EArities]
cdecl:103 [in MetaCoq.Erasure.EEtaExpandedFix]
cdecl:1031 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cdecl:1031 [in MetaCoq.Erasure.ErasureFunction]
cdecl:104 [in MetaCoq.Template.WfAst]
cdecl:1048 [in MetaCoq.Template.Typing]
cdecl:105 [in MetaCoq.Erasure.Prelim]
cdecl:106 [in MetaCoq.PCUIC.PCUICInversion]
cdecl:1067 [in MetaCoq.Template.Typing]
cdecl:107 [in MetaCoq.Erasure.EGlobalEnv]
cdecl:107 [in MetaCoq.PCUIC.PCUICSR]
cdecl:1079 [in MetaCoq.Template.Typing]
cdecl:109 [in MetaCoq.Erasure.EDeps]
cdecl:109 [in MetaCoq.Erasure.EWcbvEval]
cdecl:11 [in MetaCoq.Erasure.EInlineProjections]
cdecl:110 [in MetaCoq.Erasure.EInlineProjections]
cdecl:113 [in MetaCoq.PCUIC.Syntax.PCUICCases]
cdecl:115 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cdecl:115 [in MetaCoq.Erasure.EWcbvEval]
cdecl:1152 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cdecl:116 [in MetaCoq.Erasure.EInlineProjections]
cdecl:117 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
cdecl:118 [in MetaCoq.Erasure.EWcbvEvalInd]
cdecl:118 [in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
cdecl:121 [in MetaCoq.PCUIC.Syntax.PCUICCases]
cdecl:122 [in MetaCoq.Template.EtaExpand]
cdecl:123 [in MetaCoq.PCUIC.PCUICTyping]
cdecl:125 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cdecl:125 [in MetaCoq.Erasure.Prelim]
cdecl:126 [in MetaCoq.Erasure.EWcbvEval]
cdecl:128 [in MetaCoq.PCUIC.PCUICAlpha]
cdecl:129 [in MetaCoq.PCUIC.PCUICWeakeningEnv]
cdecl:130 [in MetaCoq.Erasure.EWcbvEvalInd]
cdecl:131 [in MetaCoq.PCUIC.PCUICWcbvEval]
cdecl:131 [in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
cdecl:132 [in MetaCoq.PCUIC.PCUICInversion]
cdecl:133 [in MetaCoq.Template.WcbvEval]
cdecl:135 [in MetaCoq.Erasure.EWcbvEval]
cdecl:137 [in MetaCoq.PCUIC.PCUICEtaExpand]
cdecl:139 [in MetaCoq.Erasure.EOptimizePropDiscr]
cdecl:14 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cdecl:140 [in MetaCoq.PCUIC.PCUICAlpha]
cdecl:143 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
cdecl:143 [in MetaCoq.PCUIC.PCUICTyping]
cdecl:144 [in MetaCoq.Template.AstUtils]
cdecl:145 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
cdecl:146 [in MetaCoq.Template.EtaExpand]
cdecl:146 [in MetaCoq.Erasure.ErasureProperties]
cdecl:147 [in MetaCoq.PCUIC.PCUICEtaExpand]
cdecl:147 [in MetaCoq.Erasure.EWcbvEvalInd]
cdecl:149 [in MetaCoq.PCUIC.PCUICWcbvEval]
cdecl:15 [in MetaCoq.Template.EnvironmentTyping]
cdecl:151 [in MetaCoq.Erasure.EDeps]
cdecl:151 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
cdecl:152 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cdecl:152 [in MetaCoq.Erasure.EWcbvEval]
cdecl:153 [in MetaCoq.PCUIC.PCUICProgress]
cdecl:154 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
cdecl:154 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
cdecl:155 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
cdecl:155 [in MetaCoq.PCUIC.PCUICInversion]
cdecl:156 [in MetaCoq.PCUIC.Syntax.PCUICCases]
cdecl:157 [in MetaCoq.PCUIC.PCUICSR]
cdecl:159 [in MetaCoq.Erasure.Extract]
cdecl:16 [in MetaCoq.PCUIC.PCUICGlobalEnv]
cdecl:16 [in MetaCoq.PCUIC.TemplateToPCUICExpanded]
cdecl:160 [in MetaCoq.PCUIC.Syntax.PCUICCases]
cdecl:161 [in MetaCoq.Erasure.EWcbvEvalInd]
cdecl:162 [in MetaCoq.PCUIC.Syntax.PCUICCases]
cdecl:162 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
cdecl:165 [in MetaCoq.Template.WcbvEval]
cdecl:166 [in MetaCoq.PCUIC.Syntax.PCUICCases]
cdecl:166 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
cdecl:166 [in MetaCoq.Erasure.EWcbvEval]
cdecl:169 [in MetaCoq.PCUIC.PCUICSR]
cdecl:170 [in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
cdecl:172 [in MetaCoq.PCUIC.PCUICProgress]
cdecl:175 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
cdecl:179 [in MetaCoq.Template.TypingWf]
cdecl:180 [in MetaCoq.Erasure.EWcbvEval]
cdecl:181 [in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
cdecl:183 [in MetaCoq.PCUIC.PCUICInductives]
cdecl:183 [in MetaCoq.PCUIC.PCUICAlpha]
cdecl:183 [in MetaCoq.Template.TypingWf]
cdecl:184 [in MetaCoq.PCUIC.PCUICProgress]
cdecl:184 [in MetaCoq.Template.WcbvEval]
cdecl:186 [in MetaCoq.Erasure.EConstructorsAsBlocks]
cdecl:19 [in MetaCoq.Erasure.EGlobalEnv]
cdecl:191 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
cdecl:192 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
cdecl:192 [in MetaCoq.Erasure.EConstructorsAsBlocks]
cdecl:193 [in MetaCoq.PCUIC.PCUICAlpha]
cdecl:194 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
cdecl:194 [in MetaCoq.PCUIC.Syntax.PCUICCases]
cdecl:194 [in MetaCoq.PCUIC.PCUICSR]
cdecl:196 [in MetaCoq.Template.EtaExpand]
cdecl:196 [in MetaCoq.PCUIC.PCUICElimination]
cdecl:196 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
cdecl:196 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
cdecl:199 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
cdecl:199 [in MetaCoq.Template.TypingWf]
cdecl:20 [in MetaCoq.Template.EnvironmentTyping]
cdecl:200 [in MetaCoq.PCUIC.Syntax.PCUICCases]
cdecl:200 [in MetaCoq.Erasure.EWcbvEval]
cdecl:203 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
cdecl:203 [in MetaCoq.Erasure.EConstructorsAsBlocks]
cdecl:203 [in MetaCoq.Template.TypingWf]
cdecl:205 [in MetaCoq.PCUIC.Syntax.PCUICCases]
cdecl:205 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
cdecl:205 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
cdecl:207 [in MetaCoq.Erasure.Extract]
cdecl:209 [in MetaCoq.PCUIC.PCUICInductives]
cdecl:210 [in MetaCoq.PCUIC.Syntax.PCUICCases]
cdecl:211 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
cdecl:211 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
cdecl:212 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
cdecl:214 [in MetaCoq.PCUIC.PCUICWcbvEval]
cdecl:214 [in MetaCoq.Erasure.EEtaExpanded]
cdecl:216 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
cdecl:217 [in MetaCoq.PCUIC.PCUICSubstitution]
cdecl:218 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
cdecl:218 [in MetaCoq.PCUIC.PCUICInductives]
cdecl:219 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
cdecl:219 [in MetaCoq.PCUIC.PCUICTyping]
cdecl:222 [in MetaCoq.Erasure.Extract]
cdecl:223 [in MetaCoq.PCUIC.Syntax.PCUICCases]
cdecl:223 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
cdecl:225 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
cdecl:227 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
cdecl:227 [in MetaCoq.PCUIC.PCUICSubstitution]
cdecl:227 [in MetaCoq.Erasure.EConstructorsAsBlocks]
cdecl:227 [in MetaCoq.Template.WcbvEval]
cdecl:229 [in MetaCoq.PCUIC.PCUICWcbvEval]
cdecl:229 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
cdecl:231 [in MetaCoq.Template.EtaExpand]
cdecl:232 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
cdecl:232 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
cdecl:235 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
cdecl:235 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
cdecl:237 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
cdecl:24 [in MetaCoq.PCUIC.PCUICGlobalEnv]
cdecl:24 [in MetaCoq.Erasure.EGlobalEnv]
cdecl:240 [in MetaCoq.Template.TypingWf]
cdecl:241 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
cdecl:242 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
cdecl:242 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
cdecl:243 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cdecl:246 [in MetaCoq.Template.EtaExpand]
cdecl:249 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
cdecl:249 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
cdecl:250 [in MetaCoq.Template.WcbvEval]
cdecl:250 [in MetaCoq.Erasure.EEtaExpanded]
cdecl:255 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
cdecl:261 [in MetaCoq.PCUIC.PCUICWcbvEval]
cdecl:261 [in MetaCoq.Erasure.EWcbvEval]
cdecl:263 [in MetaCoq.SafeChecker.PCUICSafeChecker]
cdecl:264 [in MetaCoq.Template.Typing]
cdecl:269 [in MetaCoq.Erasure.EWcbvEval]
cdecl:272 [in MetaCoq.Erasure.EEtaExpanded]
cdecl:272 [in MetaCoq.Template.TypingWf]
cdecl:275 [in MetaCoq.PCUIC.PCUICWfUniverses]
cdecl:279 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cdecl:279 [in MetaCoq.Erasure.EEtaExpanded]
cdecl:28 [in MetaCoq.Erasure.EWcbvEvalInd]
cdecl:283 [in MetaCoq.SafeChecker.PCUICSafeChecker]
cdecl:284 [in MetaCoq.PCUIC.PCUICInductives]
cdecl:284 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cdecl:285 [in MetaCoq.Template.EtaExpand]
cdecl:29 [in MetaCoq.PCUIC.TemplateToPCUIC]
cdecl:297 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cdecl:30 [in MetaCoq.Erasure.ErasureCorrectness]
cdecl:30 [in MetaCoq.Erasure.EEnvMap]
cdecl:303 [in MetaCoq.PCUIC.PCUICProgress]
cdecl:307 [in MetaCoq.Template.TypingWf]
cdecl:31 [in MetaCoq.PCUIC.PCUICSafeLemmata]
cdecl:314 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cdecl:316 [in MetaCoq.Erasure.EArities]
cdecl:322 [in MetaCoq.PCUIC.PCUICProgress]
cdecl:324 [in MetaCoq.SafeChecker.PCUICSafeChecker]
cdecl:333 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cdecl:334 [in MetaCoq.PCUIC.PCUICProgress]
cdecl:337 [in MetaCoq.PCUIC.PCUICInductives]
cdecl:342 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cdecl:345 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
cdecl:347 [in MetaCoq.PCUIC.PCUICInductives]
cdecl:35 [in MetaCoq.Template.EnvironmentTyping]
cdecl:35 [in MetaCoq.Erasure.EEnvMap]
cdecl:351 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
cdecl:353 [in MetaCoq.SafeChecker.PCUICSafeChecker]
cdecl:357 [in MetaCoq.Template.Ast]
cdecl:357 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
cdecl:36 [in MetaCoq.Erasure.EWcbvEval]
cdecl:361 [in MetaCoq.Erasure.ERemoveParams]
cdecl:363 [in MetaCoq.Template.Ast]
cdecl:366 [in MetaCoq.Template.Ast]
cdecl:367 [in MetaCoq.PCUIC.PCUICWcbvEval]
cdecl:37 [in MetaCoq.PCUIC.PCUICWcbvEval]
cdecl:37 [in MetaCoq.PCUIC.PCUICGlobalEnv]
cdecl:373 [in MetaCoq.PCUIC.PCUICWcbvEval]
cdecl:376 [in MetaCoq.Template.Ast]
cdecl:38 [in MetaCoq.Template.EnvironmentTyping]
cdecl:381 [in MetaCoq.Erasure.EEtaExpandedFix]
cdecl:386 [in MetaCoq.PCUIC.PCUICProgress]
cdecl:387 [in MetaCoq.PCUIC.PCUICInductives]
cdecl:387 [in MetaCoq.Erasure.ERemoveParams]
cdecl:388 [in MetaCoq.Erasure.EEtaExpandedFix]
cdecl:389 [in MetaCoq.Template.Ast]
cdecl:39 [in MetaCoq.Template.WfAst]
cdecl:39 [in MetaCoq.PCUIC.TemplateToPCUIC]
cdecl:39 [in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
cdecl:392 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
cdecl:397 [in MetaCoq.PCUIC.PCUICProgress]
cdecl:403 [in MetaCoq.Template.Ast]
cdecl:406 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
cdecl:407 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
cdecl:409 [in MetaCoq.PCUIC.PCUICProgress]
cdecl:41 [in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
cdecl:410 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
cdecl:415 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
cdecl:42 [in MetaCoq.PCUIC.PCUICGlobalEnv]
cdecl:421 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
cdecl:422 [in MetaCoq.Template.EtaExpand]
cdecl:423 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
cdecl:437 [in MetaCoq.PCUIC.PCUICInductives]
cdecl:44 [in MetaCoq.Erasure.EWcbvEvalInd]
cdecl:442 [in MetaCoq.PCUIC.PCUICProgress]
cdecl:45 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
cdecl:45 [in MetaCoq.PCUIC.PCUICSR]
cdecl:45 [in MetaCoq.Erasure.EWcbvEval]
cdecl:452 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
cdecl:456 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cdecl:46 [in MetaCoq.Template.WcbvEval]
cdecl:460 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
cdecl:461 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
cdecl:463 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
cdecl:469 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cdecl:47 [in MetaCoq.Erasure.EEtaExpandedFix]
cdecl:47 [in MetaCoq.Erasure.EGlobalEnv]
cdecl:475 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cdecl:479 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
cdecl:492 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
cdecl:5 [in MetaCoq.PCUIC.PCUICTyping]
cdecl:50 [in MetaCoq.Erasure.EGlobalEnv]
cdecl:503 [in MetaCoq.Template.EtaExpand]
cdecl:51 [in MetaCoq.PCUIC.Conversion.PCUICClosedConv]
cdecl:52 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
cdecl:53 [in MetaCoq.PCUIC.PCUICCasesContexts]
cdecl:54 [in MetaCoq.Template.WfAst]
cdecl:54 [in MetaCoq.PCUIC.TemplateToPCUICExpanded]
cdecl:54 [in MetaCoq.Erasure.EGenericMapEnv]
cdecl:545 [in MetaCoq.PCUIC.PCUICTyping]
cdecl:548 [in MetaCoq.Template.EnvironmentTyping]
cdecl:55 [in MetaCoq.Erasure.EGlobalEnv]
cdecl:551 [in MetaCoq.Template.EnvironmentTyping]
cdecl:557 [in MetaCoq.Template.EnvironmentTyping]
cdecl:56 [in MetaCoq.PCUIC.Syntax.PCUICCases]
cdecl:564 [in MetaCoq.PCUIC.PCUICTyping]
cdecl:569 [in MetaCoq.PCUIC.PCUICSR]
cdecl:57 [in MetaCoq.Template.EnvironmentTyping]
cdecl:57 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cdecl:57 [in MetaCoq.Erasure.EEnvMap]
cdecl:576 [in MetaCoq.PCUIC.PCUICTyping]
cdecl:576 [in MetaCoq.PCUIC.PCUICSR]
cdecl:58 [in MetaCoq.PCUIC.PCUICCasesContexts]
cdecl:586 [in MetaCoq.PCUIC.PCUICSR]
cdecl:59 [in MetaCoq.PCUIC.Syntax.PCUICCases]
cdecl:593 [in MetaCoq.Template.EnvironmentTyping]
cdecl:6 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
cdecl:60 [in MetaCoq.PCUIC.PCUICEtaExpand]
cdecl:60 [in MetaCoq.Erasure.EGenericMapEnv]
cdecl:602 [in MetaCoq.Template.EnvironmentTyping]
cdecl:61 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
cdecl:62 [in MetaCoq.Template.EnvironmentTyping]
cdecl:62 [in MetaCoq.PCUIC.Syntax.PCUICCases]
cdecl:62 [in MetaCoq.Erasure.EGlobalEnv]
cdecl:624 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cdecl:63 [in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
cdecl:646 [in MetaCoq.Template.Typing]
cdecl:648 [in MetaCoq.PCUIC.PCUICSR]
cdecl:65 [in MetaCoq.PCUIC.Syntax.PCUICCases]
cdecl:66 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
cdecl:660 [in MetaCoq.Template.Typing]
cdecl:660 [in MetaCoq.PCUIC.PCUICSR]
cdecl:668 [in MetaCoq.Template.Typing]
cdecl:67 [in MetaCoq.Template.EtaExpand]
cdecl:67 [in MetaCoq.Template.EnvironmentTyping]
cdecl:67 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cdecl:671 [in MetaCoq.Erasure.ErasureFunction]
cdecl:671 [in MetaCoq.PCUIC.PCUICSR]
cdecl:672 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
cdecl:673 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
cdecl:675 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cdecl:68 [in MetaCoq.Erasure.EArities]
cdecl:682 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cdecl:698 [in MetaCoq.SafeChecker.PCUICTypeChecker]
cdecl:7 [in MetaCoq.Template.Typing]
cdecl:700 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cdecl:71 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
cdecl:720 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
cdecl:73 [in MetaCoq.Template.EnvironmentTyping]
cdecl:73 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cdecl:73 [in MetaCoq.PCUIC.Syntax.PCUICCases]
cdecl:73 [in MetaCoq.Template.WcbvEval]
cdecl:730 [in MetaCoq.PCUIC.PCUICSR]
cdecl:734 [in MetaCoq.SafeChecker.PCUICTypeChecker]
cdecl:74 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
cdecl:74 [in MetaCoq.Erasure.EGlobalEnv]
cdecl:740 [in MetaCoq.SafeChecker.PCUICTypeChecker]
cdecl:745 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
cdecl:75 [in MetaCoq.PCUIC.PCUICWcbvEval]
cdecl:751 [in MetaCoq.SafeChecker.PCUICTypeChecker]
cdecl:752 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cdecl:76 [in MetaCoq.PCUIC.PCUICElimination]
cdecl:76 [in MetaCoq.PCUIC.PCUICCasesContexts]
cdecl:77 [in MetaCoq.Erasure.EAst]
cdecl:77 [in MetaCoq.PCUIC.PCUICTyping]
cdecl:774 [in MetaCoq.SafeChecker.PCUICTypeChecker]
cdecl:78 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
cdecl:78 [in MetaCoq.PCUIC.Syntax.PCUICCases]
cdecl:79 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cdecl:79 [in MetaCoq.Erasure.EGlobalEnv]
cdecl:833 [in MetaCoq.SafeChecker.PCUICSafeChecker]
cdecl:837 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
cdecl:85 [in MetaCoq.Erasure.EGlobalEnv]
cdecl:86 [in MetaCoq.Erasure.Prelim]
cdecl:868 [in MetaCoq.PCUIC.PCUICTyping]
cdecl:886 [in MetaCoq.SafeChecker.PCUICSafeChecker]
cdecl:887 [in MetaCoq.PCUIC.PCUICTyping]
cdecl:899 [in MetaCoq.PCUIC.PCUICTyping]
cdecl:90 [in MetaCoq.PCUIC.PCUICWcbvEval]
cdecl:91 [in MetaCoq.Erasure.EDeps]
cdecl:91 [in MetaCoq.Template.WcbvEval]
cdecl:91 [in MetaCoq.PCUIC.utils.PCUICPretty]
cdecl:916 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cdecl:92 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
cdecl:92 [in MetaCoq.Erasure.EGlobalEnv]
cdecl:924 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cdecl:93 [in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
cdecl:94 [in MetaCoq.Erasure.Prelim]
cdecl:950 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cdecl:952 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cdecl:966 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cdecl:97 [in MetaCoq.Template.Typing]
cdecl:98 [in MetaCoq.PCUIC.Syntax.PCUICCases]
cdecl:98 [in MetaCoq.Erasure.EGlobalEnv]
cdecl:981 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cdecl:984 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cdecl:99 [in MetaCoq.Erasure.Prelim]
Ceq:1664 [in MetaCoq.Translations.MiniHoTT]
Ceq:1670 [in MetaCoq.Translations.MiniHoTT]
Ceq:1672 [in MetaCoq.Translations.MiniHoTT_paths]
Ceq:1678 [in MetaCoq.Translations.MiniHoTT_paths]
cfix:73 [in MetaCoq.PCUIC.Syntax.PCUICViews]
cf:1 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
cf:1 [in MetaCoq.PCUIC.PCUICProgress]
cf:1 [in MetaCoq.PCUIC.Typing.PCUICInstTyp]
cf:1 [in MetaCoq.PCUIC.PCUICElimination]
cf:1 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
cf:1 [in MetaCoq.PCUIC.PCUICSafeLemmata]
cf:1 [in MetaCoq.PCUIC.PCUICArities]
cf:1 [in MetaCoq.PCUIC.PCUICWfUniverses]
cf:1 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
cf:1 [in MetaCoq.PCUIC.PCUICSubstitution]
cf:1 [in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
cf:1 [in MetaCoq.Template.TemplateProgram]
cf:1 [in MetaCoq.PCUIC.PCUICValidity]
cf:1 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cf:1 [in MetaCoq.PCUIC.PCUICCumulProp]
cf:1 [in MetaCoq.PCUIC.PCUICInversion]
cf:1 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
cf:1 [in MetaCoq.PCUIC.PCUICAlpha]
cf:1 [in MetaCoq.SafeChecker.PCUICWfEnv]
cf:1 [in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
cf:1 [in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
cf:1 [in MetaCoq.PCUIC.Syntax.PCUICRenameDef]
cf:1 [in MetaCoq.PCUIC.PCUICSN]
cf:1 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
cf:1 [in MetaCoq.Erasure.ErasureFunction]
cf:1 [in MetaCoq.PCUIC.PCUICConvCumInversion]
cf:1 [in MetaCoq.SafeChecker.PCUICSafeReduce]
cf:1 [in MetaCoq.PCUIC.PCUICPrincipality]
cf:1 [in MetaCoq.Erasure.ETransform]
cf:1 [in MetaCoq.PCUIC.Typing.PCUICWeakeningTyp]
cf:1 [in MetaCoq.PCUIC.PCUICGeneration]
cf:1 [in MetaCoq.PCUIC.PCUICConversion]
cf:1 [in MetaCoq.PCUIC.Bidirectional.BDUnique]
cf:1 [in MetaCoq.PCUIC.Typing.PCUICNamelessTyp]
cf:1 [in MetaCoq.PCUIC.PCUICSR]
cf:1 [in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
cf:1 [in MetaCoq.PCUIC.Conversion.PCUICClosedConv]
cf:1 [in MetaCoq.PCUIC.PCUICContextReduction]
cf:1 [in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
cf:1 [in MetaCoq.PCUIC.PCUICSpine]
cf:10 [in MetaCoq.PCUIC.PCUICSN]
cf:100 [in MetaCoq.PCUIC.PCUICCumulativity]
cf:1004 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cf:101 [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
cf:101 [in MetaCoq.Template.TypingWf]
cf:102 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
cf:102 [in MetaCoq.PCUIC.PCUICSubstitution]
cf:102 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cf:102 [in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
cf:102 [in MetaCoq.PCUIC.TemplateToPCUICExpanded]
cf:1024 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cf:1028 [in MetaCoq.PCUIC.PCUICConversion]
cf:103 [in MetaCoq.PCUIC.PCUICValidity]
cf:1036 [in MetaCoq.PCUIC.PCUICConversion]
cf:1037 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cf:1046 [in MetaCoq.PCUIC.PCUICConversion]
cf:1049 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cf:105 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
cf:105 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
cf:1053 [in MetaCoq.PCUIC.PCUICConversion]
CF:106 [in MetaCoq.PCUIC.PCUICWeakeningEnv]
cf:106 [in MetaCoq.Template.TypingWf]
cf:1068 [in MetaCoq.PCUIC.PCUICConversion]
cf:107 [in MetaCoq.PCUIC.PCUICElimination]
cf:107 [in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
cf:1073 [in MetaCoq.PCUIC.PCUICConversion]
cf:1074 [in MetaCoq.SafeChecker.PCUICSafeChecker]
cf:1075 [in MetaCoq.SafeChecker.PCUICSafeChecker]
cf:108 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
cf:108 [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
cf:108 [in MetaCoq.PCUIC.PCUICSpine]
cf:1081 [in MetaCoq.PCUIC.PCUICConversion]
cf:1087 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cf:1088 [in MetaCoq.PCUIC.PCUICConversion]
cf:1095 [in MetaCoq.PCUIC.PCUICConversion]
cf:1098 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cf:11 [in MetaCoq.PCUIC.PCUICTransform]
cf:11 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
cf:11 [in MetaCoq.PCUIC.PCUICSubstitution]
cf:11 [in MetaCoq.SafeChecker.PCUICSafeReduce]
cf:11 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
cf:11 [in MetaCoq.PCUIC.PCUICSR]
cf:110 [in MetaCoq.PCUIC.PCUICSR]
cf:1101 [in MetaCoq.PCUIC.PCUICConversion]
cf:111 [in MetaCoq.PCUIC.PCUICElimination]
cf:1119 [in MetaCoq.PCUIC.PCUICConversion]
cf:112 [in MetaCoq.PCUIC.PCUICValidity]
cf:112 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cf:112 [in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
cf:112 [in MetaCoq.Erasure.Prelim]
cf:1122 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cf:1128 [in MetaCoq.PCUIC.PCUICConversion]
cf:113 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
cf:113 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
cf:113 [in MetaCoq.PCUIC.PCUICSubstitution]
cf:113 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
cf:1132 [in MetaCoq.Erasure.ErasureFunction]
cf:1137 [in MetaCoq.PCUIC.PCUICConversion]
cf:114 [in MetaCoq.Template.TypingWf]
cf:1148 [in MetaCoq.Erasure.ErasureFunction]
cf:115 [in MetaCoq.PCUIC.PCUICElimination]
cf:115 [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
cf:117 [in MetaCoq.PCUIC.PCUICSR]
cf:1175 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cf:1177 [in MetaCoq.PCUIC.PCUICConversion]
cf:118 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
cf:118 [in MetaCoq.PCUIC.PCUICContexts]
cf:1180 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cf:1185 [in MetaCoq.Erasure.ErasureFunction]
cf:1187 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cf:119 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
cf:119 [in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
cf:119 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
cf:1193 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cf:1199 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cf:12 [in MetaCoq.PCUIC.PCUICProgress]
cf:12 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
cf:12 [in MetaCoq.PCUIC.PCUICInductives]
cf:12 [in MetaCoq.PCUIC.PCUICConvCumInversion]
cf:12 [in MetaCoq.Erasure.Erasure]
cf:12 [in MetaCoq.PCUIC.PCUICConversion]
cf:120 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
cf:120 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
cf:120 [in MetaCoq.PCUIC.PCUICSubstitution]
cf:1205 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cf:121 [in MetaCoq.PCUIC.PCUICElimination]
cf:1210 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cf:1217 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cf:1219 [in MetaCoq.PCUIC.PCUICConversion]
cf:122 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
cf:1232 [in MetaCoq.PCUIC.PCUICConfluence]
cf:124 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
cf:1240 [in MetaCoq.PCUIC.PCUICConfluence]
cf:1246 [in MetaCoq.PCUIC.PCUICConversion]
cf:125 [in MetaCoq.PCUIC.PCUICCumulativity]
cf:125 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
cf:1258 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cf:126 [in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
cf:126 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
cf:1265 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cf:1266 [in MetaCoq.PCUIC.PCUICConversion]
cf:1272 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cf:1272 [in MetaCoq.Erasure.ErasureFunction]
cf:1279 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cf:128 [in MetaCoq.PCUIC.PCUICSR]
cf:128 [in MetaCoq.PCUIC.PCUICSpine]
cf:1287 [in MetaCoq.Erasure.ErasureFunction]
cf:129 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
cf:129 [in MetaCoq.SafeChecker.PCUICWfEnv]
cf:1292 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cf:1297 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cf:13 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
cf:13 [in MetaCoq.PCUIC.PCUICSafeLemmata]
cf:13 [in MetaCoq.PCUIC.PCUICArities]
cf:13 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
cf:13 [in MetaCoq.SafeChecker.PCUICWfEnv]
cf:13 [in MetaCoq.SafeChecker.PCUICSafeChecker]
cf:13 [in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
cf:130 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
cf:1300 [in MetaCoq.Erasure.ErasureFunction]
cf:131 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
cf:131 [in MetaCoq.PCUIC.PCUICCumulativity]
cf:1312 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cf:1319 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cf:1327 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cf:133 [in MetaCoq.Erasure.EArities]
cf:133 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
cf:1332 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cf:1347 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cf:1348 [in MetaCoq.Erasure.ErasureFunction]
cf:135 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
cf:135 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
cf:135 [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
cf:135 [in MetaCoq.Template.TypingWf]
cf:1350 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cf:1352 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cf:1354 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cf:136 [in MetaCoq.PCUIC.PCUICSR]
cf:1363 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cf:1368 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cf:137 [in MetaCoq.PCUIC.PCUICElimination]
cf:137 [in MetaCoq.PCUIC.PCUICCumulativity]
cf:137 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
cf:138 [in MetaCoq.PCUIC.PCUICInductives]
cf:1380 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cf:139 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
cf:139 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cf:139 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
cf:1397 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cf:14 [in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
cf:14 [in MetaCoq.SafeChecker.PCUICSafeChecker]
cf:140 [in MetaCoq.PCUIC.PCUICCumulativity]
cf:140 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
cf:140 [in MetaCoq.PCUIC.PCUICCanonicity]
cf:1401 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cf:1404 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cf:1414 [in MetaCoq.Erasure.ErasureFunction]
cf:1417 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
cf:143 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
cf:143 [in MetaCoq.PCUIC.PCUICSpine]
cf:144 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
cf:144 [in MetaCoq.PCUIC.PCUICElimination]
cf:144 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
cf:144 [in MetaCoq.PCUIC.PCUICSR]
cf:146 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
cf:146 [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
cf:1460 [in MetaCoq.Erasure.ErasureFunction]
cf:1468 [in MetaCoq.Erasure.ErasureFunction]
cf:147 [in MetaCoq.PCUIC.PCUICCumulativity]
cf:147 [in MetaCoq.PCUIC.PCUICInductives]
cf:1475 [in MetaCoq.SafeChecker.PCUICSafeReduce]
cf:1477 [in MetaCoq.Erasure.ErasureFunction]
cf:15 [in MetaCoq.Erasure.Erasure]
cf:150 [in MetaCoq.PCUIC.PCUICSR]
cf:1509 [in MetaCoq.Erasure.ErasureFunction]
cf:151 [in MetaCoq.PCUIC.PCUICCumulativity]
cf:1516 [in MetaCoq.Erasure.ErasureFunction]
cf:152 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
cf:152 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
cf:153 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
cf:154 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
cf:154 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
cf:155 [in MetaCoq.PCUIC.PCUICInductives]
cf:156 [in MetaCoq.PCUIC.PCUICCumulativity]
cf:157 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
cf:158 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
cf:159 [in MetaCoq.PCUIC.PCUICElimination]
cf:16 [in MetaCoq.PCUIC.PCUICSubstitution]
cf:16 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cf:16 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
cf:16 [in MetaCoq.SafeChecker.SafeTemplateChecker]
cf:16 [in MetaCoq.PCUIC.PCUICSpine]
cf:160 [in MetaCoq.PCUIC.PCUICSR]
cf:161 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
cf:162 [in MetaCoq.PCUIC.PCUICCumulativity]
cf:162 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
cf:162 [in MetaCoq.PCUIC.PCUICTyping]
cf:163 [in MetaCoq.PCUIC.PCUICInductives]
cf:164 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
cf:165 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
cf:165 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
cf:166 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cf:166 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
cf:167 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
cf:168 [in MetaCoq.PCUIC.PCUICTyping]
cf:169 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
cf:169 [in MetaCoq.PCUIC.PCUICInductives]
cf:17 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
cf:17 [in MetaCoq.PCUIC.PCUICElimination]
cf:17 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
cf:17 [in MetaCoq.PCUIC.PCUICCanonicity]
cf:170 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
cf:170 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
cf:170 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
cf:170 [in MetaCoq.PCUIC.PCUICSR]
cf:171 [in MetaCoq.Template.common.uGraph]
cf:171 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
cf:173 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
cf:174 [in MetaCoq.PCUIC.PCUICTyping]
cf:174 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
cf:174 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
cf:176 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
cf:176 [in MetaCoq.PCUIC.PCUICElimination]
cf:176 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
cf:176 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
cf:178 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
cf:178 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
cf:179 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
cf:179 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cf:179 [in MetaCoq.Template.common.uGraph]
cf:179 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
cf:18 [in MetaCoq.PCUIC.PCUICWeakeningEnv]
cf:18 [in MetaCoq.PCUIC.PCUICSafeLemmata]
cf:18 [in MetaCoq.PCUIC.PCUICConvCumInversion]
cf:18 [in MetaCoq.SafeChecker.PCUICSafeConversion]
cf:18 [in MetaCoq.Erasure.Erasure]
cf:18 [in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
cf:180 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
cf:180 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
cf:181 [in MetaCoq.PCUIC.PCUICElimination]
cf:181 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
cf:184 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
cf:185 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
cf:186 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
cf:187 [in MetaCoq.PCUIC.PCUICSR]
cf:187 [in MetaCoq.PCUIC.PCUICContexts]
cf:188 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
cf:189 [in MetaCoq.PCUIC.PCUICTyping]
cf:19 [in MetaCoq.PCUIC.PCUICTransform]
cf:19 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
cf:19 [in MetaCoq.PCUIC.PCUICSR]
cf:191 [in MetaCoq.PCUIC.PCUICElimination]
cf:191 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
cf:191 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
cf:192 [in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
cf:195 [in MetaCoq.PCUIC.PCUICInductives]
cf:195 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
cf:195 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
cf:196 [in MetaCoq.PCUIC.PCUICTyping]
cf:196 [in MetaCoq.PCUIC.PCUICSR]
cf:198 [in MetaCoq.PCUIC.PCUICElimination]
cf:198 [in MetaCoq.Erasure.EArities]
cf:198 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
cf:198 [in MetaCoq.PCUIC.PCUICInductives]
cf:199 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
cf:199 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cf:20 [in MetaCoq.PCUIC.PCUICCumulativity]
cf:20 [in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
cf:20 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
cf:20 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
cf:20 [in MetaCoq.Erasure.ErasureFunction]
cf:20 [in MetaCoq.PCUIC.PCUICPrincipality]
cf:20 [in MetaCoq.Erasure.ETransform]
cf:200 [in MetaCoq.PCUIC.PCUICSubstitution]
cf:200 [in MetaCoq.PCUIC.PCUICTyping]
cf:200 [in MetaCoq.PCUIC.PCUICContexts]
cf:201 [in MetaCoq.PCUIC.PCUICInductives]
cf:202 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
cf:202 [in MetaCoq.Template.Universes]
cf:202 [in MetaCoq.Erasure.EArities]
cf:203 [in MetaCoq.SafeChecker.PCUICWfEnv]
cf:204 [in MetaCoq.PCUIC.PCUICInductives]
cf:205 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
cf:205 [in MetaCoq.PCUIC.PCUICSubstitution]
cf:205 [in MetaCoq.PCUIC.PCUICContexts]
cf:206 [in MetaCoq.PCUIC.PCUICElimination]
cf:206 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
cf:206 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
cf:206 [in MetaCoq.SafeChecker.PCUICWfEnv]
cf:206 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
cf:206 [in MetaCoq.PCUIC.PCUICTyping]
cf:207 [in MetaCoq.Template.TypingWf]
cf:208 [in MetaCoq.SafeChecker.PCUICWfEnv]
cf:208 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
cf:209 [in MetaCoq.PCUIC.PCUICSR]
cf:209 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
cf:21 [in MetaCoq.PCUIC.Typing.PCUICInstTyp]
cf:210 [in MetaCoq.PCUIC.PCUICSubstitution]
cf:210 [in MetaCoq.SafeChecker.PCUICWfEnv]
cf:211 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cf:212 [in MetaCoq.PCUIC.PCUICProgress]
cf:212 [in MetaCoq.PCUIC.PCUICInductives]
cf:213 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
cf:213 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
cf:213 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
cf:214 [in MetaCoq.PCUIC.PCUICElimination]
cf:214 [in MetaCoq.SafeChecker.PCUICWfEnv]
cf:214 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cf:215 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
cf:215 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
cf:216 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cf:216 [in MetaCoq.SafeChecker.PCUICWfEnv]
cf:217 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
cf:217 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
cf:218 [in MetaCoq.SafeChecker.PCUICWfEnv]
cf:219 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
cf:219 [in MetaCoq.PCUIC.PCUICSubstitution]
cf:219 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cf:22 [in MetaCoq.SafeChecker.PCUICConsistency]
cf:22 [in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
cf:220 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
cf:221 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
cf:221 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
cf:221 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
cf:222 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
cf:222 [in MetaCoq.PCUIC.PCUICTyping]
cf:223 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cf:224 [in MetaCoq.PCUIC.PCUICConversion]
cf:224 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
cf:226 [in MetaCoq.SafeChecker.PCUICWfEnv]
cf:227 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cf:228 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
cf:229 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cf:229 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
cf:229 [in MetaCoq.Template.TypingWf]
cf:23 [in MetaCoq.PCUIC.PCUICWeakeningEnv]
cf:23 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
cf:230 [in MetaCoq.PCUIC.PCUICConversion]
cf:231 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
cf:232 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
cf:233 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cf:236 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
cf:236 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
cf:237 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
cf:238 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
cf:239 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cf:24 [in MetaCoq.PCUIC.PCUICInductives]
cf:24 [in MetaCoq.SafeChecker.PCUICSafeChecker]
cf:24 [in MetaCoq.PCUIC.PCUICSpine]
cf:24 [in MetaCoq.SafeChecker.PCUICTypeChecker]
cf:243 [in MetaCoq.PCUIC.PCUICEquality]
cf:244 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
cf:244 [in MetaCoq.PCUIC.PCUICTyping]
cf:245 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
cf:245 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
cf:249 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cf:25 [in MetaCoq.PCUIC.PCUICCumulativity]
cf:25 [in MetaCoq.Erasure.ErasureCorrectness]
cf:25 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
cf:25 [in MetaCoq.PCUIC.Typing.PCUICWeakeningTyp]
cf:25 [in MetaCoq.PCUIC.Syntax.PCUICInstDef]
cf:250 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
cf:251 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
cf:251 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
cf:252 [in MetaCoq.PCUIC.PCUICSR]
cf:253 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
cf:253 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cf:253 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
cf:258 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cf:258 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
cf:259 [in MetaCoq.PCUIC.PCUICSR]
cf:261 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cf:261 [in MetaCoq.Template.common.uGraph]
cf:263 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cf:264 [in MetaCoq.PCUIC.PCUICSR]
cf:265 [in MetaCoq.PCUIC.PCUICSubstitution]
cf:266 [in MetaCoq.PCUIC.PCUICEquality]
cf:266 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cf:27 [in MetaCoq.PCUIC.PCUICElimination]
cf:27 [in MetaCoq.PCUIC.PCUICArities]
cf:27 [in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
cf:27 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cf:270 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cf:271 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
cf:271 [in MetaCoq.PCUIC.PCUICSR]
cf:273 [in MetaCoq.Template.TypingWf]
cf:274 [in MetaCoq.PCUIC.PCUICConversion]
cf:275 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
cf:276 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
cf:278 [in MetaCoq.PCUIC.PCUICSR]
cf:279 [in MetaCoq.PCUIC.PCUICInductives]
cf:279 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cf:28 [in MetaCoq.PCUIC.PCUICWeakeningEnv]
cf:28 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
cf:28 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
cf:28 [in MetaCoq.SafeChecker.PCUICWfEnv]
cf:28 [in MetaCoq.PCUIC.PCUICSR]
cf:28 [in MetaCoq.SafeChecker.PCUICTypeChecker]
cf:281 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
cf:282 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
cf:284 [in MetaCoq.PCUIC.PCUICSpine]
cf:285 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cf:286 [in MetaCoq.PCUIC.PCUICInductives]
cf:286 [in MetaCoq.PCUIC.PCUICSR]
cf:287 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
cf:288 [in MetaCoq.PCUIC.PCUICEquality]
cf:288 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
cf:29 [in MetaCoq.PCUIC.PCUICCumulativity]
cf:29 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
cf:29 [in MetaCoq.PCUIC.PCUICFirstorder]
cf:29 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
cf:29 [in MetaCoq.PCUIC.Conversion.PCUICClosedConv]
cf:29 [in MetaCoq.PCUIC.PCUICContexts]
cf:292 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
cf:293 [in MetaCoq.PCUIC.PCUICSafeLemmata]
cf:293 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
cf:294 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cf:294 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
cf:295 [in MetaCoq.PCUIC.PCUICEquality]
cf:295 [in MetaCoq.PCUIC.PCUICTyping]
cf:297 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
cf:297 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
cf:297 [in MetaCoq.PCUIC.PCUICTyping]
cf:298 [in MetaCoq.PCUIC.PCUICEquality]
cf:298 [in MetaCoq.PCUIC.PCUICSR]
cf:3 [in MetaCoq.SafeChecker.SafeTemplateChecker]
cf:30 [in MetaCoq.PCUIC.Typing.PCUICInstTyp]
cf:30 [in MetaCoq.PCUIC.PCUICSpine]
cf:300 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
cf:301 [in MetaCoq.PCUIC.PCUICEquality]
cf:302 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
cf:302 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
cf:302 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
cf:303 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cf:304 [in MetaCoq.PCUIC.PCUICInductives]
cf:304 [in MetaCoq.PCUIC.PCUICEquality]
cf:304 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
cf:305 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cf:31 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
cf:31 [in MetaCoq.PCUIC.PCUICSubstitution]
cf:31 [in MetaCoq.PCUIC.PCUICInductives]
cf:31 [in MetaCoq.PCUIC.PCUICPrincipality]
cf:310 [in MetaCoq.PCUIC.PCUICInductives]
cf:311 [in MetaCoq.PCUIC.PCUICSubstitution]
cf:315 [in MetaCoq.Template.Checker]
cf:315 [in MetaCoq.PCUIC.PCUICConfluence]
cf:315 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
cf:316 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
cf:32 [in MetaCoq.PCUIC.PCUICWeakeningEnv]
cf:32 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
cf:32 [in MetaCoq.Erasure.ErasureCorrectness]
cf:32 [in MetaCoq.PCUIC.Typing.PCUICWeakeningTyp]
cf:32 [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
cf:320 [in MetaCoq.Erasure.EArities]
cf:320 [in MetaCoq.PCUIC.PCUICContextConversion]
cf:321 [in MetaCoq.PCUIC.PCUICInductives]
cf:323 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
cf:325 [in MetaCoq.PCUIC.PCUICConfluence]
cf:325 [in MetaCoq.PCUIC.PCUICContextConversion]
cf:326 [in MetaCoq.PCUIC.PCUICSubstitution]
cf:327 [in MetaCoq.PCUIC.PCUICEquality]
cf:327 [in MetaCoq.PCUIC.PCUICSR]
cf:33 [in MetaCoq.PCUIC.PCUICProgress]
cf:33 [in MetaCoq.PCUIC.PCUICCumulativity]
cf:33 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
cf:33 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
cf:33 [in MetaCoq.PCUIC.PCUICSafeLemmata]
cf:33 [in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
cf:331 [in MetaCoq.PCUIC.PCUICContextConversion]
cf:332 [in MetaCoq.PCUIC.PCUICInductives]
cf:333 [in MetaCoq.PCUIC.PCUICContextConversion]
cf:336 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cf:337 [in MetaCoq.PCUIC.PCUICContextConversion]
cf:34 [in MetaCoq.PCUIC.PCUICArities]
cf:34 [in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
cf:34 [in MetaCoq.PCUIC.PCUICContexts]
cf:341 [in MetaCoq.PCUIC.PCUICContextConversion]
cf:342 [in MetaCoq.PCUIC.PCUICInductives]
cf:345 [in MetaCoq.PCUIC.PCUICSubstitution]
cf:345 [in MetaCoq.PCUIC.PCUICContextConversion]
cf:347 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cf:348 [in MetaCoq.PCUIC.PCUICTyping]
cf:35 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
cf:35 [in MetaCoq.PCUIC.PCUICPrincipality]
cf:35 [in MetaCoq.PCUIC.PCUICGuardCondition]
cf:35 [in MetaCoq.PCUIC.PCUICSpine]
cf:350 [in MetaCoq.PCUIC.PCUICContextConversion]
cf:355 [in MetaCoq.PCUIC.PCUICInductives]
cf:356 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cf:356 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
cf:356 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
cf:36 [in MetaCoq.PCUIC.PCUICWeakeningEnv]
cf:36 [in MetaCoq.PCUIC.PCUICInductives]
cf:36 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cf:36 [in MetaCoq.PCUIC.PCUICEquality]
cf:36 [in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
cf:36 [in MetaCoq.PCUIC.PCUICSR]
cf:36 [in MetaCoq.SafeChecker.PCUICTypeChecker]
cf:361 [in MetaCoq.PCUIC.PCUICInductives]
cf:362 [in MetaCoq.PCUIC.PCUICContextConversion]
cf:366 [in MetaCoq.PCUIC.PCUICInductives]
cf:367 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
cf:367 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cf:369 [in MetaCoq.Template.EtaExpand]
cf:369 [in MetaCoq.PCUIC.PCUICProgress]
cf:369 [in MetaCoq.PCUIC.PCUICSubstitution]
cf:37 [in MetaCoq.PCUIC.PCUICElimination]
cf:37 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
cf:37 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
cf:372 [in MetaCoq.PCUIC.PCUICInductives]
cf:375 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cf:375 [in MetaCoq.Template.Checker]
cf:377 [in MetaCoq.PCUIC.PCUICInductives]
cf:378 [in MetaCoq.PCUIC.PCUICContextConversion]
cf:379 [in MetaCoq.PCUIC.PCUICProgress]
cf:38 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
cf:38 [in MetaCoq.PCUIC.Typing.PCUICInstTyp]
cf:38 [in MetaCoq.PCUIC.PCUICConvCumInversion]
cf:38 [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
cf:38 [in MetaCoq.PCUIC.TemplateToPCUICExpanded]
cf:382 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
cf:382 [in MetaCoq.PCUIC.PCUICInductives]
cf:382 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cf:383 [in MetaCoq.PCUIC.PCUICContextConversion]
cf:385 [in MetaCoq.SafeChecker.PCUICEqualityDec]
cf:386 [in MetaCoq.PCUIC.PCUICSubstitution]
cf:387 [in MetaCoq.PCUIC.PCUICProgress]
cf:387 [in MetaCoq.PCUIC.PCUICEquality]
cf:39 [in MetaCoq.PCUIC.PCUICPrincipality]
cf:39 [in MetaCoq.PCUIC.PCUICContexts]
cf:390 [in MetaCoq.PCUIC.PCUICInductives]
cf:390 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cf:390 [in MetaCoq.PCUIC.PCUICEquality]
cf:390 [in MetaCoq.PCUIC.PCUICContextConversion]
cf:395 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
cf:396 [in MetaCoq.PCUIC.PCUICSubstitution]
cf:396 [in MetaCoq.PCUIC.PCUICContextConversion]
cf:397 [in MetaCoq.PCUIC.PCUICSubstitution]
cf:398 [in MetaCoq.PCUIC.PCUICSubstitution]
cf:399 [in MetaCoq.PCUIC.PCUICProgress]
cf:399 [in MetaCoq.PCUIC.PCUICInductives]
cf:4 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
cf:4 [in MetaCoq.PCUIC.PCUICSN]
cf:4 [in MetaCoq.SafeChecker.PCUICSafeConversion]
cf:4 [in MetaCoq.PCUIC.PCUICConversion]
cf:4 [in MetaCoq.PCUIC.PCUICContexts]
cf:40 [in MetaCoq.PCUIC.PCUICWeakeningEnv]
cf:40 [in MetaCoq.PCUIC.PCUICCumulativity]
cf:40 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
cf:40 [in MetaCoq.PCUIC.PCUICSubstitution]
cf:40 [in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
cf:40 [in MetaCoq.PCUIC.Typing.PCUICWeakeningTyp]
cf:40 [in MetaCoq.PCUIC.Conversion.PCUICClosedConv]
cf:40 [in MetaCoq.PCUIC.PCUICSpine]
cf:400 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
cf:400 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cf:401 [in MetaCoq.PCUIC.PCUICContextConversion]
cf:403 [in MetaCoq.PCUIC.PCUICSubstitution]
cf:403 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cf:403 [in MetaCoq.PCUIC.PCUICConversion]
cf:406 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cf:408 [in MetaCoq.PCUIC.PCUICContextConversion]
cf:412 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cf:413 [in MetaCoq.PCUIC.PCUICInductives]
cf:413 [in MetaCoq.PCUIC.PCUICConversion]
cf:414 [in MetaCoq.Template.EtaExpand]
cf:416 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cf:416 [in MetaCoq.PCUIC.PCUICContextConversion]
cf:417 [in MetaCoq.PCUIC.PCUICProgress]
cf:42 [in MetaCoq.PCUIC.PCUICProgress]
cf:42 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
cf:422 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
cf:423 [in MetaCoq.PCUIC.PCUICSpine]
cf:424 [in MetaCoq.Template.EtaExpand]
cf:424 [in MetaCoq.PCUIC.PCUICProgress]
cf:428 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
cf:429 [in MetaCoq.PCUIC.PCUICInductives]
cf:429 [in MetaCoq.PCUIC.PCUICConversion]
cf:43 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cf:43 [in MetaCoq.PCUIC.PCUICPrincipality]
cf:43 [in MetaCoq.Template.EnvMap]
cf:43 [in MetaCoq.PCUIC.TemplateToPCUICExpanded]
cf:430 [in MetaCoq.Template.EtaExpand]
cf:431 [in MetaCoq.PCUIC.PCUICSubstitution]
cf:431 [in MetaCoq.PCUIC.PCUICEquality]
cf:432 [in MetaCoq.PCUIC.PCUICProgress]
cf:434 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
cf:434 [in MetaCoq.PCUIC.PCUICConversion]
cf:436 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cf:437 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
cf:438 [in MetaCoq.PCUIC.PCUICSubstitution]
cf:438 [in MetaCoq.PCUIC.PCUICEquality]
cf:439 [in MetaCoq.Template.EtaExpand]
cf:439 [in MetaCoq.Template.EnvironmentTyping]
cf:44 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
cf:44 [in MetaCoq.PCUIC.PCUICWeakeningEnv]
cf:44 [in MetaCoq.PCUIC.PCUICCumulativity]
cf:44 [in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
cf:44 [in MetaCoq.PCUIC.PCUICGlobalEnv]
cf:440 [in MetaCoq.PCUIC.PCUICConversion]
cf:441 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
cf:442 [in MetaCoq.PCUIC.PCUICInductives]
cf:443 [in MetaCoq.PCUIC.PCUICProgress]
cf:446 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
cf:446 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cf:449 [in MetaCoq.PCUIC.PCUICProgress]
cf:45 [in MetaCoq.PCUIC.PCUICArities]
cf:45 [in MetaCoq.SafeChecker.PCUICTypeChecker]
cf:452 [in MetaCoq.PCUIC.PCUICTyping]
cf:453 [in MetaCoq.PCUIC.PCUICProgress]
cf:453 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
cf:453 [in MetaCoq.PCUIC.PCUICSubstitution]
cf:458 [in MetaCoq.PCUIC.PCUICSubstitution]
cf:459 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cf:46 [in MetaCoq.PCUIC.PCUICSubstitution]
cf:46 [in MetaCoq.PCUIC.Conversion.PCUICClosedConv]
cf:460 [in MetaCoq.PCUIC.PCUICNormal]
cf:461 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cf:466 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
cf:467 [in MetaCoq.Template.Universes]
cf:469 [in MetaCoq.Template.common.uGraph]
cf:469 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cf:47 [in MetaCoq.PCUIC.PCUICCumulativity]
cf:47 [in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
cf:47 [in MetaCoq.PCUIC.PCUICPrincipality]
cf:47 [in MetaCoq.PCUIC.PCUICContexts]
cf:47 [in MetaCoq.PCUIC.PCUICSpine]
cf:470 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cf:470 [in MetaCoq.PCUIC.PCUICSpine]
cf:472 [in MetaCoq.PCUIC.PCUICNormal]
cf:472 [in MetaCoq.PCUIC.PCUICEquality]
cf:474 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
cf:476 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cf:477 [in MetaCoq.PCUIC.PCUICNormal]
cf:477 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
cf:479 [in MetaCoq.PCUIC.PCUICEquality]
cf:48 [in MetaCoq.PCUIC.PCUICWeakeningEnv]
cf:48 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
cf:48 [in MetaCoq.PCUIC.Typing.PCUICWeakeningTyp]
cf:48 [in MetaCoq.PCUIC.TemplateToPCUICExpanded]
cf:48 [in MetaCoq.SafeChecker.PCUICSafeChecker]
cf:481 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
cf:483 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cf:484 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
cf:487 [in MetaCoq.PCUIC.PCUICNormal]
cf:489 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cf:49 [in MetaCoq.PCUIC.PCUICElimination]
cf:49 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
cf:49 [in MetaCoq.PCUIC.PCUICGlobalEnv]
cf:491 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
cf:494 [in MetaCoq.PCUIC.PCUICConversion]
cf:495 [in MetaCoq.PCUIC.PCUICInductives]
cf:496 [in MetaCoq.PCUIC.PCUICNormal]
cf:496 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cf:497 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
cf:5 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
cf:5 [in MetaCoq.PCUIC.PCUICArities]
cf:5 [in MetaCoq.PCUIC.PCUICAlpha]
cf:5 [in MetaCoq.SafeChecker.SafeTemplateChecker]
cf:5 [in MetaCoq.PCUIC.PCUICCanonicity]
cf:50 [in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
cf:50 [in MetaCoq.PCUIC.PCUICCanonicity]
cf:500 [in MetaCoq.PCUIC.PCUICConversion]
cf:500 [in MetaCoq.PCUIC.PCUICSR]
cf:500 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
cf:501 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cf:506 [in MetaCoq.PCUIC.PCUICSR]
cf:507 [in MetaCoq.PCUIC.PCUICInductives]
cf:508 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cf:509 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cf:51 [in MetaCoq.PCUIC.PCUICConvCumInversion]
cf:51 [in MetaCoq.PCUIC.PCUICPrincipality]
cf:512 [in MetaCoq.PCUIC.PCUICSR]
cf:514 [in MetaCoq.PCUIC.PCUICNormal]
cf:516 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cf:518 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cf:519 [in MetaCoq.PCUIC.PCUICInductives]
cf:519 [in MetaCoq.PCUIC.PCUICSR]
cf:52 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
cf:52 [in MetaCoq.PCUIC.PCUICCumulativity]
cf:52 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
cf:52 [in MetaCoq.PCUIC.PCUICSubstitution]
cf:52 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cf:52 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
cf:52 [in MetaCoq.PCUIC.Conversion.PCUICClosedConv]
cf:522 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cf:526 [in MetaCoq.Template.Typing]
cf:526 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cf:526 [in MetaCoq.PCUIC.PCUICSR]
cf:527 [in MetaCoq.Template.EtaExpand]
cf:528 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
cf:53 [in MetaCoq.PCUIC.PCUICWeakeningEnv]
cf:53 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
cf:53 [in MetaCoq.Erasure.Prelim]
cf:530 [in MetaCoq.PCUIC.PCUICInductives]
cf:531 [in MetaCoq.Template.EtaExpand]
cf:533 [in MetaCoq.PCUIC.PCUICSR]
cf:536 [in MetaCoq.PCUIC.PCUICInductives]
cf:536 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cf:537 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cf:538 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
cf:539 [in MetaCoq.PCUIC.PCUICNormal]
cf:54 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
cf:54 [in MetaCoq.PCUIC.Typing.PCUICWeakeningTyp]
cf:54 [in MetaCoq.PCUIC.PCUICSpine]
cf:540 [in MetaCoq.Template.EtaExpand]
cf:540 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
cf:541 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cf:542 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
cf:544 [in MetaCoq.Template.EtaExpand]
cf:545 [in MetaCoq.PCUIC.PCUICSR]
cf:545 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
cf:549 [in MetaCoq.PCUIC.PCUICEquality]
cf:55 [in MetaCoq.SafeChecker.PCUICWfEnv]
cf:55 [in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
cf:55 [in MetaCoq.PCUIC.PCUICGlobalEnv]
cf:55 [in MetaCoq.PCUIC.PCUICContexts]
cf:551 [in MetaCoq.PCUIC.PCUICSR]
cf:553 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
cf:556 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
cf:556 [in MetaCoq.PCUIC.PCUICSR]
cf:556 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
cf:557 [in MetaCoq.PCUIC.PCUICEquality]
cf:559 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
cf:56 [in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
cf:56 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
cf:56 [in MetaCoq.PCUIC.PCUICSR]
cf:562 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
cf:562 [in MetaCoq.Template.Typing]
cf:562 [in MetaCoq.PCUIC.PCUICEquality]
cf:563 [in MetaCoq.PCUIC.PCUICSubstitution]
cf:563 [in MetaCoq.PCUIC.PCUICSR]
cf:568 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cf:569 [in MetaCoq.PCUIC.PCUICInductives]
cf:57 [in MetaCoq.PCUIC.PCUICCumulativity]
cf:57 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
cf:57 [in MetaCoq.PCUIC.TemplateToPCUICExpanded]
cf:570 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
cf:570 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
cf:570 [in MetaCoq.PCUIC.PCUICSR]
cf:575 [in MetaCoq.PCUIC.PCUICInductives]
cf:58 [in MetaCoq.PCUIC.PCUICElimination]
cf:58 [in MetaCoq.PCUIC.PCUICWeakeningEnv]
cf:58 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
cf:58 [in MetaCoq.PCUIC.PCUICGlobalEnv]
cf:580 [in MetaCoq.PCUIC.PCUICSR]
cf:582 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
cf:582 [in MetaCoq.PCUIC.PCUICSubstitution]
cf:582 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cf:588 [in MetaCoq.PCUIC.PCUICSR]
cf:59 [in MetaCoq.PCUIC.PCUICProgress]
cf:59 [in MetaCoq.SafeChecker.PCUICWfEnv]
cf:591 [in MetaCoq.PCUIC.PCUICSubstitution]
cf:596 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
cf:599 [in MetaCoq.PCUIC.PCUICSubstitution]
cf:6 [in MetaCoq.SafeChecker.Extraction]
cf:6 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
cf:6 [in MetaCoq.PCUIC.PCUICInductives]
cf:6 [in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
cf:6 [in MetaCoq.SafeChecker.PCUICSafeReduce]
cf:6 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
cf:6 [in MetaCoq.SafeChecker.PCUICTypeChecker]
cf:60 [in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
cf:604 [in MetaCoq.PCUIC.PCUICParallelReduction]
cf:605 [in MetaCoq.PCUIC.PCUICSR]
cf:606 [in MetaCoq.PCUIC.PCUICSubstitution]
cf:606 [in MetaCoq.PCUIC.PCUICInductives]
cf:606 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cf:607 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
cf:61 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
cf:61 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cf:61 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cf:61 [in MetaCoq.PCUIC.PCUICGlobalEnv]
cf:612 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cf:614 [in MetaCoq.PCUIC.PCUICInductives]
cf:615 [in MetaCoq.PCUIC.PCUICSubstitution]
cf:616 [in MetaCoq.PCUIC.PCUICSR]
cf:617 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cf:618 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
cf:62 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
cf:62 [in MetaCoq.PCUIC.PCUICSubstitution]
cf:62 [in MetaCoq.SafeChecker.PCUICSafeReduce]
cf:62 [in MetaCoq.PCUIC.PCUICPrincipality]
cf:62 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
cf:62 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
cf:62 [in MetaCoq.SafeChecker.PCUICTypeChecker]
cf:623 [in MetaCoq.Template.common.uGraph]
cf:623 [in MetaCoq.PCUIC.PCUICSR]
cf:624 [in MetaCoq.PCUIC.PCUICSubstitution]
cf:626 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cf:627 [in MetaCoq.Template.common.uGraph]
cf:629 [in MetaCoq.PCUIC.PCUICInductives]
cf:629 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cf:63 [in MetaCoq.PCUIC.PCUICCumulativity]
cf:63 [in MetaCoq.SafeChecker.PCUICWfEnv]
cf:63 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
cf:63 [in MetaCoq.PCUIC.TemplateToPCUICExpanded]
cf:63 [in MetaCoq.PCUIC.PCUICContexts]
cf:63 [in MetaCoq.Erasure.EOptimizePropDiscr]
cf:630 [in MetaCoq.PCUIC.PCUICSR]
cf:631 [in MetaCoq.Template.common.uGraph]
cf:633 [in MetaCoq.PCUIC.PCUICConfluence]
cf:634 [in MetaCoq.PCUIC.PCUICSubstitution]
cf:636 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cf:636 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cf:637 [in MetaCoq.PCUIC.PCUICInductives]
cf:637 [in MetaCoq.Template.common.uGraph]
cf:638 [in MetaCoq.PCUIC.PCUICSR]
cf:639 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
cf:64 [in MetaCoq.PCUIC.PCUICWeakeningEnv]
cf:64 [in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
cf:64 [in MetaCoq.PCUIC.PCUICConvCumInversion]
cf:64 [in MetaCoq.PCUIC.Typing.PCUICWeakeningTyp]
cf:64 [in MetaCoq.Erasure.Prelim]
cf:643 [in MetaCoq.PCUIC.PCUICSubstitution]
cf:643 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cf:643 [in MetaCoq.SafeChecker.PCUICSafeConversion]
cf:644 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cf:645 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
cf:645 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cf:647 [in MetaCoq.PCUIC.PCUICInductives]
cf:647 [in MetaCoq.PCUIC.PCUICEquality]
cf:648 [in MetaCoq.Template.common.uGraph]
cf:65 [in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
cf:651 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
cf:652 [in MetaCoq.Template.Universes]
cf:653 [in MetaCoq.PCUIC.PCUICSR]
cf:654 [in MetaCoq.Template.common.uGraph]
cf:655 [in MetaCoq.PCUIC.PCUICEquality]
cf:657 [in MetaCoq.PCUIC.PCUICConfluence]
cf:658 [in MetaCoq.Template.Universes]
cf:659 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
cf:659 [in MetaCoq.PCUIC.PCUICEquality]
cf:66 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
cf:66 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
cf:66 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
cf:66 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
cf:662 [in MetaCoq.Template.Universes]
cf:663 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cf:665 [in MetaCoq.PCUIC.PCUICConfluence]
cf:665 [in MetaCoq.PCUIC.PCUICSR]
cf:666 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
cf:667 [in MetaCoq.Template.common.uGraph]
cf:668 [in MetaCoq.Template.common.uGraph]
cf:669 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cf:67 [in MetaCoq.SafeChecker.PCUICWfReduction]
cf:67 [in MetaCoq.PCUIC.PCUICSR]
cf:67 [in MetaCoq.PCUIC.TemplateToPCUICExpanded]
cf:672 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cf:673 [in MetaCoq.Template.Universes]
cf:675 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
cf:676 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cf:676 [in MetaCoq.PCUIC.PCUICSR]
cf:677 [in MetaCoq.Template.common.uGraph]
cf:68 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
cf:68 [in MetaCoq.PCUIC.PCUICElimination]
cf:681 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cf:682 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
cf:684 [in MetaCoq.Template.common.uGraph]
cf:688 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cf:688 [in MetaCoq.PCUIC.PCUICSR]
cf:69 [in MetaCoq.PCUIC.PCUICCumulativity]
cf:69 [in MetaCoq.PCUIC.PCUICPrincipality]
cf:69 [in MetaCoq.Erasure.EOptimizePropDiscr]
cf:690 [in MetaCoq.Erasure.ErasureFunction]
cf:693 [in MetaCoq.Template.EnvironmentTyping]
cf:694 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cf:694 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cf:694 [in MetaCoq.PCUIC.PCUICSR]
cf:697 [in MetaCoq.Template.common.uGraph]
cf:699 [in MetaCoq.PCUIC.PCUICConfluence]
cf:7 [in MetaCoq.PCUIC.Typing.PCUICInstTyp]
cf:7 [in MetaCoq.PCUIC.PCUICElimination]
cf:7 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cf:7 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
cf:7 [in MetaCoq.Erasure.ErasureFunction]
cf:7 [in MetaCoq.PCUIC.PCUICConvCumInversion]
cf:7 [in MetaCoq.SafeChecker.SafeTemplateChecker]
cf:7 [in MetaCoq.PCUIC.PCUICProgram]
cf:7 [in MetaCoq.PCUIC.Conversion.PCUICClosedConv]
cf:70 [in MetaCoq.SafeChecker.PCUICWfEnv]
cf:70 [in MetaCoq.PCUIC.PCUICConvCumInversion]
cf:70 [in MetaCoq.Template.TypingWf]
cf:70 [in MetaCoq.PCUIC.PCUICContexts]
cf:700 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cf:703 [in MetaCoq.PCUIC.PCUICSR]
cf:704 [in MetaCoq.Template.Typing]
cf:705 [in MetaCoq.Template.common.uGraph]
cf:705 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cf:708 [in MetaCoq.Template.EnvironmentTyping]
cf:709 [in MetaCoq.PCUIC.PCUICSR]
cf:71 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
cf:71 [in MetaCoq.PCUIC.Typing.PCUICWeakeningTyp]
cf:710 [in MetaCoq.Template.common.uGraph]
cf:711 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cf:712 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cf:715 [in MetaCoq.Template.common.uGraph]
cf:715 [in MetaCoq.PCUIC.PCUICSR]
cf:72 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
cf:72 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
cf:72 [in MetaCoq.PCUIC.PCUICSpine]
cf:721 [in MetaCoq.PCUIC.PCUICSR]
cf:723 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
cf:723 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cf:73 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cf:73 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
cf:731 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
cf:733 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
cf:733 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cf:733 [in MetaCoq.PCUIC.PCUICParallelReduction]
cf:734 [in MetaCoq.PCUIC.PCUICSR]
cf:74 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
cf:74 [in MetaCoq.PCUIC.PCUICCumulativity]
CF:74 [in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
cf:741 [in MetaCoq.PCUIC.PCUICSR]
cf:744 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cf:747 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cf:75 [in MetaCoq.PCUIC.PCUICInductives]
cf:75 [in MetaCoq.PCUIC.PCUICSR]
cf:750 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cf:753 [in MetaCoq.PCUIC.PCUICSR]
cf:757 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cf:759 [in MetaCoq.PCUIC.PCUICSR]
cf:761 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cf:763 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
cf:763 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cf:766 [in MetaCoq.PCUIC.PCUICSR]
cf:769 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cf:77 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
cf:77 [in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
cf:77 [in MetaCoq.PCUIC.Typing.PCUICWeakeningTyp]
cf:77 [in MetaCoq.Template.TypingWf]
cf:77 [in MetaCoq.PCUIC.PCUICContexts]
cf:772 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cf:773 [in MetaCoq.PCUIC.PCUICSR]
cf:78 [in MetaCoq.PCUIC.PCUICElimination]
cf:780 [in MetaCoq.PCUIC.PCUICTyping]
cf:780 [in MetaCoq.PCUIC.PCUICSR]
cf:781 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cf:782 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cf:786 [in MetaCoq.PCUIC.PCUICSR]
cf:788 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
cf:788 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cf:788 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cf:79 [in MetaCoq.PCUIC.PCUICCumulativity]
cf:79 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
cf:79 [in MetaCoq.PCUIC.PCUICSpine]
cf:792 [in MetaCoq.PCUIC.PCUICSR]
cf:793 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cf:798 [in MetaCoq.PCUIC.PCUICSR]
cf:8 [in MetaCoq.PCUIC.PCUICTransform]
cf:8 [in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
cf:8 [in MetaCoq.SafeChecker.PCUICSafeConversion]
cf:8 [in MetaCoq.PCUIC.PCUICConversion]
cf:8 [in MetaCoq.PCUIC.PCUICContextConversion]
cf:80 [in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
cf:80 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
cf:80 [in MetaCoq.PCUIC.PCUICConvCumInversion]
cf:801 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cf:801 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cf:802 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
cf:805 [in MetaCoq.PCUIC.PCUICSR]
cf:806 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
cf:81 [in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
cf:81 [in MetaCoq.PCUIC.PCUICSR]
cf:811 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cf:812 [in MetaCoq.PCUIC.PCUICSR]
cf:82 [in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
cf:828 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
cf:83 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
cf:83 [in MetaCoq.Template.TypingWf]
cf:83 [in MetaCoq.PCUIC.PCUICContexts]
cf:833 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
cf:84 [in MetaCoq.PCUIC.PCUICCumulativity]
cf:84 [in MetaCoq.PCUIC.Typing.PCUICWeakeningTyp]
cf:842 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
cf:846 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cf:85 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
cf:850 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
cf:851 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cf:852 [in MetaCoq.Erasure.ErasureFunction]
cf:857 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cf:86 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
cf:860 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
cf:860 [in MetaCoq.PCUIC.PCUICConfluence]
cf:863 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cf:867 [in MetaCoq.PCUIC.PCUICConfluence]
cf:869 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cf:87 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
cf:87 [in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
cf:87 [in MetaCoq.PCUIC.PCUICConversion]
cf:87 [in MetaCoq.PCUIC.PCUICContextConversion]
cf:87 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
cf:873 [in MetaCoq.PCUIC.PCUICConfluence]
cf:875 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
cf:877 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cf:88 [in MetaCoq.PCUIC.PCUICSubstitution]
cf:88 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cf:88 [in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
cf:88 [in MetaCoq.PCUIC.TemplateToPCUICExpanded]
cf:88 [in MetaCoq.Template.TypingWf]
cf:884 [in MetaCoq.PCUIC.PCUICConfluence]
cf:884 [in MetaCoq.PCUIC.PCUICSR]
cf:885 [in MetaCoq.PCUIC.PCUICConversion]
cf:886 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cf:89 [in MetaCoq.PCUIC.PCUICValidity]
cf:890 [in MetaCoq.PCUIC.PCUICConfluence]
cf:892 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
cf:898 [in MetaCoq.PCUIC.PCUICConfluence]
cf:899 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
cf:9 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
cf:9 [in MetaCoq.PCUIC.PCUICRedTypeIrrelevance]
cf:9 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
cf:9 [in MetaCoq.Examples.typing_correctness]
cf:90 [in MetaCoq.PCUIC.PCUICContextConversion]
cf:90 [in MetaCoq.PCUIC.PCUICSpine]
cf:902 [in MetaCoq.PCUIC.PCUICConfluence]
cf:903 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cf:908 [in MetaCoq.PCUIC.PCUICConfluence]
cf:91 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
cf:91 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
cf:911 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
cf:913 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
cf:915 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
cf:919 [in MetaCoq.PCUIC.PCUICConfluence]
cf:92 [in MetaCoq.PCUIC.Typing.PCUICWeakeningTyp]
cf:925 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cf:927 [in MetaCoq.PCUIC.PCUICTyping]
cf:93 [in MetaCoq.Erasure.ESubstitution]
cf:93 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
cf:93 [in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
cf:93 [in MetaCoq.PCUIC.TemplateToPCUICExpanded]
cf:93 [in MetaCoq.Template.TypingWf]
cf:934 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cf:936 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cf:94 [in MetaCoq.PCUIC.PCUICCumulativity]
cf:94 [in MetaCoq.PCUIC.PCUICPrincipality]
cf:94 [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
cf:943 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cf:943 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cf:949 [in MetaCoq.Template.Typing]
cf:95 [in MetaCoq.PCUIC.PCUICWeakeningEnv]
cf:95 [in MetaCoq.PCUIC.PCUICValidity]
cf:95 [in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
cf:953 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cf:96 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
cf:964 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cf:97 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
cf:97 [in MetaCoq.PCUIC.PCUICSubstitution]
cf:97 [in MetaCoq.SafeChecker.PCUICWfReduction]
cf:97 [in MetaCoq.PCUIC.Typing.PCUICWeakeningTyp]
cf:97 [in MetaCoq.PCUIC.PCUICSpine]
cf:971 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cf:975 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cf:98 [in MetaCoq.Template.EnvironmentTyping]
cf:98 [in MetaCoq.Template.common.uGraph]
cf:98 [in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
cf:987 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cf:99 [in MetaCoq.PCUIC.PCUICElimination]
cf:99 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
cf:99 [in MetaCoq.PCUIC.TemplateToPCUICExpanded]
cf:995 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
checkctx:960 [in MetaCoq.SafeChecker.PCUICSafeChecker]
checking_size:133 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
checking_size:399 [in MetaCoq.Template.EnvironmentTyping]
checking:211 [in MetaCoq.Template.EnvironmentTyping]
checking:251 [in MetaCoq.Template.EnvironmentTyping]
checking:288 [in MetaCoq.Template.EnvironmentTyping]
checking:360 [in MetaCoq.Template.EnvironmentTyping]
checking:393 [in MetaCoq.Template.EnvironmentTyping]
checks:29 [in MetaCoq.PCUIC.PCUICTyping]
checks:37 [in MetaCoq.PCUIC.PCUICTyping]
checks:590 [in MetaCoq.Template.Typing]
checks:597 [in MetaCoq.Template.Typing]
checkts:306 [in MetaCoq.SafeChecker.PCUICSafeChecker]
checkty:163 [in MetaCoq.SafeChecker.PCUICSafeChecker]
checkty:165 [in MetaCoq.SafeChecker.PCUICSafeChecker]
checkty:184 [in MetaCoq.SafeChecker.PCUICSafeChecker]
checkt:305 [in MetaCoq.SafeChecker.PCUICSafeChecker]
checkt:486 [in MetaCoq.SafeChecker.PCUICTypeChecker]
check_bodies:1012 [in MetaCoq.SafeChecker.PCUICSafeChecker]
check_npars:1007 [in MetaCoq.SafeChecker.PCUICSafeChecker]
check_pars:1006 [in MetaCoq.SafeChecker.PCUICSafeChecker]
check_var:1005 [in MetaCoq.SafeChecker.PCUICSafeChecker]
check_projs:898 [in MetaCoq.SafeChecker.PCUICSafeChecker]
check_length:894 [in MetaCoq.SafeChecker.PCUICSafeChecker]
check_elim:893 [in MetaCoq.SafeChecker.PCUICSafeChecker]
check_indices:892 [in MetaCoq.SafeChecker.PCUICSafeChecker]
check_eq:847 [in MetaCoq.SafeChecker.PCUICSafeChecker]
check_rel:846 [in MetaCoq.SafeChecker.PCUICSafeChecker]
check_na:845 [in MetaCoq.SafeChecker.PCUICSafeChecker]
check_indices:725 [in MetaCoq.SafeChecker.PCUICSafeChecker]
check_args:724 [in MetaCoq.SafeChecker.PCUICSafeChecker]
check_leq:698 [in MetaCoq.SafeChecker.PCUICSafeChecker]
check_closed:555 [in MetaCoq.SafeChecker.PCUICSafeChecker]
check_brs:1097 [in MetaCoq.SafeChecker.PCUICTypeChecker]
check_wfpctx_conv:1090 [in MetaCoq.SafeChecker.PCUICTypeChecker]
check_coind:1082 [in MetaCoq.SafeChecker.PCUICTypeChecker]
check_eq_bcontext:767 [in MetaCoq.SafeChecker.PCUICTypeChecker]
check:1244 [in MetaCoq.SafeChecker.PCUICSafeConversion]
check:177 [in MetaCoq.Template.EnvironmentTyping]
check:223 [in MetaCoq.SafeChecker.PCUICSafeChecker]
check:275 [in MetaCoq.SafeChecker.PCUICErrors]
check:396 [in MetaCoq.Template.Checker]
check:835 [in MetaCoq.SafeChecker.PCUICSafeConversion]
checkΔ:162 [in MetaCoq.SafeChecker.PCUICSafeChecker]
checkΔ:164 [in MetaCoq.SafeChecker.PCUICSafeChecker]
chop_args:1083 [in MetaCoq.SafeChecker.PCUICTypeChecker]
ci_relevance':40 [in MetaCoq.Template.Reflect]
ci_npar':39 [in MetaCoq.Template.Reflect]
ci_ind':38 [in MetaCoq.Template.Reflect]
ci_relevance:37 [in MetaCoq.Template.Reflect]
ci_npar:36 [in MetaCoq.Template.Reflect]
ci_ind:35 [in MetaCoq.Template.Reflect]
ci':119 [in MetaCoq.PCUIC.PCUICConvCumInversion]
ci':1467 [in MetaCoq.SafeChecker.PCUICSafeConversion]
ci':174 [in MetaCoq.Template.Checker]
ci':2082 [in MetaCoq.SafeChecker.PCUICSafeConversion]
ci':34 [in MetaCoq.Template.Reflect]
ci':42 [in MetaCoq.Translations.param_original]
ci':561 [in MetaCoq.SafeChecker.PCUICSafeConversion]
ci':58 [in MetaCoq.SafeChecker.PCUICErrors]
ci':68 [in MetaCoq.SafeChecker.PCUICErrors]
ci':78 [in MetaCoq.SafeChecker.PCUICErrors]
ci1:2146 [in MetaCoq.SafeChecker.PCUICSafeConversion]
ci1:2368 [in MetaCoq.SafeChecker.PCUICSafeConversion]
ci1:2383 [in MetaCoq.SafeChecker.PCUICSafeConversion]
ci2:2152 [in MetaCoq.SafeChecker.PCUICSafeConversion]
ci2:2374 [in MetaCoq.SafeChecker.PCUICSafeConversion]
ci2:2389 [in MetaCoq.SafeChecker.PCUICSafeConversion]
ci:1010 [in MetaCoq.PCUIC.PCUICInductiveInversion]
ci:1027 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
ci:103 [in MetaCoq.PCUIC.PCUICEtaExpand]
ci:103 [in MetaCoq.PCUIC.PCUICSR]
ci:1054 [in MetaCoq.Template.Typing]
ci:108 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
ci:108 [in MetaCoq.PCUIC.PCUICInversion]
ci:113 [in MetaCoq.Erasure.Extract]
ci:113 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
ci:114 [in MetaCoq.PCUIC.Syntax.PCUICCases]
ci:115 [in MetaCoq.PCUIC.PCUICConvCumInversion]
ci:123 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
ci:123 [in MetaCoq.Template.EtaExpand]
ci:124 [in MetaCoq.PCUIC.PCUICTyping]
ci:1248 [in MetaCoq.SafeChecker.PCUICSafeConversion]
ci:126 [in MetaCoq.Template.AstUtils]
ci:1279 [in MetaCoq.SafeChecker.PCUICSafeConversion]
ci:137 [in MetaCoq.PCUIC.PCUICInversion]
ci:137 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
ci:1430 [in MetaCoq.SafeChecker.PCUICSafeReduce]
ci:1461 [in MetaCoq.SafeChecker.PCUICSafeConversion]
ci:15 [in MetaCoq.PCUIC.PCUICReduction]
ci:153 [in MetaCoq.PCUIC.PCUICSR]
ci:157 [in MetaCoq.Erasure.ErasureProperties]
ci:159 [in MetaCoq.PCUIC.PCUICProgress]
ci:162 [in MetaCoq.Erasure.ErasureProperties]
ci:162 [in MetaCoq.Template.WcbvEval]
ci:164 [in MetaCoq.PCUIC.PCUICSR]
ci:169 [in MetaCoq.Erasure.ErasureProperties]
ci:173 [in MetaCoq.Template.Checker]
ci:174 [in MetaCoq.PCUIC.PCUICReduction]
ci:176 [in MetaCoq.Erasure.ErasureProperties]
ci:180 [in MetaCoq.PCUIC.Syntax.PCUICCases]
ci:184 [in MetaCoq.PCUIC.Syntax.PCUICCases]
ci:185 [in MetaCoq.PCUIC.PCUICElimination]
ci:188 [in MetaCoq.PCUIC.PCUICReduction]
ci:189 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
ci:190 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
ci:192 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
ci:192 [in MetaCoq.PCUIC.PCUICParallelReduction]
ci:196 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
ci:198 [in MetaCoq.Template.EtaExpand]
ci:199 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
ci:20 [in MetaCoq.Erasure.ESpineView]
ci:200 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
ci:205 [in MetaCoq.PCUIC.PCUICWcbvEval]
ci:2059 [in MetaCoq.SafeChecker.PCUICSafeConversion]
ci:206 [in MetaCoq.Template.Ast]
ci:2081 [in MetaCoq.SafeChecker.PCUICSafeConversion]
ci:209 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
ci:209 [in MetaCoq.PCUIC.PCUICTyping]
ci:21 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
ci:210 [in MetaCoq.PCUIC.PCUICWcbvEval]
ci:212 [in MetaCoq.PCUIC.PCUICParallelReduction]
ci:214 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
ci:216 [in MetaCoq.PCUIC.Syntax.PCUICCases]
ci:216 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
ci:217 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
ci:219 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
ci:220 [in MetaCoq.PCUIC.PCUICInductiveInversion]
ci:223 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
ci:224 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
ci:225 [in MetaCoq.PCUIC.PCUICTyping]
ci:230 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
ci:230 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
ci:234 [in MetaCoq.SafeChecker.PCUICSafeReduce]
ci:2340 [in MetaCoq.SafeChecker.PCUICSafeConversion]
ci:236 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
ci:238 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
ci:239 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
ci:24 [in MetaCoq.PCUIC.PCUICSafeLemmata]
ci:242 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
ci:242 [in MetaCoq.PCUIC.PCUICReduction]
ci:243 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
ci:247 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
ci:248 [in MetaCoq.PCUIC.PCUICReduction]
ci:260 [in MetaCoq.PCUIC.PCUICReduction]
ci:261 [in MetaCoq.Template.Typing]
ci:264 [in MetaCoq.PCUIC.PCUICParallelReduction]
ci:27 [in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
ci:276 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
ci:277 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
ci:280 [in MetaCoq.PCUIC.PCUICSafeLemmata]
ci:282 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
ci:29 [in MetaCoq.Template.Induction]
ci:295 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
ci:295 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
ci:297 [in MetaCoq.PCUIC.PCUICSafeLemmata]
ci:3 [in MetaCoq.PCUIC.PCUICProgress]
ci:30 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
ci:309 [in MetaCoq.PCUIC.PCUICProgress]
ci:310 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
ci:311 [in MetaCoq.PCUIC.PCUICWcbvEval]
ci:32 [in MetaCoq.Template.BasicAst]
ci:322 [in MetaCoq.Erasure.EArities]
ci:322 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
ci:326 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
ci:327 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
ci:33 [in MetaCoq.Template.WfAst]
ci:33 [in MetaCoq.Template.Reflect]
ci:33 [in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
ci:331 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
ci:332 [in MetaCoq.Erasure.EArities]
ci:34 [in MetaCoq.SafeChecker.PCUICWfReduction]
ci:342 [in MetaCoq.Template.Typing]
ci:35 [in MetaCoq.PCUIC.PCUICEtaExpand]
ci:35 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
ci:354 [in MetaCoq.PCUIC.PCUICSR]
ci:359 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
ci:36 [in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
ci:368 [in MetaCoq.PCUIC.PCUICParallelReduction]
ci:368 [in MetaCoq.PCUIC.PCUICSR]
ci:373 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
ci:377 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
ci:378 [in MetaCoq.PCUIC.PCUICNormal]
ci:38 [in MetaCoq.SafeChecker.PCUICWfReduction]
ci:381 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
ci:383 [in MetaCoq.PCUIC.PCUICSpine]
ci:384 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
ci:387 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
ci:391 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
ci:392 [in MetaCoq.PCUIC.PCUICParallelReduction]
ci:394 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
ci:405 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
ci:408 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
ci:41 [in MetaCoq.PCUIC.PCUICElimination]
ci:416 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
ci:419 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
ci:422 [in MetaCoq.PCUIC.PCUICSR]
ci:428 [in MetaCoq.PCUIC.PCUICSR]
ci:438 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
ci:44 [in MetaCoq.PCUIC.PCUICTyping]
ci:440 [in MetaCoq.PCUIC.PCUICProgress]
ci:440 [in MetaCoq.PCUIC.PCUICSR]
ci:445 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
ci:459 [in MetaCoq.PCUIC.PCUICParallelReduction]
ci:46 [in MetaCoq.Erasure.Extract]
ci:4665 [in MetaCoq.SafeChecker.PCUICSafeConversion]
ci:467 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
ci:476 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
ci:4863 [in MetaCoq.SafeChecker.PCUICSafeConversion]
ci:4872 [in MetaCoq.SafeChecker.PCUICSafeConversion]
ci:489 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
ci:5 [in MetaCoq.PCUIC.PCUICSafeLemmata]
ci:50 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
ci:53 [in MetaCoq.PCUIC.PCUICElimination]
ci:53 [in MetaCoq.SafeChecker.PCUICErrors]
ci:54 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
ci:551 [in MetaCoq.PCUIC.PCUICTyping]
ci:557 [in MetaCoq.SafeChecker.PCUICSafeConversion]
ci:57 [in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
ci:592 [in MetaCoq.PCUIC.PCUICSpine]
ci:60 [in MetaCoq.PCUIC.Syntax.PCUICCases]
ci:62 [in MetaCoq.PCUIC.PCUICElimination]
ci:621 [in MetaCoq.PCUIC.PCUICConversion]
ci:63 [in MetaCoq.SafeChecker.PCUICErrors]
ci:633 [in MetaCoq.PCUIC.PCUICInductives]
ci:641 [in MetaCoq.PCUIC.PCUICInductives]
ci:648 [in MetaCoq.Template.Typing]
ci:65 [in MetaCoq.PCUIC.PCUICValidity]
ci:651 [in MetaCoq.PCUIC.PCUICInductives]
ci:656 [in MetaCoq.PCUIC.PCUICConversion]
ci:66 [in MetaCoq.PCUIC.PCUICTyping]
ci:664 [in MetaCoq.PCUIC.PCUICConversion]
ci:669 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
ci:68 [in MetaCoq.Template.Induction]
ci:70 [in MetaCoq.PCUIC.PCUICWcbvEval]
ci:70 [in MetaCoq.Template.WcbvEval]
ci:708 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
ci:708 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
ci:715 [in MetaCoq.SafeChecker.PCUICTypeChecker]
ci:73 [in MetaCoq.SafeChecker.PCUICErrors]
ci:73 [in MetaCoq.PCUIC.PCUICReduction]
ci:742 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
ci:769 [in MetaCoq.SafeChecker.PCUICTypeChecker]
ci:772 [in MetaCoq.SafeChecker.PCUICTypeChecker]
ci:80 [in MetaCoq.PCUIC.PCUICReduction]
ci:804 [in MetaCoq.PCUIC.PCUICInductiveInversion]
ci:812 [in MetaCoq.SafeChecker.PCUICSafeConversion]
ci:85 [in MetaCoq.PCUIC.PCUICReduction]
ci:874 [in MetaCoq.PCUIC.PCUICTyping]
ci:876 [in MetaCoq.PCUIC.PCUICReduction]
ci:891 [in MetaCoq.PCUIC.PCUICReduction]
ci:896 [in MetaCoq.PCUIC.PCUICReduction]
ci:90 [in MetaCoq.PCUIC.PCUICReduction]
ci:901 [in MetaCoq.PCUIC.PCUICReduction]
ci:909 [in MetaCoq.PCUIC.PCUICInductiveInversion]
ci:909 [in MetaCoq.PCUIC.PCUICReduction]
ci:913 [in MetaCoq.PCUIC.PCUICInductiveInversion]
ci:94 [in MetaCoq.Template.Typing]
ci:941 [in MetaCoq.PCUIC.PCUICInductiveInversion]
ci:947 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
ci:954 [in MetaCoq.PCUIC.PCUICReduction]
ci:959 [in MetaCoq.PCUIC.PCUICInductiveInversion]
ci:966 [in MetaCoq.PCUIC.PCUICReduction]
ci:977 [in MetaCoq.PCUIC.PCUICInductiveInversion]
ci:98 [in MetaCoq.Template.WfAst]
ci:987 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
ci:993 [in MetaCoq.PCUIC.PCUICInductiveInversion]
closedargs:570 [in MetaCoq.SafeChecker.PCUICSafeChecker]
cl:103 [in MetaCoq.Examples.tauto]
cl:27 [in MetaCoq.Examples.tauto]
cl:60 [in MetaCoq.Examples.tauto]
cl:92 [in MetaCoq.Examples.tauto]
cmp:11 [in MetaCoq.Template.utils.MCCompare]
cnv:266 [in MetaCoq.Template.Checker]
cnv:267 [in MetaCoq.Template.Checker]
codom':197 [in MetaCoq.PCUIC.PCUICConversion]
codom':206 [in MetaCoq.PCUIC.PCUICConversion]
codom':215 [in MetaCoq.PCUIC.PCUICConversion]
codom':223 [in MetaCoq.PCUIC.PCUICConversion]
codom:116 [in MetaCoq.PCUIC.PCUICConversion]
codom:116 [in MetaCoq.PCUIC.PCUICCanonicity]
codom:122 [in MetaCoq.PCUIC.PCUICConversion]
codom:128 [in MetaCoq.PCUIC.PCUICCanonicity]
codom:194 [in MetaCoq.PCUIC.PCUICConversion]
codom:202 [in MetaCoq.PCUIC.PCUICConversion]
codom:211 [in MetaCoq.PCUIC.PCUICConversion]
codom:211 [in MetaCoq.PCUIC.PCUICCanonicity]
codom:222 [in MetaCoq.PCUIC.PCUICConversion]
codom:366 [in MetaCoq.PCUIC.PCUICSpine]
codom:367 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
codom:466 [in MetaCoq.PCUIC.PCUICConversion]
codom:473 [in MetaCoq.PCUIC.PCUICConversion]
codom:496 [in MetaCoq.SafeChecker.PCUICSafeChecker]
codom:74 [in MetaCoq.Erasure.EOptimizePropDiscr]
coe:104 [in MetaCoq.PCUIC.utils.PCUICUtils]
coe:21 [in MetaCoq.PCUIC.utils.PCUICUtils]
coe:62 [in MetaCoq.PCUIC.utils.PCUICUtils]
compare_global_instance_gen:60 [in MetaCoq.SafeChecker.PCUICEqualityDec]
compose:131 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
compose:143 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
compose:158 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
compose:170 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
compose:182 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
conclargs:363 [in MetaCoq.SafeChecker.PCUICSafeChecker]
concl:583 [in MetaCoq.PCUIC.PCUICSpine]
cons:121 [in MetaCoq.PCUIC.PCUICInversion]
cons:55 [in MetaCoq.PCUIC.PCUICTyping]
convts:512 [in MetaCoq.SafeChecker.PCUICTypeChecker]
convt:511 [in MetaCoq.SafeChecker.PCUICTypeChecker]
conv_pb:56 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
conv_pb:49 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
conv_pctx:123 [in MetaCoq.PCUIC.PCUICInversion]
conv_pb:91 [in MetaCoq.SafeChecker.PCUICWfEnv]
conv_pb:282 [in MetaCoq.Template.Checker]
conv_pctx:57 [in MetaCoq.PCUIC.PCUICTyping]
count:5 [in MetaCoq.Template.EtaExpand]
cproperty:257 [in MetaCoq.Template.EnvironmentTyping]
cproperty:290 [in MetaCoq.Template.EnvironmentTyping]
cred:213 [in MetaCoq.Template.Checker]
cred:218 [in MetaCoq.Template.Checker]
cred:270 [in MetaCoq.Template.Checker]
csize:366 [in MetaCoq.Template.EnvironmentTyping]
css:413 [in MetaCoq.SafeChecker.PCUICSafeChecker]
cstrapp:101 [in MetaCoq.PCUIC.Syntax.PCUICCases]
cstrapp:393 [in MetaCoq.Template.Ast]
cstrs:10 [in MetaCoq.SafeChecker.PCUICTypeChecker]
cstrs:2 [in MetaCoq.SafeChecker.PCUICSafeChecker]
cstrs:202 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
cstrs:34 [in MetaCoq.SafeChecker.PCUICSafeChecker]
cstrs:340 [in MetaCoq.Template.Checker]
cstrs:37 [in MetaCoq.SafeChecker.PCUICSafeChecker]
cstrs:4 [in MetaCoq.Examples.constructor_tac]
cstrs:407 [in MetaCoq.SafeChecker.PCUICSafeChecker]
cstrs:492 [in MetaCoq.Template.Universes]
cstrs:511 [in MetaCoq.Template.EnvironmentTyping]
cstrs:513 [in MetaCoq.Template.common.uGraph]
cstrs:515 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cstrs:517 [in MetaCoq.Template.common.uGraph]
cstrs:519 [in MetaCoq.Template.common.uGraph]
cstrs:520 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cstrs:526 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cstrs:529 [in MetaCoq.Template.EnvironmentTyping]
cstrs:532 [in MetaCoq.Template.EnvironmentTyping]
cstrs:533 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cstrs:536 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cstrs:544 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cstrs:547 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cstrs:558 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cstrs:60 [in MetaCoq.Template.Checker]
cstrs:618 [in MetaCoq.SafeChecker.PCUICSafeChecker]
cstrs:627 [in MetaCoq.SafeChecker.PCUICSafeChecker]
cstrs:666 [in MetaCoq.Template.common.uGraph]
cstrs:672 [in MetaCoq.Template.EnvironmentTyping]
cstrs:73 [in MetaCoq.Template.Checker]
cstrs:91 [in MetaCoq.Template.Checker]
cstrv:533 [in MetaCoq.Template.EnvironmentTyping]
cstr_br_ctx:1020 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cstr_br_ctx:968 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cstr:12 [in MetaCoq.Template.EnvironmentTyping]
cstr:16 [in MetaCoq.Erasure.EGlobalEnv]
cstr:160 [in MetaCoq.Erasure.Extract]
cstr:391 [in MetaCoq.Template.Ast]
cstr:402 [in MetaCoq.Template.Universes]
cstr:405 [in MetaCoq.Template.Universes]
cstr:410 [in MetaCoq.SafeChecker.PCUICSafeChecker]
cstr:486 [in MetaCoq.Template.Universes]
cstr:512 [in MetaCoq.Template.common.uGraph]
cstr:530 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cstr:60 [in MetaCoq.Erasure.EPretty]
cstr:622 [in MetaCoq.SafeChecker.PCUICSafeChecker]
cstr:625 [in MetaCoq.SafeChecker.PCUICSafeChecker]
cstr:641 [in MetaCoq.SafeChecker.PCUICSafeChecker]
cstr:72 [in MetaCoq.PCUIC.Syntax.PCUICViews]
cstr:76 [in MetaCoq.Erasure.EPretty]
cstr:99 [in MetaCoq.PCUIC.Syntax.PCUICCases]
cst':138 [in MetaCoq.Erasure.EDeps]
cst':410 [in MetaCoq.Template.Universes]
cst':828 [in MetaCoq.Erasure.ErasureFunction]
cst:1027 [in MetaCoq.Template.Typing]
cst:103 [in MetaCoq.PCUIC.PCUICWeakeningEnv]
cst:111 [in MetaCoq.PCUIC.PCUICTyping]
cst:12 [in MetaCoq.SafeChecker.PCUICSafeConversion]
cst:1282 [in MetaCoq.PCUIC.PCUICConfluence]
cst:132 [in MetaCoq.PCUIC.PCUICProgress]
cst:137 [in MetaCoq.Erasure.EDeps]
cst:146 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
cst:149 [in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
cst:155 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
cst:159 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
cst:178 [in MetaCoq.PCUIC.PCUICSubstitution]
cst:182 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
cst:184 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
cst:189 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
cst:193 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
cst:246 [in MetaCoq.Template.TypingWf]
cst:27 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
cst:282 [in MetaCoq.PCUIC.PCUICProgress]
cst:29 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
cst:3 [in MetaCoq.Erasure.EExtends]
cst:31 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
cst:378 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
cst:38 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
cst:39 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
cst:409 [in MetaCoq.Template.Universes]
cst:431 [in MetaCoq.Template.Universes]
cst:46 [in MetaCoq.PCUIC.PCUICWfUniverses]
cst:462 [in MetaCoq.Template.Universes]
cst:524 [in MetaCoq.PCUIC.PCUICTyping]
cst:55 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cst:56 [in MetaCoq.Template.Checker]
cst:57 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
cst:58 [in MetaCoq.Template.Checker]
cst:60 [in MetaCoq.PCUIC.Typing.PCUICWeakeningTyp]
cst:632 [in MetaCoq.Template.Typing]
cst:689 [in MetaCoq.SafeChecker.PCUICSafeConversion]
cst:70 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
cst:74 [in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
cst:79 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
cst:827 [in MetaCoq.Erasure.ErasureFunction]
cst:847 [in MetaCoq.PCUIC.PCUICTyping]
cs'':44 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
cs':43 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
cs0:623 [in MetaCoq.SafeChecker.PCUICSafeChecker]
cs0:642 [in MetaCoq.SafeChecker.PCUICSafeChecker]
cs:123 [in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
cs:133 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
cs:142 [in MetaCoq.PCUIC.PCUICInductives]
cs:1422 [in MetaCoq.Erasure.ErasureFunction]
cs:143 [in MetaCoq.PCUIC.PCUICElimination]
cs:149 [in MetaCoq.PCUIC.PCUICElimination]
cs:201 [in MetaCoq.Template.TypingWf]
cs:214 [in MetaCoq.Template.TypingWf]
cs:218 [in MetaCoq.PCUIC.PCUICSubstitution]
cs:228 [in MetaCoq.PCUIC.PCUICSubstitution]
cs:29 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
cs:304 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cs:325 [in MetaCoq.SafeChecker.PCUICSafeChecker]
cs:33 [in MetaCoq.SafeChecker.PCUICWfEnv]
cs:354 [in MetaCoq.SafeChecker.PCUICSafeChecker]
cs:368 [in MetaCoq.SafeChecker.PCUICSafeChecker]
cs:408 [in MetaCoq.SafeChecker.PCUICSafeChecker]
cs:411 [in MetaCoq.SafeChecker.PCUICSafeChecker]
cs:42 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
cs:456 [in MetaCoq.Template.Universes]
cs:458 [in MetaCoq.PCUIC.PCUICInductiveInversion]
cs:485 [in MetaCoq.Template.Universes]
CS:504 [in MetaCoq.Template.Universes]
CS:525 [in MetaCoq.Template.Universes]
cs:544 [in MetaCoq.Template.EnvironmentTyping]
cs:583 [in MetaCoq.SafeChecker.PCUICSafeChecker]
cs:619 [in MetaCoq.SafeChecker.PCUICSafeChecker]
cs:628 [in MetaCoq.SafeChecker.PCUICSafeChecker]
cs:644 [in MetaCoq.SafeChecker.PCUICSafeChecker]
cs:713 [in MetaCoq.SafeChecker.PCUICSafeChecker]
cs:76 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
cs:808 [in MetaCoq.SafeChecker.PCUICSafeChecker]
cs:811 [in MetaCoq.SafeChecker.PCUICSafeChecker]
cs:816 [in MetaCoq.SafeChecker.PCUICSafeChecker]
cs:819 [in MetaCoq.SafeChecker.PCUICSafeChecker]
cs:834 [in MetaCoq.SafeChecker.PCUICSafeChecker]
cs:853 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
cs:887 [in MetaCoq.SafeChecker.PCUICSafeChecker]
cs:905 [in MetaCoq.SafeChecker.PCUICSafeChecker]
cs:914 [in MetaCoq.SafeChecker.PCUICSafeChecker]
cs:918 [in MetaCoq.SafeChecker.PCUICSafeChecker]
cs:921 [in MetaCoq.SafeChecker.PCUICSafeChecker]
cs:931 [in MetaCoq.SafeChecker.PCUICSafeChecker]
cs:98 [in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
cs:992 [in MetaCoq.SafeChecker.PCUICSafeChecker]
ctors':103 [in MetaCoq.Translations.times_bool_fun]
ctors':105 [in MetaCoq.Translations.times_bool_fun]
ctors:114 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
ctors:114 [in MetaCoq.Translations.param_cheap_packed]
ctors:116 [in MetaCoq.Translations.param_cheap_packed]
ctors:140 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
ctors:172 [in MetaCoq.PCUIC.Syntax.PCUICCases]
ctors:216 [in MetaCoq.PCUIC.PCUICTyping]
ctors:238 [in MetaCoq.PCUIC.PCUICTyping]
ctors:25 [in MetaCoq.Examples.add_constructor]
ctors:672 [in MetaCoq.Erasure.ErasureFunction]
ctors:735 [in MetaCoq.SafeChecker.PCUICTypeChecker]
ctors:746 [in MetaCoq.SafeChecker.PCUICTypeChecker]
ctors:77 [in MetaCoq.Erasure.EPretty]
ctor_type':119 [in MetaCoq.Translations.times_bool_fun]
ctor_type':118 [in MetaCoq.Translations.times_bool_fun]
ctor:111 [in MetaCoq.Template.TypingWf]
ctor:15 [in MetaCoq.Examples.add_constructor]
ctor:186 [in MetaCoq.Template.TypingWf]
ctor:192 [in MetaCoq.Template.TypingWf]
ctor:21 [in MetaCoq.Examples.add_constructor]
ctrs':17 [in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
ctrs':625 [in MetaCoq.Template.Universes]
ctrs':630 [in MetaCoq.Template.Universes]
ctrs':634 [in MetaCoq.Template.Universes]
ctrs0:172 [in MetaCoq.Template.common.uGraph]
ctrs1:548 [in MetaCoq.Template.common.uGraph]
ctrs1:613 [in MetaCoq.Template.common.uGraph]
ctrs2:549 [in MetaCoq.Template.common.uGraph]
ctrs2:614 [in MetaCoq.Template.common.uGraph]
ctrs:107 [in MetaCoq.Template.common.uGraph]
ctrs:109 [in MetaCoq.Template.common.uGraph]
ctrs:114 [in MetaCoq.Template.common.uGraph]
ctrs:116 [in MetaCoq.Template.common.uGraph]
ctrs:120 [in MetaCoq.SafeChecker.PCUICWfEnv]
ctrs:121 [in MetaCoq.Template.common.uGraph]
ctrs:129 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
ctrs:132 [in MetaCoq.Template.common.uGraph]
ctrs:135 [in MetaCoq.Template.common.uGraph]
ctrs:136 [in MetaCoq.Template.common.uGraph]
ctrs:137 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
ctrs:139 [in MetaCoq.Template.common.uGraph]
ctrs:140 [in MetaCoq.Template.common.uGraph]
ctrs:140 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
ctrs:143 [in MetaCoq.Template.common.uGraph]
ctrs:145 [in MetaCoq.Template.common.uGraph]
ctrs:148 [in MetaCoq.Template.common.uGraph]
ctrs:149 [in MetaCoq.Template.common.uGraph]
ctrs:152 [in MetaCoq.Template.common.uGraph]
ctrs:153 [in MetaCoq.Template.common.uGraph]
ctrs:156 [in MetaCoq.Template.common.uGraph]
ctrs:16 [in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
ctrs:164 [in MetaCoq.Template.common.uGraph]
ctrs:170 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
ctrs:173 [in MetaCoq.Template.common.uGraph]
ctrs:195 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
ctrs:196 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
ctrs:199 [in MetaCoq.Template.common.uGraph]
ctrs:421 [in MetaCoq.Template.Checker]
ctrs:428 [in MetaCoq.Template.Universes]
ctrs:440 [in MetaCoq.Template.common.uGraph]
ctrs:443 [in MetaCoq.Template.common.uGraph]
ctrs:483 [in MetaCoq.Template.Universes]
ctrs:522 [in MetaCoq.Template.common.uGraph]
ctrs:523 [in MetaCoq.Template.common.uGraph]
ctrs:541 [in MetaCoq.Template.Universes]
ctrs:544 [in MetaCoq.Template.Universes]
ctrs:547 [in MetaCoq.Template.Universes]
ctrs:550 [in MetaCoq.PCUIC.PCUICInductiveInversion]
ctrs:624 [in MetaCoq.Template.Universes]
ctrs:629 [in MetaCoq.Template.Universes]
ctrs:633 [in MetaCoq.Template.Universes]
ctrs:68 [in MetaCoq.PCUIC.PCUICWeakeningEnv]
ctrs:717 [in MetaCoq.Template.Universes]
ctrs:83 [in MetaCoq.Template.common.uGraph]
ctr:177 [in MetaCoq.Template.common.uGraph]
ctr:178 [in MetaCoq.Template.common.uGraph]
ctr:200 [in MetaCoq.Template.common.uGraph]
ctr:215 [in MetaCoq.Template.common.uGraph]
ctr:218 [in MetaCoq.Template.common.uGraph]
ctr:423 [in MetaCoq.Template.Checker]
ctxinds:986 [in MetaCoq.SafeChecker.PCUICSafeChecker]
ctxs:164 [in MetaCoq.PCUIC.PCUICSpine]
ctxs:170 [in MetaCoq.PCUIC.PCUICSpine]
ctxs:69 [in MetaCoq.PCUIC.PCUICContexts]
ctxs:76 [in MetaCoq.PCUIC.PCUICContexts]
ctxs:82 [in MetaCoq.PCUIC.PCUICContexts]
ctxs:88 [in MetaCoq.PCUIC.PCUICContexts]
ctxs:983 [in MetaCoq.SafeChecker.PCUICSafeChecker]
ctx'':277 [in MetaCoq.PCUIC.PCUICEquality]
ctx'':286 [in MetaCoq.PCUIC.PCUICSubstitution]
ctx'':304 [in MetaCoq.PCUIC.PCUICConfluence]
ctx'':55 [in MetaCoq.PCUIC.PCUICContextSubst]
ctx':106 [in MetaCoq.Template.AstUtils]
ctx':107 [in MetaCoq.PCUIC.utils.PCUICOnOne]
ctx':11 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
ctx':114 [in MetaCoq.Template.AstUtils]
ctx':116 [in MetaCoq.PCUIC.PCUICAlpha]
ctx':122 [in MetaCoq.Template.TypingWf]
ctx':126 [in MetaCoq.Template.TypingWf]
ctx':128 [in MetaCoq.PCUIC.utils.PCUICOnOne]
ctx':130 [in MetaCoq.SafeChecker.PCUICEqualityDec]
ctx':1372 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
ctx':138 [in MetaCoq.PCUIC.PCUICAlpha]
ctx':144 [in MetaCoq.SafeChecker.PCUICEqualityDec]
ctx':186 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
ctx':188 [in MetaCoq.PCUIC.PCUICAlpha]
ctx':189 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
ctx':198 [in MetaCoq.PCUIC.PCUICAlpha]
ctx':251 [in MetaCoq.PCUIC.PCUICSR]
ctx':256 [in MetaCoq.PCUIC.PCUICEquality]
ctx':262 [in MetaCoq.PCUIC.PCUICAlpha]
ctx':269 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
ctx':271 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
ctx':272 [in MetaCoq.PCUIC.PCUICSubstitution]
ctx':276 [in MetaCoq.PCUIC.PCUICEquality]
ctx':28 [in MetaCoq.PCUIC.PCUICAlpha]
ctx':283 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
ctx':284 [in MetaCoq.PCUIC.PCUICSubstitution]
ctx':289 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
ctx':303 [in MetaCoq.PCUIC.PCUICConfluence]
ctx':338 [in MetaCoq.SafeChecker.PCUICSafeChecker]
ctx':35 [in MetaCoq.PCUIC.Conversion.PCUICClosedConv]
ctx':36 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
ctx':363 [in MetaCoq.PCUIC.PCUICEquality]
ctx':38 [in MetaCoq.Erasure.EPretty]
ctx':4 [in MetaCoq.PCUIC.PCUICAlpha]
ctx':428 [in MetaCoq.PCUIC.PCUICConversion]
ctx':456 [in MetaCoq.PCUIC.PCUICInductives]
ctx':50 [in MetaCoq.PCUIC.PCUICConvCumInversion]
ctx':504 [in MetaCoq.PCUIC.PCUICInductives]
ctx':51 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
ctx':51 [in MetaCoq.PCUIC.utils.PCUICPretty]
ctx':516 [in MetaCoq.PCUIC.PCUICInductives]
ctx':528 [in MetaCoq.PCUIC.PCUICInductives]
ctx':53 [in MetaCoq.PCUIC.PCUICContextSubst]
ctx':534 [in MetaCoq.Template.EtaExpand]
ctx':597 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
ctx':603 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
ctx':61 [in MetaCoq.Template.Pretty]
ctx':626 [in MetaCoq.PCUIC.PCUICEquality]
ctx':633 [in MetaCoq.PCUIC.PCUICParallelReduction]
ctx':633 [in MetaCoq.PCUIC.PCUICEquality]
ctx':64 [in MetaCoq.PCUIC.PCUICArities]
ctx':642 [in MetaCoq.PCUIC.PCUICParallelReduction]
ctx':69 [in MetaCoq.PCUIC.PCUICContextSubst]
ctx':69 [in MetaCoq.PCUIC.PCUICSpine]
ctx':75 [in MetaCoq.PCUIC.utils.PCUICOnOne]
ctx':77 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
ctx':825 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
ctx':834 [in MetaCoq.PCUIC.PCUICInductiveInversion]
ctx':843 [in MetaCoq.PCUIC.PCUICInductiveInversion]
ctx':89 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
ctx':9 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
ctx':934 [in MetaCoq.PCUIC.PCUICConversion]
ctx':96 [in MetaCoq.PCUIC.TemplateToPCUICExpanded]
ctx':99 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
ctx0:31 [in MetaCoq.PCUIC.PCUICAlpha]
ctx1:33 [in MetaCoq.PCUIC.PCUICAlpha]
ctx1:416 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
ctx1:485 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
ctx1:510 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
ctx1:540 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
ctx2:414 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
ctx2:483 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
ctx2:508 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
ctx2:538 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
ctx:10 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
ctx:10 [in MetaCoq.PCUIC.PCUICSafeLemmata]
ctx:10 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
ctx:10 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
ctx:102 [in MetaCoq.PCUIC.utils.PCUICOnOne]
ctx:105 [in MetaCoq.Template.AstUtils]
ctx:106 [in MetaCoq.PCUIC.utils.PCUICOnOne]
ctx:107 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
ctx:1105 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
ctx:112 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
ctx:112 [in MetaCoq.PCUIC.PCUICContexts]
ctx:113 [in MetaCoq.Template.TypingWf]
ctx:113 [in MetaCoq.Template.AstUtils]
ctx:115 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
ctx:115 [in MetaCoq.PCUIC.PCUICAlpha]
ctx:1161 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
ctx:117 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
ctx:119 [in MetaCoq.Template.TypingWf]
ctx:120 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
ctx:121 [in MetaCoq.Template.TypingWf]
ctx:122 [in MetaCoq.PCUIC.PCUICEtaExpand]
ctx:124 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
ctx:124 [in MetaCoq.Template.TypingWf]
ctx:125 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
ctx:125 [in MetaCoq.PCUIC.PCUICEtaExpand]
ctx:127 [in MetaCoq.PCUIC.utils.PCUICOnOne]
ctx:129 [in MetaCoq.SafeChecker.PCUICEqualityDec]
ctx:13 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
ctx:1333 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
ctx:137 [in MetaCoq.Template.EtaExpand]
ctx:137 [in MetaCoq.PCUIC.PCUICAlpha]
ctx:1371 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
ctx:1375 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
ctx:1393 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
ctx:1396 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
ctx:14 [in MetaCoq.Template.UnivSubst]
ctx:143 [in MetaCoq.SafeChecker.PCUICEqualityDec]
ctx:144 [in MetaCoq.Template.Checker]
ctx:145 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
ctx:15 [in MetaCoq.PCUIC.PCUICContextSubst]
ctx:15 [in MetaCoq.PCUIC.PCUICContexts]
ctx:150 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
ctx:154 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
ctx:156 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
ctx:160 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
ctx:165 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
ctx:168 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
ctx:168 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
ctx:17 [in MetaCoq.Template.UnivSubst]
ctx:17 [in MetaCoq.PCUIC.PCUICContexts]
ctx:172 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
ctx:172 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
ctx:173 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
ctx:175 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
ctx:176 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
ctx:176 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
ctx:177 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
ctx:178 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
ctx:180 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
ctx:180 [in MetaCoq.Template.LiftSubst]
ctx:181 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
ctx:183 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
ctx:185 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
ctx:186 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
ctx:187 [in MetaCoq.PCUIC.PCUICAlpha]
ctx:188 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
ctx:189 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
ctx:190 [in MetaCoq.PCUIC.PCUICSubstitution]
ctx:190 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
ctx:193 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
ctx:193 [in MetaCoq.Template.TypingWf]
ctx:194 [in MetaCoq.PCUIC.PCUICSubstitution]
ctx:194 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
ctx:195 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
ctx:196 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
ctx:197 [in MetaCoq.PCUIC.PCUICAlpha]
ctx:200 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
ctx:204 [in MetaCoq.PCUIC.PCUICTyping]
ctx:207 [in MetaCoq.Template.Environment]
ctx:207 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
ctx:209 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
ctx:21 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
ctx:21 [in MetaCoq.PCUIC.PCUICContextReduction]
ctx:215 [in MetaCoq.Template.EtaExpand]
ctx:217 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
ctx:219 [in MetaCoq.Template.EtaExpand]
ctx:219 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
ctx:22 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
ctx:223 [in MetaCoq.Template.BasicAst]
ctx:223 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
ctx:228 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
ctx:23 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
ctx:23 [in MetaCoq.PCUIC.Syntax.PCUICUnivSubst]
ctx:23 [in MetaCoq.Template.UnivSubst]
ctx:231 [in MetaCoq.Template.BasicAst]
ctx:233 [in MetaCoq.PCUIC.PCUICEquality]
ctx:237 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
ctx:239 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
ctx:24 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
ctx:24 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
ctx:240 [in MetaCoq.PCUIC.PCUICSubstitution]
ctx:241 [in MetaCoq.Template.EtaExpand]
ctx:247 [in MetaCoq.PCUIC.PCUICAst]
ctx:248 [in MetaCoq.PCUIC.PCUICWfUniverses]
ctx:250 [in MetaCoq.PCUIC.PCUICSR]
ctx:251 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
ctx:253 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
ctx:255 [in MetaCoq.PCUIC.PCUICEquality]
ctx:258 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
ctx:26 [in MetaCoq.PCUIC.Syntax.PCUICUnivSubst]
ctx:260 [in MetaCoq.PCUIC.PCUICAlpha]
ctx:263 [in MetaCoq.Template.BasicAst]
ctx:263 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
ctx:267 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
ctx:27 [in MetaCoq.PCUIC.PCUICAlpha]
ctx:270 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
ctx:270 [in MetaCoq.PCUIC.PCUICSubstitution]
ctx:272 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
ctx:275 [in MetaCoq.PCUIC.PCUICEquality]
ctx:275 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
ctx:276 [in MetaCoq.Template.BasicAst]
ctx:276 [in MetaCoq.PCUIC.PCUICSubstitution]
ctx:278 [in MetaCoq.PCUIC.PCUICSubstitution]
ctx:28 [in MetaCoq.PCUIC.PCUICContextSubst]
ctx:280 [in MetaCoq.PCUIC.PCUICSubstitution]
ctx:281 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
ctx:283 [in MetaCoq.Template.BasicAst]
ctx:284 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
ctx:285 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
ctx:287 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
ctx:287 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
ctx:291 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
ctx:297 [in MetaCoq.Template.BasicAst]
ctx:297 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
ctx:298 [in MetaCoq.Template.EtaExpand]
ctx:3 [in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
ctx:3 [in MetaCoq.PCUIC.PCUICAlpha]
ctx:302 [in MetaCoq.PCUIC.PCUICConfluence]
ctx:303 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
ctx:306 [in MetaCoq.Template.EtaExpand]
ctx:309 [in MetaCoq.Template.BasicAst]
ctx:31 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
ctx:310 [in MetaCoq.PCUIC.PCUICAst]
ctx:311 [in MetaCoq.PCUIC.PCUICNormal]
ctx:315 [in MetaCoq.PCUIC.PCUICAst]
ctx:326 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
ctx:326 [in MetaCoq.PCUIC.PCUICSpine]
ctx:329 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
ctx:33 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
ctx:33 [in MetaCoq.PCUIC.Syntax.PCUICUnivSubst]
ctx:330 [in MetaCoq.PCUIC.PCUICSpine]
ctx:332 [in MetaCoq.Template.BasicAst]
ctx:332 [in MetaCoq.PCUIC.PCUICSpine]
ctx:333 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
ctx:335 [in MetaCoq.SafeChecker.PCUICSafeChecker]
ctx:336 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
ctx:34 [in MetaCoq.PCUIC.Conversion.PCUICClosedConv]
ctx:340 [in MetaCoq.Template.BasicAst]
ctx:344 [in MetaCoq.Template.BasicAst]
ctx:347 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
ctx:348 [in MetaCoq.Template.BasicAst]
ctx:35 [in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
ctx:35 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
ctx:352 [in MetaCoq.Template.BasicAst]
ctx:355 [in MetaCoq.Template.BasicAst]
ctx:36 [in MetaCoq.PCUIC.Conversion.PCUICClosedConv]
ctx:362 [in MetaCoq.PCUIC.PCUICEquality]
ctx:367 [in MetaCoq.Template.BasicAst]
ctx:368 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
ctx:37 [in MetaCoq.Template.EtaExpand]
ctx:371 [in MetaCoq.Template.BasicAst]
ctx:372 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
ctx:373 [in MetaCoq.Template.BasicAst]
ctx:374 [in MetaCoq.Template.BasicAst]
ctx:376 [in MetaCoq.Template.BasicAst]
ctx:376 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
ctx:378 [in MetaCoq.Template.BasicAst]
ctx:38 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
ctx:383 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
ctx:39 [in MetaCoq.Erasure.EEtaExpandedFix]
ctx:39 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
ctx:4 [in MetaCoq.PCUIC.TemplateToPCUICExpanded]
ctx:40 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
ctx:401 [in MetaCoq.PCUIC.PCUICAst]
ctx:402 [in MetaCoq.PCUIC.PCUICSpine]
ctx:403 [in MetaCoq.PCUIC.PCUICReduction]
ctx:415 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
ctx:418 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
ctx:426 [in MetaCoq.PCUIC.PCUICConversion]
ctx:43 [in MetaCoq.SafeChecker.PCUICSafeChecker]
ctx:435 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
ctx:44 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
ctx:440 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
ctx:443 [in MetaCoq.Template.EnvironmentTyping]
ctx:45 [in MetaCoq.Template.EtaExpand]
ctx:453 [in MetaCoq.PCUIC.PCUICInductives]
ctx:455 [in MetaCoq.PCUIC.PCUICAst]
ctx:474 [in MetaCoq.Template.EnvironmentTyping]
ctx:476 [in MetaCoq.PCUIC.PCUICReduction]
ctx:479 [in MetaCoq.PCUIC.PCUICAst]
ctx:48 [in MetaCoq.PCUIC.PCUICInductiveInversion]
ctx:486 [in MetaCoq.PCUIC.PCUICAst]
ctx:49 [in MetaCoq.PCUIC.PCUICConvCumInversion]
ctx:490 [in MetaCoq.Template.EnvironmentTyping]
ctx:493 [in MetaCoq.PCUIC.PCUICAst]
ctx:499 [in MetaCoq.PCUIC.PCUICInductives]
ctx:50 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
ctx:50 [in MetaCoq.PCUIC.PCUICContextSubst]
ctx:501 [in MetaCoq.PCUIC.PCUICSubstitution]
ctx:501 [in MetaCoq.PCUIC.PCUICAst]
ctx:51 [in MetaCoq.PCUIC.PCUICEtaExpand]
ctx:51 [in MetaCoq.PCUIC.PCUICContextReduction]
ctx:511 [in MetaCoq.PCUIC.PCUICInductives]
ctx:511 [in MetaCoq.PCUIC.PCUICAst]
ctx:520 [in MetaCoq.PCUIC.PCUICAst]
ctx:523 [in MetaCoq.PCUIC.PCUICInductives]
ctx:527 [in MetaCoq.PCUIC.PCUICAst]
ctx:529 [in MetaCoq.Template.EtaExpand]
ctx:530 [in MetaCoq.PCUIC.PCUICAst]
ctx:533 [in MetaCoq.Template.EtaExpand]
ctx:539 [in MetaCoq.Template.EtaExpand]
ctx:55 [in MetaCoq.PCUIC.Conversion.PCUICClosedConv]
ctx:56 [in MetaCoq.PCUIC.PCUICContextSubst]
ctx:569 [in MetaCoq.PCUIC.PCUICAst]
ctx:573 [in MetaCoq.PCUIC.PCUICAst]
ctx:573 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
ctx:577 [in MetaCoq.PCUIC.PCUICAst]
ctx:58 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
ctx:581 [in MetaCoq.PCUIC.PCUICAst]
ctx:586 [in MetaCoq.PCUIC.PCUICAst]
ctx:59 [in MetaCoq.PCUIC.PCUICContextSubst]
ctx:595 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
ctx:60 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
ctx:601 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
ctx:61 [in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
ctx:61 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
ctx:62 [in MetaCoq.Template.Environment]
ctx:621 [in MetaCoq.PCUIC.PCUICParallelReduction]
ctx:625 [in MetaCoq.PCUIC.PCUICEquality]
ctx:63 [in MetaCoq.Template.EtaExpand]
ctx:63 [in MetaCoq.PCUIC.PCUICContextSubst]
ctx:63 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
ctx:632 [in MetaCoq.PCUIC.PCUICParallelReduction]
ctx:632 [in MetaCoq.PCUIC.PCUICEquality]
ctx:64 [in MetaCoq.PCUIC.PCUICEtaExpand]
ctx:641 [in MetaCoq.PCUIC.PCUICParallelReduction]
ctx:642 [in MetaCoq.PCUIC.PCUICConfluence]
ctx:644 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
ctx:651 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
ctx:652 [in MetaCoq.PCUIC.PCUICReduction]
ctx:652 [in MetaCoq.PCUIC.PCUICSpine]
ctx:66 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
ctx:661 [in MetaCoq.PCUIC.PCUICReduction]
ctx:665 [in MetaCoq.PCUIC.PCUICReduction]
ctx:68 [in MetaCoq.PCUIC.PCUICPrincipality]
ctx:68 [in MetaCoq.PCUIC.PCUICContextSubst]
ctx:68 [in MetaCoq.PCUIC.PCUICSpine]
ctx:703 [in MetaCoq.PCUIC.PCUICReduction]
ctx:71 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
ctx:711 [in MetaCoq.PCUIC.PCUICReduction]
ctx:714 [in MetaCoq.PCUIC.PCUICReduction]
ctx:72 [in MetaCoq.PCUIC.PCUICSubstitution]
ctx:72 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
ctx:72 [in MetaCoq.PCUIC.PCUICContextSubst]
ctx:732 [in MetaCoq.PCUIC.PCUICEquality]
ctx:74 [in MetaCoq.PCUIC.utils.PCUICOnOne]
ctx:75 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
ctx:75 [in MetaCoq.PCUIC.PCUICSubstitution]
ctx:760 [in MetaCoq.Template.Universes]
ctx:761 [in MetaCoq.Template.Universes]
ctx:77 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
ctx:77 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
ctx:78 [in MetaCoq.PCUIC.PCUICWfUniverses]
ctx:78 [in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
ctx:795 [in MetaCoq.PCUIC.PCUICReduction]
ctx:8 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
ctx:8 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
ctx:80 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
ctx:80 [in MetaCoq.PCUIC.TemplateToPCUICExpanded]
ctx:82 [in MetaCoq.PCUIC.PCUICWfUniverses]
ctx:824 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
ctx:833 [in MetaCoq.PCUIC.PCUICInductiveInversion]
ctx:833 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
ctx:837 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
ctx:84 [in MetaCoq.PCUIC.PCUICConversion]
ctx:842 [in MetaCoq.PCUIC.PCUICInductiveInversion]
ctx:843 [in MetaCoq.PCUIC.PCUICParallelReduction]
ctx:85 [in MetaCoq.PCUIC.TemplateToPCUICExpanded]
ctx:88 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
ctx:88 [in MetaCoq.PCUIC.PCUICWeakeningEnv]
ctx:88 [in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
ctx:89 [in MetaCoq.Erasure.EEtaExpandedFix]
ctx:894 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
ctx:903 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
ctx:91 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
ctx:92 [in MetaCoq.Erasure.EEtaExpandedFix]
ctx:92 [in MetaCoq.PCUIC.TemplateToPCUICExpanded]
ctx:929 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
ctx:933 [in MetaCoq.PCUIC.PCUICConversion]
ctx:936 [in MetaCoq.PCUIC.PCUICReduction]
ctx:937 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
ctx:94 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
ctx:943 [in MetaCoq.PCUIC.PCUICReduction]
ctx:95 [in MetaCoq.PCUIC.TemplateToPCUICExpanded]
ctx:973 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
ctx:98 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
cty:1073 [in MetaCoq.SafeChecker.PCUICTypeChecker]
cty:165 [in MetaCoq.PCUIC.PCUICSafeLemmata]
cty:172 [in MetaCoq.PCUIC.PCUICSafeLemmata]
cty:229 [in MetaCoq.PCUIC.PCUICSubstitution]
ct':13 [in MetaCoq.SafeChecker.PCUICTypeChecker]
ct':15 [in MetaCoq.SafeChecker.PCUICTypeChecker]
ct':17 [in MetaCoq.SafeChecker.PCUICTypeChecker]
ct':19 [in MetaCoq.SafeChecker.PCUICTypeChecker]
ct:368 [in MetaCoq.Template.Universes]
cumb:355 [in MetaCoq.SafeChecker.PCUICTypeChecker]
cumt:243 [in MetaCoq.SafeChecker.PCUICSafeChecker]
cumt:354 [in MetaCoq.SafeChecker.PCUICTypeChecker]
cumt:356 [in MetaCoq.SafeChecker.PCUICTypeChecker]
cumul_gen:405 [in MetaCoq.Template.EnvironmentTyping]
cumul:1 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
cumul:947 [in MetaCoq.Template.Typing]
cunivss:610 [in MetaCoq.Template.EnvironmentTyping]
cunivs:535 [in MetaCoq.Template.EtaExpand]
cunivs:558 [in MetaCoq.Template.EnvironmentTyping]
cunivs:612 [in MetaCoq.Template.EnvironmentTyping]
cunivs:97 [in MetaCoq.PCUIC.TemplateToPCUICExpanded]
cuniv:152 [in MetaCoq.SafeChecker.PCUICWfEnv]
cu:1086 [in MetaCoq.SafeChecker.PCUICTypeChecker]
cu:167 [in MetaCoq.PCUIC.PCUICSafeLemmata]
cu:174 [in MetaCoq.PCUIC.PCUICSafeLemmata]
c_ty:1098 [in MetaCoq.SafeChecker.PCUICTypeChecker]
c'red:271 [in MetaCoq.Template.Checker]
c':101 [in MetaCoq.PCUIC.PCUICSafeLemmata]
c':101 [in MetaCoq.PCUIC.PCUICReduction]
c':104 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
c':106 [in MetaCoq.PCUIC.PCUICSafeLemmata]
c':107 [in MetaCoq.Template.Checker]
c':108 [in MetaCoq.Template.Checker]
c':117 [in MetaCoq.Erasure.Extract]
c':12 [in MetaCoq.PCUIC.PCUICRedTypeIrrelevance]
c':122 [in MetaCoq.Template.TermEquality]
c':1258 [in MetaCoq.SafeChecker.PCUICSafeConversion]
c':127 [in MetaCoq.Erasure.Extract]
c':1287 [in MetaCoq.SafeChecker.PCUICSafeConversion]
c':129 [in MetaCoq.Template.TermEquality]
c':130 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
c':131 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
c':132 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
c':133 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
c':134 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
c':144 [in MetaCoq.Template.TermEquality]
c':1469 [in MetaCoq.SafeChecker.PCUICSafeConversion]
c':156 [in MetaCoq.PCUIC.PCUICConvCumInversion]
c':166 [in MetaCoq.PCUIC.PCUICEquality]
c':17 [in MetaCoq.Erasure.EReflect]
c':171 [in MetaCoq.Erasure.ErasureProperties]
c':173 [in MetaCoq.PCUIC.PCUICEquality]
c':178 [in MetaCoq.Erasure.ErasureProperties]
c':180 [in MetaCoq.Template.Typing]
c':185 [in MetaCoq.Erasure.ErasureProperties]
c':195 [in MetaCoq.Template.Typing]
c':2086 [in MetaCoq.SafeChecker.PCUICSafeConversion]
c':2107 [in MetaCoq.SafeChecker.PCUICSafeConversion]
c':215 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
c':2348 [in MetaCoq.SafeChecker.PCUICSafeConversion]
C':2481 [in MetaCoq.Template.utils.All_Forall]
c':257 [in MetaCoq.PCUIC.PCUICReduction]
c':261 [in MetaCoq.PCUIC.PCUICSafeLemmata]
c':270 [in MetaCoq.PCUIC.PCUICSafeLemmata]
c':270 [in MetaCoq.PCUIC.PCUICReduction]
c':275 [in MetaCoq.PCUIC.PCUICParallelReduction]
c':299 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
c':30 [in MetaCoq.Template.Reflect]
c':302 [in MetaCoq.PCUIC.PCUICNormal]
c':313 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
c':321 [in MetaCoq.PCUIC.PCUICNormal]
c':337 [in MetaCoq.PCUIC.PCUICNormal]
c':358 [in MetaCoq.Template.Typing]
c':375 [in MetaCoq.Template.Typing]
c':390 [in MetaCoq.PCUIC.PCUICNormal]
c':413 [in MetaCoq.Erasure.ErasureFunction]
c':415 [in MetaCoq.Erasure.ErasureFunction]
c':437 [in MetaCoq.PCUIC.PCUICSR]
c':450 [in MetaCoq.PCUIC.PCUICSR]
c':458 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
c':471 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
c':472 [in MetaCoq.PCUIC.PCUICParallelReduction]
c':4877 [in MetaCoq.SafeChecker.PCUICSafeConversion]
c':50 [in MetaCoq.Erasure.Extract]
c':5100 [in MetaCoq.SafeChecker.PCUICSafeConversion]
c':551 [in MetaCoq.PCUIC.PCUICInductiveInversion]
c':552 [in MetaCoq.PCUIC.PCUICInductiveInversion]
c':553 [in MetaCoq.PCUIC.PCUICInductiveInversion]
c':554 [in MetaCoq.PCUIC.PCUICInductiveInversion]
c':555 [in MetaCoq.PCUIC.PCUICInductiveInversion]
c':56 [in MetaCoq.Erasure.Extract]
c':563 [in MetaCoq.SafeChecker.PCUICSafeConversion]
c':568 [in MetaCoq.SafeChecker.PCUICSafeConversion]
c':60 [in MetaCoq.SafeChecker.PCUICErrors]
c':668 [in MetaCoq.PCUIC.PCUICConversion]
c':70 [in MetaCoq.SafeChecker.PCUICErrors]
c':713 [in MetaCoq.SafeChecker.PCUICSafeConversion]
c':793 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
c':80 [in MetaCoq.SafeChecker.PCUICErrors]
c':819 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
c':82 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
c':87 [in MetaCoq.SafeChecker.PCUICErrors]
c':88 [in MetaCoq.PCUIC.PCUICReduction]
c':905 [in MetaCoq.PCUIC.PCUICReduction]
c':92 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
c':972 [in MetaCoq.PCUIC.PCUICReduction]
c':988 [in MetaCoq.PCUIC.PCUICReduction]
c0:267 [in MetaCoq.PCUIC.PCUICParallelReduction]
c0:27 [in MetaCoq.Erasure.Prelim]
c0:44 [in MetaCoq.Erasure.EArities]
c0:462 [in MetaCoq.PCUIC.PCUICParallelReduction]
c0:47 [in MetaCoq.Erasure.EArities]
c0:820 [in MetaCoq.PCUIC.PCUICParallelReduction]
c1:126 [in MetaCoq.Translations.param_cheap_packed]
c1:132 [in MetaCoq.Translations.param_cheap_packed]
c1:2148 [in MetaCoq.SafeChecker.PCUICSafeConversion]
c1:2370 [in MetaCoq.SafeChecker.PCUICSafeConversion]
c1:2385 [in MetaCoq.SafeChecker.PCUICSafeConversion]
c1:268 [in MetaCoq.PCUIC.PCUICParallelReduction]
c1:3 [in MetaCoq.SafeChecker.PCUICErrors]
c1:463 [in MetaCoq.PCUIC.PCUICParallelReduction]
c1:541 [in MetaCoq.SafeChecker.PCUICSafeConversion]
C1:901 [in MetaCoq.Translations.MiniHoTT]
C1:909 [in MetaCoq.Translations.MiniHoTT_paths]
c2:2154 [in MetaCoq.SafeChecker.PCUICSafeConversion]
c2:2376 [in MetaCoq.SafeChecker.PCUICSafeConversion]
c2:2391 [in MetaCoq.SafeChecker.PCUICSafeConversion]
c2:4 [in MetaCoq.SafeChecker.PCUICErrors]
c2:543 [in MetaCoq.SafeChecker.PCUICSafeConversion]
C2:902 [in MetaCoq.Translations.MiniHoTT]
C2:910 [in MetaCoq.Translations.MiniHoTT_paths]
c:1 [in MetaCoq.Template.utils.MCCompare]
c:1 [in MetaCoq.SafeChecker.PCUICConsistency]
c:100 [in MetaCoq.PCUIC.PCUICWeakeningEnv]
c:100 [in MetaCoq.PCUIC.PCUICSafeLemmata]
c:100 [in MetaCoq.Template.common.uGraph]
c:100 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
c:100 [in MetaCoq.PCUIC.PCUICReduction]
c:100 [in MetaCoq.Erasure.Prelim]
C:1006 [in MetaCoq.Translations.MiniHoTT]
C:1006 [in MetaCoq.Translations.MiniHoTT_paths]
c:101 [in MetaCoq.Erasure.EInlineProjections]
c:101 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
C:1014 [in MetaCoq.Translations.MiniHoTT_paths]
c:102 [in MetaCoq.PCUIC.PCUICElimination]
c:102 [in MetaCoq.Erasure.EWellformed]
c:102 [in MetaCoq.PCUIC.PCUICContexts]
C:1021 [in MetaCoq.Translations.MiniHoTT]
c:1021 [in MetaCoq.SafeChecker.PCUICSafeChecker]
c:1028 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
c:1028 [in MetaCoq.Erasure.ErasureFunction]
c:1028 [in MetaCoq.Translations.MiniHoTT]
C:1029 [in MetaCoq.Translations.MiniHoTT_paths]
c:103 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
C:103 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
c:103 [in MetaCoq.Erasure.EWcbvEval]
c:1036 [in MetaCoq.Translations.MiniHoTT_paths]
c:104 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
c:105 [in MetaCoq.PCUIC.PCUICSafeLemmata]
c:105 [in MetaCoq.Template.Pretty]
c:1056 [in MetaCoq.Template.Typing]
c:106 [in MetaCoq.Erasure.EGlobalEnv]
c:107 [in MetaCoq.Erasure.EInlineProjections]
C:1072 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
c:1075 [in MetaCoq.Template.Typing]
c:1077 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
c:108 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
c:109 [in MetaCoq.Erasure.EArities]
c:11 [in MetaCoq.PCUIC.PCUICRedTypeIrrelevance]
c:11 [in MetaCoq.Erasure.Extract]
c:110 [in MetaCoq.PCUIC.PCUICInversion]
c:110 [in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
c:110 [in MetaCoq.Erasure.ErasureProperties]
c:111 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
C:1119 [in MetaCoq.Template.utils.All_Forall]
c:112 [in MetaCoq.Template.Pretty]
C:1128 [in MetaCoq.Template.utils.All_Forall]
c:113 [in MetaCoq.Template.EtaExpand]
c:113 [in MetaCoq.Erasure.EInlineProjections]
c:113 [in MetaCoq.Erasure.EWcbvEvalInd]
c:113 [in MetaCoq.Template.Checker]
C:1137 [in MetaCoq.Template.utils.All_Forall]
c:114 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
C:1146 [in MetaCoq.Template.utils.All_Forall]
c:115 [in MetaCoq.Erasure.Extract]
C:1155 [in MetaCoq.Template.utils.All_Forall]
c:116 [in MetaCoq.Erasure.EWellformed]
C:1164 [in MetaCoq.Template.utils.All_Forall]
C:117 [in MetaCoq.Template.utils.All_Forall]
c:117 [in MetaCoq.PCUIC.PCUICAst]
C:1181 [in MetaCoq.PCUIC.PCUICReduction]
C:119 [in MetaCoq.Template.utils.MCList]
c:12 [in MetaCoq.Template.utils.MCCompare]
c:12 [in MetaCoq.PCUIC.PCUICFirstorder]
C:12 [in MetaCoq.Template.utils.MCUtils]
C:12 [in MetaCoq.Template.utils.MCProd]
c:12 [in MetaCoq.Erasure.EReflect]
c:120 [in MetaCoq.Erasure.EArities]
c:120 [in MetaCoq.PCUIC.Syntax.PCUICCases]
c:120 [in MetaCoq.PCUIC.PCUICAst]
c:120 [in MetaCoq.Template.Environment]
c:121 [in MetaCoq.Template.TermEquality]
c:121 [in MetaCoq.Erasure.EGlobalEnv]
c:121 [in MetaCoq.Erasure.EOptimizePropDiscr]
c:122 [in MetaCoq.Erasure.EWellformed]
c:123 [in MetaCoq.Erasure.EWcbvEval]
c:123 [in MetaCoq.Erasure.EOptimizePropDiscr]
c:124 [in MetaCoq.Template.Typing]
c:124 [in MetaCoq.Template.utils.bytestring]
c:124 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
C:124 [in MetaCoq.PCUIC.Syntax.PCUICCases]
c:124 [in MetaCoq.Template.Checker]
c:124 [in MetaCoq.Template.Environment]
c:124 [in MetaCoq.Template.AstUtils]
c:1248 [in MetaCoq.Translations.MiniHoTT]
c:1252 [in MetaCoq.SafeChecker.PCUICSafeConversion]
c:1256 [in MetaCoq.Translations.MiniHoTT_paths]
c:126 [in MetaCoq.Erasure.Extract]
c:126 [in MetaCoq.PCUIC.PCUICTyping]
c:126 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
c:1263 [in MetaCoq.Template.Typing]
c:1267 [in MetaCoq.PCUIC.PCUICConfluence]
c:127 [in MetaCoq.PCUIC.PCUICWcbvEval]
c:127 [in MetaCoq.Erasure.EEtaExpanded]
c:1273 [in MetaCoq.PCUIC.PCUICConfluence]
c:1279 [in MetaCoq.PCUIC.PCUICConfluence]
c:128 [in MetaCoq.Template.TermEquality]
c:128 [in MetaCoq.Erasure.EWellformed]
c:128 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
c:128 [in MetaCoq.Template.AstUtils]
c:1281 [in MetaCoq.SafeChecker.PCUICSafeConversion]
c:1286 [in MetaCoq.PCUIC.PCUICConfluence]
c:129 [in MetaCoq.Template.WcbvEval]
c:13 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
C:13 [in MetaCoq.PCUIC.PCUICPrincipality]
c:13 [in MetaCoq.PCUIC.TemplateToPCUICExpanded]
C:13 [in MetaCoq.Template.utils.MCPrelude]
c:132 [in MetaCoq.PCUIC.PCUICEquality]
c:132 [in MetaCoq.Erasure.EWcbvEval]
c:133 [in MetaCoq.PCUIC.PCUICWeakeningEnv]
c:133 [in MetaCoq.PCUIC.PCUICEtaExpand]
c:133 [in MetaCoq.Erasure.EOptimizePropDiscr]
c:1342 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
c:136 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
c:136 [in MetaCoq.Erasure.EOptimizePropDiscr]
c:1372 [in MetaCoq.Translations.MiniHoTT]
c:1380 [in MetaCoq.Translations.MiniHoTT_paths]
c:139 [in MetaCoq.PCUIC.PCUICInversion]
c:139 [in MetaCoq.PCUIC.PCUICAlpha]
c:139 [in MetaCoq.PCUIC.PCUICTyping]
c:139 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
c:14 [in MetaCoq.Template.EtaExpand]
c:14 [in MetaCoq.Template.Checker]
c:141 [in MetaCoq.Template.TermEquality]
c:141 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
c:142 [in MetaCoq.Template.EtaExpand]
c:142 [in MetaCoq.Erasure.ErasureProperties]
c:142 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
C:1427 [in MetaCoq.Translations.MiniHoTT]
c:1430 [in MetaCoq.Translations.MiniHoTT]
C:1435 [in MetaCoq.Translations.MiniHoTT_paths]
C:1436 [in MetaCoq.Translations.MiniHoTT]
c:1438 [in MetaCoq.Translations.MiniHoTT_paths]
c:144 [in MetaCoq.Erasure.EWcbvEvalInd]
C:1440 [in MetaCoq.Translations.MiniHoTT]
C:1444 [in MetaCoq.Translations.MiniHoTT_paths]
C:1447 [in MetaCoq.Translations.MiniHoTT]
C:1448 [in MetaCoq.Translations.MiniHoTT_paths]
c:145 [in MetaCoq.PCUIC.PCUICWcbvEval]
C:1455 [in MetaCoq.Translations.MiniHoTT_paths]
C:146 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
c:1463 [in MetaCoq.SafeChecker.PCUICSafeConversion]
C:1476 [in MetaCoq.Translations.MiniHoTT]
C:1484 [in MetaCoq.Translations.MiniHoTT]
C:1484 [in MetaCoq.Translations.MiniHoTT_paths]
c:149 [in MetaCoq.Erasure.EWcbvEval]
C:1491 [in MetaCoq.Translations.MiniHoTT]
C:1492 [in MetaCoq.Translations.MiniHoTT_paths]
C:1499 [in MetaCoq.Translations.MiniHoTT]
C:1499 [in MetaCoq.Translations.MiniHoTT_paths]
c:15 [in MetaCoq.Template.Checker]
c:150 [in MetaCoq.PCUIC.PCUICInversion]
C:1506 [in MetaCoq.Translations.MiniHoTT]
C:1507 [in MetaCoq.Translations.MiniHoTT_paths]
C:1514 [in MetaCoq.Translations.MiniHoTT_paths]
C:1518 [in MetaCoq.Translations.MiniHoTT]
C:1526 [in MetaCoq.Translations.MiniHoTT_paths]
c:154 [in MetaCoq.PCUIC.PCUICConvCumInversion]
c:154 [in MetaCoq.PCUIC.PCUICSR]
c:157 [in MetaCoq.Template.WfAst]
c:157 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
c:157 [in MetaCoq.Template.WcbvEval]
c:158 [in MetaCoq.Erasure.EWcbvEvalInd]
C:16 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
c:16 [in MetaCoq.SafeChecker.PCUICConsistency]
c:16 [in MetaCoq.SafeChecker.PCUICSafeConversion]
c:16 [in MetaCoq.Template.Checker]
c:16 [in MetaCoq.PCUIC.Syntax.PCUICUnivSubst]
c:16 [in MetaCoq.PCUIC.PCUICReduction]
C:1605 [in MetaCoq.Translations.MiniHoTT]
c:161 [in MetaCoq.PCUIC.PCUICProgress]
c:161 [in MetaCoq.Erasure.ERemoveParams]
C:1613 [in MetaCoq.Translations.MiniHoTT_paths]
C:1618 [in MetaCoq.Translations.MiniHoTT]
C:1619 [in MetaCoq.Template.utils.All_Forall]
c:162 [in MetaCoq.Template.Typing]
c:162 [in MetaCoq.Template.Checker]
C:1625 [in MetaCoq.Translations.MiniHoTT]
C:1626 [in MetaCoq.Translations.MiniHoTT_paths]
c:163 [in MetaCoq.PCUIC.PCUICSafeLemmata]
c:163 [in MetaCoq.Erasure.EWcbvEval]
C:1631 [in MetaCoq.Translations.MiniHoTT]
C:1633 [in MetaCoq.Translations.MiniHoTT_paths]
C:1639 [in MetaCoq.Translations.MiniHoTT_paths]
C:1644 [in MetaCoq.Translations.MiniHoTT]
C:165 [in MetaCoq.Template.utils.MCList]
c:165 [in MetaCoq.PCUIC.PCUICEquality]
C:1651 [in MetaCoq.Translations.MiniHoTT]
C:1652 [in MetaCoq.Translations.MiniHoTT_paths]
C:1657 [in MetaCoq.Translations.MiniHoTT]
C:1659 [in MetaCoq.Translations.MiniHoTT_paths]
c:166 [in MetaCoq.Erasure.EEtaExpandedFix]
c:166 [in MetaCoq.Erasure.ERemoveParams]
C:1662 [in MetaCoq.Translations.MiniHoTT]
C:1665 [in MetaCoq.Translations.MiniHoTT_paths]
C:1668 [in MetaCoq.Translations.MiniHoTT]
c:167 [in MetaCoq.SafeChecker.PCUICErrors]
c:167 [in MetaCoq.Template.Checker]
c:167 [in MetaCoq.Template.WcbvEval]
c:167 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
C:1670 [in MetaCoq.Translations.MiniHoTT_paths]
C:1676 [in MetaCoq.Translations.MiniHoTT_paths]
c:168 [in MetaCoq.SafeChecker.PCUICErrors]
c:169 [in MetaCoq.SafeChecker.PCUICErrors]
c:169 [in MetaCoq.Template.Checker]
c:170 [in MetaCoq.PCUIC.PCUICSafeLemmata]
c:170 [in MetaCoq.Erasure.ErasureProperties]
C:1703 [in MetaCoq.Template.utils.All_Forall]
C:1704 [in MetaCoq.Translations.MiniHoTT]
C:1712 [in MetaCoq.Translations.MiniHoTT_paths]
c:172 [in MetaCoq.PCUIC.PCUICEquality]
c:173 [in MetaCoq.Template.BasicAst]
c:173 [in MetaCoq.Template.Typing]
C:174 [in MetaCoq.Template.utils.MCList]
c:175 [in MetaCoq.PCUIC.PCUICReduction]
c:177 [in MetaCoq.Erasure.ErasureProperties]
c:177 [in MetaCoq.Erasure.EWcbvEval]
c:179 [in MetaCoq.Template.Typing]
c:18 [in MetaCoq.Template.utils.MCCompare]
c:18 [in MetaCoq.PCUIC.PCUICGlobalEnv]
c:18 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
c:18 [in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
c:180 [in MetaCoq.PCUIC.PCUICProgress]
c:181 [in MetaCoq.PCUIC.PCUICCumulProp]
c:183 [in MetaCoq.Erasure.EConstructorsAsBlocks]
C:183 [in MetaCoq.PCUIC.PCUICConversion]
c:184 [in MetaCoq.Erasure.ErasureProperties]
c:184 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
c:185 [in MetaCoq.Template.EtaExpand]
C:186 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
c:187 [in MetaCoq.PCUIC.PCUICElimination]
c:187 [in MetaCoq.Template.Typing]
c:189 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
C:19 [in MetaCoq.PCUIC.PCUICPrincipality]
C:19 [in MetaCoq.Template.utils.MCProd]
c:19 [in MetaCoq.Template.UnivSubst]
c:190 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
c:191 [in MetaCoq.PCUIC.PCUICSR]
c:192 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
c:192 [in MetaCoq.SafeChecker.PCUICErrors]
c:193 [in MetaCoq.Template.BasicAst]
c:193 [in MetaCoq.PCUIC.PCUICParallelReduction]
C:1936 [in MetaCoq.Template.utils.All_Forall]
c:194 [in MetaCoq.Template.Typing]
c:194 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
c:195 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
C:1956 [in MetaCoq.Template.utils.All_Forall]
c:196 [in MetaCoq.Erasure.EEtaExpanded]
c:197 [in MetaCoq.Erasure.EWcbvEval]
c:198 [in MetaCoq.PCUIC.PCUICSubstitution]
C:198 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
c:198 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
c:199 [in MetaCoq.Template.Ast]
c:2 [in MetaCoq.PCUIC.PCUICGlobalEnv]
c:200 [in MetaCoq.Erasure.EConstructorsAsBlocks]
c:200 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
c:201 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
c:201 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
c:202 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
c:202 [in MetaCoq.PCUIC.PCUICWcbvEval]
c:202 [in MetaCoq.SafeChecker.PCUICErrors]
c:203 [in MetaCoq.PCUIC.PCUICElimination]
c:203 [in MetaCoq.Template.BasicAst]
c:204 [in MetaCoq.Erasure.Extract]
c:204 [in MetaCoq.Template.common.uGraph]
c:204 [in MetaCoq.PCUIC.PCUICReduction]
c:205 [in MetaCoq.Template.common.uGraph]
c:205 [in MetaCoq.Erasure.EWcbvEval]
c:206 [in MetaCoq.Template.common.uGraph]
c:2061 [in MetaCoq.SafeChecker.PCUICSafeConversion]
c:2085 [in MetaCoq.SafeChecker.PCUICSafeConversion]
c:209 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
c:209 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
C:209 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
c:2096 [in MetaCoq.SafeChecker.PCUICSafeConversion]
C:21 [in MetaCoq.PCUIC.PCUICCanonicity]
c:210 [in MetaCoq.PCUIC.PCUICElimination]
c:210 [in MetaCoq.Template.BasicAst]
c:210 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
c:2106 [in MetaCoq.SafeChecker.PCUICSafeConversion]
c:211 [in MetaCoq.PCUIC.PCUICWcbvEval]
c:211 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
c:211 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
c:212 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
c:212 [in MetaCoq.Template.Checker]
c:213 [in MetaCoq.SafeChecker.PCUICSafeReduce]
C:2133 [in MetaCoq.Template.utils.All_Forall]
c:214 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
C:214 [in MetaCoq.Template.utils.All_Forall]
C:2145 [in MetaCoq.Template.utils.All_Forall]
c:216 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
c:217 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
c:217 [in MetaCoq.Template.Checker]
C:217 [in MetaCoq.Template.TypingWf]
c:218 [in MetaCoq.SafeChecker.PCUICSafeReduce]
c:2180 [in MetaCoq.Template.utils.All_Forall]
c:2189 [in MetaCoq.Template.utils.All_Forall]
C:219 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
c:22 [in MetaCoq.Template.common.uGraph]
c:220 [in MetaCoq.PCUIC.PCUICNormal]
c:220 [in MetaCoq.SafeChecker.PCUICSafeReduce]
c:221 [in MetaCoq.Erasure.EConstructorsAsBlocks]
c:221 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
c:221 [in MetaCoq.Template.Checker]
c:222 [in MetaCoq.PCUIC.PCUICInductives]
c:222 [in MetaCoq.PCUIC.PCUICAst]
C:2224 [in MetaCoq.Template.utils.All_Forall]
c:223 [in MetaCoq.Template.WcbvEval]
C:2239 [in MetaCoq.Template.utils.All_Forall]
c:224 [in MetaCoq.Template.Checker]
C:225 [in MetaCoq.Template.utils.All_Forall]
c:226 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
c:227 [in MetaCoq.Template.EtaExpand]
c:229 [in MetaCoq.Erasure.EEtaExpanded]
c:23 [in MetaCoq.PCUIC.PCUICValidity]
c:23 [in MetaCoq.PCUIC.PCUICPrincipality]
c:232 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
c:233 [in MetaCoq.PCUIC.PCUICSafeLemmata]
c:234 [in MetaCoq.Erasure.EConstructorsAsBlocks]
c:234 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
c:2342 [in MetaCoq.SafeChecker.PCUICSafeConversion]
c:235 [in MetaCoq.PCUIC.PCUICInductiveInversion]
C:236 [in MetaCoq.Template.utils.All_Forall]
C:236 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
c:236 [in MetaCoq.PCUIC.PCUICParallelReduction]
c:236 [in MetaCoq.SafeChecker.PCUICSafeReduce]
C:2369 [in MetaCoq.Translations.MiniHoTT]
C:2377 [in MetaCoq.Translations.MiniHoTT_paths]
c:238 [in MetaCoq.Erasure.EConstructorsAsBlocks]
C:2380 [in MetaCoq.Translations.MiniHoTT]
C:2388 [in MetaCoq.Translations.MiniHoTT_paths]
C:2392 [in MetaCoq.Translations.MiniHoTT]
C:24 [in MetaCoq.PCUIC.PCUICCumulProp]
c:24 [in MetaCoq.Erasure.ESpineView]
C:24 [in MetaCoq.PCUIC.PCUICCanonicity]
c:24 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
c:240 [in MetaCoq.SafeChecker.PCUICSafeReduce]
C:2400 [in MetaCoq.Translations.MiniHoTT_paths]
c:241 [in MetaCoq.Erasure.Extract]
c:241 [in MetaCoq.PCUIC.PCUICParallelReduction]
c:241 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
C:2415 [in MetaCoq.Translations.MiniHoTT]
C:2423 [in MetaCoq.Translations.MiniHoTT_paths]
C:2426 [in MetaCoq.Translations.MiniHoTT]
C:2434 [in MetaCoq.Translations.MiniHoTT_paths]
c:244 [in MetaCoq.SafeChecker.PCUICSafeConversion]
C:2440 [in MetaCoq.Translations.MiniHoTT]
C:2448 [in MetaCoq.Translations.MiniHoTT_paths]
c:245 [in MetaCoq.PCUIC.PCUICInductiveInversion]
c:245 [in MetaCoq.PCUIC.PCUICReduction]
C:2453 [in MetaCoq.Translations.MiniHoTT]
c:246 [in MetaCoq.Template.WcbvEval]
C:2461 [in MetaCoq.Translations.MiniHoTT_paths]
C:2478 [in MetaCoq.Template.utils.All_Forall]
C:248 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
C:2492 [in MetaCoq.Translations.MiniHoTT]
c:2498 [in MetaCoq.Translations.MiniHoTT]
c:25 [in MetaCoq.Template.utils.MCCompare]
c:25 [in MetaCoq.Erasure.EEtaExpandedFix]
c:25 [in MetaCoq.Erasure.Prelim]
C:2500 [in MetaCoq.Translations.MiniHoTT_paths]
c:2502 [in MetaCoq.Translations.MiniHoTT]
C:2506 [in MetaCoq.Template.utils.All_Forall]
c:2506 [in MetaCoq.Translations.MiniHoTT_paths]
c:251 [in MetaCoq.PCUIC.PCUICReduction]
c:2510 [in MetaCoq.Translations.MiniHoTT_paths]
C:2524 [in MetaCoq.Template.utils.All_Forall]
C:2540 [in MetaCoq.Template.utils.All_Forall]
c:255 [in MetaCoq.PCUIC.PCUICTyping]
C:2551 [in MetaCoq.Template.utils.All_Forall]
c:256 [in MetaCoq.PCUIC.PCUICReduction]
C:2565 [in MetaCoq.Template.utils.All_Forall]
c:257 [in MetaCoq.PCUIC.PCUICWcbvEval]
c:258 [in MetaCoq.Erasure.EWcbvEval]
C:2581 [in MetaCoq.Template.utils.All_Forall]
C:2583 [in MetaCoq.Translations.MiniHoTT]
C:259 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
C:2591 [in MetaCoq.Translations.MiniHoTT_paths]
C:2592 [in MetaCoq.Template.utils.All_Forall]
c:2593 [in MetaCoq.Translations.MiniHoTT]
c:26 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
c:26 [in MetaCoq.Erasure.EEnvMap]
c:26 [in MetaCoq.Erasure.EEtaExpanded]
c:260 [in MetaCoq.PCUIC.PCUICSafeLemmata]
C:260 [in MetaCoq.Template.utils.MCList]
c:2601 [in MetaCoq.Translations.MiniHoTT_paths]
C:2603 [in MetaCoq.Template.utils.All_Forall]
c:262 [in MetaCoq.PCUIC.PCUICReduction]
C:265 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
c:265 [in MetaCoq.Template.Typing]
c:2650 [in MetaCoq.Translations.MiniHoTT]
C:2653 [in MetaCoq.Translations.MiniHoTT]
c:2658 [in MetaCoq.Translations.MiniHoTT_paths]
c:266 [in MetaCoq.PCUIC.PCUICInductiveInversion]
c:266 [in MetaCoq.Erasure.EWcbvEval]
C:2661 [in MetaCoq.Translations.MiniHoTT_paths]
C:268 [in MetaCoq.Template.utils.MCList]
c:268 [in MetaCoq.Template.Ast]
c:269 [in MetaCoq.PCUIC.PCUICSafeLemmata]
c:269 [in MetaCoq.PCUIC.PCUICReduction]
c:27 [in MetaCoq.Erasure.ErasureCorrectness]
C:27 [in MetaCoq.PCUIC.Syntax.PCUICReflect]
C:27 [in MetaCoq.Template.utils.MCProd]
c:274 [in MetaCoq.PCUIC.PCUICParallelReduction]
C:275 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
c:275 [in MetaCoq.PCUIC.PCUICInductiveInversion]
c:278 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
c:279 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
c:28 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
c:28 [in MetaCoq.PCUIC.Syntax.PCUICNamelessDef]
C:2839 [in MetaCoq.Translations.MiniHoTT]
C:2847 [in MetaCoq.Translations.MiniHoTT_paths]
C:287 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
C:287 [in MetaCoq.Template.utils.MCList]
C:2879 [in MetaCoq.Translations.MiniHoTT]
c:288 [in MetaCoq.PCUIC.PCUICNormal]
C:2887 [in MetaCoq.Translations.MiniHoTT_paths]
C:2889 [in MetaCoq.Translations.MiniHoTT]
c:289 [in MetaCoq.PCUIC.PCUICSpine]
C:2897 [in MetaCoq.Translations.MiniHoTT_paths]
c:29 [in MetaCoq.PCUIC.PCUICValidity]
c:29 [in MetaCoq.Template.Checker]
c:29 [in MetaCoq.PCUIC.Syntax.PCUICUnivSubst]
c:29 [in MetaCoq.Template.Reflect]
c:29 [in MetaCoq.PCUIC.Syntax.PCUICNamelessDef]
c:290 [in MetaCoq.PCUIC.PCUICSafeLemmata]
C:2900 [in MetaCoq.Translations.MiniHoTT]
C:2908 [in MetaCoq.Translations.MiniHoTT_paths]
c:294 [in MetaCoq.PCUIC.PCUICNormal]
c:295 [in MetaCoq.Template.Typing]
c:295 [in MetaCoq.PCUIC.PCUICInductives]
c:295 [in MetaCoq.PCUIC.PCUICSpine]
c:298 [in MetaCoq.Erasure.EEtaExpandedFix]
c:298 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
c:3 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
C:3 [in MetaCoq.Template.utils.MCProd]
c:30 [in MetaCoq.Template.Normal]
c:30 [in MetaCoq.Erasure.EWcbvEvalInd]
c:30 [in MetaCoq.Template.Checker]
c:300 [in MetaCoq.PCUIC.PCUICNormal]
C:305 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
c:306 [in MetaCoq.PCUIC.PCUICNormal]
c:307 [in MetaCoq.PCUIC.PCUICWcbvEval]
c:31 [in MetaCoq.PCUIC.PCUICEtaExpand]
c:31 [in MetaCoq.Template.Kernames]
c:311 [in MetaCoq.PCUIC.PCUICProgress]
c:311 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
c:312 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
c:313 [in MetaCoq.Erasure.EArities]
c:313 [in MetaCoq.Template.WcbvEval]
C:313 [in MetaCoq.PCUIC.PCUICConversion]
c:314 [in MetaCoq.PCUIC.PCUICWcbvEval]
c:316 [in MetaCoq.Template.BasicAst]
c:316 [in MetaCoq.PCUIC.PCUICNormal]
C:316 [in MetaCoq.PCUIC.PCUICConversion]
c:32 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
C:32 [in MetaCoq.Template.utils.MCProd]
c:320 [in MetaCoq.PCUIC.PCUICNormal]
c:328 [in MetaCoq.Erasure.EArities]
C:329 [in MetaCoq.PCUIC.PCUICConversion]
c:330 [in MetaCoq.PCUIC.PCUICProgress]
c:330 [in MetaCoq.PCUIC.PCUICInductives]
C:336 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
c:336 [in MetaCoq.PCUIC.PCUICNormal]
C:336 [in MetaCoq.PCUIC.PCUICConversion]
c:339 [in MetaCoq.Template.Typing]
C:339 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
c:340 [in MetaCoq.PCUIC.PCUICSpine]
c:346 [in MetaCoq.Erasure.ERemoveParams]
c:346 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
C:349 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
c:349 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
C:35 [in MetaCoq.Template.utils.All_Forall]
c:35 [in MetaCoq.Template.WfAst]
c:35 [in MetaCoq.Template.Kernames]
c:351 [in MetaCoq.Template.Typing]
c:351 [in MetaCoq.PCUIC.PCUICConversion]
c:351 [in MetaCoq.PCUIC.PCUICSpine]
c:352 [in MetaCoq.Erasure.ERemoveParams]
c:355 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
c:355 [in MetaCoq.PCUIC.PCUICSR]
c:357 [in MetaCoq.Template.Typing]
c:358 [in MetaCoq.Erasure.ERemoveParams]
c:358 [in MetaCoq.PCUIC.PCUICSpine]
c:36 [in MetaCoq.SafeChecker.PCUICWfReduction]
C:361 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
c:363 [in MetaCoq.PCUIC.PCUICProgress]
c:364 [in MetaCoq.PCUIC.PCUICSpine]
c:366 [in MetaCoq.Template.Typing]
c:369 [in MetaCoq.PCUIC.PCUICParallelReduction]
c:37 [in MetaCoq.Template.Normal]
c:37 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
c:373 [in MetaCoq.PCUIC.PCUICSpine]
C:374 [in MetaCoq.Template.utils.All_Forall]
c:374 [in MetaCoq.Template.Typing]
c:374 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
c:378 [in MetaCoq.PCUIC.PCUICSpine]
c:379 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
C:38 [in MetaCoq.Template.utils.MCList]
c:38 [in MetaCoq.Erasure.EWcbvEval]
c:383 [in MetaCoq.PCUIC.PCUICProgress]
c:384 [in MetaCoq.PCUIC.PCUICSR]
C:386 [in MetaCoq.Template.utils.All_Forall]
c:386 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
c:387 [in MetaCoq.PCUIC.PCUICSubstitution]
c:388 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
c:389 [in MetaCoq.PCUIC.PCUICNormal]
c:39 [in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
c:391 [in MetaCoq.PCUIC.PCUICProgress]
c:391 [in MetaCoq.SafeChecker.PCUICTypeChecker]
C:395 [in MetaCoq.Template.utils.All_Forall]
c:395 [in MetaCoq.PCUIC.PCUICWcbvEval]
c:396 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
C:397 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
C:398 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
c:40 [in MetaCoq.Template.Normal]
c:40 [in MetaCoq.SafeChecker.PCUICWfReduction]
C:40 [in MetaCoq.Template.utils.MCProd]
c:40 [in MetaCoq.Erasure.EGenericMapEnv]
c:400 [in MetaCoq.SafeChecker.PCUICTypeChecker]
c:403 [in MetaCoq.PCUIC.PCUICProgress]
C:403 [in MetaCoq.Template.utils.All_Forall]
c:403 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
c:405 [in MetaCoq.Template.EtaExpand]
C:407 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
c:409 [in MetaCoq.Erasure.EWcbvEval]
c:41 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
C:41 [in MetaCoq.PCUIC.PCUICCanonicity]
c:41 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
c:41 [in MetaCoq.PCUIC.PCUICReduction]
c:411 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
C:414 [in MetaCoq.PCUIC.PCUICNormal]
c:416 [in MetaCoq.Erasure.EWcbvEval]
c:42 [in MetaCoq.Erasure.EArities]
c:42 [in MetaCoq.Template.common.uGraph]
c:420 [in MetaCoq.PCUIC.PCUICParallelReduction]
c:425 [in MetaCoq.PCUIC.PCUICSR]
c:426 [in MetaCoq.PCUIC.PCUICParallelReduction]
c:43 [in MetaCoq.SafeChecker.PCUICWfReduction]
c:43 [in MetaCoq.Erasure.EGlobalEnv]
c:431 [in MetaCoq.PCUIC.PCUICSR]
c:435 [in MetaCoq.PCUIC.PCUICInductives]
c:436 [in MetaCoq.PCUIC.PCUICSR]
c:437 [in MetaCoq.Erasure.EWcbvEval]
C:44 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
c:442 [in MetaCoq.PCUIC.PCUICSR]
C:445 [in MetaCoq.PCUIC.PCUICInductives]
c:449 [in MetaCoq.PCUIC.PCUICSR]
c:449 [in MetaCoq.Erasure.EWcbvEval]
c:457 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
c:46 [in MetaCoq.Template.common.uGraph]
c:46 [in MetaCoq.Erasure.EWcbvEvalInd]
c:46 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
C:46 [in MetaCoq.Template.utils.MCProd]
c:46 [in MetaCoq.Erasure.EGenericMapEnv]
c:4667 [in MetaCoq.SafeChecker.PCUICSafeConversion]
C:47 [in MetaCoq.Template.utils.MCList]
c:47 [in MetaCoq.Template.Kernames]
c:47 [in MetaCoq.Erasure.EWcbvEval]
c:47 [in MetaCoq.Template.Induction]
c:470 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
c:471 [in MetaCoq.PCUIC.PCUICParallelReduction]
c:472 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
c:48 [in MetaCoq.PCUIC.PCUICElimination]
c:48 [in MetaCoq.Erasure.Extract]
C:480 [in MetaCoq.Translations.MiniHoTT]
c:4865 [in MetaCoq.SafeChecker.PCUICSafeConversion]
c:4874 [in MetaCoq.SafeChecker.PCUICSafeConversion]
C:488 [in MetaCoq.Translations.MiniHoTT]
C:488 [in MetaCoq.Translations.MiniHoTT_paths]
c:4880 [in MetaCoq.SafeChecker.PCUICSafeConversion]
c:49 [in MetaCoq.Erasure.EGlobalEnv]
c:49 [in MetaCoq.PCUIC.Conversion.PCUICClosedConv]
c:493 [in MetaCoq.Template.Universes]
C:496 [in MetaCoq.Translations.MiniHoTT_paths]
c:5 [in MetaCoq.SafeChecker.PCUICConsistency]
c:5 [in MetaCoq.SafeChecker.PCUICErrors]
C:5 [in MetaCoq.Template.utils.MCUtils]
c:501 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
c:503 [in MetaCoq.PCUIC.PCUICInductives]
C:504 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
c:508 [in MetaCoq.Template.EnvironmentTyping]
c:5091 [in MetaCoq.SafeChecker.PCUICSafeConversion]
c:5098 [in MetaCoq.SafeChecker.PCUICSafeConversion]
c:51 [in MetaCoq.PCUIC.PCUICNormal]
c:51 [in MetaCoq.Erasure.EGenericMapEnv]
c:510 [in MetaCoq.Erasure.EEtaExpandedFix]
c:515 [in MetaCoq.PCUIC.PCUICInductives]
c:52 [in MetaCoq.Template.common.uGraph]
C:52 [in MetaCoq.Template.utils.MCOption]
C:526 [in MetaCoq.Examples.tauto]
C:529 [in MetaCoq.Examples.tauto]
C:53 [in MetaCoq.Examples.demo]
c:53 [in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
c:53 [in MetaCoq.PCUIC.utils.PCUICPretty]
c:54 [in MetaCoq.PCUIC.PCUICNormal]
c:54 [in MetaCoq.PCUIC.PCUICSR]
c:546 [in MetaCoq.Template.common.uGraph]
c:549 [in MetaCoq.PCUIC.PCUICInductiveInversion]
c:55 [in MetaCoq.Erasure.Extract]
c:55 [in MetaCoq.SafeChecker.PCUICErrors]
c:553 [in MetaCoq.PCUIC.PCUICTyping]
c:554 [in MetaCoq.Template.common.uGraph]
c:559 [in MetaCoq.SafeChecker.PCUICSafeConversion]
c:56 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
c:56 [in MetaCoq.PCUIC.PCUICEtaExpand]
c:56 [in MetaCoq.Erasure.EEnvMap]
c:561 [in MetaCoq.PCUIC.PCUICInductiveInversion]
c:566 [in MetaCoq.SafeChecker.PCUICSafeConversion]
c:568 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
c:57 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
c:57 [in MetaCoq.Erasure.EGenericMapEnv]
c:572 [in MetaCoq.PCUIC.PCUICTyping]
c:58 [in MetaCoq.Erasure.EAst]
C:58 [in MetaCoq.Translations.MiniHoTT]
C:585 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
c:59 [in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
C:596 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
c:598 [in MetaCoq.PCUIC.PCUICConversion]
c:599 [in MetaCoq.Template.Universes]
C:6 [in MetaCoq.PCUIC.TemplateToPCUIC]
c:6 [in MetaCoq.PCUIC.PCUICTyping]
c:603 [in MetaCoq.PCUIC.PCUICConversion]
c:606 [in MetaCoq.Template.Universes]
c:607 [in MetaCoq.PCUIC.PCUICConversion]
c:608 [in MetaCoq.Template.Typing]
C:61 [in MetaCoq.PCUIC.PCUICArities]
c:612 [in MetaCoq.PCUIC.PCUICConversion]
c:622 [in MetaCoq.PCUIC.PCUICConversion]
c:63 [in MetaCoq.Template.Reflect]
c:635 [in MetaCoq.PCUIC.PCUICInductiveInversion]
c:64 [in MetaCoq.PCUIC.PCUICElimination]
c:64 [in MetaCoq.PCUIC.PCUICWcbvEval]
c:64 [in MetaCoq.Template.WcbvEval]
c:64 [in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
C:640 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
c:642 [in MetaCoq.PCUIC.PCUICInductiveInversion]
c:643 [in MetaCoq.Template.common.uGraph]
c:644 [in MetaCoq.PCUIC.PCUICConversion]
c:645 [in MetaCoq.Template.common.uGraph]
c:647 [in MetaCoq.Template.common.uGraph]
c:65 [in MetaCoq.SafeChecker.PCUICErrors]
c:65 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
c:650 [in MetaCoq.Template.Typing]
c:650 [in MetaCoq.Template.common.uGraph]
c:652 [in MetaCoq.Template.common.uGraph]
c:658 [in MetaCoq.PCUIC.PCUICInductives]
c:658 [in MetaCoq.PCUIC.PCUICConversion]
c:66 [in MetaCoq.Template.utils.MCCompare]
C:66 [in MetaCoq.Translations.MiniHoTT_paths]
c:664 [in MetaCoq.Template.Typing]
c:667 [in MetaCoq.PCUIC.PCUICConversion]
c:667 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
C:668 [in MetaCoq.Translations.MiniHoTT]
c:670 [in MetaCoq.Template.EnvironmentTyping]
C:676 [in MetaCoq.Translations.MiniHoTT_paths]
C:679 [in MetaCoq.Translations.MiniHoTT]
c:68 [in MetaCoq.PCUIC.PCUICNormal]
c:686 [in MetaCoq.SafeChecker.PCUICSafeConversion]
C:687 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
C:687 [in MetaCoq.Translations.MiniHoTT_paths]
C:688 [in MetaCoq.Translations.MiniHoTT]
c:69 [in MetaCoq.Template.Normal]
c:69 [in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
C:696 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
C:696 [in MetaCoq.Translations.MiniHoTT_paths]
c:697 [in MetaCoq.PCUIC.PCUICInductiveInversion]
c:7 [in MetaCoq.Template.UnivSubst]
c:70 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
c:70 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
C:701 [in MetaCoq.Translations.MiniHoTT]
C:708 [in MetaCoq.Template.utils.MCList]
c:709 [in MetaCoq.SafeChecker.PCUICSafeConversion]
C:709 [in MetaCoq.Translations.MiniHoTT_paths]
c:71 [in MetaCoq.Erasure.EEtaExpandedFix]
c:710 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
c:715 [in MetaCoq.Template.Universes]
c:718 [in MetaCoq.Template.Universes]
C:718 [in MetaCoq.Template.utils.MCList]
c:72 [in MetaCoq.PCUIC.PCUICWcbvEval]
c:72 [in MetaCoq.PCUIC.PCUICNormal]
C:722 [in MetaCoq.Template.utils.MCList]
C:73 [in MetaCoq.Erasure.EArities]
c:733 [in MetaCoq.Template.Typing]
C:735 [in MetaCoq.Template.utils.MCList]
C:74 [in MetaCoq.Template.monad_utils]
c:74 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
C:746 [in MetaCoq.Template.utils.MCList]
c:75 [in MetaCoq.PCUIC.PCUICNormal]
c:75 [in MetaCoq.SafeChecker.PCUICErrors]
c:75 [in MetaCoq.Template.WcbvEval]
c:76 [in MetaCoq.Template.Normal]
c:76 [in MetaCoq.PCUIC.PCUICReduction]
c:77 [in MetaCoq.Template.WfAst]
c:77 [in MetaCoq.PCUIC.PCUICNormal]
C:77 [in MetaCoq.Translations.times_bool_fun2]
C:78 [in MetaCoq.Template.BasicAst]
C:783 [in MetaCoq.Translations.MiniHoTT]
c:79 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
c:79 [in MetaCoq.Template.Normal]
c:79 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
C:791 [in MetaCoq.Translations.MiniHoTT]
C:791 [in MetaCoq.Translations.MiniHoTT_paths]
c:792 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
C:795 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
C:799 [in MetaCoq.Translations.MiniHoTT_paths]
c:8 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
c:8 [in MetaCoq.Template.Typing]
c:8 [in MetaCoq.Template.Induction]
C:802 [in MetaCoq.Translations.MiniHoTT]
c:81 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
C:810 [in MetaCoq.Translations.MiniHoTT_paths]
C:812 [in MetaCoq.Translations.MiniHoTT]
c:818 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
c:819 [in MetaCoq.PCUIC.PCUICParallelReduction]
c:82 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
C:820 [in MetaCoq.Translations.MiniHoTT_paths]
C:823 [in MetaCoq.Translations.MiniHoTT]
C:83 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
c:83 [in MetaCoq.PCUIC.PCUICReduction]
c:83 [in MetaCoq.Erasure.Prelim]
C:831 [in MetaCoq.Translations.MiniHoTT_paths]
C:834 [in MetaCoq.Translations.MiniHoTT]
c:84 [in MetaCoq.SafeChecker.PCUICErrors]
c:84 [in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
C:842 [in MetaCoq.Translations.MiniHoTT_paths]
C:86 [in MetaCoq.Template.BasicAst]
c:86 [in MetaCoq.PCUIC.PCUICWeakeningEnv]
c:86 [in MetaCoq.SafeChecker.PCUICWfEnv]
c:864 [in MetaCoq.Template.utils.wGraph]
c:87 [in MetaCoq.PCUIC.PCUICReduction]
c:870 [in MetaCoq.Template.utils.wGraph]
C:872 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
c:876 [in MetaCoq.PCUIC.PCUICTyping]
c:878 [in MetaCoq.PCUIC.PCUICReduction]
c:88 [in MetaCoq.Erasure.EDeps]
c:88 [in MetaCoq.Erasure.EInlineProjections]
c:88 [in MetaCoq.Template.TermEquality]
c:89 [in MetaCoq.PCUIC.PCUICInversion]
c:89 [in MetaCoq.Erasure.EGlobalEnv]
c:893 [in MetaCoq.PCUIC.PCUICReduction]
c:895 [in MetaCoq.PCUIC.PCUICTyping]
c:898 [in MetaCoq.PCUIC.PCUICReduction]
c:9 [in MetaCoq.PCUIC.PCUICProgress]
c:9 [in MetaCoq.PCUIC.TemplateToPCUICExpanded]
c:9 [in MetaCoq.Examples.add_constructor]
c:90 [in MetaCoq.PCUIC.PCUICWeakeningEnv]
c:90 [in MetaCoq.Erasure.EInlineProjections]
c:903 [in MetaCoq.PCUIC.PCUICReduction]
c:91 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
c:91 [in MetaCoq.PCUIC.PCUICSubstitution]
c:91 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
c:91 [in MetaCoq.Erasure.Prelim]
c:911 [in MetaCoq.PCUIC.PCUICReduction]
C:913 [in MetaCoq.Translations.MiniHoTT]
c:919 [in MetaCoq.Translations.MiniHoTT]
C:919 [in MetaCoq.PCUIC.PCUICReduction]
c:92 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
c:92 [in MetaCoq.PCUIC.PCUICReduction]
C:921 [in MetaCoq.Translations.MiniHoTT_paths]
C:924 [in MetaCoq.Template.utils.MCList]
c:927 [in MetaCoq.Translations.MiniHoTT_paths]
c:93 [in MetaCoq.PCUIC.PCUICWeakeningEnv]
c:934 [in MetaCoq.PCUIC.PCUICTyping]
c:94 [in MetaCoq.Template.Pretty]
c:95 [in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
c:95 [in MetaCoq.Erasure.EGlobalEnv]
c:956 [in MetaCoq.PCUIC.PCUICReduction]
c:962 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
c:968 [in MetaCoq.PCUIC.PCUICReduction]
c:97 [in MetaCoq.PCUIC.PCUICEtaExpand]
c:97 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
c:97 [in MetaCoq.Erasure.EWellformed]
c:97 [in MetaCoq.PCUIC.utils.PCUICPretty]
c:98 [in MetaCoq.Template.Typing]
c:980 [in MetaCoq.Template.Typing]
c:987 [in MetaCoq.PCUIC.PCUICReduction]
C:988 [in MetaCoq.Translations.MiniHoTT]
c:99 [in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
c:99 [in MetaCoq.Erasure.EAstUtils]
C:996 [in MetaCoq.Translations.MiniHoTT_paths]
C:998 [in MetaCoq.Translations.MiniHoTT]



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)