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)

W (binder)

wat:1730 [in MetaCoq.SafeChecker.PCUICSafeReduce]
wcon:127 [in MetaCoq.Erasure.EInlineProjections]
wcon:142 [in MetaCoq.Erasure.EOptimizePropDiscr]
wcon:37 [in MetaCoq.Erasure.ETransform]
wcon:371 [in MetaCoq.Erasure.ERemoveParams]
wcon:450 [in MetaCoq.Erasure.EEtaExpandedFix]
wcon:498 [in MetaCoq.Erasure.EEtaExpandedFix]
wcon:550 [in MetaCoq.Erasure.EEtaExpandedFix]
wcon:559 [in MetaCoq.Erasure.EEtaExpandedFix]
wcon:62 [in MetaCoq.Erasure.ETransform]
wcon:73 [in MetaCoq.Erasure.ETransform]
wcon:83 [in MetaCoq.Erasure.ETransform]
wcon:95 [in MetaCoq.Erasure.ETransform]
weight_on_edge:935 [in MetaCoq.Template.utils.wGraph]
weight_on_edge:926 [in MetaCoq.Template.utils.wGraph]
weight_on_edge:918 [in MetaCoq.Template.utils.wGraph]
weight_on_edge:896 [in MetaCoq.Template.utils.wGraph]
weight_on_edge:889 [in MetaCoq.Template.utils.wGraph]
wfars:974 [in MetaCoq.SafeChecker.PCUICSafeChecker]
wfar:350 [in MetaCoq.SafeChecker.PCUICSafeChecker]
wfar:403 [in MetaCoq.SafeChecker.PCUICSafeChecker]
wfar:631 [in MetaCoq.SafeChecker.PCUICSafeChecker]
wfar:797 [in MetaCoq.SafeChecker.PCUICSafeChecker]
wfA:264 [in MetaCoq.SafeChecker.PCUICTypeChecker]
wfcofix:1111 [in MetaCoq.SafeChecker.PCUICTypeChecker]
wfcs:932 [in MetaCoq.SafeChecker.PCUICSafeChecker]
wfd':231 [in MetaCoq.SafeChecker.PCUICSafeChecker]
wfd:229 [in MetaCoq.SafeChecker.PCUICSafeChecker]
wfext:10 [in MetaCoq.Erasure.ETransform]
wfext:1318 [in MetaCoq.Erasure.ErasureFunction]
wfext:1335 [in MetaCoq.Erasure.ErasureFunction]
wfext:1356 [in MetaCoq.Erasure.ErasureFunction]
wfext:1371 [in MetaCoq.Erasure.ErasureFunction]
wfext:1393 [in MetaCoq.Erasure.ErasureFunction]
wfext:946 [in MetaCoq.Erasure.ErasureFunction]
wfext:958 [in MetaCoq.SafeChecker.PCUICSafeChecker]
wfe:9 [in MetaCoq.Erasure.ETransform]
wffix:1107 [in MetaCoq.SafeChecker.PCUICTypeChecker]
wfg:551 [in MetaCoq.SafeChecker.PCUICTypeChecker]
wfi:935 [in MetaCoq.SafeChecker.PCUICSafeChecker]
wfl':273 [in MetaCoq.SafeChecker.PCUICSafeChecker]
wfl':298 [in MetaCoq.SafeChecker.PCUICSafeChecker]
wfl:1 [in MetaCoq.Erasure.ErasureCorrectness]
wfl:11 [in MetaCoq.Erasure.EProgram]
wfl:127 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
wfl:1307 [in MetaCoq.Erasure.ErasureFunction]
wfl:1314 [in MetaCoq.Erasure.ErasureFunction]
wfl:1331 [in MetaCoq.Erasure.ErasureFunction]
wfl:1367 [in MetaCoq.Erasure.ErasureFunction]
wfl:1389 [in MetaCoq.Erasure.ErasureFunction]
wfl:155 [in MetaCoq.Erasure.ErasureProperties]
wfl:16 [in MetaCoq.Erasure.EWcbvEval]
wfl:160 [in MetaCoq.Erasure.ErasureProperties]
wfl:167 [in MetaCoq.Erasure.ErasureProperties]
wfl:170 [in MetaCoq.Erasure.EWcbvEval]
wfl:174 [in MetaCoq.Erasure.ErasureProperties]
wfl:181 [in MetaCoq.Erasure.ErasureProperties]
wfl:271 [in MetaCoq.SafeChecker.PCUICSafeChecker]
wfl:296 [in MetaCoq.SafeChecker.PCUICSafeChecker]
wfl:311 [in MetaCoq.Erasure.EWcbvEval]
wfl:317 [in MetaCoq.Erasure.EWcbvEval]
wfl:343 [in MetaCoq.Erasure.EWcbvEval]
wfl:352 [in MetaCoq.Erasure.EWcbvEval]
wfl:362 [in MetaCoq.Erasure.EWcbvEval]
wfl:370 [in MetaCoq.Erasure.ERemoveParams]
wfl:375 [in MetaCoq.Erasure.EWcbvEval]
wfl:381 [in MetaCoq.Erasure.EWcbvEval]
wfl:399 [in MetaCoq.Erasure.EWcbvEval]
wfl:421 [in MetaCoq.Erasure.EWcbvEval]
wfl:434 [in MetaCoq.Erasure.EWcbvEval]
wfl:457 [in MetaCoq.Erasure.EWcbvEval]
wfl:5 [in MetaCoq.Erasure.EProgram]
wfl:54 [in MetaCoq.Erasure.EDeps]
wfl:59 [in MetaCoq.Erasure.EInlineProjections]
wfl:59 [in MetaCoq.Erasure.EOptimizePropDiscr]
wfl:64 [in MetaCoq.Erasure.EInlineProjections]
wfl:81 [in MetaCoq.Erasure.Prelim]
wfl:88 [in MetaCoq.Erasure.Prelim]
wfl:92 [in MetaCoq.Erasure.EOptimizePropDiscr]
wfl:942 [in MetaCoq.Erasure.ErasureFunction]
wfl:95 [in MetaCoq.Erasure.Prelim]
wfl:97 [in MetaCoq.Erasure.EOptimizePropDiscr]
wfparams:928 [in MetaCoq.SafeChecker.PCUICSafeChecker]
wfpars:352 [in MetaCoq.SafeChecker.PCUICSafeChecker]
wfpars:405 [in MetaCoq.SafeChecker.PCUICSafeChecker]
wfpars:633 [in MetaCoq.SafeChecker.PCUICSafeChecker]
wfpars:799 [in MetaCoq.SafeChecker.PCUICSafeChecker]
wfpars:972 [in MetaCoq.SafeChecker.PCUICSafeChecker]
wfpret:730 [in MetaCoq.SafeChecker.PCUICTypeChecker]
wfP:107 [in MetaCoq.Template.LiftSubst]
wfp:1094 [in MetaCoq.SafeChecker.PCUICTypeChecker]
wfP:112 [in MetaCoq.Template.LiftSubst]
wfp:726 [in MetaCoq.SafeChecker.PCUICTypeChecker]
wfty:577 [in MetaCoq.SafeChecker.PCUICSafeChecker]
wfty:579 [in MetaCoq.SafeChecker.PCUICSafeChecker]
wft:219 [in MetaCoq.SafeChecker.PCUICSafeChecker]
wfunivs:650 [in MetaCoq.SafeChecker.PCUICSafeChecker]
wfu:221 [in MetaCoq.SafeChecker.PCUICSafeChecker]
wfu:651 [in MetaCoq.SafeChecker.PCUICTypeChecker]
wfX:344 [in MetaCoq.SafeChecker.PCUICSafeChecker]
wfX:438 [in MetaCoq.SafeChecker.PCUICSafeChecker]
wfX:445 [in MetaCoq.SafeChecker.PCUICSafeChecker]
wfX:456 [in MetaCoq.SafeChecker.PCUICSafeChecker]
wfX:466 [in MetaCoq.SafeChecker.PCUICSafeChecker]
wfX:494 [in MetaCoq.Template.Universes]
wfX:534 [in MetaCoq.SafeChecker.PCUICSafeChecker]
wfX:715 [in MetaCoq.SafeChecker.PCUICSafeChecker]
wfX:940 [in MetaCoq.SafeChecker.PCUICSafeChecker]
wfX:948 [in MetaCoq.SafeChecker.PCUICSafeChecker]
wf_term:196 [in MetaCoq.Template.EnvironmentTyping]
wf_brs:130 [in MetaCoq.PCUIC.PCUICInversion]
wf_pctx:122 [in MetaCoq.PCUIC.PCUICInversion]
wf_pred:120 [in MetaCoq.PCUIC.PCUICInversion]
wf_brs:75 [in MetaCoq.PCUIC.PCUICTyping]
wf_local_fun:62 [in MetaCoq.PCUIC.PCUICTyping]
wf_pctx:56 [in MetaCoq.PCUIC.PCUICTyping]
wf_pred:54 [in MetaCoq.PCUIC.PCUICTyping]
wf_local_fun:40 [in MetaCoq.PCUIC.PCUICTyping]
wf_:1031 [in MetaCoq.SafeChecker.PCUICSafeChecker]
wf_bodies:1109 [in MetaCoq.SafeChecker.PCUICTypeChecker]
wf_types:1108 [in MetaCoq.SafeChecker.PCUICTypeChecker]
wf_bodies:1105 [in MetaCoq.SafeChecker.PCUICTypeChecker]
wf_types:1104 [in MetaCoq.SafeChecker.PCUICTypeChecker]
wf_types:805 [in MetaCoq.SafeChecker.PCUICTypeChecker]
wf':130 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
wf':167 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
wf':233 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
wf:101 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
wf:128 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
wf:165 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
wf:231 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
wf:25 [in MetaCoq.Erasure.EWellformed]
wf:31 [in MetaCoq.Erasure.ErasureCorrectness]
wf:430 [in MetaCoq.PCUIC.PCUICSpine]
wf:443 [in MetaCoq.PCUIC.PCUICSpine]
wf:531 [in MetaCoq.SafeChecker.PCUICSafeConversion]
wf:577 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
wf:591 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
wf:92 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
wf:975 [in MetaCoq.Erasure.ErasureFunction]
wfΓ':276 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
wfΓ':342 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
wfΓ':357 [in MetaCoq.Template.EnvironmentTyping]
wfΓ':433 [in MetaCoq.PCUIC.PCUICSpine]
wfΓ':446 [in MetaCoq.PCUIC.PCUICSpine]
wfΓ':460 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
wfΓ':56 [in MetaCoq.PCUIC.Conversion.PCUICClosedConv]
wfΓ:1003 [in MetaCoq.PCUIC.PCUICTyping]
wfΓ:1005 [in MetaCoq.Template.Typing]
wfΓ:1007 [in MetaCoq.PCUIC.PCUICTyping]
wfΓ:1015 [in MetaCoq.Template.Typing]
wfΓ:1019 [in MetaCoq.PCUIC.PCUICTyping]
wfΓ:1026 [in MetaCoq.Template.Typing]
wfΓ:1033 [in MetaCoq.Template.Typing]
wfΓ:104 [in MetaCoq.SafeChecker.PCUICSafeChecker]
wfΓ:1040 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΓ:1042 [in MetaCoq.Template.Typing]
wfΓ:1047 [in MetaCoq.SafeChecker.PCUICSafeChecker]
wfΓ:105 [in MetaCoq.PCUIC.PCUICProgress]
wfΓ:1053 [in MetaCoq.Template.Typing]
wfΓ:1053 [in MetaCoq.SafeChecker.PCUICSafeChecker]
wfΓ:1060 [in MetaCoq.SafeChecker.PCUICSafeChecker]
wfΓ:1066 [in MetaCoq.SafeChecker.PCUICSafeChecker]
wfΓ:1073 [in MetaCoq.Template.Typing]
wfΓ:1086 [in MetaCoq.Template.Typing]
wfΓ:109 [in MetaCoq.PCUIC.Bidirectional.BDUnique]
wfΓ:1094 [in MetaCoq.Template.Typing]
wfΓ:1102 [in MetaCoq.Template.Typing]
wfΓ:115 [in MetaCoq.PCUIC.PCUICProgress]
wfΓ:117 [in MetaCoq.SafeChecker.PCUICSafeChecker]
wfΓ:121 [in MetaCoq.PCUIC.Bidirectional.BDUnique]
wfΓ:124 [in MetaCoq.SafeChecker.PCUICSafeChecker]
wfΓ:1298 [in MetaCoq.Template.Typing]
wfΓ:1303 [in MetaCoq.Template.Typing]
wfΓ:131 [in MetaCoq.PCUIC.PCUICProgress]
wfΓ:131 [in MetaCoq.SafeChecker.PCUICSafeChecker]
wfΓ:1313 [in MetaCoq.Template.Typing]
wfΓ:1317 [in MetaCoq.Template.Typing]
wfΓ:1330 [in MetaCoq.Template.Typing]
wfΓ:134 [in MetaCoq.PCUIC.Bidirectional.BDUnique]
wfΓ:138 [in MetaCoq.PCUIC.PCUICProgress]
wfΓ:146 [in MetaCoq.PCUIC.Bidirectional.BDUnique]
wfΓ:147 [in MetaCoq.PCUIC.PCUICProgress]
wfΓ:156 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
wfΓ:158 [in MetaCoq.PCUIC.PCUICProgress]
wfΓ:158 [in MetaCoq.SafeChecker.PCUICSafeChecker]
wfΓ:17 [in MetaCoq.Examples.metacoq_tour_prelude]
wfΓ:170 [in MetaCoq.SafeChecker.PCUICSafeChecker]
wfΓ:178 [in MetaCoq.PCUIC.PCUICProgress]
wfΓ:18 [in MetaCoq.Examples.typing_correctness]
wfΓ:191 [in MetaCoq.PCUIC.PCUICProgress]
wfΓ:199 [in MetaCoq.PCUIC.PCUICProgress]
wfΓ:207 [in MetaCoq.PCUIC.PCUICProgress]
wfΓ:216 [in MetaCoq.PCUIC.PCUICProgress]
wfΓ:225 [in MetaCoq.PCUIC.PCUICProgress]
wfΓ:229 [in MetaCoq.PCUIC.PCUICProgress]
wfΓ:235 [in MetaCoq.PCUIC.PCUICProgress]
wfΓ:240 [in MetaCoq.PCUIC.PCUICProgress]
wfΓ:242 [in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΓ:249 [in MetaCoq.PCUIC.PCUICProgress]
wfΓ:250 [in MetaCoq.Template.TypingWf]
wfΓ:251 [in MetaCoq.SafeChecker.PCUICSafeChecker]
wfΓ:258 [in MetaCoq.PCUIC.PCUICProgress]
wfΓ:268 [in MetaCoq.PCUIC.PCUICProgress]
wfΓ:27 [in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
wfΓ:273 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
wfΓ:276 [in MetaCoq.Template.TypingWf]
wfΓ:281 [in MetaCoq.PCUIC.PCUICProgress]
wfΓ:284 [in MetaCoq.Template.TypingWf]
wfΓ:288 [in MetaCoq.PCUIC.PCUICProgress]
wfΓ:292 [in MetaCoq.SafeChecker.PCUICSafeChecker]
wfΓ:297 [in MetaCoq.PCUIC.PCUICProgress]
wfΓ:308 [in MetaCoq.PCUIC.PCUICProgress]
wfΓ:316 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
wfΓ:323 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
wfΓ:328 [in MetaCoq.PCUIC.PCUICProgress]
wfΓ:339 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
wfΓ:340 [in MetaCoq.PCUIC.PCUICTyping]
wfΓ:341 [in MetaCoq.PCUIC.PCUICProgress]
wfΓ:349 [in MetaCoq.PCUIC.PCUICProgress]
wfΓ:356 [in MetaCoq.Template.EnvironmentTyping]
wfΓ:357 [in MetaCoq.PCUIC.PCUICProgress]
wfΓ:4 [in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
wfΓ:42 [in MetaCoq.PCUIC.Bidirectional.BDUnique]
wfΓ:440 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
wfΓ:456 [in MetaCoq.PCUIC.PCUICTyping]
wfΓ:457 [in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΓ:465 [in MetaCoq.PCUIC.PCUICTyping]
wfΓ:469 [in MetaCoq.PCUIC.PCUICTyping]
wfΓ:475 [in MetaCoq.PCUIC.PCUICTyping]
wfΓ:480 [in MetaCoq.PCUIC.PCUICTyping]
wfΓ:484 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
wfΓ:489 [in MetaCoq.PCUIC.PCUICTyping]
wfΓ:498 [in MetaCoq.PCUIC.PCUICTyping]
wfΓ:500 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
wfΓ:508 [in MetaCoq.PCUIC.PCUICTyping]
wfΓ:51 [in MetaCoq.PCUIC.Bidirectional.BDUnique]
wfΓ:523 [in MetaCoq.PCUIC.PCUICTyping]
wfΓ:530 [in MetaCoq.PCUIC.PCUICTyping]
wfΓ:531 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
wfΓ:539 [in MetaCoq.PCUIC.PCUICTyping]
wfΓ:550 [in MetaCoq.PCUIC.PCUICTyping]
wfΓ:562 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
wfΓ:570 [in MetaCoq.PCUIC.PCUICTyping]
wfΓ:576 [in MetaCoq.SafeChecker.PCUICSafeChecker]
wfΓ:578 [in MetaCoq.SafeChecker.PCUICSafeChecker]
wfΓ:583 [in MetaCoq.PCUIC.PCUICTyping]
wfΓ:59 [in MetaCoq.PCUIC.Bidirectional.BDUnique]
wfΓ:591 [in MetaCoq.PCUIC.PCUICTyping]
wfΓ:599 [in MetaCoq.PCUIC.PCUICTyping]
wfΓ:63 [in MetaCoq.PCUIC.PCUICProgress]
wfΓ:67 [in MetaCoq.PCUIC.Bidirectional.BDUnique]
wfΓ:69 [in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
wfΓ:7 [in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
wfΓ:713 [in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΓ:717 [in MetaCoq.SafeChecker.PCUICSafeChecker]
wfΓ:72 [in MetaCoq.PCUIC.PCUICProgress]
wfΓ:75 [in MetaCoq.PCUIC.Bidirectional.BDUnique]
wfΓ:76 [in MetaCoq.PCUIC.PCUICProgress]
wfΓ:775 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΓ:777 [in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΓ:784 [in MetaCoq.PCUIC.PCUICTyping]
wfΓ:788 [in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΓ:793 [in MetaCoq.PCUIC.PCUICTyping]
wfΓ:795 [in MetaCoq.Template.Typing]
wfΓ:797 [in MetaCoq.PCUIC.PCUICTyping]
wfΓ:800 [in MetaCoq.Template.Typing]
wfΓ:803 [in MetaCoq.PCUIC.PCUICTyping]
wfΓ:808 [in MetaCoq.PCUIC.PCUICTyping]
wfΓ:810 [in MetaCoq.Template.Typing]
wfΓ:817 [in MetaCoq.PCUIC.PCUICTyping]
wfΓ:819 [in MetaCoq.Template.Typing]
wfΓ:82 [in MetaCoq.PCUIC.PCUICProgress]
wfΓ:826 [in MetaCoq.PCUIC.PCUICTyping]
wfΓ:83 [in MetaCoq.PCUIC.Bidirectional.BDUnique]
wfΓ:836 [in MetaCoq.PCUIC.PCUICTyping]
wfΓ:846 [in MetaCoq.PCUIC.PCUICTyping]
wfΓ:85 [in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
wfΓ:853 [in MetaCoq.PCUIC.PCUICTyping]
wfΓ:862 [in MetaCoq.PCUIC.PCUICTyping]
wfΓ:87 [in MetaCoq.PCUIC.PCUICProgress]
wfΓ:873 [in MetaCoq.PCUIC.PCUICTyping]
wfΓ:89 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
wfΓ:893 [in MetaCoq.PCUIC.PCUICTyping]
wfΓ:906 [in MetaCoq.PCUIC.PCUICTyping]
wfΓ:914 [in MetaCoq.PCUIC.PCUICTyping]
wfΓ:922 [in MetaCoq.PCUIC.PCUICTyping]
wfΓ:953 [in MetaCoq.Template.Typing]
wfΓ:953 [in MetaCoq.SafeChecker.PCUICSafeChecker]
wfΓ:96 [in MetaCoq.PCUIC.PCUICProgress]
wfΓ:964 [in MetaCoq.Template.Typing]
wfΓ:968 [in MetaCoq.Template.Typing]
wfΓ:97 [in MetaCoq.PCUIC.Bidirectional.BDUnique]
wfΓ:974 [in MetaCoq.Template.Typing]
wfΓ:979 [in MetaCoq.Template.Typing]
wfΓ:98 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
wfΓ:983 [in MetaCoq.PCUIC.PCUICTyping]
wfΓ:987 [in MetaCoq.Template.Typing]
wfΓ:994 [in MetaCoq.PCUIC.PCUICTyping]
wfΓ:996 [in MetaCoq.Template.Typing]
wfΔ':211 [in MetaCoq.SafeChecker.PCUICSafeChecker]
wfΔ':411 [in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΔ:209 [in MetaCoq.SafeChecker.PCUICSafeChecker]
wfΔ:253 [in MetaCoq.SafeChecker.PCUICSafeChecker]
wfΔ:261 [in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΔ:267 [in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΔ:408 [in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΔ:461 [in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΔ:809 [in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΔ:87 [in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
wfΣ':1322 [in MetaCoq.SafeChecker.PCUICSafeReduce]
wfΣ':181 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
wfΣ':224 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
wfΣ':358 [in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ':364 [in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ':533 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
wfΣ':642 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
wfΣ':647 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ':978 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ0:484 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
wfΣ0:486 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
wfΣ0:492 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
wfΣ0:494 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
wfΣ0:496 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
wfΣ0:498 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
wfΣ0:579 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
wfΣ0:584 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
wfΣ:10 [in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:10 [in MetaCoq.PCUIC.PCUICConversion]
wfΣ:10 [in MetaCoq.PCUIC.PCUICContextConversion]
wfΣ:100 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
wfΣ:100 [in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
wfΣ:1001 [in MetaCoq.PCUIC.PCUICParallelReduction]
wfΣ:1003 [in MetaCoq.Template.Typing]
wfΣ:1006 [in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:1008 [in MetaCoq.PCUIC.PCUICParallelReduction]
wfΣ:101 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
wfΣ:101 [in MetaCoq.PCUIC.TemplateToPCUICExpanded]
wfΣ:1013 [in MetaCoq.Template.Typing]
wfΣ:1017 [in MetaCoq.PCUIC.PCUICParallelReduction]
wfΣ:102 [in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
wfΣ:1024 [in MetaCoq.Template.Typing]
wfΣ:1026 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:1028 [in MetaCoq.PCUIC.PCUICParallelReduction]
wfΣ:103 [in MetaCoq.PCUIC.PCUICProgress]
wfΣ:103 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
wfΣ:103 [in MetaCoq.Erasure.Prelim]
wfΣ:1031 [in MetaCoq.Template.Typing]
wfΣ:1039 [in MetaCoq.PCUIC.PCUICParallelReduction]
wfΣ:104 [in MetaCoq.SafeChecker.PCUICWfReduction]
wfΣ:104 [in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
wfΣ:1040 [in MetaCoq.Template.Typing]
wfΣ:1048 [in MetaCoq.PCUIC.PCUICConversion]
wfΣ:105 [in MetaCoq.PCUIC.PCUICValidity]
wfΣ:1051 [in MetaCoq.Template.Typing]
wfΣ:1055 [in MetaCoq.PCUIC.PCUICConversion]
wfΣ:107 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
wfΣ:107 [in MetaCoq.PCUIC.Bidirectional.BDUnique]
wfΣ:107 [in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
wfΣ:1071 [in MetaCoq.Template.Typing]
wfΣ:1075 [in MetaCoq.PCUIC.PCUICConversion]
wfΣ:108 [in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
wfΣ:1084 [in MetaCoq.Template.Typing]
wfΣ:1089 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:109 [in MetaCoq.SafeChecker.PCUICWfEnv]
wfΣ:109 [in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
wfΣ:1092 [in MetaCoq.Template.Typing]
wfΣ:1092 [in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:11 [in MetaCoq.Erasure.ErasureProperties]
wfΣ:11 [in MetaCoq.PCUIC.PCUICCanonicity]
wfΣ:110 [in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:1100 [in MetaCoq.Template.Typing]
wfΣ:1100 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:1108 [in MetaCoq.Template.Typing]
wfΣ:111 [in MetaCoq.PCUIC.PCUICCumulProp]
wfΣ:1113 [in MetaCoq.Template.Typing]
wfΣ:1115 [in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:1118 [in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:112 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
wfΣ:1121 [in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:1122 [in MetaCoq.PCUIC.PCUICConversion]
wfΣ:1124 [in MetaCoq.Template.Typing]
wfΣ:1124 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:1124 [in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:1129 [in MetaCoq.Template.Typing]
wfΣ:1129 [in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:113 [in MetaCoq.PCUIC.PCUICProgress]
wfΣ:1131 [in MetaCoq.PCUIC.PCUICConversion]
wfΣ:1137 [in MetaCoq.Erasure.ErasureFunction]
wfΣ:1139 [in MetaCoq.PCUIC.PCUICConversion]
wfΣ:114 [in MetaCoq.Erasure.EArities]
wfΣ:114 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
wfΣ:114 [in MetaCoq.PCUIC.PCUICValidity]
wfΣ:114 [in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:114 [in MetaCoq.SafeChecker.PCUICWfEnv]
wfΣ:114 [in MetaCoq.SafeChecker.PCUICWfReduction]
wfΣ:114 [in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
wfΣ:114 [in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
wfΣ:114 [in MetaCoq.Erasure.Prelim]
wfΣ:115 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
wfΣ:1153 [in MetaCoq.Erasure.ErasureFunction]
wfΣ:117 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
wfΣ:117 [in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
wfΣ:1177 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:1179 [in MetaCoq.PCUIC.PCUICConversion]
wfΣ:118 [in MetaCoq.PCUIC.PCUICCumulProp]
wfΣ:1182 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:119 [in MetaCoq.SafeChecker.PCUICWfEnv]
wfΣ:119 [in MetaCoq.PCUIC.Bidirectional.BDUnique]
wfΣ:119 [in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
wfΣ:1192 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:1198 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:1199 [in MetaCoq.Erasure.ErasureFunction]
wfΣ:12 [in MetaCoq.PCUIC.PCUICCumulProp]
wfΣ:12 [in MetaCoq.Erasure.ETransform]
wfΣ:120 [in MetaCoq.PCUIC.PCUICElimination]
wfΣ:120 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
wfΣ:120 [in MetaCoq.PCUIC.PCUICContexts]
wfΣ:120 [in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
wfΣ:1201 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:1207 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:121 [in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
wfΣ:121 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
wfΣ:121 [in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
wfΣ:121 [in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
wfΣ:1211 [in MetaCoq.Erasure.ErasureFunction]
wfΣ:1212 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:1221 [in MetaCoq.PCUIC.PCUICConversion]
wfΣ:1223 [in MetaCoq.Erasure.ErasureFunction]
wfΣ:123 [in MetaCoq.PCUIC.PCUICCumulProp]
wfΣ:1233 [in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:1236 [in MetaCoq.Erasure.ErasureFunction]
wfΣ:1239 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:124 [in MetaCoq.SafeChecker.PCUICWfEnv]
wfΣ:1241 [in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:1242 [in MetaCoq.PCUIC.PCUICConfluence]
wfΣ:1243 [in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:1245 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:1246 [in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:1248 [in MetaCoq.PCUIC.PCUICConversion]
wfΣ:1251 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:1251 [in MetaCoq.Erasure.ErasureFunction]
wfΣ:1264 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:1265 [in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:1268 [in MetaCoq.SafeChecker.PCUICSafeReduce]
wfΣ:1268 [in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:1268 [in MetaCoq.PCUIC.PCUICConversion]
wfΣ:1271 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:1273 [in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:1278 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:128 [in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
wfΣ:128 [in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
wfΣ:1281 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:1285 [in MetaCoq.SafeChecker.PCUICSafeReduce]
wfΣ:1289 [in MetaCoq.SafeChecker.PCUICSafeReduce]
wfΣ:129 [in MetaCoq.PCUIC.PCUICProgress]
wfΣ:129 [in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
wfΣ:1293 [in MetaCoq.Erasure.ErasureFunction]
wfΣ:1294 [in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:1296 [in MetaCoq.SafeChecker.PCUICSafeReduce]
wfΣ:1297 [in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:13 [in MetaCoq.PCUIC.PCUICSR]
wfΣ:130 [in MetaCoq.PCUIC.PCUICFirstorder]
wfΣ:1300 [in MetaCoq.SafeChecker.PCUICSafeReduce]
wfΣ:1301 [in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:1304 [in MetaCoq.SafeChecker.PCUICSafeReduce]
wfΣ:1308 [in MetaCoq.SafeChecker.PCUICSafeReduce]
wfΣ:1309 [in MetaCoq.Erasure.ErasureFunction]
wfΣ:1317 [in MetaCoq.SafeChecker.PCUICSafeReduce]
wfΣ:132 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
wfΣ:132 [in MetaCoq.PCUIC.Bidirectional.BDUnique]
wfΣ:1328 [in MetaCoq.SafeChecker.PCUICSafeReduce]
wfΣ:133 [in MetaCoq.Erasure.ErasureProperties]
wfΣ:133 [in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:1334 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:1334 [in MetaCoq.SafeChecker.PCUICSafeReduce]
wfΣ:135 [in MetaCoq.Erasure.EArities]
wfΣ:135 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
wfΣ:135 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
wfΣ:135 [in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
wfΣ:1359 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:136 [in MetaCoq.PCUIC.PCUICProgress]
wfΣ:136 [in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
wfΣ:1365 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:137 [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
wfΣ:1370 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:138 [in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:1382 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:139 [in MetaCoq.PCUIC.PCUICFirstorder]
wfΣ:14 [in MetaCoq.PCUIC.PCUICInductives]
wfΣ:14 [in MetaCoq.PCUIC.PCUICConvCumInversion]
wfΣ:140 [in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
wfΣ:1403 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:141 [in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:141 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
wfΣ:1419 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
wfΣ:142 [in MetaCoq.SafeChecker.PCUICSafeReduce]
wfΣ:142 [in MetaCoq.PCUIC.PCUICCanonicity]
wfΣ:144 [in MetaCoq.PCUIC.Bidirectional.BDUnique]
wfΣ:144 [in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
wfΣ:1447 [in MetaCoq.SafeChecker.PCUICSafeReduce]
wfΣ:145 [in MetaCoq.PCUIC.PCUICProgress]
wfΣ:145 [in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
wfΣ:145 [in MetaCoq.PCUIC.PCUICSpine]
wfΣ:146 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
wfΣ:146 [in MetaCoq.SafeChecker.PCUICSafeReduce]
wfΣ:1471 [in MetaCoq.SafeChecker.PCUICSafeReduce]
wfΣ:1475 [in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:148 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
wfΣ:148 [in MetaCoq.PCUIC.PCUICAlpha]
wfΣ:148 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
wfΣ:148 [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
wfΣ:148 [in MetaCoq.SafeChecker.PCUICSafeChecker]
wfΣ:1480 [in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:1483 [in MetaCoq.SafeChecker.PCUICSafeReduce]
wfΣ:1488 [in MetaCoq.SafeChecker.PCUICSafeReduce]
wfΣ:149 [in MetaCoq.PCUIC.PCUICSR]
wfΣ:1492 [in MetaCoq.SafeChecker.PCUICSafeReduce]
wfΣ:1496 [in MetaCoq.SafeChecker.PCUICSafeReduce]
wfΣ:150 [in MetaCoq.Erasure.ErasureProperties]
wfΣ:151 [in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
wfΣ:151 [in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
wfΣ:152 [in MetaCoq.PCUIC.PCUICSR]
wfΣ:1522 [in MetaCoq.Erasure.ErasureFunction]
wfΣ:1525 [in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:1531 [in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:154 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
wfΣ:1540 [in MetaCoq.Erasure.ErasureFunction]
wfΣ:1544 [in MetaCoq.SafeChecker.PCUICSafeReduce]
wfΣ:155 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
wfΣ:155 [in MetaCoq.PCUIC.Bidirectional.BDUnique]
wfΣ:1551 [in MetaCoq.SafeChecker.PCUICSafeReduce]
wfΣ:1557 [in MetaCoq.SafeChecker.PCUICSafeReduce]
wfΣ:156 [in MetaCoq.PCUIC.PCUICProgress]
wfΣ:156 [in MetaCoq.SafeChecker.PCUICSafeReduce]
wfΣ:157 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
wfΣ:158 [in MetaCoq.PCUIC.PCUICFirstorder]
wfΣ:159 [in MetaCoq.PCUIC.PCUICCumulProp]
wfΣ:159 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
wfΣ:16 [in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
wfΣ:160 [in MetaCoq.SafeChecker.PCUICSafeReduce]
wfΣ:1608 [in MetaCoq.SafeChecker.PCUICSafeReduce]
wfΣ:1617 [in MetaCoq.SafeChecker.PCUICSafeReduce]
wfΣ:162 [in MetaCoq.PCUIC.PCUICSR]
wfΣ:1623 [in MetaCoq.SafeChecker.PCUICSafeReduce]
wfΣ:164 [in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
wfΣ:165 [in MetaCoq.PCUIC.PCUICInductives]
wfΣ:165 [in MetaCoq.PCUIC.PCUICCumulProp]
wfΣ:167 [in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:17 [in MetaCoq.PCUIC.PCUICSafeLemmata]
wfΣ:171 [in MetaCoq.PCUIC.PCUICInductives]
wfΣ:171 [in MetaCoq.PCUIC.PCUICCumulProp]
wfΣ:171 [in MetaCoq.SafeChecker.PCUICSafeReduce]
wfΣ:171 [in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
wfΣ:172 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
wfΣ:172 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
wfΣ:172 [in MetaCoq.PCUIC.PCUICSR]
wfΣ:172 [in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:1727 [in MetaCoq.SafeChecker.PCUICSafeReduce]
wfΣ:173 [in MetaCoq.SafeChecker.PCUICSafeReduce]
wfΣ:175 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
wfΣ:175 [in MetaCoq.PCUIC.PCUICFirstorder]
wfΣ:1754 [in MetaCoq.SafeChecker.PCUICSafeReduce]
wfΣ:1759 [in MetaCoq.SafeChecker.PCUICSafeReduce]
wfΣ:176 [in MetaCoq.PCUIC.PCUICProgress]
wfΣ:176 [in MetaCoq.PCUIC.PCUICAlpha]
wfΣ:176 [in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:1765 [in MetaCoq.SafeChecker.PCUICSafeReduce]
wfΣ:177 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
wfΣ:177 [in MetaCoq.PCUIC.PCUICCumulProp]
wfΣ:177 [in MetaCoq.SafeChecker.PCUICWfEnv]
wfΣ:1770 [in MetaCoq.SafeChecker.PCUICSafeReduce]
wfΣ:178 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
wfΣ:1784 [in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:1789 [in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:179 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
wfΣ:1795 [in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:18 [in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
wfΣ:18 [in MetaCoq.PCUIC.PCUICSpine]
wfΣ:180 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
wfΣ:181 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
wfΣ:181 [in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:181 [in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:182 [in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
wfΣ:183 [in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
wfΣ:185 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
wfΣ:187 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
wfΣ:189 [in MetaCoq.PCUIC.PCUICProgress]
wfΣ:189 [in MetaCoq.PCUIC.PCUICSR]
wfΣ:189 [in MetaCoq.PCUIC.PCUICContexts]
wfΣ:19 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
wfΣ:19 [in MetaCoq.PCUIC.PCUICCanonicity]
wfΣ:190 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
wfΣ:191 [in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:194 [in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
wfΣ:195 [in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:1955 [in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:1957 [in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:197 [in MetaCoq.PCUIC.PCUICProgress]
wfΣ:197 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
wfΣ:198 [in MetaCoq.PCUIC.PCUICSR]
wfΣ:20 [in MetaCoq.PCUIC.PCUICSafeLemmata]
wfΣ:201 [in MetaCoq.PCUIC.PCUICAlpha]
wfΣ:201 [in MetaCoq.SafeChecker.PCUICWfEnv]
wfΣ:202 [in MetaCoq.PCUIC.PCUICSubstitution]
wfΣ:202 [in MetaCoq.PCUIC.PCUICContexts]
wfΣ:203 [in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:2040 [in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:2048 [in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:205 [in MetaCoq.PCUIC.PCUICProgress]
wfΣ:205 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
wfΣ:2056 [in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:207 [in MetaCoq.PCUIC.PCUICSubstitution]
wfΣ:207 [in MetaCoq.PCUIC.PCUICContexts]
wfΣ:2076 [in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:208 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
wfΣ:208 [in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:2092 [in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:2099 [in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:210 [in MetaCoq.PCUIC.PCUICAlpha]
wfΣ:211 [in MetaCoq.PCUIC.PCUICSR]
wfΣ:211 [in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:2111 [in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:212 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
wfΣ:212 [in MetaCoq.PCUIC.PCUICSubstitution]
wfΣ:2120 [in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:2134 [in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:215 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
wfΣ:2167 [in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:217 [in MetaCoq.PCUIC.PCUICCumulProp]
wfΣ:218 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
wfΣ:219 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
wfΣ:219 [in MetaCoq.PCUIC.PCUICInductives]
wfΣ:221 [in MetaCoq.PCUIC.PCUICSubstitution]
wfΣ:222 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
wfΣ:223 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
wfΣ:223 [in MetaCoq.PCUIC.PCUICProgress]
wfΣ:223 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
wfΣ:223 [in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:224 [in MetaCoq.Erasure.EArities]
wfΣ:225 [in MetaCoq.PCUIC.PCUICCumulProp]
wfΣ:225 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
wfΣ:226 [in MetaCoq.PCUIC.PCUICConversion]
wfΣ:227 [in MetaCoq.PCUIC.PCUICProgress]
wfΣ:228 [in MetaCoq.Erasure.EArities]
wfΣ:228 [in MetaCoq.PCUIC.PCUICAlpha]
wfΣ:229 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:23 [in MetaCoq.PCUIC.Typing.PCUICInstTyp]
wfΣ:23 [in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:230 [in MetaCoq.PCUIC.PCUICWfUniverses]
wfΣ:230 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
wfΣ:230 [in MetaCoq.SafeChecker.PCUICWfEnv]
wfΣ:232 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
wfΣ:232 [in MetaCoq.PCUIC.PCUICConversion]
wfΣ:233 [in MetaCoq.PCUIC.PCUICProgress]
wfΣ:233 [in MetaCoq.PCUIC.PCUICCumulProp]
wfΣ:2338 [in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:234 [in MetaCoq.PCUIC.PCUICWfUniverses]
wfΣ:234 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
wfΣ:235 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:236 [in MetaCoq.Erasure.EArities]
wfΣ:238 [in MetaCoq.PCUIC.PCUICProgress]
wfΣ:238 [in MetaCoq.PCUIC.PCUICWfUniverses]
wfΣ:238 [in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:2399 [in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:24 [in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
wfΣ:24 [in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
wfΣ:240 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
wfΣ:240 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
wfΣ:241 [in MetaCoq.PCUIC.PCUICCumulProp]
wfΣ:241 [in MetaCoq.SafeChecker.PCUICSafeChecker]
wfΣ:241 [in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:242 [in MetaCoq.PCUIC.PCUICWfUniverses]
wfΣ:243 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
wfΣ:245 [in MetaCoq.SafeChecker.PCUICSafeChecker]
wfΣ:245 [in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:246 [in MetaCoq.PCUIC.PCUICWfUniverses]
wfΣ:246 [in MetaCoq.PCUIC.PCUICCumulProp]
wfΣ:247 [in MetaCoq.PCUIC.PCUICProgress]
wfΣ:248 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
wfΣ:25 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
wfΣ:25 [in MetaCoq.Erasure.ErasureFunction]
wfΣ:25 [in MetaCoq.PCUIC.PCUICConvCumInversion]
wfΣ:25 [in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:25 [in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
wfΣ:250 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
wfΣ:254 [in MetaCoq.PCUIC.PCUICSR]
wfΣ:255 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
wfΣ:255 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
wfΣ:255 [in MetaCoq.PCUIC.PCUICCumulProp]
wfΣ:2551 [in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:256 [in MetaCoq.PCUIC.PCUICProgress]
wfΣ:256 [in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:256 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
wfΣ:257 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
wfΣ:257 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
wfΣ:259 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
wfΣ:26 [in MetaCoq.PCUIC.PCUICInductives]
wfΣ:26 [in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:260 [in MetaCoq.PCUIC.PCUICWfUniverses]
wfΣ:261 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
wfΣ:261 [in MetaCoq.PCUIC.PCUICSR]
wfΣ:261 [in MetaCoq.SafeChecker.PCUICSafeChecker]
wfΣ:263 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
wfΣ:263 [in MetaCoq.PCUIC.PCUICCumulProp]
wfΣ:263 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
wfΣ:263 [in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:264 [in MetaCoq.PCUIC.PCUICWfUniverses]
wfΣ:264 [in MetaCoq.PCUIC.PCUICAlpha]
wfΣ:265 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
wfΣ:265 [in MetaCoq.SafeChecker.PCUICSafeChecker]
wfΣ:266 [in MetaCoq.PCUIC.PCUICProgress]
wfΣ:266 [in MetaCoq.PCUIC.PCUICSR]
wfΣ:266 [in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:267 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
wfΣ:268 [in MetaCoq.PCUIC.PCUICAlpha]
wfΣ:269 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
wfΣ:269 [in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:269 [in MetaCoq.PCUIC.PCUICCumulProp]
wfΣ:269 [in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:27 [in MetaCoq.Erasure.ErasureFunction]
wfΣ:27 [in MetaCoq.PCUIC.Typing.PCUICWeakeningTyp]
wfΣ:271 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
wfΣ:273 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
wfΣ:273 [in MetaCoq.PCUIC.PCUICAlpha]
wfΣ:273 [in MetaCoq.PCUIC.PCUICSR]
wfΣ:275 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
wfΣ:275 [in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:276 [in MetaCoq.PCUIC.PCUICConversion]
wfΣ:277 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
wfΣ:277 [in MetaCoq.PCUIC.PCUICCumulProp]
wfΣ:278 [in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:278 [in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:279 [in MetaCoq.PCUIC.PCUICProgress]
wfΣ:279 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
wfΣ:279 [in MetaCoq.PCUIC.PCUICAlpha]
wfΣ:280 [in MetaCoq.PCUIC.PCUICSR]
wfΣ:281 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
wfΣ:281 [in MetaCoq.SafeChecker.PCUICSafeChecker]
wfΣ:281 [in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:282 [in MetaCoq.Template.TypingWf]
wfΣ:283 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
wfΣ:284 [in MetaCoq.Erasure.EArities]
wfΣ:285 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
wfΣ:285 [in MetaCoq.PCUIC.PCUICCumulProp]
wfΣ:285 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
wfΣ:285 [in MetaCoq.SafeChecker.PCUICSafeChecker]
wfΣ:286 [in MetaCoq.PCUIC.PCUICProgress]
wfΣ:286 [in MetaCoq.Template.TypingWf]
wfΣ:287 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
wfΣ:287 [in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:288 [in MetaCoq.PCUIC.PCUICSR]
wfΣ:288 [in MetaCoq.Template.TypingWf]
wfΣ:289 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
wfΣ:29 [in MetaCoq.PCUIC.PCUICArities]
wfΣ:29 [in MetaCoq.PCUIC.PCUICCumulProp]
wfΣ:29 [in MetaCoq.PCUIC.PCUICPrincipality]
wfΣ:290 [in MetaCoq.Erasure.EArities]
wfΣ:291 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
wfΣ:291 [in MetaCoq.PCUIC.PCUICInductives]
wfΣ:291 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
wfΣ:293 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
wfΣ:295 [in MetaCoq.PCUIC.PCUICProgress]
wfΣ:295 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
wfΣ:295 [in MetaCoq.Template.TypingWf]
wfΣ:296 [in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:297 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
wfΣ:297 [in MetaCoq.Template.TypingWf]
wfΣ:299 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
wfΣ:299 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
wfΣ:3 [in MetaCoq.PCUIC.Typing.PCUICInstTyp]
wfΣ:3 [in MetaCoq.PCUIC.PCUICSafeLemmata]
wfΣ:3 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
wfΣ:3 [in MetaCoq.PCUIC.PCUICInversion]
wfΣ:3 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
wfΣ:3 [in MetaCoq.Erasure.ErasureFunction]
wfΣ:3 [in MetaCoq.SafeChecker.PCUICSafeReduce]
wfΣ:3 [in MetaCoq.PCUIC.PCUICPrincipality]
wfΣ:3 [in MetaCoq.Erasure.ETransform]
wfΣ:3 [in MetaCoq.PCUIC.Typing.PCUICWeakeningTyp]
wfΣ:3 [in MetaCoq.PCUIC.Bidirectional.BDUnique]
wfΣ:3 [in MetaCoq.PCUIC.PCUICSR]
wfΣ:3 [in MetaCoq.PCUIC.PCUICContextReduction]
wfΣ:30 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
wfΣ:30 [in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:300 [in MetaCoq.PCUIC.PCUICSR]
wfΣ:301 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
wfΣ:303 [in MetaCoq.Template.TypingWf]
wfΣ:304 [in MetaCoq.PCUIC.PCUICCumulProp]
wfΣ:304 [in MetaCoq.SafeChecker.PCUICSafeChecker]
wfΣ:305 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:306 [in MetaCoq.PCUIC.PCUICProgress]
wfΣ:307 [in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:308 [in MetaCoq.SafeChecker.PCUICSafeChecker]
wfΣ:31 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
wfΣ:31 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
wfΣ:31 [in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
wfΣ:31 [in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
wfΣ:315 [in MetaCoq.PCUIC.PCUICInductives]
wfΣ:318 [in MetaCoq.PCUIC.PCUICTyping]
wfΣ:32 [in MetaCoq.PCUIC.Typing.PCUICInstTyp]
wfΣ:32 [in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:32 [in MetaCoq.PCUIC.PCUICSpine]
wfΣ:325 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
wfΣ:326 [in MetaCoq.PCUIC.PCUICProgress]
wfΣ:326 [in MetaCoq.PCUIC.PCUICInductives]
wfΣ:326 [in MetaCoq.PCUIC.PCUICCumulProp]
wfΣ:327 [in MetaCoq.PCUIC.PCUICTyping]
wfΣ:337 [in MetaCoq.PCUIC.PCUICCumulProp]
wfΣ:338 [in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:338 [in MetaCoq.PCUIC.PCUICTyping]
wfΣ:339 [in MetaCoq.PCUIC.PCUICProgress]
wfΣ:34 [in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
wfΣ:34 [in MetaCoq.PCUIC.Typing.PCUICWeakeningTyp]
wfΣ:342 [in MetaCoq.PCUIC.PCUICWcbvEval]
wfΣ:344 [in MetaCoq.PCUIC.PCUICCumulProp]
wfΣ:346 [in MetaCoq.Erasure.EArities]
wfΣ:347 [in MetaCoq.PCUIC.PCUICProgress]
wfΣ:347 [in MetaCoq.PCUIC.PCUICCumulProp]
wfΣ:347 [in MetaCoq.SafeChecker.PCUICSafeReduce]
wfΣ:347 [in MetaCoq.PCUIC.PCUICTyping]
wfΣ:349 [in MetaCoq.PCUIC.PCUICInductives]
wfΣ:349 [in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:35 [in MetaCoq.PCUIC.PCUICProgress]
wfΣ:35 [in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
wfΣ:352 [in MetaCoq.Erasure.EArities]
wfΣ:352 [in MetaCoq.SafeChecker.PCUICSafeReduce]
wfΣ:355 [in MetaCoq.PCUIC.PCUICProgress]
wfΣ:355 [in MetaCoq.PCUIC.PCUICCumulProp]
wfΣ:355 [in MetaCoq.SafeChecker.PCUICSafeReduce]
wfΣ:358 [in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:359 [in MetaCoq.SafeChecker.PCUICSafeReduce]
wfΣ:36 [in MetaCoq.PCUIC.PCUICArities]
wfΣ:365 [in MetaCoq.PCUIC.PCUICCumulProp]
wfΣ:369 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
wfΣ:369 [in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:37 [in MetaCoq.Erasure.EArities]
wfΣ:37 [in MetaCoq.PCUIC.PCUICSpine]
wfΣ:371 [in MetaCoq.PCUIC.PCUICProgress]
wfΣ:371 [in MetaCoq.PCUIC.PCUICSubstitution]
wfΣ:371 [in MetaCoq.SafeChecker.PCUICSafeChecker]
wfΣ:377 [in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:38 [in MetaCoq.PCUIC.PCUICInductives]
wfΣ:38 [in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
wfΣ:38 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
wfΣ:38 [in MetaCoq.PCUIC.PCUICSR]
wfΣ:38 [in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:380 [in MetaCoq.PCUIC.PCUICContextConversion]
wfΣ:381 [in MetaCoq.PCUIC.PCUICProgress]
wfΣ:381 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
wfΣ:384 [in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:385 [in MetaCoq.PCUIC.PCUICContextConversion]
wfΣ:389 [in MetaCoq.PCUIC.PCUICProgress]
wfΣ:39 [in MetaCoq.PCUIC.PCUICElimination]
wfΣ:39 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
wfΣ:39 [in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
wfΣ:392 [in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:393 [in MetaCoq.PCUIC.PCUICContextConversion]
wfΣ:398 [in MetaCoq.PCUIC.PCUICContextConversion]
wfΣ:40 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
wfΣ:40 [in MetaCoq.PCUIC.PCUICConvCumInversion]
wfΣ:40 [in MetaCoq.PCUIC.Bidirectional.BDUnique]
wfΣ:400 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
wfΣ:401 [in MetaCoq.PCUIC.PCUICProgress]
wfΣ:402 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:403 [in MetaCoq.PCUIC.PCUICContextConversion]
wfΣ:405 [in MetaCoq.PCUIC.PCUICInductives]
wfΣ:405 [in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:405 [in MetaCoq.PCUIC.PCUICConversion]
wfΣ:407 [in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:408 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:410 [in MetaCoq.PCUIC.PCUICContextConversion]
wfΣ:410 [in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:413 [in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:414 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:415 [in MetaCoq.PCUIC.PCUICConversion]
wfΣ:415 [in MetaCoq.SafeChecker.PCUICSafeChecker]
wfΣ:416 [in MetaCoq.Template.EtaExpand]
wfΣ:416 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
wfΣ:418 [in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:418 [in MetaCoq.PCUIC.PCUICContextConversion]
wfΣ:419 [in MetaCoq.PCUIC.PCUICProgress]
wfΣ:419 [in MetaCoq.PCUIC.PCUICInductives]
wfΣ:42 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
wfΣ:42 [in MetaCoq.PCUIC.Typing.PCUICWeakeningTyp]
wfΣ:42 [in MetaCoq.PCUIC.PCUICSpine]
wfΣ:421 [in MetaCoq.SafeChecker.PCUICSafeChecker]
wfΣ:424 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
wfΣ:426 [in MetaCoq.Template.EtaExpand]
wfΣ:426 [in MetaCoq.PCUIC.PCUICProgress]
wfΣ:430 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
wfΣ:433 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
wfΣ:433 [in MetaCoq.SafeChecker.PCUICSafeChecker]
wfΣ:434 [in MetaCoq.PCUIC.PCUICProgress]
wfΣ:434 [in MetaCoq.PCUIC.PCUICSubstitution]
wfΣ:436 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
wfΣ:438 [in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:4393 [in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:44 [in MetaCoq.PCUIC.PCUICProgress]
wfΣ:44 [in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:442 [in MetaCoq.PCUIC.PCUICConversion]
wfΣ:443 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
wfΣ:4430 [in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:448 [in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:45 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
wfΣ:45 [in MetaCoq.PCUIC.Conversion.PCUICClosedConv]
wfΣ:456 [in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:4577 [in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:459 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
wfΣ:46 [in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
wfΣ:46 [in MetaCoq.PCUIC.PCUICGlobalEnv]
wfΣ:460 [in MetaCoq.PCUIC.PCUICSubstitution]
wfΣ:460 [in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:461 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:462 [in MetaCoq.PCUIC.PCUICNormal]
wfΣ:463 [in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:463 [in MetaCoq.PCUIC.PCUICTyping]
wfΣ:465 [in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:467 [in MetaCoq.PCUIC.PCUICTyping]
wfΣ:4670 [in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:47 [in MetaCoq.PCUIC.PCUICArities]
wfΣ:471 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:472 [in MetaCoq.PCUIC.PCUICSpine]
wfΣ:473 [in MetaCoq.PCUIC.PCUICTyping]
wfΣ:475 [in MetaCoq.SafeChecker.PCUICSafeChecker]
wfΣ:478 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:478 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
wfΣ:478 [in MetaCoq.PCUIC.PCUICTyping]
wfΣ:479 [in MetaCoq.PCUIC.PCUICNormal]
wfΣ:48 [in MetaCoq.PCUIC.Conversion.PCUICClosedConv]
wfΣ:485 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:4861 [in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:487 [in MetaCoq.PCUIC.PCUICTyping]
wfΣ:4870 [in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:488 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
wfΣ:4882 [in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:489 [in MetaCoq.PCUIC.PCUICNormal]
wfΣ:49 [in MetaCoq.PCUIC.PCUICCumulProp]
wfΣ:49 [in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
wfΣ:49 [in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:49 [in MetaCoq.PCUIC.Bidirectional.BDUnique]
wfΣ:490 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
wfΣ:491 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:491 [in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:492 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
wfΣ:492 [in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:494 [in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:496 [in MetaCoq.PCUIC.PCUICTyping]
wfΣ:497 [in MetaCoq.PCUIC.PCUICInductives]
wfΣ:497 [in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:499 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
wfΣ:5 [in MetaCoq.PCUIC.PCUICCumulProp]
wfΣ:501 [in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:502 [in MetaCoq.PCUIC.PCUICConversion]
wfΣ:502 [in MetaCoq.PCUIC.PCUICSR]
wfΣ:503 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:506 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
wfΣ:506 [in MetaCoq.PCUIC.PCUICTyping]
wfΣ:508 [in MetaCoq.PCUIC.PCUICSR]
wfΣ:5088 [in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:509 [in MetaCoq.PCUIC.PCUICInductives]
wfΣ:5095 [in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:51 [in MetaCoq.PCUIC.PCUICElimination]
wfΣ:51 [in MetaCoq.PCUIC.PCUICSafeLemmata]
wfΣ:51 [in MetaCoq.Erasure.EArities]
wfΣ:51 [in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
wfΣ:51 [in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:510 [in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:511 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
wfΣ:511 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:514 [in MetaCoq.PCUIC.PCUICSR]
wfΣ:515 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
wfΣ:515 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
wfΣ:517 [in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:518 [in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:519 [in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:5195 [in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:52 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
wfΣ:52 [in MetaCoq.PCUIC.PCUICCanonicity]
wfΣ:520 [in MetaCoq.SafeChecker.PCUICSafeChecker]
wfΣ:5203 [in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:521 [in MetaCoq.PCUIC.PCUICInductives]
wfΣ:521 [in MetaCoq.PCUIC.PCUICTyping]
wfΣ:521 [in MetaCoq.PCUIC.PCUICSR]
wfΣ:5211 [in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:5225 [in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:524 [in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:527 [in MetaCoq.SafeChecker.PCUICSafeChecker]
wfΣ:528 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:528 [in MetaCoq.PCUIC.PCUICTyping]
wfΣ:528 [in MetaCoq.PCUIC.PCUICSR]
wfΣ:53 [in MetaCoq.SafeChecker.PCUICSafeChecker]
wfΣ:530 [in MetaCoq.Template.EtaExpand]
wfΣ:532 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
wfΣ:532 [in MetaCoq.PCUIC.PCUICInductives]
wfΣ:534 [in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:535 [in MetaCoq.PCUIC.PCUICSR]
wfΣ:536 [in MetaCoq.Template.EtaExpand]
wfΣ:537 [in MetaCoq.PCUIC.PCUICTyping]
wfΣ:538 [in MetaCoq.PCUIC.PCUICInductives]
wfΣ:538 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:54 [in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:546 [in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:548 [in MetaCoq.PCUIC.PCUICTyping]
wfΣ:55 [in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
wfΣ:550 [in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:553 [in MetaCoq.PCUIC.PCUICSR]
wfΣ:554 [in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:558 [in MetaCoq.PCUIC.PCUICSR]
wfΣ:56 [in MetaCoq.SafeChecker.PCUICSafeChecker]
wfΣ:5604 [in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:562 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
wfΣ:5644 [in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:565 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
wfΣ:565 [in MetaCoq.PCUIC.PCUICSR]
wfΣ:5651 [in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:5664 [in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:5675 [in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:568 [in MetaCoq.PCUIC.PCUICTyping]
wfΣ:569 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
wfΣ:5690 [in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:5694 [in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:5697 [in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:57 [in MetaCoq.PCUIC.PCUICSafeLemmata]
wfΣ:57 [in MetaCoq.PCUIC.PCUICConvCumInversion]
wfΣ:57 [in MetaCoq.PCUIC.Bidirectional.BDUnique]
wfΣ:57 [in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:5705 [in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:571 [in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:572 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
wfΣ:572 [in MetaCoq.PCUIC.PCUICSR]
wfΣ:577 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
wfΣ:58 [in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:58 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
wfΣ:58 [in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
wfΣ:58 [in MetaCoq.PCUIC.PCUICSR]
wfΣ:581 [in MetaCoq.PCUIC.PCUICTyping]
wfΣ:582 [in MetaCoq.PCUIC.PCUICSR]
wfΣ:584 [in MetaCoq.PCUIC.PCUICSubstitution]
wfΣ:585 [in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:589 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
wfΣ:589 [in MetaCoq.PCUIC.PCUICTyping]
wfΣ:589 [in MetaCoq.SafeChecker.PCUICSafeChecker]
wfΣ:59 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
wfΣ:59 [in MetaCoq.PCUIC.TemplateToPCUICExpanded]
wfΣ:590 [in MetaCoq.PCUIC.PCUICSR]
wfΣ:591 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
wfΣ:593 [in MetaCoq.PCUIC.PCUICSubstitution]
wfΣ:597 [in MetaCoq.PCUIC.PCUICTyping]
wfΣ:6 [in MetaCoq.Erasure.ETransform]
wfΣ:6 [in MetaCoq.PCUIC.PCUICConversion]
wfΣ:60 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
wfΣ:601 [in MetaCoq.PCUIC.PCUICSubstitution]
wfΣ:605 [in MetaCoq.PCUIC.PCUICTyping]
wfΣ:607 [in MetaCoq.PCUIC.PCUICSR]
wfΣ:608 [in MetaCoq.PCUIC.PCUICSubstitution]
wfΣ:608 [in MetaCoq.PCUIC.PCUICInductives]
wfΣ:608 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:610 [in MetaCoq.PCUIC.PCUICTyping]
wfΣ:614 [in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:616 [in MetaCoq.PCUIC.PCUICInductives]
wfΣ:617 [in MetaCoq.PCUIC.PCUICSubstitution]
wfΣ:618 [in MetaCoq.PCUIC.PCUICSR]
wfΣ:619 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:62 [in MetaCoq.Erasure.EArities]
wfΣ:620 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
wfΣ:621 [in MetaCoq.PCUIC.PCUICTyping]
wfΣ:625 [in MetaCoq.PCUIC.PCUICSR]
wfΣ:626 [in MetaCoq.PCUIC.PCUICSubstitution]
wfΣ:626 [in MetaCoq.PCUIC.PCUICTyping]
wfΣ:628 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:63 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
wfΣ:63 [in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:631 [in MetaCoq.PCUIC.PCUICInductives]
wfΣ:631 [in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:632 [in MetaCoq.PCUIC.PCUICSR]
wfΣ:635 [in MetaCoq.PCUIC.PCUICConfluence]
wfΣ:636 [in MetaCoq.PCUIC.PCUICSubstitution]
wfΣ:638 [in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:638 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:639 [in MetaCoq.PCUIC.PCUICInductives]
wfΣ:640 [in MetaCoq.PCUIC.PCUICSR]
wfΣ:641 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
wfΣ:642 [in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:645 [in MetaCoq.PCUIC.PCUICSubstitution]
wfΣ:646 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:647 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
wfΣ:647 [in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:647 [in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:649 [in MetaCoq.PCUIC.PCUICInductives]
wfΣ:65 [in MetaCoq.PCUIC.PCUICSafeLemmata]
wfΣ:65 [in MetaCoq.PCUIC.Bidirectional.BDUnique]
wfΣ:650 [in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:653 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
wfΣ:653 [in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:654 [in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:655 [in MetaCoq.PCUIC.PCUICSR]
wfΣ:658 [in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:659 [in MetaCoq.PCUIC.PCUICConfluence]
wfΣ:66 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
wfΣ:662 [in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:665 [in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:667 [in MetaCoq.PCUIC.PCUICParallelReduction]
wfΣ:667 [in MetaCoq.PCUIC.PCUICConfluence]
wfΣ:667 [in MetaCoq.PCUIC.PCUICSR]
wfΣ:668 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
wfΣ:668 [in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:67 [in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
wfΣ:67 [in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:671 [in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:674 [in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:678 [in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:678 [in MetaCoq.PCUIC.PCUICSR]
wfΣ:68 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
wfΣ:68 [in MetaCoq.SafeChecker.PCUICSafeReduce]
wfΣ:68 [in MetaCoq.Erasure.EOptimizePropDiscr]
wfΣ:681 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
wfΣ:684 [in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:69 [in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:690 [in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:691 [in MetaCoq.PCUIC.PCUICParallelReduction]
wfΣ:695 [in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:696 [in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:696 [in MetaCoq.PCUIC.PCUICSR]
wfΣ:696 [in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:70 [in MetaCoq.PCUIC.PCUICProgress]
wfΣ:70 [in MetaCoq.SafeChecker.PCUICSafeReduce]
wfΣ:70 [in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
wfΣ:701 [in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:701 [in MetaCoq.PCUIC.PCUICConfluence]
wfΣ:702 [in MetaCoq.PCUIC.PCUICParallelReduction]
wfΣ:703 [in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:705 [in MetaCoq.PCUIC.PCUICSR]
wfΣ:707 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:708 [in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:71 [in MetaCoq.Erasure.EArities]
wfΣ:711 [in MetaCoq.PCUIC.PCUICParallelReduction]
wfΣ:711 [in MetaCoq.PCUIC.PCUICSR]
wfΣ:712 [in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:716 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
wfΣ:717 [in MetaCoq.PCUIC.PCUICSR]
wfΣ:721 [in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:724 [in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:725 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
wfΣ:725 [in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:727 [in MetaCoq.PCUIC.PCUICSR]
wfΣ:729 [in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:73 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
wfΣ:73 [in MetaCoq.PCUIC.Bidirectional.BDUnique]
wfΣ:732 [in MetaCoq.Template.EnvironmentTyping]
wfΣ:735 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
wfΣ:735 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:736 [in MetaCoq.PCUIC.PCUICSR]
wfΣ:738 [in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:738 [in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:74 [in MetaCoq.PCUIC.PCUICProgress]
wfΣ:74 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
wfΣ:740 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:743 [in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:749 [in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:749 [in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:75 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
wfΣ:76 [in MetaCoq.Erasure.EArities]
wfΣ:76 [in MetaCoq.Erasure.EOptimizePropDiscr]
wfΣ:762 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:763 [in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:765 [in MetaCoq.PCUIC.PCUICSR]
wfΣ:768 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:77 [in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
wfΣ:771 [in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:772 [in MetaCoq.PCUIC.PCUICSR]
wfΣ:775 [in MetaCoq.PCUIC.PCUICSR]
wfΣ:778 [in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:78 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
wfΣ:783 [in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:786 [in MetaCoq.SafeChecker.PCUICSafeChecker]
wfΣ:787 [in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:788 [in MetaCoq.SafeChecker.PCUICSafeChecker]
wfΣ:79 [in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
wfΣ:791 [in MetaCoq.PCUIC.PCUICTyping]
wfΣ:791 [in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:795 [in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:795 [in MetaCoq.PCUIC.PCUICTyping]
wfΣ:798 [in MetaCoq.Template.Typing]
wfΣ:799 [in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:8 [in MetaCoq.PCUIC.PCUICInductives]
wfΣ:8 [in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
wfΣ:8 [in MetaCoq.SafeChecker.PCUICSafeReduce]
wfΣ:8 [in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:80 [in MetaCoq.PCUIC.PCUICProgress]
wfΣ:80 [in MetaCoq.PCUIC.PCUICInductives]
wfΣ:800 [in MetaCoq.PCUIC.PCUICSR]
wfΣ:801 [in MetaCoq.PCUIC.PCUICTyping]
wfΣ:803 [in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:806 [in MetaCoq.PCUIC.PCUICTyping]
wfΣ:807 [in MetaCoq.PCUIC.PCUICSR]
wfΣ:808 [in MetaCoq.Template.Typing]
wfΣ:808 [in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:81 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
wfΣ:81 [in MetaCoq.PCUIC.Bidirectional.BDUnique]
wfΣ:810 [in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:811 [in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:815 [in MetaCoq.PCUIC.PCUICTyping]
wfΣ:817 [in MetaCoq.Template.Typing]
wfΣ:82 [in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
wfΣ:82 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
wfΣ:82 [in MetaCoq.PCUIC.PCUICConvCumInversion]
wfΣ:824 [in MetaCoq.Template.Typing]
wfΣ:824 [in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:824 [in MetaCoq.PCUIC.PCUICTyping]
wfΣ:825 [in MetaCoq.PCUIC.PCUICSR]
wfΣ:83 [in MetaCoq.PCUIC.PCUICSR]
wfΣ:83 [in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
wfΣ:831 [in MetaCoq.PCUIC.PCUICSR]
wfΣ:832 [in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:832 [in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:834 [in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:834 [in MetaCoq.PCUIC.PCUICTyping]
wfΣ:837 [in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:84 [in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
wfΣ:84 [in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:843 [in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:843 [in MetaCoq.PCUIC.PCUICSR]
wfΣ:844 [in MetaCoq.PCUIC.PCUICTyping]
wfΣ:848 [in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:848 [in MetaCoq.PCUIC.PCUICSR]
wfΣ:85 [in MetaCoq.PCUIC.PCUICProgress]
wfΣ:851 [in MetaCoq.PCUIC.PCUICTyping]
wfΣ:853 [in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:854 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:854 [in MetaCoq.PCUIC.PCUICSR]
wfΣ:859 [in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:86 [in MetaCoq.PCUIC.Typing.PCUICWeakeningTyp]
wfΣ:860 [in MetaCoq.PCUIC.PCUICTyping]
wfΣ:862 [in MetaCoq.PCUIC.PCUICConfluence]
wfΣ:865 [in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:865 [in MetaCoq.PCUIC.PCUICSR]
wfΣ:869 [in MetaCoq.PCUIC.PCUICConfluence]
wfΣ:87 [in MetaCoq.Erasure.EArities]
wfΣ:87 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
wfΣ:87 [in MetaCoq.Erasure.Prelim]
wfΣ:87 [in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:870 [in MetaCoq.PCUIC.PCUICSR]
wfΣ:871 [in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:871 [in MetaCoq.PCUIC.PCUICTyping]
wfΣ:875 [in MetaCoq.PCUIC.PCUICConfluence]
wfΣ:875 [in MetaCoq.PCUIC.PCUICSR]
wfΣ:879 [in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:88 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
wfΣ:88 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
wfΣ:880 [in MetaCoq.PCUIC.PCUICSR]
wfΣ:882 [in MetaCoq.PCUIC.PCUICParallelReduction]
wfΣ:886 [in MetaCoq.PCUIC.PCUICConfluence]
wfΣ:887 [in MetaCoq.PCUIC.PCUICConversion]
wfΣ:888 [in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:89 [in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
wfΣ:89 [in MetaCoq.PCUIC.PCUICConversion]
wfΣ:891 [in MetaCoq.PCUIC.PCUICTyping]
wfΣ:892 [in MetaCoq.PCUIC.PCUICConfluence]
wfΣ:894 [in MetaCoq.PCUIC.PCUICParallelReduction]
wfΣ:9 [in MetaCoq.PCUIC.Typing.PCUICInstTyp]
wfΣ:9 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
wfΣ:9 [in MetaCoq.Erasure.ErasureFunction]
wfΣ:90 [in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
wfΣ:90 [in MetaCoq.SafeChecker.PCUICWfEnv]
wfΣ:90 [in MetaCoq.PCUIC.TemplateToPCUICExpanded]
wfΣ:90 [in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
wfΣ:90 [in MetaCoq.Erasure.Prelim]
wfΣ:90 [in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:900 [in MetaCoq.PCUIC.PCUICConfluence]
wfΣ:904 [in MetaCoq.PCUIC.PCUICConfluence]
wfΣ:904 [in MetaCoq.PCUIC.PCUICTyping]
wfΣ:905 [in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:91 [in MetaCoq.PCUIC.PCUICValidity]
wfΣ:91 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
wfΣ:910 [in MetaCoq.PCUIC.PCUICConfluence]
wfΣ:912 [in MetaCoq.PCUIC.PCUICTyping]
wfΣ:913 [in MetaCoq.PCUIC.PCUICParallelReduction]
wfΣ:92 [in MetaCoq.PCUIC.PCUICFirstorder]
wfΣ:92 [in MetaCoq.PCUIC.PCUICContextConversion]
wfΣ:920 [in MetaCoq.PCUIC.PCUICTyping]
wfΣ:921 [in MetaCoq.PCUIC.PCUICConfluence]
wfΣ:925 [in MetaCoq.PCUIC.PCUICParallelReduction]
wfΣ:927 [in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:93 [in MetaCoq.SafeChecker.PCUICSafeConversion]
wfΣ:93 [in MetaCoq.SafeChecker.PCUICTypeChecker]
wfΣ:936 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:938 [in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:94 [in MetaCoq.PCUIC.PCUICProgress]
wfΣ:94 [in MetaCoq.PCUIC.PCUICAlpha]
wfΣ:94 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
wfΣ:945 [in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:945 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:95 [in MetaCoq.Erasure.ESubstitution]
wfΣ:95 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
wfΣ:95 [in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
wfΣ:95 [in MetaCoq.PCUIC.Bidirectional.BDUnique]
wfΣ:95 [in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
wfΣ:955 [in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:956 [in MetaCoq.PCUIC.PCUICParallelReduction]
wfΣ:96 [in MetaCoq.Erasure.EArities]
wfΣ:96 [in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
wfΣ:96 [in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
wfΣ:962 [in MetaCoq.Template.Typing]
wfΣ:966 [in MetaCoq.Template.Typing]
wfΣ:966 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:97 [in MetaCoq.PCUIC.PCUICValidity]
wfΣ:97 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
wfΣ:97 [in MetaCoq.PCUIC.PCUICFirstorder]
wfΣ:97 [in MetaCoq.SafeChecker.PCUICWfEnv]
wfΣ:97 [in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
wfΣ:972 [in MetaCoq.Template.Typing]
wfΣ:973 [in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:977 [in MetaCoq.Template.Typing]
wfΣ:977 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wfΣ:98 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
wfΣ:98 [in MetaCoq.PCUIC.TemplateToPCUICExpanded]
wfΣ:982 [in MetaCoq.Erasure.ErasureFunction]
wfΣ:985 [in MetaCoq.Template.Typing]
wfΣ:989 [in MetaCoq.PCUIC.PCUICInductiveInversion]
wfΣ:994 [in MetaCoq.Template.Typing]
wguard:39 [in MetaCoq.Erasure.ETransform]
with_universes:155 [in MetaCoq.Template.Pretty]
with_universes:152 [in MetaCoq.Template.Pretty]
with_universes:147 [in MetaCoq.Template.Pretty]
with_universes:143 [in MetaCoq.Template.Pretty]
with_universes:133 [in MetaCoq.Template.Pretty]
with_universes:128 [in MetaCoq.Template.Pretty]
with_universes:120 [in MetaCoq.Template.Pretty]
with_universes:53 [in MetaCoq.Template.Pretty]
wi':124 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
wi':134 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
wi':161 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
wi':171 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
wi':210 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
wi':237 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
wi':73 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
wi':99 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
wi:122 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
wi:132 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
wi:1467 [in MetaCoq.Erasure.ErasureFunction]
wi:159 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
wi:169 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
wi:18 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
wi:208 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
wi:235 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
wi:71 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
wi:97 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
wrong_sizes:104 [in MetaCoq.Template.monad_utils]
wtd':279 [in MetaCoq.SafeChecker.PCUICTypeChecker]
wtd:276 [in MetaCoq.SafeChecker.PCUICTypeChecker]
wtp:10 [in MetaCoq.PCUIC.PCUICTransform]
wtp:1295 [in MetaCoq.Erasure.ErasureFunction]
wtp:1406 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wtp:1524 [in MetaCoq.Erasure.ErasureFunction]
wtp:18 [in MetaCoq.Erasure.ETransform]
wtp:22 [in MetaCoq.Erasure.ETransform]
wts':495 [in MetaCoq.SafeChecker.PCUICTypeChecker]
wts:492 [in MetaCoq.SafeChecker.PCUICTypeChecker]
wt_params:1087 [in MetaCoq.SafeChecker.PCUICTypeChecker]
wt':1388 [in MetaCoq.Erasure.ErasureFunction]
wt':1410 [in MetaCoq.Erasure.ErasureFunction]
wt':314 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
wt':464 [in MetaCoq.Erasure.ErasureFunction]
wt':470 [in MetaCoq.Erasure.ErasureFunction]
wt':474 [in MetaCoq.Erasure.ErasureFunction]
wt':479 [in MetaCoq.Erasure.ErasureFunction]
wt':483 [in MetaCoq.Erasure.ErasureFunction]
wt':487 [in MetaCoq.Erasure.ErasureFunction]
wt':493 [in MetaCoq.Erasure.ErasureFunction]
wt':498 [in MetaCoq.Erasure.ErasureFunction]
wt':504 [in MetaCoq.Erasure.ErasureFunction]
wt':509 [in MetaCoq.Erasure.ErasureFunction]
wt':514 [in MetaCoq.Erasure.ErasureFunction]
wt':520 [in MetaCoq.Erasure.ErasureFunction]
wt':525 [in MetaCoq.Erasure.ErasureFunction]
wt':531 [in MetaCoq.Erasure.ErasureFunction]
wt':536 [in MetaCoq.Erasure.ErasureFunction]
wt':541 [in MetaCoq.Erasure.ErasureFunction]
wt':689 [in MetaCoq.Erasure.ErasureFunction]
wt':702 [in MetaCoq.Erasure.ErasureFunction]
wt':712 [in MetaCoq.Erasure.ErasureFunction]
wt':720 [in MetaCoq.Erasure.ErasureFunction]
wt':725 [in MetaCoq.Erasure.ErasureFunction]
wt':731 [in MetaCoq.Erasure.ErasureFunction]
wt':736 [in MetaCoq.Erasure.ErasureFunction]
wt':741 [in MetaCoq.Erasure.ErasureFunction]
wt':747 [in MetaCoq.Erasure.ErasureFunction]
wt':752 [in MetaCoq.Erasure.ErasureFunction]
wt':758 [in MetaCoq.Erasure.ErasureFunction]
wt':763 [in MetaCoq.Erasure.ErasureFunction]
wt':768 [in MetaCoq.Erasure.ErasureFunction]
wt:1048 [in MetaCoq.Erasure.ErasureFunction]
wt:1050 [in MetaCoq.Erasure.ErasureFunction]
wt:1055 [in MetaCoq.Erasure.ErasureFunction]
wt:1057 [in MetaCoq.Erasure.ErasureFunction]
wt:1072 [in MetaCoq.Erasure.ErasureFunction]
wt:1074 [in MetaCoq.Erasure.ErasureFunction]
wt:1080 [in MetaCoq.Erasure.ErasureFunction]
wt:1083 [in MetaCoq.Erasure.ErasureFunction]
wt:1104 [in MetaCoq.Erasure.ErasureFunction]
wt:1144 [in MetaCoq.Erasure.ErasureFunction]
wt:1160 [in MetaCoq.Erasure.ErasureFunction]
wt:1171 [in MetaCoq.Erasure.ErasureFunction]
wt:1202 [in MetaCoq.Erasure.ErasureFunction]
wt:1214 [in MetaCoq.Erasure.ErasureFunction]
wt:1226 [in MetaCoq.Erasure.ErasureFunction]
wt:126 [in MetaCoq.Erasure.ErasureFunction]
wt:1313 [in MetaCoq.Erasure.ErasureFunction]
wt:1328 [in MetaCoq.Erasure.ErasureFunction]
wt:1345 [in MetaCoq.Erasure.ErasureFunction]
wt:1365 [in MetaCoq.Erasure.ErasureFunction]
wt:1385 [in MetaCoq.Erasure.ErasureFunction]
wt:1407 [in MetaCoq.Erasure.ErasureFunction]
wt:149 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
wt:1542 [in MetaCoq.SafeChecker.PCUICSafeReduce]
wt:1543 [in MetaCoq.Erasure.ErasureFunction]
wt:160 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
wt:1606 [in MetaCoq.SafeChecker.PCUICSafeReduce]
wt:163 [in MetaCoq.Erasure.ErasureFunction]
wt:170 [in MetaCoq.Erasure.ErasureFunction]
wt:238 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
wt:312 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
wt:463 [in MetaCoq.Erasure.ErasureFunction]
wt:469 [in MetaCoq.Erasure.ErasureFunction]
wt:473 [in MetaCoq.Erasure.ErasureFunction]
wt:478 [in MetaCoq.Erasure.ErasureFunction]
wt:482 [in MetaCoq.Erasure.ErasureFunction]
wt:486 [in MetaCoq.Erasure.ErasureFunction]
wt:490 [in MetaCoq.Erasure.ErasureFunction]
wt:502 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
wt:512 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
wt:517 [in MetaCoq.Erasure.ErasureFunction]
wt:523 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
wt:543 [in MetaCoq.SafeChecker.PCUICSafeChecker]
wt:546 [in MetaCoq.Erasure.ErasureFunction]
wt:552 [in MetaCoq.Erasure.ErasureFunction]
wt:557 [in MetaCoq.Erasure.ErasureFunction]
wt:561 [in MetaCoq.SafeChecker.PCUICSafeChecker]
wt:563 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
wt:573 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
wt:578 [in MetaCoq.Erasure.ErasureFunction]
wt:602 [in MetaCoq.Erasure.ErasureFunction]
wt:606 [in MetaCoq.Erasure.ErasureFunction]
wt:633 [in MetaCoq.Erasure.ErasureFunction]
wt:688 [in MetaCoq.Erasure.ErasureFunction]
wt:701 [in MetaCoq.Erasure.ErasureFunction]
wt:711 [in MetaCoq.Erasure.ErasureFunction]
wt:717 [in MetaCoq.Erasure.ErasureFunction]
wt:744 [in MetaCoq.Erasure.ErasureFunction]
wt:8 [in MetaCoq.Erasure.ETransform]
wt:81 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
wt:956 [in MetaCoq.Erasure.ErasureFunction]
w':446 [in MetaCoq.PCUIC.PCUICTyping]
w':921 [in MetaCoq.Template.Typing]
w1:126 [in MetaCoq.SafeChecker.PCUICSafeConversion]
w1:144 [in MetaCoq.SafeChecker.PCUICSafeConversion]
w1:158 [in MetaCoq.SafeChecker.PCUICSafeConversion]
w1:2800 [in MetaCoq.Translations.MiniHoTT]
w1:2808 [in MetaCoq.Translations.MiniHoTT_paths]
w2:127 [in MetaCoq.SafeChecker.PCUICSafeConversion]
w2:145 [in MetaCoq.SafeChecker.PCUICSafeConversion]
w2:159 [in MetaCoq.SafeChecker.PCUICSafeConversion]
w2:2803 [in MetaCoq.Translations.MiniHoTT]
w2:2811 [in MetaCoq.Translations.MiniHoTT_paths]
w:1006 [in MetaCoq.Template.utils.wGraph]
w:1009 [in MetaCoq.Template.utils.wGraph]
w:1262 [in MetaCoq.Translations.MiniHoTT]
w:1270 [in MetaCoq.Translations.MiniHoTT_paths]
w:219 [in MetaCoq.PCUIC.PCUICSafeLemmata]
w:229 [in MetaCoq.PCUIC.PCUICSafeLemmata]
w:2578 [in MetaCoq.Template.utils.All_Forall]
w:2791 [in MetaCoq.Translations.MiniHoTT]
w:2799 [in MetaCoq.Translations.MiniHoTT_paths]
w:2823 [in MetaCoq.Translations.MiniHoTT]
w:2831 [in MetaCoq.Translations.MiniHoTT_paths]
w:2856 [in MetaCoq.Translations.MiniHoTT]
w:2864 [in MetaCoq.Translations.MiniHoTT_paths]
w:31 [in MetaCoq.Template.utils.MCRelations]
w:337 [in MetaCoq.Template.EnvironmentTyping]
w:343 [in MetaCoq.Template.EnvironmentTyping]
w:347 [in MetaCoq.Template.EnvironmentTyping]
w:36 [in MetaCoq.SafeChecker.PCUICSafeReduce]
w:375 [in MetaCoq.Template.EnvironmentTyping]
w:443 [in MetaCoq.PCUIC.PCUICTyping]
w:445 [in MetaCoq.Translations.MiniHoTT]
w:45 [in MetaCoq.SafeChecker.PCUICSafeReduce]
w:453 [in MetaCoq.Translations.MiniHoTT_paths]
w:458 [in MetaCoq.Translations.MiniHoTT]
w:466 [in MetaCoq.Translations.MiniHoTT_paths]
w:49 [in MetaCoq.PCUIC.PCUICSafeLemmata]
w:533 [in MetaCoq.Translations.MiniHoTT]
w:541 [in MetaCoq.Translations.MiniHoTT_paths]
w:546 [in MetaCoq.Translations.MiniHoTT]
w:554 [in MetaCoq.Translations.MiniHoTT_paths]
w:566 [in MetaCoq.Translations.MiniHoTT]
w:574 [in MetaCoq.Translations.MiniHoTT_paths]
w:577 [in MetaCoq.Translations.MiniHoTT]
w:585 [in MetaCoq.Translations.MiniHoTT_paths]
w:588 [in MetaCoq.Translations.MiniHoTT]
w:596 [in MetaCoq.Translations.MiniHoTT_paths]
w:60 [in MetaCoq.Template.WfAst]
w:606 [in MetaCoq.Translations.MiniHoTT]
w:614 [in MetaCoq.Translations.MiniHoTT_paths]
w:65 [in MetaCoq.SafeChecker.PCUICSafeConversion]
w:67 [in MetaCoq.SafeChecker.PCUICSafeConversion]
w:740 [in MetaCoq.Translations.MiniHoTT]
w:748 [in MetaCoq.Translations.MiniHoTT_paths]
w:75 [in MetaCoq.SafeChecker.PCUICSafeConversion]
w:79 [in MetaCoq.SafeChecker.PCUICSafeConversion]
w:799 [in MetaCoq.Translations.MiniHoTT]
w:807 [in MetaCoq.Translations.MiniHoTT_paths]
w:886 [in MetaCoq.Translations.MiniHoTT]
w:894 [in MetaCoq.Translations.MiniHoTT_paths]
w:918 [in MetaCoq.Template.Typing]
w:92 [in MetaCoq.PCUIC.PCUICSafeLemmata]
w:926 [in MetaCoq.Translations.MiniHoTT]
w:934 [in MetaCoq.Translations.MiniHoTT_paths]
w:96 [in MetaCoq.PCUIC.PCUICSafeLemmata]



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)