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)

L (binder)

leA:100 [in MetaCoq.PCUIC.utils.PCUICUtils]
leA:140 [in MetaCoq.PCUIC.utils.PCUICUtils]
leA:17 [in MetaCoq.PCUIC.utils.PCUICUtils]
leA:3 [in MetaCoq.PCUIC.utils.PCUICUtils]
leA:39 [in MetaCoq.PCUIC.utils.PCUICUtils]
leA:46 [in MetaCoq.PCUIC.utils.PCUICUtils]
leA:58 [in MetaCoq.PCUIC.utils.PCUICUtils]
leA:75 [in MetaCoq.SafeChecker.PCUICSafeReduce]
leA:98 [in MetaCoq.SafeChecker.PCUICSafeReduce]
leB:106 [in MetaCoq.PCUIC.utils.PCUICUtils]
leB:107 [in MetaCoq.SafeChecker.PCUICSafeReduce]
leB:142 [in MetaCoq.PCUIC.utils.PCUICUtils]
leB:23 [in MetaCoq.PCUIC.utils.PCUICUtils]
leB:40 [in MetaCoq.PCUIC.utils.PCUICUtils]
leB:47 [in MetaCoq.PCUIC.utils.PCUICUtils]
leB:5 [in MetaCoq.PCUIC.utils.PCUICUtils]
leB:64 [in MetaCoq.PCUIC.utils.PCUICUtils]
leB:84 [in MetaCoq.SafeChecker.PCUICSafeReduce]
len:1004 [in MetaCoq.Template.utils.All_Forall]
leqb_levelalg_n:512 [in MetaCoq.Template.Universes]
leqb:285 [in MetaCoq.SafeChecker.PCUICEqualityDec]
leqb:316 [in MetaCoq.SafeChecker.PCUICEqualityDec]
leqty:239 [in MetaCoq.SafeChecker.PCUICSafeChecker]
lequ:12 [in MetaCoq.SafeChecker.PCUICEqualityDec]
lequ:121 [in MetaCoq.SafeChecker.PCUICEqualityDec]
lequ:132 [in MetaCoq.SafeChecker.PCUICEqualityDec]
lequ:150 [in MetaCoq.SafeChecker.PCUICEqualityDec]
lequ:171 [in MetaCoq.SafeChecker.PCUICEqualityDec]
lequ:178 [in MetaCoq.SafeChecker.PCUICEqualityDec]
lequ:188 [in MetaCoq.SafeChecker.PCUICEqualityDec]
lequ:202 [in MetaCoq.SafeChecker.PCUICEqualityDec]
lequ:21 [in MetaCoq.SafeChecker.PCUICEqualityDec]
lequ:224 [in MetaCoq.SafeChecker.PCUICEqualityDec]
lequ:31 [in MetaCoq.SafeChecker.PCUICEqualityDec]
lequ:37 [in MetaCoq.SafeChecker.PCUICEqualityDec]
lequ:62 [in MetaCoq.SafeChecker.PCUICEqualityDec]
lequ:69 [in MetaCoq.SafeChecker.PCUICEqualityDec]
leq_levelalg_n:505 [in MetaCoq.Template.Universes]
leq_term:46 [in MetaCoq.Template.TermEquality]
leq_term:110 [in MetaCoq.PCUIC.PCUICEquality]
leq_term:108 [in MetaCoq.PCUIC.PCUICEquality]
leq_term:106 [in MetaCoq.PCUIC.PCUICEquality]
leq_term:104 [in MetaCoq.PCUIC.PCUICEquality]
leq_term:102 [in MetaCoq.PCUIC.PCUICEquality]
leq_term:100 [in MetaCoq.PCUIC.PCUICEquality]
leq_term:94 [in MetaCoq.PCUIC.PCUICEquality]
leq_term:84 [in MetaCoq.PCUIC.PCUICEquality]
leq_term':76 [in MetaCoq.PCUIC.PCUICEquality]
leq_term:74 [in MetaCoq.PCUIC.PCUICEquality]
leq_term':71 [in MetaCoq.PCUIC.PCUICEquality]
leq_term:69 [in MetaCoq.PCUIC.PCUICEquality]
leq_term':67 [in MetaCoq.PCUIC.PCUICEquality]
leq_term:65 [in MetaCoq.PCUIC.PCUICEquality]
leq_term:49 [in MetaCoq.PCUIC.PCUICEquality]
leq:101 [in MetaCoq.PCUIC.PCUICConvCumInversion]
leq:107 [in MetaCoq.PCUIC.PCUICConvCumInversion]
leq:113 [in MetaCoq.PCUIC.PCUICConvCumInversion]
leq:1235 [in MetaCoq.SafeChecker.PCUICSafeConversion]
leq:1236 [in MetaCoq.PCUIC.PCUICConfluence]
leq:127 [in MetaCoq.PCUIC.PCUICConvCumInversion]
leq:128 [in MetaCoq.SafeChecker.PCUICErrors]
leq:139 [in MetaCoq.SafeChecker.PCUICErrors]
leq:139 [in MetaCoq.PCUIC.PCUICConvCumInversion]
leq:151 [in MetaCoq.PCUIC.PCUICConvCumInversion]
leq:157 [in MetaCoq.SafeChecker.PCUICErrors]
leq:161 [in MetaCoq.SafeChecker.PCUICEqualityDec]
leq:2077 [in MetaCoq.SafeChecker.PCUICSafeConversion]
leq:2100 [in MetaCoq.SafeChecker.PCUICSafeConversion]
leq:2112 [in MetaCoq.SafeChecker.PCUICSafeConversion]
leq:2121 [in MetaCoq.SafeChecker.PCUICSafeConversion]
leq:2135 [in MetaCoq.SafeChecker.PCUICSafeConversion]
leq:214 [in MetaCoq.SafeChecker.PCUICEqualityDec]
leq:222 [in MetaCoq.SafeChecker.PCUICSafeConversion]
leq:228 [in MetaCoq.Template.Checker]
leq:235 [in MetaCoq.Template.Checker]
leq:237 [in MetaCoq.SafeChecker.PCUICEqualityDec]
leq:247 [in MetaCoq.PCUIC.PCUICSafeLemmata]
leq:253 [in MetaCoq.SafeChecker.PCUICSafeConversion]
leq:2552 [in MetaCoq.SafeChecker.PCUICSafeConversion]
leq:2559 [in MetaCoq.SafeChecker.PCUICSafeConversion]
leq:273 [in MetaCoq.SafeChecker.PCUICEqualityDec]
leq:278 [in MetaCoq.SafeChecker.PCUICEqualityDec]
leq:283 [in MetaCoq.PCUIC.PCUICConfluence]
leq:326 [in MetaCoq.SafeChecker.PCUICEqualityDec]
leq:352 [in MetaCoq.SafeChecker.PCUICEqualityDec]
leq:370 [in MetaCoq.SafeChecker.PCUICEqualityDec]
leq:375 [in MetaCoq.SafeChecker.PCUICEqualityDec]
leq:380 [in MetaCoq.SafeChecker.PCUICEqualityDec]
leq:4414 [in MetaCoq.SafeChecker.PCUICSafeConversion]
leq:4566 [in MetaCoq.SafeChecker.PCUICSafeConversion]
leq:5 [in MetaCoq.SafeChecker.PCUICSafeConversion]
leq:510 [in MetaCoq.PCUIC.PCUICConversion]
leq:517 [in MetaCoq.PCUIC.PCUICConversion]
leq:52 [in MetaCoq.PCUIC.PCUICConvCumInversion]
leq:523 [in MetaCoq.PCUIC.PCUICConversion]
leq:5233 [in MetaCoq.SafeChecker.PCUICSafeConversion]
leq:529 [in MetaCoq.PCUIC.PCUICConversion]
leq:536 [in MetaCoq.PCUIC.PCUICConversion]
leq:549 [in MetaCoq.PCUIC.PCUICConversion]
leq:55 [in MetaCoq.SafeChecker.PCUICEqualityDec]
leq:5655 [in MetaCoq.SafeChecker.PCUICSafeConversion]
leq:5666 [in MetaCoq.SafeChecker.PCUICSafeConversion]
leq:5677 [in MetaCoq.SafeChecker.PCUICSafeConversion]
leq:5687 [in MetaCoq.SafeChecker.PCUICSafeConversion]
leq:5699 [in MetaCoq.SafeChecker.PCUICSafeConversion]
leq:5707 [in MetaCoq.SafeChecker.PCUICSafeConversion]
leq:59 [in MetaCoq.SafeChecker.PCUICEqualityDec]
leq:648 [in MetaCoq.SafeChecker.PCUICSafeConversion]
leq:654 [in MetaCoq.SafeChecker.PCUICSafeConversion]
leq:66 [in MetaCoq.PCUIC.PCUICConvCumInversion]
leq:663 [in MetaCoq.SafeChecker.PCUICSafeConversion]
leq:669 [in MetaCoq.SafeChecker.PCUICSafeConversion]
leq:677 [in MetaCoq.SafeChecker.PCUICSafeConversion]
leq:690 [in MetaCoq.SafeChecker.PCUICSafeConversion]
leq:696 [in MetaCoq.SafeChecker.PCUICSafeConversion]
leq:708 [in MetaCoq.SafeChecker.PCUICSafeConversion]
leq:72 [in MetaCoq.PCUIC.PCUICConvCumInversion]
leq:8 [in MetaCoq.PCUIC.PCUICConvCumInversion]
leq:824 [in MetaCoq.PCUIC.PCUICConversion]
leq:826 [in MetaCoq.SafeChecker.PCUICSafeConversion]
leq:85 [in MetaCoq.SafeChecker.PCUICEqualityDec]
leq:877 [in MetaCoq.PCUIC.PCUICConversion]
leq:92 [in MetaCoq.SafeChecker.PCUICEqualityDec]
leq:94 [in MetaCoq.PCUIC.PCUICConvCumInversion]
leq:99 [in MetaCoq.SafeChecker.PCUICWfEnv]
leterm:380 [in MetaCoq.PCUIC.PCUICCumulProp]
lets:821 [in MetaCoq.SafeChecker.PCUICSafeChecker]
levels1:611 [in MetaCoq.Template.common.uGraph]
levels2:612 [in MetaCoq.Template.common.uGraph]
levels:1 [in MetaCoq.SafeChecker.PCUICSafeChecker]
levels:1019 [in MetaCoq.SafeChecker.PCUICSafeChecker]
levels:200 [in MetaCoq.SafeChecker.PCUICErrors]
levels:401 [in MetaCoq.Template.Universes]
levels:404 [in MetaCoq.Template.Universes]
levels:468 [in MetaCoq.Template.EnvironmentTyping]
levels:520 [in MetaCoq.Template.common.uGraph]
levels:537 [in MetaCoq.Template.common.uGraph]
levels:665 [in MetaCoq.Template.common.uGraph]
levels:671 [in MetaCoq.Template.EnvironmentTyping]
levels:79 [in MetaCoq.PCUIC.PCUICWeakeningEnv]
levels:80 [in MetaCoq.SafeChecker.PCUICSafeChecker]
le':758 [in MetaCoq.PCUIC.PCUICSpine]
le:114 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
le:120 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
le:1232 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
le:126 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
le:16 [in MetaCoq.PCUIC.PCUICInversion]
le:172 [in MetaCoq.SafeChecker.PCUICErrors]
le:191 [in MetaCoq.SafeChecker.PCUICSafeChecker]
le:199 [in MetaCoq.SafeChecker.PCUICSafeChecker]
le:203 [in MetaCoq.SafeChecker.PCUICSafeChecker]
le:270 [in MetaCoq.SafeChecker.PCUICTypeChecker]
le:346 [in MetaCoq.PCUIC.PCUICSubstitution]
le:354 [in MetaCoq.PCUIC.PCUICSubstitution]
le:359 [in MetaCoq.SafeChecker.PCUICTypeChecker]
le:362 [in MetaCoq.PCUIC.PCUICSubstitution]
le:365 [in MetaCoq.SafeChecker.PCUICTypeChecker]
le:382 [in MetaCoq.PCUIC.PCUICCumulProp]
le:393 [in MetaCoq.PCUIC.PCUICInductiveInversion]
le:393 [in MetaCoq.SafeChecker.PCUICTypeChecker]
le:402 [in MetaCoq.SafeChecker.PCUICTypeChecker]
le:406 [in MetaCoq.PCUIC.PCUICInductiveInversion]
le:463 [in MetaCoq.PCUIC.PCUICSubstitution]
le:505 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
le:52 [in MetaCoq.PCUIC.PCUICSafeLemmata]
le:54 [in MetaCoq.PCUIC.PCUICArities]
le:55 [in MetaCoq.PCUIC.PCUICArities]
le:569 [in MetaCoq.PCUIC.PCUICInductiveInversion]
le:583 [in MetaCoq.PCUIC.PCUICInductiveInversion]
le:611 [in MetaCoq.PCUIC.PCUICInductiveInversion]
le:627 [in MetaCoq.PCUIC.PCUICSubstitution]
le:63 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
le:679 [in MetaCoq.PCUIC.PCUICSR]
le:69 [in MetaCoq.PCUIC.PCUICSR]
le:745 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
le:749 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
le:751 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
le:756 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
le:77 [in MetaCoq.PCUIC.PCUICSR]
le:82 [in MetaCoq.SafeChecker.PCUICTypeChecker]
le:85 [in MetaCoq.PCUIC.PCUICAlpha]
le:90 [in MetaCoq.PCUIC.PCUICAlpha]
le:92 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
le:939 [in MetaCoq.PCUIC.PCUICConversion]
le:944 [in MetaCoq.PCUIC.PCUICConversion]
le:947 [in MetaCoq.PCUIC.PCUICConversion]
le:95 [in MetaCoq.PCUIC.PCUICAlpha]
le:953 [in MetaCoq.PCUIC.PCUICConversion]
lH:159 [in MetaCoq.Translations.param_cheap_packed]
LI:100 [in MetaCoq.Translations.times_bool_fun]
LI:101 [in MetaCoq.Translations.times_bool_fun]
lls:111 [in MetaCoq.Examples.tauto]
lls:120 [in MetaCoq.Examples.tauto]
lls:77 [in MetaCoq.Examples.tauto]
ll:164 [in MetaCoq.PCUIC.PCUICConfluence]
ll:165 [in MetaCoq.PCUIC.PCUICConfluence]
lookup:20 [in MetaCoq.PCUIC.PCUICTyping]
lookup:27 [in MetaCoq.PCUIC.PCUICTyping]
lookup:35 [in MetaCoq.PCUIC.PCUICTyping]
ls0:114 [in MetaCoq.Examples.tauto]
ls0:123 [in MetaCoq.Examples.tauto]
ls:108 [in MetaCoq.Examples.tauto]
ls:117 [in MetaCoq.Examples.tauto]
ls:126 [in MetaCoq.Examples.tauto]
ls:129 [in MetaCoq.Examples.tauto]
ls:138 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
ls:54 [in MetaCoq.PCUIC.PCUICGlobalEnv]
ls:73 [in MetaCoq.Examples.tauto]
ls:93 [in MetaCoq.Examples.tauto]
ls:96 [in MetaCoq.Examples.tauto]
ls:99 [in MetaCoq.Examples.tauto]
lt:316 [in MetaCoq.Template.common.uGraph]
lt:321 [in MetaCoq.Template.common.uGraph]
lt:331 [in MetaCoq.Template.common.uGraph]
lt:363 [in MetaCoq.Template.common.uGraph]
lt:397 [in MetaCoq.Template.common.uGraph]
lt:402 [in MetaCoq.Template.common.uGraph]
lt:409 [in MetaCoq.Template.common.uGraph]
lt:416 [in MetaCoq.Template.common.uGraph]
lt:485 [in MetaCoq.Template.common.uGraph]
lu':32 [in MetaCoq.Translations.standard_model]
lvls:439 [in MetaCoq.Template.Universes]
lvs:154 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
lvs:90 [in MetaCoq.Template.EnvironmentTyping]
lx:1187 [in MetaCoq.PCUIC.PCUICReduction]
l'x:1188 [in MetaCoq.PCUIC.PCUICReduction]
l''':1850 [in MetaCoq.Template.utils.All_Forall]
l''':2574 [in MetaCoq.Template.utils.All_Forall]
l'':1177 [in MetaCoq.PCUIC.PCUICReduction]
l'':14 [in MetaCoq.SafeChecker.PCUICTypeChecker]
l'':16 [in MetaCoq.SafeChecker.PCUICTypeChecker]
l'':18 [in MetaCoq.SafeChecker.PCUICTypeChecker]
l'':1845 [in MetaCoq.Template.utils.All_Forall]
l'':19 [in MetaCoq.PCUIC.PCUICRedTypeIrrelevance]
l'':20 [in MetaCoq.SafeChecker.PCUICTypeChecker]
l'':21 [in MetaCoq.PCUIC.PCUICCumulProp]
l'':2232 [in MetaCoq.Template.utils.All_Forall]
l'':2246 [in MetaCoq.Template.utils.All_Forall]
l'':2485 [in MetaCoq.Template.utils.All_Forall]
l'':2498 [in MetaCoq.Template.utils.All_Forall]
l'':2573 [in MetaCoq.Template.utils.All_Forall]
l'':2586 [in MetaCoq.Template.utils.All_Forall]
l'':2597 [in MetaCoq.Template.utils.All_Forall]
l'':280 [in MetaCoq.Template.utils.MCList]
l'':419 [in MetaCoq.PCUIC.PCUICNormal]
l'':44 [in MetaCoq.Template.utils.All_Forall]
l'':509 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
l'':520 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
l'':558 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
l'':753 [in MetaCoq.PCUIC.PCUICReduction]
l'':814 [in MetaCoq.PCUIC.PCUICParallelReduction]
l'':923 [in MetaCoq.PCUIC.PCUICReduction]
l':10 [in MetaCoq.PCUIC.TemplateToPCUIC]
l':10 [in MetaCoq.Erasure.EAstUtils]
l':101 [in MetaCoq.PCUIC.PCUICConfluence]
l':101 [in MetaCoq.SafeChecker.PCUICEqualityDec]
l':1010 [in MetaCoq.Template.utils.All_Forall]
l':1012 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
l':1014 [in MetaCoq.Template.utils.All_Forall]
l':103 [in MetaCoq.SafeChecker.PCUICWfEnv]
l':1051 [in MetaCoq.Template.utils.All_Forall]
l':1051 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
l':106 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
l':1063 [in MetaCoq.Template.utils.All_Forall]
l':107 [in MetaCoq.Template.utils.All_Forall]
l':1071 [in MetaCoq.Template.utils.All_Forall]
L':108 [in MetaCoq.Translations.times_bool_fun]
l':1081 [in MetaCoq.Template.utils.All_Forall]
L':109 [in MetaCoq.Translations.times_bool_fun]
l':1093 [in MetaCoq.Template.utils.All_Forall]
l':110 [in MetaCoq.PCUIC.PCUICConfluence]
l':1102 [in MetaCoq.Template.utils.All_Forall]
l':1111 [in MetaCoq.Template.utils.All_Forall]
l':1116 [in MetaCoq.Template.utils.All_Forall]
l':1116 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
l':112 [in MetaCoq.PCUIC.PCUICCumulativity]
l':1122 [in MetaCoq.Template.utils.All_Forall]
l':1131 [in MetaCoq.Template.utils.All_Forall]
l':1140 [in MetaCoq.Template.utils.All_Forall]
l':1146 [in MetaCoq.PCUIC.PCUICReduction]
l':1149 [in MetaCoq.Template.utils.All_Forall]
l':1158 [in MetaCoq.Template.utils.All_Forall]
l':1159 [in MetaCoq.PCUIC.PCUICReduction]
l':1167 [in MetaCoq.Template.utils.All_Forall]
l':1176 [in MetaCoq.PCUIC.PCUICReduction]
l':118 [in MetaCoq.PCUIC.PCUICReduction]
l':1184 [in MetaCoq.PCUIC.PCUICReduction]
l':121 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
l':1215 [in MetaCoq.Template.utils.All_Forall]
l':123 [in MetaCoq.Template.utils.All_Forall]
l':1237 [in MetaCoq.PCUIC.PCUICConversion]
l':124 [in MetaCoq.PCUIC.PCUICCumulativity]
l':1245 [in MetaCoq.PCUIC.PCUICConversion]
l':125 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
L':126 [in MetaCoq.Translations.times_bool_fun]
l':126 [in MetaCoq.PCUIC.Syntax.PCUICCases]
l':1268 [in MetaCoq.Template.Typing]
L':127 [in MetaCoq.Translations.times_bool_fun]
l':1273 [in MetaCoq.Template.utils.All_Forall]
l':1279 [in MetaCoq.Template.Typing]
l':1281 [in MetaCoq.Template.utils.All_Forall]
l':129 [in MetaCoq.PCUIC.Syntax.PCUICCases]
l':129 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
l':131 [in MetaCoq.PCUIC.PCUICConfluence]
l':134 [in MetaCoq.PCUIC.PCUICContexts]
l':1356 [in MetaCoq.Template.utils.All_Forall]
l':137 [in MetaCoq.Template.LiftSubst]
l':138 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
l':1391 [in MetaCoq.Template.utils.All_Forall]
l':1398 [in MetaCoq.Template.utils.All_Forall]
l':1408 [in MetaCoq.Template.utils.All_Forall]
l':141 [in MetaCoq.Template.TypingWf]
l':1416 [in MetaCoq.Template.utils.All_Forall]
l':142 [in MetaCoq.Template.LiftSubst]
l':1421 [in MetaCoq.Template.utils.All_Forall]
l':1425 [in MetaCoq.Template.utils.All_Forall]
l':143 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
l':1436 [in MetaCoq.Template.utils.All_Forall]
l':1443 [in MetaCoq.Template.utils.All_Forall]
l':1448 [in MetaCoq.Template.utils.All_Forall]
l':1455 [in MetaCoq.Template.utils.All_Forall]
l':1490 [in MetaCoq.Template.utils.All_Forall]
l':15 [in MetaCoq.PCUIC.TemplateToPCUIC]
l':15 [in MetaCoq.Erasure.EAstUtils]
l':1505 [in MetaCoq.Template.utils.All_Forall]
l':1522 [in MetaCoq.Template.utils.All_Forall]
l':1528 [in MetaCoq.Template.utils.All_Forall]
l':1535 [in MetaCoq.Template.utils.All_Forall]
l':1543 [in MetaCoq.Template.utils.All_Forall]
l':1550 [in MetaCoq.Template.utils.All_Forall]
l':1556 [in MetaCoq.Template.utils.All_Forall]
l':1565 [in MetaCoq.Template.utils.All_Forall]
l':1580 [in MetaCoq.Template.utils.All_Forall]
l':1603 [in MetaCoq.Template.utils.All_Forall]
l':161 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
l':1614 [in MetaCoq.Template.utils.All_Forall]
l':1623 [in MetaCoq.Template.utils.All_Forall]
l':1631 [in MetaCoq.Template.utils.All_Forall]
l':1639 [in MetaCoq.Template.utils.All_Forall]
l':164 [in MetaCoq.Erasure.EDeps]
l':164 [in MetaCoq.Erasure.ELiftSubst]
l':1647 [in MetaCoq.Template.utils.All_Forall]
l':165 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
l':1654 [in MetaCoq.Template.utils.All_Forall]
l':1662 [in MetaCoq.Template.utils.All_Forall]
l':167 [in MetaCoq.SafeChecker.PCUICEqualityDec]
l':1670 [in MetaCoq.Template.utils.All_Forall]
l':1678 [in MetaCoq.Template.utils.All_Forall]
l':168 [in MetaCoq.Erasure.ELiftSubst]
l':1686 [in MetaCoq.Template.utils.All_Forall]
l':169 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
l':1695 [in MetaCoq.Template.utils.All_Forall]
l':17 [in MetaCoq.PCUIC.TemplateToPCUIC]
l':17 [in MetaCoq.PCUIC.PCUICConvCumInversion]
l':17 [in MetaCoq.Erasure.EAstUtils]
l':1718 [in MetaCoq.Template.utils.All_Forall]
l':1730 [in MetaCoq.Template.utils.All_Forall]
l':1738 [in MetaCoq.Template.utils.All_Forall]
l':1743 [in MetaCoq.Template.utils.All_Forall]
l':1755 [in MetaCoq.Template.utils.All_Forall]
l':1770 [in MetaCoq.Template.utils.All_Forall]
l':1778 [in MetaCoq.Template.utils.All_Forall]
l':1785 [in MetaCoq.Template.utils.All_Forall]
l':1792 [in MetaCoq.Template.utils.All_Forall]
l':18 [in MetaCoq.PCUIC.PCUICRedTypeIrrelevance]
l':1804 [in MetaCoq.Template.utils.All_Forall]
l':1812 [in MetaCoq.Template.utils.All_Forall]
l':1824 [in MetaCoq.Template.utils.All_Forall]
l':1829 [in MetaCoq.Template.utils.All_Forall]
l':1833 [in MetaCoq.Template.utils.All_Forall]
l':1844 [in MetaCoq.Template.utils.All_Forall]
l':1854 [in MetaCoq.Template.utils.All_Forall]
l':186 [in MetaCoq.Template.utils.All_Forall]
l':1862 [in MetaCoq.Template.utils.All_Forall]
l':1869 [in MetaCoq.Template.utils.All_Forall]
l':19 [in MetaCoq.PCUIC.PCUICCumulProp]
l':191 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
l':1918 [in MetaCoq.Template.utils.All_Forall]
l':193 [in MetaCoq.Template.utils.All_Forall]
l':1942 [in MetaCoq.Template.utils.All_Forall]
l':196 [in MetaCoq.Template.Environment]
l':1960 [in MetaCoq.Template.utils.All_Forall]
l':1976 [in MetaCoq.Template.utils.All_Forall]
l':1981 [in MetaCoq.Template.utils.All_Forall]
l':1994 [in MetaCoq.Template.utils.All_Forall]
l':200 [in MetaCoq.Template.utils.All_Forall]
l':2007 [in MetaCoq.Template.utils.All_Forall]
l':2013 [in MetaCoq.Template.utils.All_Forall]
l':2021 [in MetaCoq.Template.utils.All_Forall]
l':2028 [in MetaCoq.Template.utils.All_Forall]
l':203 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
l':2034 [in MetaCoq.Template.utils.All_Forall]
l':204 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
l':2040 [in MetaCoq.Template.utils.All_Forall]
l':2059 [in MetaCoq.Template.utils.All_Forall]
l':2064 [in MetaCoq.Template.utils.All_Forall]
l':207 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
l':2073 [in MetaCoq.Template.utils.All_Forall]
l':2083 [in MetaCoq.Template.utils.All_Forall]
l':209 [in MetaCoq.Template.utils.All_Forall]
l':2090 [in MetaCoq.Template.utils.All_Forall]
l':2098 [in MetaCoq.Template.utils.All_Forall]
l':2105 [in MetaCoq.Template.utils.All_Forall]
l':211 [in MetaCoq.PCUIC.PCUICNormal]
l':2112 [in MetaCoq.Template.utils.All_Forall]
l':212 [in MetaCoq.Template.Typing]
l':213 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
l':214 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
l':2140 [in MetaCoq.Template.utils.All_Forall]
l':2151 [in MetaCoq.Template.utils.All_Forall]
l':2160 [in MetaCoq.Template.utils.All_Forall]
l':2168 [in MetaCoq.Template.utils.All_Forall]
l':217 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
l':2176 [in MetaCoq.Template.utils.All_Forall]
l':2185 [in MetaCoq.Template.utils.All_Forall]
l':22 [in MetaCoq.Template.utils.All_Forall]
l':22 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
l':22 [in MetaCoq.PCUIC.PCUICParallelReduction]
l':220 [in MetaCoq.Template.utils.All_Forall]
l':220 [in MetaCoq.SafeChecker.PCUICEqualityDec]
l':223 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
l':2231 [in MetaCoq.Template.utils.All_Forall]
l':224 [in MetaCoq.Template.TypingWf]
l':2245 [in MetaCoq.Template.utils.All_Forall]
l':23 [in MetaCoq.PCUIC.PCUICConfluence]
l':231 [in MetaCoq.Template.utils.All_Forall]
l':235 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
l':2364 [in MetaCoq.SafeChecker.PCUICSafeConversion]
l':240 [in MetaCoq.Template.utils.MCList]
l':242 [in MetaCoq.Template.utils.All_Forall]
l':243 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
l':243 [in MetaCoq.SafeChecker.PCUICEqualityDec]
l':2448 [in MetaCoq.Template.utils.All_Forall]
l':2457 [in MetaCoq.Template.utils.All_Forall]
l':248 [in MetaCoq.Template.TermEquality]
l':2484 [in MetaCoq.Template.utils.All_Forall]
l':249 [in MetaCoq.PCUIC.Syntax.PCUICCases]
l':2497 [in MetaCoq.Template.utils.All_Forall]
l':25 [in MetaCoq.Template.AstUtils]
l':250 [in MetaCoq.Template.utils.All_Forall]
l':253 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
l':255 [in MetaCoq.Template.TermEquality]
l':2572 [in MetaCoq.Template.utils.All_Forall]
l':258 [in MetaCoq.Template.utils.All_Forall]
l':258 [in MetaCoq.SafeChecker.PCUICEqualityDec]
l':2585 [in MetaCoq.Template.utils.All_Forall]
l':2596 [in MetaCoq.Template.utils.All_Forall]
l':26 [in MetaCoq.Erasure.Extract]
l':260 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
l':262 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
l':264 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
l':266 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
l':266 [in MetaCoq.Template.TypingWf]
l':267 [in MetaCoq.Template.utils.All_Forall]
l':269 [in MetaCoq.SafeChecker.PCUICSafeChecker]
l':270 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
l':277 [in MetaCoq.Template.utils.All_Forall]
l':277 [in MetaCoq.SafeChecker.PCUICEqualityDec]
l':279 [in MetaCoq.Template.utils.MCList]
l':280 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
l':282 [in MetaCoq.SafeChecker.PCUICEqualityDec]
l':283 [in MetaCoq.Template.utils.MCList]
l':284 [in MetaCoq.Erasure.EWcbvEval]
l':286 [in MetaCoq.PCUIC.PCUICWcbvEval]
l':287 [in MetaCoq.Template.utils.All_Forall]
l':287 [in MetaCoq.Template.WcbvEval]
l':288 [in MetaCoq.Erasure.ERemoveParams]
l':290 [in MetaCoq.Erasure.ERemoveParams]
l':291 [in MetaCoq.PCUIC.PCUICParallelReduction]
l':291 [in MetaCoq.Template.WcbvEval]
l':292 [in MetaCoq.Erasure.ERemoveParams]
l':292 [in MetaCoq.PCUIC.PCUICReduction]
l':293 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
l':294 [in MetaCoq.Template.common.uGraph]
l':294 [in MetaCoq.Erasure.ERemoveParams]
l':294 [in MetaCoq.SafeChecker.PCUICSafeChecker]
l':296 [in MetaCoq.Erasure.ERemoveParams]
l':297 [in MetaCoq.Template.common.uGraph]
l':298 [in MetaCoq.Erasure.ERemoveParams]
l':30 [in MetaCoq.PCUIC.PCUICParallelReduction]
L':30 [in MetaCoq.Erasure.ErasureProperties]
l':301 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
l':301 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
l':302 [in MetaCoq.Template.common.uGraph]
l':307 [in MetaCoq.Template.common.uGraph]
l':310 [in MetaCoq.Template.common.uGraph]
l':312 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
l':313 [in MetaCoq.Template.common.uGraph]
l':314 [in MetaCoq.Template.utils.All_Forall]
l':316 [in MetaCoq.PCUIC.PCUICSR]
l':318 [in MetaCoq.Template.utils.All_Forall]
l':318 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
l':32 [in MetaCoq.PCUIC.PCUICConfluence]
l':32 [in MetaCoq.Erasure.EAstUtils]
l':320 [in MetaCoq.Template.WcbvEval]
l':328 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
l':331 [in MetaCoq.Template.utils.MCList]
l':332 [in MetaCoq.SafeChecker.PCUICEqualityDec]
l':335 [in MetaCoq.Template.utils.All_Forall]
l':337 [in MetaCoq.Template.utils.MCList]
l':34 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
l':343 [in MetaCoq.Template.utils.All_Forall]
l':344 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
l':346 [in MetaCoq.PCUIC.PCUICConversion]
l':349 [in MetaCoq.Template.TypingWf]
l':35 [in MetaCoq.Template.Universes]
l':350 [in MetaCoq.Template.utils.All_Forall]
l':354 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
l':358 [in MetaCoq.Template.utils.All_Forall]
l':358 [in MetaCoq.PCUIC.PCUICConversion]
l':358 [in MetaCoq.SafeChecker.PCUICEqualityDec]
L':36 [in MetaCoq.Erasure.ErasureProperties]
l':36 [in MetaCoq.Template.AstUtils]
l':361 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
l':363 [in MetaCoq.Template.utils.All_Forall]
l':364 [in MetaCoq.PCUIC.PCUICConversion]
l':365 [in MetaCoq.PCUIC.PCUICNormal]
l':366 [in MetaCoq.PCUIC.PCUICSubstitution]
l':372 [in MetaCoq.PCUIC.PCUICConversion]
l':374 [in MetaCoq.SafeChecker.PCUICEqualityDec]
l':377 [in MetaCoq.Template.utils.All_Forall]
l':377 [in MetaCoq.PCUIC.PCUICConversion]
l':379 [in MetaCoq.SafeChecker.PCUICSafeChecker]
l':379 [in MetaCoq.SafeChecker.PCUICEqualityDec]
l':380 [in MetaCoq.PCUIC.PCUICConversion]
l':384 [in MetaCoq.SafeChecker.PCUICEqualityDec]
l':385 [in MetaCoq.Template.utils.MCList]
l':386 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
l':389 [in MetaCoq.Template.utils.All_Forall]
l':389 [in MetaCoq.SafeChecker.PCUICSafeChecker]
l':39 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
l':392 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
l':394 [in MetaCoq.PCUIC.PCUICConversion]
l':399 [in MetaCoq.Template.utils.All_Forall]
l':399 [in MetaCoq.Template.Typing]
l':4 [in MetaCoq.PCUIC.utils.PCUICOnOne]
l':402 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
l':402 [in MetaCoq.PCUIC.PCUICConversion]
l':402 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
l':407 [in MetaCoq.Template.utils.All_Forall]
l':41 [in MetaCoq.Template.utils.MCList]
l':41 [in MetaCoq.PCUIC.PCUICConfluence]
l':412 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
l':412 [in MetaCoq.Erasure.ErasureFunction]
l':412 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
l':416 [in MetaCoq.Template.utils.All_Forall]
l':418 [in MetaCoq.PCUIC.PCUICNormal]
l':42 [in MetaCoq.PCUIC.PCUICParallelReduction]
l':424 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
l':426 [in MetaCoq.Template.utils.All_Forall]
l':428 [in MetaCoq.PCUIC.PCUICEquality]
l':43 [in MetaCoq.Template.utils.All_Forall]
l':430 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
l':433 [in MetaCoq.Template.utils.MCList]
l':44 [in MetaCoq.PCUIC.PCUICCanonicity]
l':44 [in MetaCoq.Erasure.Prelim]
l':451 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
l':453 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
L':46 [in MetaCoq.Erasure.ErasureProperties]
l':46 [in MetaCoq.Template.AstUtils]
l':463 [in MetaCoq.PCUIC.PCUICEquality]
l':47 [in MetaCoq.Template.TypingWf]
l':472 [in MetaCoq.Template.Universes]
l':472 [in MetaCoq.PCUIC.PCUICSR]
l':475 [in MetaCoq.Template.Universes]
l':481 [in MetaCoq.Template.utils.MCList]
l':486 [in MetaCoq.SafeChecker.PCUICSafeChecker]
l':49 [in MetaCoq.Template.monad_utils]
l':496 [in MetaCoq.Template.utils.MCList]
l':496 [in MetaCoq.PCUIC.PCUICParallelReduction]
l':497 [in MetaCoq.Template.utils.All_Forall]
l':50 [in MetaCoq.Erasure.EInduction]
l':50 [in MetaCoq.PCUIC.PCUICConfluence]
l':50 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
l':500 [in MetaCoq.Template.common.uGraph]
l':506 [in MetaCoq.Template.common.uGraph]
l':508 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
l':51 [in MetaCoq.Template.utils.MCList]
l':51 [in MetaCoq.PCUIC.PCUICSR]
l':51 [in MetaCoq.Erasure.EAstUtils]
l':514 [in MetaCoq.PCUIC.PCUICEquality]
l':518 [in MetaCoq.Template.utils.MCList]
l':519 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
l':522 [in MetaCoq.Template.utils.MCList]
l':523 [in MetaCoq.PCUIC.PCUICEquality]
l':528 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
l':538 [in MetaCoq.Template.utils.MCList]
l':538 [in MetaCoq.PCUIC.PCUICEquality]
l':54 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
l':541 [in MetaCoq.Template.utils.All_Forall]
l':544 [in MetaCoq.Template.utils.MCList]
l':546 [in MetaCoq.PCUIC.PCUICEquality]
l':553 [in MetaCoq.Template.utils.MCList]
l':554 [in MetaCoq.Erasure.EEtaExpandedFix]
l':557 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
l':56 [in MetaCoq.Erasure.EAstUtils]
l':564 [in MetaCoq.Template.common.uGraph]
l':569 [in MetaCoq.Template.common.uGraph]
l':57 [in MetaCoq.PCUIC.PCUICConfluence]
l':571 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
l':579 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
l':581 [in MetaCoq.Template.utils.All_Forall]
l':585 [in MetaCoq.PCUIC.PCUICConversion]
l':59 [in MetaCoq.Erasure.EInduction]
L':59 [in MetaCoq.Erasure.EArities]
l':590 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
l':591 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
l':592 [in MetaCoq.Template.utils.All_Forall]
l':592 [in MetaCoq.Template.common.uGraph]
l':592 [in MetaCoq.PCUIC.PCUICConversion]
l':594 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
l':597 [in MetaCoq.Template.utils.All_Forall]
l':597 [in MetaCoq.Template.common.uGraph]
l':6 [in MetaCoq.Template.utils.MCList]
l':6 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
l':60 [in MetaCoq.Erasure.EArities]
l':60 [in MetaCoq.Template.monad_utils]
l':60 [in MetaCoq.Erasure.EAstUtils]
l':601 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
l':602 [in MetaCoq.Template.utils.All_Forall]
l':607 [in MetaCoq.Template.utils.MCList]
l':608 [in MetaCoq.Template.utils.All_Forall]
l':613 [in MetaCoq.Template.utils.All_Forall]
l':620 [in MetaCoq.Template.utils.All_Forall]
l':623 [in MetaCoq.PCUIC.PCUICEquality]
l':629 [in MetaCoq.Template.utils.All_Forall]
l':63 [in MetaCoq.Erasure.EAstUtils]
l':634 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
l':639 [in MetaCoq.Template.utils.All_Forall]
l':642 [in MetaCoq.Template.utils.All_Forall]
l':646 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
l':65 [in MetaCoq.PCUIC.PCUICConfluence]
l':655 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
L':66 [in MetaCoq.Translations.times_bool_fun]
l':668 [in MetaCoq.PCUIC.PCUICInductiveInversion]
L':67 [in MetaCoq.Translations.times_bool_fun]
l':67 [in MetaCoq.Template.utils.ReflectEq]
l':67 [in MetaCoq.PCUIC.Syntax.PCUICReflect]
l':67 [in MetaCoq.Template.monad_utils]
l':671 [in MetaCoq.Template.utils.All_Forall]
l':671 [in MetaCoq.PCUIC.PCUICEquality]
l':680 [in MetaCoq.Template.utils.All_Forall]
l':685 [in MetaCoq.Template.utils.All_Forall]
l':689 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
l':69 [in MetaCoq.Template.Reflect]
l':692 [in MetaCoq.Template.utils.All_Forall]
l':693 [in MetaCoq.Template.utils.MCList]
l':697 [in MetaCoq.Template.utils.MCList]
l':699 [in MetaCoq.Template.Universes]
l':699 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
l':7 [in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
l':701 [in MetaCoq.Template.Universes]
l':701 [in MetaCoq.Template.utils.All_Forall]
l':71 [in MetaCoq.Template.utils.MCOption]
l':712 [in MetaCoq.Template.utils.MCList]
l':727 [in MetaCoq.Template.utils.MCList]
l':727 [in MetaCoq.PCUIC.PCUICReduction]
l':73 [in MetaCoq.Template.Reflect]
l':739 [in MetaCoq.PCUIC.PCUICReduction]
l':740 [in MetaCoq.Template.utils.MCList]
l':742 [in MetaCoq.Template.utils.All_Forall]
l':747 [in MetaCoq.PCUIC.PCUICReduction]
l':750 [in MetaCoq.Template.utils.MCList]
l':752 [in MetaCoq.PCUIC.PCUICReduction]
l':756 [in MetaCoq.Template.utils.All_Forall]
l':756 [in MetaCoq.Template.utils.MCList]
l':757 [in MetaCoq.PCUIC.PCUICReduction]
l':761 [in MetaCoq.Template.utils.MCList]
l':762 [in MetaCoq.Template.utils.All_Forall]
l':762 [in MetaCoq.PCUIC.PCUICReduction]
l':766 [in MetaCoq.PCUIC.PCUICReduction]
l':768 [in MetaCoq.Template.utils.All_Forall]
l':77 [in MetaCoq.Template.Reflect]
l':77 [in MetaCoq.Template.utils.MCOption]
l':77 [in MetaCoq.PCUIC.PCUICConfluence]
l':776 [in MetaCoq.Template.utils.All_Forall]
l':777 [in MetaCoq.PCUIC.PCUICReduction]
l':78 [in MetaCoq.Template.monad_utils]
l':78 [in MetaCoq.Erasure.EAstUtils]
l':783 [in MetaCoq.Template.utils.All_Forall]
l':786 [in MetaCoq.PCUIC.PCUICReduction]
l':79 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
l':792 [in MetaCoq.Template.utils.All_Forall]
l':792 [in MetaCoq.PCUIC.PCUICReduction]
l':799 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
l':802 [in MetaCoq.PCUIC.PCUICReduction]
l':803 [in MetaCoq.Template.utils.All_Forall]
l':807 [in MetaCoq.PCUIC.PCUICReduction]
l':81 [in MetaCoq.Template.Universes]
l':81 [in MetaCoq.Erasure.Extract]
l':81 [in MetaCoq.Template.Reflect]
l':812 [in MetaCoq.PCUIC.PCUICReduction]
l':813 [in MetaCoq.PCUIC.PCUICParallelReduction]
l':815 [in MetaCoq.Template.utils.All_Forall]
l':816 [in MetaCoq.PCUIC.PCUICReduction]
l':819 [in MetaCoq.Template.utils.All_Forall]
l':821 [in MetaCoq.PCUIC.PCUICInductiveInversion]
l':822 [in MetaCoq.PCUIC.PCUICReduction]
l':824 [in MetaCoq.Template.utils.MCList]
l':824 [in MetaCoq.PCUIC.PCUICReduction]
l':833 [in MetaCoq.Template.utils.MCList]
l':833 [in MetaCoq.PCUIC.PCUICReduction]
l':84 [in MetaCoq.PCUIC.PCUICParallelReduction]
l':849 [in MetaCoq.Template.utils.MCList]
l':85 [in MetaCoq.PCUIC.PCUICWeakeningEnv]
l':853 [in MetaCoq.Template.utils.All_Forall]
l':86 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
l':86 [in MetaCoq.Template.utils.All_Forall]
l':864 [in MetaCoq.Template.utils.All_Forall]
l':870 [in MetaCoq.Template.utils.All_Forall]
l':878 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
l':879 [in MetaCoq.Template.utils.All_Forall]
l':88 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
l':887 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
l':90 [in MetaCoq.SafeChecker.PCUICEqualityDec]
l':905 [in MetaCoq.Template.utils.All_Forall]
l':908 [in MetaCoq.PCUIC.PCUICReduction]
l':915 [in MetaCoq.Template.utils.All_Forall]
l':92 [in MetaCoq.PCUIC.PCUICConfluence]
l':922 [in MetaCoq.PCUIC.PCUICReduction]
l':927 [in MetaCoq.Template.utils.MCList]
l':929 [in MetaCoq.PCUIC.PCUICReduction]
l':932 [in MetaCoq.Template.utils.All_Forall]
l':938 [in MetaCoq.Template.utils.All_Forall]
l':939 [in MetaCoq.PCUIC.PCUICTyping]
l':945 [in MetaCoq.Template.utils.All_Forall]
l':945 [in MetaCoq.PCUIC.PCUICTyping]
l':954 [in MetaCoq.Template.utils.All_Forall]
l':962 [in MetaCoq.PCUIC.PCUICReduction]
l':964 [in MetaCoq.Template.utils.All_Forall]
l':97 [in MetaCoq.SafeChecker.PCUICEqualityDec]
l':973 [in MetaCoq.Template.utils.All_Forall]
l':983 [in MetaCoq.Template.utils.All_Forall]
l':995 [in MetaCoq.Template.utils.All_Forall]
l0':1999 [in MetaCoq.Template.utils.All_Forall]
l0':2606 [in MetaCoq.Template.utils.All_Forall]
l0':593 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
l0:1485 [in MetaCoq.Template.utils.All_Forall]
l0:1494 [in MetaCoq.Template.utils.All_Forall]
l0:1500 [in MetaCoq.Template.utils.All_Forall]
l0:1509 [in MetaCoq.Template.utils.All_Forall]
l0:1998 [in MetaCoq.Template.utils.All_Forall]
l0:2605 [in MetaCoq.Template.utils.All_Forall]
l0:592 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
l0:69 [in MetaCoq.SafeChecker.PCUICWfEnv]
l1'':817 [in MetaCoq.PCUIC.PCUICParallelReduction]
l1':1516 [in MetaCoq.Template.utils.All_Forall]
l1':2001 [in MetaCoq.Template.utils.All_Forall]
l1':2608 [in MetaCoq.Template.utils.All_Forall]
l1':382 [in MetaCoq.Template.Universes]
l1':393 [in MetaCoq.Template.Universes]
l1':816 [in MetaCoq.PCUIC.PCUICParallelReduction]
l1:1019 [in MetaCoq.Template.utils.All_Forall]
l1:1034 [in MetaCoq.Template.utils.All_Forall]
l1:111 [in MetaCoq.Template.monad_utils]
l1:115 [in MetaCoq.Template.utils.MCList]
l1:1186 [in MetaCoq.Template.utils.wGraph]
l1:122 [in MetaCoq.Erasure.EConstructorsAsBlocks]
l1:1229 [in MetaCoq.Template.utils.All_Forall]
l1:1238 [in MetaCoq.Template.utils.All_Forall]
l1:1249 [in MetaCoq.Template.utils.All_Forall]
l1:1262 [in MetaCoq.Template.utils.All_Forall]
l1:133 [in MetaCoq.SafeChecker.PCUICErrors]
l1:144 [in MetaCoq.SafeChecker.PCUICErrors]
l1:1461 [in MetaCoq.Template.utils.All_Forall]
l1:1472 [in MetaCoq.Template.utils.All_Forall]
l1:1477 [in MetaCoq.Template.utils.All_Forall]
l1:1514 [in MetaCoq.Template.utils.All_Forall]
l1:153 [in MetaCoq.SafeChecker.PCUICErrors]
l1:1570 [in MetaCoq.Template.utils.All_Forall]
l1:16 [in MetaCoq.Template.Universes]
l1:1711 [in MetaCoq.Template.utils.All_Forall]
L1:1760 [in MetaCoq.Template.utils.All_Forall]
l1:1950 [in MetaCoq.Template.utils.All_Forall]
l1:197 [in MetaCoq.SafeChecker.PCUICErrors]
l1:2000 [in MetaCoq.Template.utils.All_Forall]
l1:2048 [in MetaCoq.Template.utils.All_Forall]
l1:222 [in MetaCoq.PCUIC.PCUICSR]
l1:231 [in MetaCoq.Template.Checker]
l1:235 [in MetaCoq.PCUIC.PCUICSR]
l1:238 [in MetaCoq.Template.Checker]
l1:249 [in MetaCoq.Template.Checker]
l1:2607 [in MetaCoq.Template.utils.All_Forall]
l1:280 [in MetaCoq.SafeChecker.PCUICErrors]
l1:287 [in MetaCoq.SafeChecker.PCUICErrors]
l1:294 [in MetaCoq.SafeChecker.PCUICErrors]
l1:299 [in MetaCoq.SafeChecker.PCUICErrors]
l1:3 [in MetaCoq.Template.Reflect]
l1:306 [in MetaCoq.SafeChecker.PCUICErrors]
l1:32 [in MetaCoq.Template.utils.MCCompare]
l1:32 [in MetaCoq.Template.Universes]
l1:335 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
l1:34 [in MetaCoq.Template.utils.MCCompare]
L1:340 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
L1:343 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
l1:36 [in MetaCoq.Template.Universes]
l1:367 [in MetaCoq.Template.Universes]
l1:372 [in MetaCoq.Template.Universes]
l1:376 [in MetaCoq.Template.Universes]
l1:38 [in MetaCoq.Template.utils.MCCompare]
l1:381 [in MetaCoq.Template.Universes]
l1:389 [in MetaCoq.Template.Universes]
l1:395 [in MetaCoq.Template.utils.MCList]
l1:403 [in MetaCoq.Template.common.uGraph]
L1:41 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
l1:412 [in MetaCoq.Template.utils.MCList]
l1:417 [in MetaCoq.Template.common.uGraph]
l1:42 [in MetaCoq.Template.Universes]
L1:42 [in MetaCoq.Erasure.ErasureProperties]
l1:424 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
l1:432 [in MetaCoq.Template.common.uGraph]
l1:4400 [in MetaCoq.SafeChecker.PCUICSafeConversion]
l1:4418 [in MetaCoq.SafeChecker.PCUICSafeConversion]
l1:447 [in MetaCoq.Template.common.uGraph]
l1:502 [in MetaCoq.PCUIC.PCUICEquality]
l1:527 [in MetaCoq.Template.utils.MCList]
l1:528 [in MetaCoq.PCUIC.PCUICEquality]
l1:551 [in MetaCoq.Template.common.uGraph]
l1:57 [in MetaCoq.Template.Universes]
l1:645 [in MetaCoq.Template.utils.All_Forall]
l1:657 [in MetaCoq.Template.utils.All_Forall]
l1:67 [in MetaCoq.Template.utils.MCCompare]
l1:687 [in MetaCoq.Template.utils.MCList]
l1:7 [in MetaCoq.Template.Reflect]
l1:705 [in MetaCoq.Template.utils.All_Forall]
l1:717 [in MetaCoq.Template.utils.All_Forall]
l1:721 [in MetaCoq.PCUIC.PCUICReduction]
l1:776 [in MetaCoq.Template.Universes]
l1:789 [in MetaCoq.Template.utils.MCList]
l1:815 [in MetaCoq.PCUIC.PCUICParallelReduction]
l1:820 [in MetaCoq.Template.utils.MCList]
l1:822 [in MetaCoq.Template.utils.MCList]
l1:823 [in MetaCoq.Template.utils.All_Forall]
l1:827 [in MetaCoq.Template.utils.MCList]
l1:837 [in MetaCoq.Template.utils.All_Forall]
l1:838 [in MetaCoq.Template.utils.MCList]
l1:843 [in MetaCoq.Template.utils.MCList]
l1:845 [in MetaCoq.Template.utils.MCList]
l1:847 [in MetaCoq.Template.utils.MCList]
l1:85 [in MetaCoq.SafeChecker.PCUICSafeChecker]
l1:850 [in MetaCoq.Template.utils.MCList]
l1:852 [in MetaCoq.Template.utils.MCList]
l1:854 [in MetaCoq.Template.utils.MCList]
l1:90 [in MetaCoq.Template.Universes]
l2':1517 [in MetaCoq.Template.utils.All_Forall]
l2':375 [in MetaCoq.Template.Universes]
l2':380 [in MetaCoq.Template.Universes]
l2':386 [in MetaCoq.Template.Universes]
l2':391 [in MetaCoq.Template.Universes]
L2':44 [in MetaCoq.Erasure.ErasureProperties]
l2:1020 [in MetaCoq.Template.utils.All_Forall]
l2:1035 [in MetaCoq.Template.utils.All_Forall]
l2:112 [in MetaCoq.Template.monad_utils]
l2:116 [in MetaCoq.Template.utils.MCList]
l2:1187 [in MetaCoq.Template.utils.wGraph]
l2:123 [in MetaCoq.Erasure.EConstructorsAsBlocks]
l2:1250 [in MetaCoq.Template.utils.All_Forall]
l2:1263 [in MetaCoq.Template.utils.All_Forall]
l2:137 [in MetaCoq.SafeChecker.PCUICErrors]
l2:1462 [in MetaCoq.Template.utils.All_Forall]
l2:1473 [in MetaCoq.Template.utils.All_Forall]
l2:1478 [in MetaCoq.Template.utils.All_Forall]
l2:148 [in MetaCoq.SafeChecker.PCUICErrors]
l2:1515 [in MetaCoq.Template.utils.All_Forall]
l2:156 [in MetaCoq.SafeChecker.PCUICErrors]
l2:1571 [in MetaCoq.Template.utils.All_Forall]
l2:17 [in MetaCoq.Template.Universes]
l2:1712 [in MetaCoq.Template.utils.All_Forall]
L2:1761 [in MetaCoq.Template.utils.All_Forall]
l2:195 [in MetaCoq.SafeChecker.PCUICErrors]
l2:1951 [in MetaCoq.Template.utils.All_Forall]
l2:2049 [in MetaCoq.Template.utils.All_Forall]
l2:223 [in MetaCoq.PCUIC.PCUICSR]
l2:233 [in MetaCoq.Template.Checker]
l2:236 [in MetaCoq.PCUIC.PCUICSR]
l2:240 [in MetaCoq.Template.Checker]
l2:250 [in MetaCoq.Template.Checker]
l2:300 [in MetaCoq.SafeChecker.PCUICErrors]
l2:307 [in MetaCoq.SafeChecker.PCUICErrors]
l2:33 [in MetaCoq.Template.utils.MCCompare]
l2:33 [in MetaCoq.Template.Universes]
l2:336 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
L2:341 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
L2:344 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
l2:35 [in MetaCoq.Template.utils.MCCompare]
l2:369 [in MetaCoq.Template.Universes]
l2:37 [in MetaCoq.Template.Universes]
l2:374 [in MetaCoq.Template.Universes]
l2:379 [in MetaCoq.Template.Universes]
l2:385 [in MetaCoq.Template.Universes]
l2:387 [in MetaCoq.Template.Universes]
l2:39 [in MetaCoq.Template.utils.MCCompare]
l2:396 [in MetaCoq.Template.utils.MCList]
l2:4 [in MetaCoq.Template.Reflect]
l2:404 [in MetaCoq.Template.common.uGraph]
l2:413 [in MetaCoq.Template.utils.MCList]
l2:418 [in MetaCoq.Template.common.uGraph]
L2:42 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
l2:425 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
l2:43 [in MetaCoq.Template.Universes]
L2:43 [in MetaCoq.Erasure.ErasureProperties]
l2:433 [in MetaCoq.Template.common.uGraph]
l2:4423 [in MetaCoq.SafeChecker.PCUICSafeConversion]
l2:448 [in MetaCoq.Template.common.uGraph]
l2:504 [in MetaCoq.PCUIC.PCUICEquality]
l2:528 [in MetaCoq.Template.utils.MCList]
l2:530 [in MetaCoq.PCUIC.PCUICEquality]
l2:552 [in MetaCoq.Template.common.uGraph]
l2:58 [in MetaCoq.Template.Universes]
l2:646 [in MetaCoq.Template.utils.All_Forall]
l2:658 [in MetaCoq.Template.utils.All_Forall]
l2:68 [in MetaCoq.Template.utils.MCCompare]
l2:688 [in MetaCoq.Template.utils.MCList]
l2:706 [in MetaCoq.Template.utils.All_Forall]
l2:718 [in MetaCoq.Template.utils.All_Forall]
l2:722 [in MetaCoq.PCUIC.PCUICReduction]
l2:774 [in MetaCoq.Template.Universes]
l2:790 [in MetaCoq.Template.utils.MCList]
l2:8 [in MetaCoq.Template.Reflect]
l2:821 [in MetaCoq.Template.utils.MCList]
l2:823 [in MetaCoq.Template.utils.MCList]
l2:824 [in MetaCoq.Template.utils.All_Forall]
l2:828 [in MetaCoq.Template.utils.MCList]
l2:838 [in MetaCoq.Template.utils.All_Forall]
l2:839 [in MetaCoq.Template.utils.MCList]
l2:84 [in MetaCoq.SafeChecker.PCUICSafeChecker]
l2:844 [in MetaCoq.Template.utils.MCList]
l2:846 [in MetaCoq.Template.utils.MCList]
l2:848 [in MetaCoq.Template.utils.MCList]
l2:851 [in MetaCoq.Template.utils.MCList]
l2:853 [in MetaCoq.Template.utils.MCList]
l2:855 [in MetaCoq.Template.utils.MCList]
l2:91 [in MetaCoq.Template.Universes]
l3:1021 [in MetaCoq.Template.utils.All_Forall]
l3:1036 [in MetaCoq.Template.utils.All_Forall]
l3:1713 [in MetaCoq.Template.utils.All_Forall]
l3:224 [in MetaCoq.PCUIC.PCUICSR]
l3:237 [in MetaCoq.PCUIC.PCUICSR]
l3:337 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
l3:426 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
l3:647 [in MetaCoq.Template.utils.All_Forall]
l3:659 [in MetaCoq.Template.utils.All_Forall]
l3:707 [in MetaCoq.Template.utils.All_Forall]
l3:825 [in MetaCoq.Template.utils.All_Forall]
l3:839 [in MetaCoq.Template.utils.All_Forall]
l4:1030 [in MetaCoq.Template.utils.All_Forall]
l4:1045 [in MetaCoq.Template.utils.All_Forall]
l4:655 [in MetaCoq.Template.utils.All_Forall]
l4:667 [in MetaCoq.Template.utils.All_Forall]
l4:834 [in MetaCoq.Template.utils.All_Forall]
l4:848 [in MetaCoq.Template.utils.All_Forall]
l:10 [in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
l:10 [in MetaCoq.Erasure.EOptimizePropDiscr]
l:100 [in MetaCoq.Template.utils.All_Forall]
l:100 [in MetaCoq.Template.utils.MCList]
L:100 [in MetaCoq.Translations.param_cheap_packed]
l:100 [in MetaCoq.PCUIC.PCUICConfluence]
l:100 [in MetaCoq.SafeChecker.PCUICEqualityDec]
l:1002 [in MetaCoq.Template.utils.All_Forall]
L:1005 [in MetaCoq.Template.utils.All_Forall]
l:1006 [in MetaCoq.PCUIC.PCUICReduction]
l:1007 [in MetaCoq.PCUIC.PCUICReduction]
l:1008 [in MetaCoq.PCUIC.PCUICReduction]
l:1009 [in MetaCoq.Template.utils.All_Forall]
l:1009 [in MetaCoq.PCUIC.PCUICReduction]
l:101 [in MetaCoq.PCUIC.PCUICNormal]
l:1011 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
l:1013 [in MetaCoq.Template.utils.All_Forall]
l:1017 [in MetaCoq.Template.Typing]
l:102 [in MetaCoq.Template.utils.MCList]
l:102 [in MetaCoq.SafeChecker.PCUICWfEnv]
L:102 [in MetaCoq.Translations.param_cheap_packed]
l:102 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
l:102 [in MetaCoq.Template.LiftSubst]
l:1020 [in MetaCoq.SafeChecker.PCUICSafeChecker]
l:103 [in MetaCoq.Template.WfAst]
l:103 [in MetaCoq.Erasure.EAstUtils]
l:1032 [in MetaCoq.PCUIC.PCUICReduction]
l:1033 [in MetaCoq.PCUIC.PCUICReduction]
l:1034 [in MetaCoq.PCUIC.PCUICReduction]
l:1035 [in MetaCoq.PCUIC.PCUICReduction]
l:105 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
l:105 [in MetaCoq.Template.EnvironmentTyping]
l:105 [in MetaCoq.Erasure.EAstUtils]
l:105 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
l:1050 [in MetaCoq.Template.utils.All_Forall]
l:1050 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
l:106 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
L:106 [in MetaCoq.Translations.times_bool_fun]
l:106 [in MetaCoq.Template.utils.All_Forall]
l:106 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
l:106 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
l:1062 [in MetaCoq.Template.utils.All_Forall]
L:107 [in MetaCoq.Translations.times_bool_fun]
l:107 [in MetaCoq.Template.utils.MCList]
l:107 [in MetaCoq.PCUIC.Syntax.PCUICViews]
l:107 [in MetaCoq.Erasure.ELiftSubst]
l:107 [in MetaCoq.PCUIC.PCUICContextConversion]
l:1070 [in MetaCoq.Template.utils.All_Forall]
l:1075 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
l:1077 [in MetaCoq.PCUIC.PCUICReduction]
l:1078 [in MetaCoq.Template.utils.wGraph]
l:1078 [in MetaCoq.PCUIC.PCUICReduction]
l:1079 [in MetaCoq.PCUIC.PCUICReduction]
l:108 [in MetaCoq.Template.utils.MCList]
L:108 [in MetaCoq.Translations.param_cheap_packed]
l:1080 [in MetaCoq.Template.utils.All_Forall]
l:1080 [in MetaCoq.PCUIC.PCUICReduction]
l:1081 [in MetaCoq.Template.utils.wGraph]
l:1084 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
l:1086 [in MetaCoq.Erasure.ErasureFunction]
l:109 [in MetaCoq.PCUIC.PCUICConfluence]
l:1091 [in MetaCoq.Erasure.ErasureFunction]
l:1092 [in MetaCoq.Template.utils.All_Forall]
l:1095 [in MetaCoq.Erasure.ErasureFunction]
l:1099 [in MetaCoq.Erasure.ErasureFunction]
l:11 [in MetaCoq.Template.Universes]
l:11 [in MetaCoq.Erasure.EArities]
l:11 [in MetaCoq.Template.utils.MCList]
l:11 [in MetaCoq.Template.Typing]
l:11 [in MetaCoq.Template.utils.MCString]
l:11 [in MetaCoq.Template.utils.wGraph]
l:11 [in MetaCoq.Examples.add_constructor]
l:110 [in MetaCoq.Template.Universes]
l:110 [in MetaCoq.PCUIC.PCUICCumulativity]
l:110 [in MetaCoq.Template.utils.MCList]
l:1101 [in MetaCoq.Template.utils.All_Forall]
l:1103 [in MetaCoq.PCUIC.PCUICReduction]
l:1104 [in MetaCoq.PCUIC.PCUICReduction]
l:1105 [in MetaCoq.PCUIC.PCUICReduction]
l:1106 [in MetaCoq.PCUIC.PCUICReduction]
l:1107 [in MetaCoq.Erasure.ErasureFunction]
l:1110 [in MetaCoq.Template.utils.All_Forall]
l:1112 [in MetaCoq.Erasure.ErasureFunction]
l:1115 [in MetaCoq.Template.utils.All_Forall]
l:1115 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
l:1116 [in MetaCoq.Erasure.ErasureFunction]
l:112 [in MetaCoq.Template.AstUtils]
l:1120 [in MetaCoq.Erasure.ErasureFunction]
l:1121 [in MetaCoq.Template.utils.All_Forall]
l:1130 [in MetaCoq.Template.utils.All_Forall]
l:1139 [in MetaCoq.Template.utils.All_Forall]
l:114 [in MetaCoq.Template.utils.All_Forall]
l:1142 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
l:1145 [in MetaCoq.PCUIC.PCUICReduction]
l:1147 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
l:1148 [in MetaCoq.Template.utils.All_Forall]
l:115 [in MetaCoq.Template.Checker]
l:1153 [in MetaCoq.PCUIC.PCUICReduction]
l:1154 [in MetaCoq.Template.utils.wGraph]
l:1154 [in MetaCoq.PCUIC.PCUICReduction]
l:1155 [in MetaCoq.PCUIC.PCUICReduction]
l:1156 [in MetaCoq.PCUIC.PCUICReduction]
l:1157 [in MetaCoq.Template.utils.All_Forall]
l:1158 [in MetaCoq.PCUIC.PCUICReduction]
l:116 [in MetaCoq.Translations.param_binary]
l:116 [in MetaCoq.Erasure.ERemoveParams]
l:1163 [in MetaCoq.Template.utils.wGraph]
l:1166 [in MetaCoq.Template.utils.All_Forall]
l:117 [in MetaCoq.PCUIC.PCUICReduction]
l:1170 [in MetaCoq.PCUIC.PCUICReduction]
l:1173 [in MetaCoq.Template.utils.All_Forall]
l:1175 [in MetaCoq.PCUIC.PCUICReduction]
l:1178 [in MetaCoq.Template.utils.All_Forall]
l:118 [in MetaCoq.Erasure.EConstructorsAsBlocks]
l:118 [in MetaCoq.Template.Ast]
l:1183 [in MetaCoq.PCUIC.PCUICReduction]
l:1185 [in MetaCoq.Template.utils.All_Forall]
L:119 [in MetaCoq.PCUIC.PCUICProgress]
l:119 [in MetaCoq.Erasure.EInduction]
l:1192 [in MetaCoq.Template.utils.All_Forall]
l:1199 [in MetaCoq.Template.utils.All_Forall]
l:12 [in MetaCoq.SafeChecker.PCUICWfEnv]
l:12 [in MetaCoq.Erasure.EAstUtils]
l:12 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
l:12 [in MetaCoq.SafeChecker.PCUICTypeChecker]
l:120 [in MetaCoq.Translations.param_binary]
l:120 [in MetaCoq.Erasure.EEtaExpanded]
l:120 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
l:1205 [in MetaCoq.Template.utils.All_Forall]
l:1206 [in MetaCoq.PCUIC.PCUICConversion]
l:121 [in MetaCoq.Erasure.EConstructorsAsBlocks]
l:121 [in MetaCoq.Erasure.EAstUtils]
l:1210 [in MetaCoq.Template.utils.All_Forall]
l:1214 [in MetaCoq.Template.utils.All_Forall]
l:1219 [in MetaCoq.Template.utils.All_Forall]
l:122 [in MetaCoq.PCUIC.PCUICCumulativity]
l:122 [in MetaCoq.Template.utils.All_Forall]
l:122 [in MetaCoq.Template.utils.MCList]
l:123 [in MetaCoq.Template.BasicAst]
l:123 [in MetaCoq.Template.Ast]
l:123 [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
l:123 [in MetaCoq.Erasure.EGlobalEnv]
l:1236 [in MetaCoq.PCUIC.PCUICConversion]
l:124 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
L:124 [in MetaCoq.Translations.times_bool_fun]
l:124 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
l:124 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
l:1244 [in MetaCoq.PCUIC.PCUICConversion]
L:125 [in MetaCoq.Translations.times_bool_fun]
l:125 [in MetaCoq.Template.utils.MCList]
l:125 [in MetaCoq.Template.EnvironmentTyping]
l:125 [in MetaCoq.PCUIC.Syntax.PCUICCases]
l:125 [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
l:126 [in MetaCoq.Translations.param_binary]
l:126 [in MetaCoq.Template.Ast]
l:1260 [in MetaCoq.SafeChecker.PCUICSafeReduce]
l:1264 [in MetaCoq.SafeChecker.PCUICSafeReduce]
l:1267 [in MetaCoq.Template.Typing]
l:127 [in MetaCoq.Erasure.EEtaExpandedFix]
l:127 [in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
l:1272 [in MetaCoq.Template.utils.All_Forall]
l:1278 [in MetaCoq.Template.Typing]
l:128 [in MetaCoq.Template.utils.All_Forall]
l:128 [in MetaCoq.PCUIC.Syntax.PCUICCases]
l:128 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
l:128 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
l:128 [in MetaCoq.Erasure.EOptimizePropDiscr]
l:1280 [in MetaCoq.Template.utils.All_Forall]
l:1284 [in MetaCoq.Template.utils.All_Forall]
l:1286 [in MetaCoq.Template.Typing]
l:1289 [in MetaCoq.Template.utils.All_Forall]
l:1294 [in MetaCoq.Template.utils.All_Forall]
l:13 [in MetaCoq.PCUIC.PCUICWeakeningEnv]
l:13 [in MetaCoq.PCUIC.Syntax.PCUICViews]
l:13 [in MetaCoq.PCUIC.PCUICWfUniverses]
l:13 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
l:13 [in MetaCoq.Erasure.ESpineView]
l:13 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
l:130 [in MetaCoq.PCUIC.PCUICSafeLemmata]
L:130 [in MetaCoq.Erasure.EArities]
l:130 [in MetaCoq.PCUIC.PCUICConfluence]
l:130 [in MetaCoq.Erasure.EGlobalEnv]
l:1300 [in MetaCoq.Template.utils.All_Forall]
l:1301 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
l:1305 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
l:1306 [in MetaCoq.Template.utils.All_Forall]
l:131 [in MetaCoq.Template.utils.MCList]
l:131 [in MetaCoq.Template.EnvironmentTyping]
l:131 [in MetaCoq.Erasure.EEtaExpanded]
l:1314 [in MetaCoq.Template.utils.All_Forall]
l:132 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
l:132 [in MetaCoq.Template.utils.MCList]
l:132 [in MetaCoq.Erasure.ELiftSubst]
l:1321 [in MetaCoq.Template.utils.All_Forall]
l:1329 [in MetaCoq.Template.utils.All_Forall]
l:133 [in MetaCoq.Template.utils.All_Forall]
L:133 [in MetaCoq.Translations.param_cheap_packed]
l:133 [in MetaCoq.PCUIC.PCUICContexts]
l:1334 [in MetaCoq.Template.utils.All_Forall]
l:1339 [in MetaCoq.Template.utils.All_Forall]
l:134 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
l:134 [in MetaCoq.Template.utils.bytestring]
l:1345 [in MetaCoq.Template.utils.All_Forall]
l:135 [in MetaCoq.Template.utils.MCList]
l:1350 [in MetaCoq.Template.utils.All_Forall]
l:1355 [in MetaCoq.Template.utils.All_Forall]
L:1358 [in MetaCoq.Template.utils.All_Forall]
l:136 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
l:136 [in MetaCoq.Template.utils.MCList]
l:136 [in MetaCoq.Erasure.ELiftSubst]
l:136 [in MetaCoq.Template.LiftSubst]
l:1366 [in MetaCoq.Template.utils.All_Forall]
l:137 [in MetaCoq.Translations.times_bool_fun]
l:137 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
l:137 [in MetaCoq.Template.Ast]
l:137 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
l:1376 [in MetaCoq.Template.utils.All_Forall]
l:138 [in MetaCoq.Template.utils.All_Forall]
l:138 [in MetaCoq.Template.utils.bytestring]
l:138 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
l:138 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
l:1383 [in MetaCoq.Template.utils.All_Forall]
l:139 [in MetaCoq.Translations.times_bool_fun]
L:139 [in MetaCoq.Translations.param_cheap_packed]
l:1390 [in MetaCoq.Template.utils.All_Forall]
l:1393 [in MetaCoq.SafeChecker.PCUICSafeReduce]
l:1397 [in MetaCoq.Template.utils.All_Forall]
l:14 [in MetaCoq.Template.Universes]
l:14 [in MetaCoq.PCUIC.TemplateToPCUIC]
l:14 [in MetaCoq.Erasure.EAstUtils]
l:140 [in MetaCoq.Template.TypingWf]
l:1401 [in MetaCoq.Template.utils.All_Forall]
l:1407 [in MetaCoq.Template.utils.All_Forall]
l:141 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
l:141 [in MetaCoq.Template.utils.MCList]
l:141 [in MetaCoq.Template.LiftSubst]
l:1415 [in MetaCoq.Template.utils.All_Forall]
l:142 [in MetaCoq.Template.utils.All_Forall]
l:142 [in MetaCoq.Template.utils.bytestring]
l:142 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
l:1420 [in MetaCoq.Template.utils.All_Forall]
l:1424 [in MetaCoq.Template.utils.All_Forall]
l:143 [in MetaCoq.Template.utils.bytestring]
l:143 [in MetaCoq.Template.Ast]
l:1435 [in MetaCoq.Template.utils.All_Forall]
l:144 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
l:1442 [in MetaCoq.Template.utils.All_Forall]
l:1447 [in MetaCoq.Template.utils.All_Forall]
l:145 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
l:1454 [in MetaCoq.Template.utils.All_Forall]
l:146 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
l:146 [in MetaCoq.SafeChecker.PCUICEqualityDec]
l:1469 [in MetaCoq.Template.utils.All_Forall]
l:147 [in MetaCoq.Template.Universes]
l:147 [in MetaCoq.Template.utils.MCList]
l:147 [in MetaCoq.Erasure.ERemoveParams]
l:148 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
l:1484 [in MetaCoq.Template.utils.All_Forall]
l:1489 [in MetaCoq.Template.utils.All_Forall]
l:149 [in MetaCoq.Template.utils.bytestring]
l:149 [in MetaCoq.Template.WcbvEval]
l:149 [in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
l:149 [in MetaCoq.Template.LiftSubst]
l:1493 [in MetaCoq.Template.utils.All_Forall]
l:1499 [in MetaCoq.Template.utils.All_Forall]
l:15 [in MetaCoq.PCUIC.Typing.PCUICInstTyp]
l:15 [in MetaCoq.PCUIC.PCUICWfUniverses]
l:15 [in MetaCoq.Template.utils.MCString]
l:15 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
l:15 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
l:1504 [in MetaCoq.Template.utils.All_Forall]
l:1508 [in MetaCoq.Template.utils.All_Forall]
l:151 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
l:151 [in MetaCoq.Template.Ast]
l:151 [in MetaCoq.PCUIC.PCUICCanonicity]
l:152 [in MetaCoq.Template.utils.All_Forall]
l:152 [in MetaCoq.PCUIC.PCUICSubstitution]
l:1521 [in MetaCoq.Template.utils.All_Forall]
l:1527 [in MetaCoq.Template.utils.All_Forall]
l:153 [in MetaCoq.Template.utils.bytestring]
l:153 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
l:1534 [in MetaCoq.Template.utils.All_Forall]
l:1542 [in MetaCoq.Template.utils.All_Forall]
l:1549 [in MetaCoq.Template.utils.All_Forall]
l:155 [in MetaCoq.Template.utils.MCList]
l:155 [in MetaCoq.Erasure.EWcbvEvalInd]
l:155 [in MetaCoq.Template.monad_utils]
l:1555 [in MetaCoq.Template.utils.All_Forall]
l:156 [in MetaCoq.PCUIC.PCUICElimination]
l:156 [in MetaCoq.Template.utils.All_Forall]
l:1564 [in MetaCoq.Template.utils.All_Forall]
l:157 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
l:1574 [in MetaCoq.Template.utils.All_Forall]
l:1579 [in MetaCoq.Template.utils.All_Forall]
l:158 [in MetaCoq.Template.Universes]
l:158 [in MetaCoq.Translations.param_cheap_packed]
l:158 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
l:158 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
l:1585 [in MetaCoq.Template.utils.All_Forall]
l:1589 [in MetaCoq.Template.utils.All_Forall]
l:159 [in MetaCoq.Examples.tauto]
l:1593 [in MetaCoq.Template.utils.All_Forall]
l:1597 [in MetaCoq.Template.utils.All_Forall]
l:16 [in MetaCoq.PCUIC.TemplateToPCUIC]
l:16 [in MetaCoq.PCUIC.PCUICConvCumInversion]
l:160 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
l:160 [in MetaCoq.Template.Ast]
l:1602 [in MetaCoq.Template.utils.All_Forall]
l:161 [in MetaCoq.Template.utils.All_Forall]
L:161 [in MetaCoq.Erasure.EArities]
l:161 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
l:1613 [in MetaCoq.Template.utils.All_Forall]
l:162 [in MetaCoq.Template.utils.MCList]
l:1621 [in MetaCoq.SafeChecker.PCUICSafeReduce]
l:1622 [in MetaCoq.Template.utils.All_Forall]
l:163 [in MetaCoq.Erasure.EDeps]
l:163 [in MetaCoq.Examples.tauto]
l:163 [in MetaCoq.Erasure.ELiftSubst]
l:163 [in MetaCoq.Template.LiftSubst]
l:1630 [in MetaCoq.Template.utils.All_Forall]
l:1638 [in MetaCoq.Template.utils.All_Forall]
l:164 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
l:164 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
l:164 [in MetaCoq.Template.AstUtils]
l:1646 [in MetaCoq.Template.utils.All_Forall]
l:165 [in MetaCoq.Erasure.EConstructorsAsBlocks]
l:1653 [in MetaCoq.Template.utils.All_Forall]
l:166 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
l:166 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
l:166 [in MetaCoq.SafeChecker.PCUICEqualityDec]
l:1661 [in MetaCoq.Template.utils.All_Forall]
l:1669 [in MetaCoq.Template.utils.All_Forall]
l:167 [in MetaCoq.Template.utils.All_Forall]
l:167 [in MetaCoq.Erasure.ELiftSubst]
l:1677 [in MetaCoq.Template.utils.All_Forall]
l:168 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
l:168 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
l:168 [in MetaCoq.Erasure.EWcbvEvalInd]
l:1685 [in MetaCoq.Template.utils.All_Forall]
l:169 [in MetaCoq.Template.utils.MCList]
l:169 [in MetaCoq.Template.monad_utils]
l:1694 [in MetaCoq.Template.utils.All_Forall]
l:17 [in MetaCoq.PCUIC.PCUICRedTypeIrrelevance]
l:17 [in MetaCoq.PCUIC.utils.PCUICSize]
l:17 [in MetaCoq.Template.AstUtils]
l:170 [in MetaCoq.Template.Ast]
l:1717 [in MetaCoq.Template.utils.All_Forall]
l:172 [in MetaCoq.Erasure.EEtaExpandedFix]
l:172 [in MetaCoq.Template.utils.All_Forall]
l:1729 [in MetaCoq.Template.utils.All_Forall]
l:1736 [in MetaCoq.SafeChecker.PCUICSafeReduce]
l:1737 [in MetaCoq.Template.utils.All_Forall]
l:174 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
l:1742 [in MetaCoq.Template.utils.All_Forall]
l:1743 [in MetaCoq.SafeChecker.PCUICSafeReduce]
l:1744 [in MetaCoq.SafeChecker.PCUICSafeReduce]
l:1746 [in MetaCoq.SafeChecker.PCUICSafeReduce]
l:175 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
l:175 [in MetaCoq.Examples.tauto]
l:175 [in MetaCoq.Template.LiftSubst]
l:1754 [in MetaCoq.Template.utils.All_Forall]
l:176 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
l:176 [in MetaCoq.PCUIC.PCUICWcbvEval]
l:1769 [in MetaCoq.Template.utils.All_Forall]
l:177 [in MetaCoq.Template.utils.All_Forall]
l:177 [in MetaCoq.Template.utils.MCList]
l:177 [in MetaCoq.Template.LiftSubst]
l:1777 [in MetaCoq.Template.utils.All_Forall]
l:178 [in MetaCoq.PCUIC.PCUICWcbvEval]
l:1784 [in MetaCoq.Template.utils.All_Forall]
l:179 [in MetaCoq.Template.BasicAst]
l:1791 [in MetaCoq.Template.utils.All_Forall]
l:1798 [in MetaCoq.Template.utils.All_Forall]
l:18 [in MetaCoq.Template.Typing]
l:18 [in MetaCoq.PCUIC.PCUICCumulProp]
l:18 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
l:180 [in MetaCoq.Template.monad_utils]
l:1803 [in MetaCoq.Template.utils.All_Forall]
l:181 [in MetaCoq.Template.utils.All_Forall]
l:1811 [in MetaCoq.Template.utils.All_Forall]
l:1818 [in MetaCoq.Template.utils.All_Forall]
l:182 [in MetaCoq.Examples.tauto]
l:1823 [in MetaCoq.Template.utils.All_Forall]
l:1828 [in MetaCoq.Template.utils.All_Forall]
l:183 [in MetaCoq.Template.common.uGraph]
l:1832 [in MetaCoq.Template.utils.All_Forall]
l:184 [in MetaCoq.PCUIC.PCUICSafeLemmata]
l:184 [in MetaCoq.Template.utils.MCList]
l:184 [in MetaCoq.Examples.tauto]
l:184 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
l:184 [in MetaCoq.Erasure.EWcbvEval]
l:1843 [in MetaCoq.Template.utils.All_Forall]
l:185 [in MetaCoq.Template.utils.All_Forall]
l:185 [in MetaCoq.Template.Environment]
l:1853 [in MetaCoq.Template.utils.All_Forall]
l:186 [in MetaCoq.PCUIC.PCUICSafeLemmata]
L:186 [in MetaCoq.PCUIC.PCUICConfluence]
l:186 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
l:1861 [in MetaCoq.Template.utils.All_Forall]
l:1868 [in MetaCoq.Template.utils.All_Forall]
l:187 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
l:1876 [in MetaCoq.Template.utils.All_Forall]
l:188 [in MetaCoq.PCUIC.PCUICSafeLemmata]
l:1883 [in MetaCoq.Template.utils.All_Forall]
l:189 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
l:189 [in MetaCoq.Template.utils.MCList]
l:1890 [in MetaCoq.Template.utils.All_Forall]
l:1893 [in MetaCoq.Template.utils.All_Forall]
l:1899 [in MetaCoq.Template.utils.All_Forall]
l:19 [in MetaCoq.Erasure.EInduction]
l:19 [in MetaCoq.Erasure.EAstUtils]
l:190 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
l:1907 [in MetaCoq.Template.utils.All_Forall]
l:191 [in MetaCoq.Erasure.Extract]
l:191 [in MetaCoq.Template.Environment]
L:191 [in MetaCoq.PCUIC.PCUICConfluence]
l:1912 [in MetaCoq.Template.utils.All_Forall]
l:1917 [in MetaCoq.Template.utils.All_Forall]
l:192 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
l:192 [in MetaCoq.Template.utils.All_Forall]
l:1922 [in MetaCoq.Template.utils.All_Forall]
l:1927 [in MetaCoq.Template.utils.All_Forall]
l:193 [in MetaCoq.Template.monad_utils]
l:1932 [in MetaCoq.Template.utils.All_Forall]
l:194 [in MetaCoq.Template.common.uGraph]
l:1941 [in MetaCoq.Template.utils.All_Forall]
l:195 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
l:195 [in MetaCoq.PCUIC.PCUICSafeLemmata]
l:195 [in MetaCoq.Template.utils.MCList]
l:195 [in MetaCoq.Template.Environment]
l:195 [in MetaCoq.Erasure.EWcbvEval]
l:1959 [in MetaCoq.Template.utils.All_Forall]
l:196 [in MetaCoq.Erasure.EInduction]
L:196 [in MetaCoq.Erasure.EArities]
l:196 [in MetaCoq.Template.common.uGraph]
L:196 [in MetaCoq.PCUIC.PCUICConfluence]
l:196 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
l:196 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
l:197 [in MetaCoq.PCUIC.PCUICSafeLemmata]
l:197 [in MetaCoq.Template.common.uGraph]
l:197 [in MetaCoq.Examples.tauto]
l:1975 [in MetaCoq.Template.utils.All_Forall]
l:198 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
l:198 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
l:198 [in MetaCoq.Template.Environment]
l:198 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
l:1980 [in MetaCoq.Template.utils.All_Forall]
l:199 [in MetaCoq.Template.Universes]
l:199 [in MetaCoq.Template.utils.All_Forall]
l:199 [in MetaCoq.Template.utils.MCList]
l:1993 [in MetaCoq.Template.utils.All_Forall]
l:2 [in MetaCoq.Erasure.EAstUtils]
l:2 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
l:20 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
l:20 [in MetaCoq.PCUIC.utils.PCUICSize]
l:20 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
l:20 [in MetaCoq.PCUIC.PCUICContexts]
l:20 [in MetaCoq.Erasure.EOptimizePropDiscr]
l:200 [in MetaCoq.Template.BasicAst]
l:2006 [in MetaCoq.Template.utils.All_Forall]
l:201 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
l:201 [in MetaCoq.Template.utils.MCList]
L:201 [in MetaCoq.PCUIC.PCUICConfluence]
l:201 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
l:2012 [in MetaCoq.Template.utils.All_Forall]
l:202 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
l:202 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
l:2020 [in MetaCoq.Template.utils.All_Forall]
l:2027 [in MetaCoq.Template.utils.All_Forall]
l:203 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
l:203 [in MetaCoq.Template.utils.All_Forall]
l:203 [in MetaCoq.Erasure.EWcbvEval]
l:2033 [in MetaCoq.Template.utils.All_Forall]
l:2039 [in MetaCoq.Template.utils.All_Forall]
l:204 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
l:204 [in MetaCoq.Template.monad_utils]
l:204 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
l:204 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
l:2043 [in MetaCoq.Template.utils.All_Forall]
l:2053 [in MetaCoq.SafeChecker.PCUICSafeConversion]
l:2054 [in MetaCoq.Template.utils.All_Forall]
l:2058 [in MetaCoq.Template.utils.All_Forall]
l:206 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
l:206 [in MetaCoq.Erasure.EConstructorsAsBlocks]
l:2063 [in MetaCoq.Template.utils.All_Forall]
l:2072 [in MetaCoq.Template.utils.All_Forall]
l:2078 [in MetaCoq.Template.utils.All_Forall]
l:208 [in MetaCoq.Template.utils.All_Forall]
l:208 [in MetaCoq.Erasure.EConstructorsAsBlocks]
l:2082 [in MetaCoq.Template.utils.All_Forall]
l:2089 [in MetaCoq.Template.utils.All_Forall]
l:209 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
l:209 [in MetaCoq.Template.utils.MCList]
l:209 [in MetaCoq.Template.Checker]
l:209 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
l:2097 [in MetaCoq.Template.utils.All_Forall]
l:21 [in MetaCoq.Template.utils.All_Forall]
l:21 [in MetaCoq.Template.utils.MCList]
l:21 [in MetaCoq.PCUIC.PCUICWfUniverses]
l:21 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
l:21 [in MetaCoq.Erasure.EInlineProjections]
l:21 [in MetaCoq.PCUIC.PCUICParallelReduction]
l:21 [in MetaCoq.Template.Induction]
l:21 [in MetaCoq.SafeChecker.PCUICTypeChecker]
l:210 [in MetaCoq.PCUIC.PCUICNormal]
l:210 [in MetaCoq.Template.Environment]
L:210 [in MetaCoq.PCUIC.PCUICConfluence]
l:2104 [in MetaCoq.Template.utils.All_Forall]
l:211 [in MetaCoq.Template.Typing]
l:2111 [in MetaCoq.Template.utils.All_Forall]
l:2117 [in MetaCoq.Template.utils.All_Forall]
l:212 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
l:212 [in MetaCoq.Template.common.uGraph]
l:2121 [in MetaCoq.Template.utils.All_Forall]
l:213 [in MetaCoq.Erasure.ErasureFunction]
l:213 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
l:2139 [in MetaCoq.Template.utils.All_Forall]
l:214 [in MetaCoq.PCUIC.PCUICContextConversion]
L:215 [in MetaCoq.PCUIC.PCUICConfluence]
l:2150 [in MetaCoq.Template.utils.All_Forall]
l:2159 [in MetaCoq.Template.utils.All_Forall]
l:216 [in MetaCoq.Erasure.EInduction]
l:216 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
l:2167 [in MetaCoq.Template.utils.All_Forall]
l:217 [in MetaCoq.Template.utils.MCList]
l:217 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
l:2175 [in MetaCoq.Template.utils.All_Forall]
l:2184 [in MetaCoq.Template.utils.All_Forall]
l:219 [in MetaCoq.Template.utils.All_Forall]
l:219 [in MetaCoq.SafeChecker.PCUICEqualityDec]
l:2196 [in MetaCoq.Template.utils.All_Forall]
l:22 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
l:22 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
l:22 [in MetaCoq.PCUIC.PCUICConfluence]
l:22 [in MetaCoq.Erasure.EAstUtils]
l:220 [in MetaCoq.Template.common.uGraph]
l:2203 [in MetaCoq.Template.utils.All_Forall]
l:221 [in MetaCoq.Template.common.uGraph]
l:222 [in MetaCoq.Template.utils.MCList]
l:222 [in MetaCoq.Template.Checker]
l:222 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
l:223 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
l:223 [in MetaCoq.Template.TypingWf]
l:2230 [in MetaCoq.Template.utils.All_Forall]
l:224 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
l:224 [in MetaCoq.Template.utils.MCList]
l:2244 [in MetaCoq.Template.utils.All_Forall]
l:225 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
l:227 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
l:228 [in MetaCoq.Template.utils.MCList]
l:228 [in MetaCoq.PCUIC.Syntax.PCUICCases]
l:228 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
l:228 [in MetaCoq.Template.Environment]
l:229 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
l:230 [in MetaCoq.Template.utils.All_Forall]
l:232 [in MetaCoq.Template.utils.MCList]
l:233 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
l:233 [in MetaCoq.Template.common.uGraph]
l:234 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
l:234 [in MetaCoq.Template.Environment]
l:235 [in MetaCoq.PCUIC.PCUICSafeLemmata]
l:235 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
l:235 [in MetaCoq.PCUIC.Syntax.PCUICCases]
l:235 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
l:236 [in MetaCoq.Template.utils.MCList]
l:236 [in MetaCoq.Template.Environment]
l:2363 [in MetaCoq.SafeChecker.PCUICSafeConversion]
l:237 [in MetaCoq.PCUIC.PCUICInductiveInversion]
l:238 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
l:238 [in MetaCoq.Template.common.uGraph]
l:239 [in MetaCoq.Template.utils.MCList]
L:239 [in MetaCoq.Erasure.EWcbvEval]
l:24 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
l:24 [in MetaCoq.Erasure.EArities]
l:24 [in MetaCoq.Template.AstUtils]
l:240 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
l:241 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
l:241 [in MetaCoq.Template.utils.All_Forall]
l:241 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
l:241 [in MetaCoq.PCUIC.PCUICAst]
l:242 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
l:242 [in MetaCoq.Template.common.uGraph]
l:242 [in MetaCoq.Template.utils.wGraph]
l:242 [in MetaCoq.SafeChecker.PCUICEqualityDec]
l:243 [in MetaCoq.Template.common.uGraph]
l:244 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
L:244 [in MetaCoq.PCUIC.PCUICConfluence]
l:2447 [in MetaCoq.Template.utils.All_Forall]
l:245 [in MetaCoq.Template.Universes]
l:2456 [in MetaCoq.Template.utils.All_Forall]
l:246 [in MetaCoq.PCUIC.PCUICSubstitution]
l:246 [in MetaCoq.Template.TermEquality]
l:247 [in MetaCoq.Template.utils.MCList]
l:247 [in MetaCoq.PCUIC.PCUICInductiveInversion]
l:247 [in MetaCoq.Template.utils.wGraph]
l:2475 [in MetaCoq.Template.utils.All_Forall]
l:248 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
l:248 [in MetaCoq.PCUIC.Syntax.PCUICCases]
l:2483 [in MetaCoq.Template.utils.All_Forall]
l:249 [in MetaCoq.Template.utils.All_Forall]
L:249 [in MetaCoq.PCUIC.PCUICConfluence]
l:2496 [in MetaCoq.Template.utils.All_Forall]
l:25 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
l:25 [in MetaCoq.Erasure.Extract]
l:25 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
l:251 [in MetaCoq.Template.Typing]
l:2512 [in MetaCoq.Template.utils.All_Forall]
l:252 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
l:252 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
l:253 [in MetaCoq.Template.TermEquality]
L:254 [in MetaCoq.PCUIC.PCUICConfluence]
l:254 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
l:2546 [in MetaCoq.Template.utils.All_Forall]
l:255 [in MetaCoq.Template.utils.MCList]
l:2557 [in MetaCoq.Template.utils.All_Forall]
l:257 [in MetaCoq.Template.utils.All_Forall]
l:257 [in MetaCoq.SafeChecker.PCUICEqualityDec]
l:2571 [in MetaCoq.Template.utils.All_Forall]
l:258 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
l:2584 [in MetaCoq.Template.utils.All_Forall]
l:259 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
L:259 [in MetaCoq.PCUIC.PCUICConfluence]
l:259 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
l:2595 [in MetaCoq.Template.utils.All_Forall]
l:26 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
l:26 [in MetaCoq.Template.common.uGraph]
l:26 [in MetaCoq.Erasure.EOptimizePropDiscr]
l:261 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
l:262 [in MetaCoq.Template.Universes]
l:262 [in MetaCoq.Template.utils.MCList]
l:263 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
l:265 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
l:265 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
l:265 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
l:265 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
l:265 [in MetaCoq.Template.TypingWf]
l:266 [in MetaCoq.Template.utils.All_Forall]
l:267 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
L:268 [in MetaCoq.PCUIC.PCUICConfluence]
l:268 [in MetaCoq.SafeChecker.PCUICSafeChecker]
l:269 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
l:269 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
L:27 [in MetaCoq.Erasure.ErasureProperties]
l:27 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
l:270 [in MetaCoq.Template.utils.MCList]
L:272 [in MetaCoq.PCUIC.PCUICProgress]
l:272 [in MetaCoq.Template.common.uGraph]
l:273 [in MetaCoq.Template.common.uGraph]
l:273 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
L:273 [in MetaCoq.PCUIC.PCUICConfluence]
l:274 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
l:275 [in MetaCoq.Template.common.uGraph]
l:275 [in MetaCoq.Template.WcbvEval]
l:276 [in MetaCoq.Template.utils.All_Forall]
l:276 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
l:276 [in MetaCoq.SafeChecker.PCUICEqualityDec]
l:277 [in MetaCoq.Template.WcbvEval]
l:278 [in MetaCoq.Template.EtaExpand]
l:278 [in MetaCoq.Template.utils.MCList]
l:279 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
l:28 [in MetaCoq.Erasure.EArities]
l:28 [in MetaCoq.Template.utils.MCList]
l:28 [in MetaCoq.Template.common.uGraph]
l:28 [in MetaCoq.Erasure.EAstUtils]
l:280 [in MetaCoq.Template.Universes]
l:280 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
l:280 [in MetaCoq.Template.common.uGraph]
l:281 [in MetaCoq.SafeChecker.PCUICEqualityDec]
l:282 [in MetaCoq.Template.utils.MCList]
l:282 [in MetaCoq.Template.common.uGraph]
l:283 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
l:283 [in MetaCoq.Template.WcbvEval]
l:283 [in MetaCoq.Erasure.EWcbvEval]
l:284 [in MetaCoq.Template.Universes]
l:284 [in MetaCoq.Template.common.uGraph]
l:285 [in MetaCoq.PCUIC.PCUICWcbvEval]
l:286 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
l:286 [in MetaCoq.Template.utils.All_Forall]
L:286 [in MetaCoq.Template.common.uGraph]
l:286 [in MetaCoq.Template.WcbvEval]
l:287 [in MetaCoq.Template.Ast]
l:287 [in MetaCoq.PCUIC.PCUICCumulProp]
l:287 [in MetaCoq.Template.common.uGraph]
l:287 [in MetaCoq.Erasure.ERemoveParams]
l:288 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
l:288 [in MetaCoq.SafeChecker.PCUICSafeChecker]
l:289 [in MetaCoq.Erasure.ERemoveParams]
l:29 [in MetaCoq.PCUIC.Syntax.PCUICViews]
l:29 [in MetaCoq.Template.Normal]
l:29 [in MetaCoq.PCUIC.PCUICParallelReduction]
l:29 [in MetaCoq.Erasure.EEtaExpanded]
l:29 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
l:29 [in MetaCoq.Template.AstUtils]
l:290 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
l:290 [in MetaCoq.Template.utils.MCList]
l:290 [in MetaCoq.PCUIC.PCUICParallelReduction]
L:290 [in MetaCoq.Template.common.uGraph]
l:290 [in MetaCoq.Template.WcbvEval]
l:291 [in MetaCoq.Template.common.uGraph]
l:291 [in MetaCoq.Erasure.ERemoveParams]
l:291 [in MetaCoq.PCUIC.PCUICReduction]
l:292 [in MetaCoq.PCUIC.PCUICSafeLemmata]
l:292 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
l:293 [in MetaCoq.Template.utils.All_Forall]
l:293 [in MetaCoq.Template.common.uGraph]
l:293 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
l:293 [in MetaCoq.Erasure.ERemoveParams]
l:293 [in MetaCoq.SafeChecker.PCUICSafeChecker]
l:293 [in MetaCoq.SafeChecker.PCUICEqualityDec]
l:295 [in MetaCoq.PCUIC.PCUICSubstitution]
l:295 [in MetaCoq.Erasure.ERemoveParams]
l:296 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
l:296 [in MetaCoq.Template.utils.All_Forall]
l:296 [in MetaCoq.Template.utils.MCList]
l:296 [in MetaCoq.Template.common.uGraph]
l:297 [in MetaCoq.Erasure.ERemoveParams]
l:297 [in MetaCoq.SafeChecker.PCUICEqualityDec]
l:298 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
l:299 [in MetaCoq.Template.utils.All_Forall]
l:299 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
l:3 [in MetaCoq.PCUIC.utils.PCUICOnOne]
l:3 [in MetaCoq.Template.utils.wGraph]
l:3 [in MetaCoq.SafeChecker.PCUICTypeChecker]
l:30 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
l:30 [in MetaCoq.Template.utils.MCList]
l:30 [in MetaCoq.Template.common.uGraph]
l:30 [in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
l:30 [in MetaCoq.Erasure.EAstUtils]
l:30 [in MetaCoq.Erasure.ECSubst]
l:300 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
l:300 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
l:300 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
l:301 [in MetaCoq.Template.utils.MCList]
l:301 [in MetaCoq.Template.common.uGraph]
l:302 [in MetaCoq.Template.Universes]
l:302 [in MetaCoq.Template.utils.All_Forall]
l:304 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
l:304 [in MetaCoq.SafeChecker.PCUICEqualityDec]
l:305 [in MetaCoq.Template.utils.All_Forall]
l:305 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
l:306 [in MetaCoq.Template.common.uGraph]
l:307 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
l:308 [in MetaCoq.Erasure.EEtaExpandedFix]
l:309 [in MetaCoq.Template.utils.All_Forall]
l:309 [in MetaCoq.Template.utils.MCList]
l:309 [in MetaCoq.Template.common.uGraph]
l:309 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
l:309 [in MetaCoq.Erasure.ERemoveParams]
l:309 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
l:31 [in MetaCoq.Template.utils.All_Forall]
L:31 [in MetaCoq.Erasure.EArities]
l:31 [in MetaCoq.Template.TemplateMonad.Core]
l:31 [in MetaCoq.Erasure.EWellformed]
l:31 [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
l:31 [in MetaCoq.PCUIC.PCUICConfluence]
l:311 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
l:311 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
l:311 [in MetaCoq.Erasure.ERemoveParams]
l:311 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
l:312 [in MetaCoq.Template.common.uGraph]
l:313 [in MetaCoq.Template.utils.All_Forall]
l:313 [in MetaCoq.Erasure.ERemoveParams]
l:314 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
l:315 [in MetaCoq.Template.utils.MCList]
l:315 [in MetaCoq.PCUIC.PCUICSR]
l:315 [in MetaCoq.SafeChecker.PCUICSafeChecker]
l:317 [in MetaCoq.Template.utils.All_Forall]
l:317 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
l:317 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
l:317 [in MetaCoq.Erasure.ERemoveParams]
l:317 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
l:319 [in MetaCoq.Template.WcbvEval]
l:32 [in MetaCoq.PCUIC.PCUICInversion]
l:32 [in MetaCoq.Erasure.EOptimizePropDiscr]
l:32 [in MetaCoq.Template.AstUtils]
l:32 [in MetaCoq.Template.Induction]
l:320 [in MetaCoq.Template.utils.All_Forall]
l:320 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
l:320 [in MetaCoq.SafeChecker.PCUICSafeChecker]
l:321 [in MetaCoq.Erasure.ERemoveParams]
l:322 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
l:322 [in MetaCoq.Template.utils.MCList]
l:323 [in MetaCoq.Erasure.EEtaExpandedFix]
l:324 [in MetaCoq.Template.Universes]
l:324 [in MetaCoq.Erasure.EWcbvEval]
l:325 [in MetaCoq.Erasure.ERemoveParams]
l:326 [in MetaCoq.Template.Ast]
l:326 [in MetaCoq.Erasure.EWcbvEval]
l:327 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
l:327 [in MetaCoq.Template.Checker]
l:328 [in MetaCoq.Template.utils.All_Forall]
l:329 [in MetaCoq.Template.Ast]
l:33 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
l:330 [in MetaCoq.Template.utils.MCList]
l:331 [in MetaCoq.Template.TypingWf]
l:331 [in MetaCoq.SafeChecker.PCUICEqualityDec]
l:334 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
l:334 [in MetaCoq.Template.utils.All_Forall]
l:336 [in MetaCoq.Template.utils.MCList]
l:34 [in MetaCoq.Template.Universes]
l:34 [in MetaCoq.Erasure.ECSubst]
l:34 [in MetaCoq.Template.LiftSubst]
l:341 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
l:341 [in MetaCoq.Template.TypingWf]
l:342 [in MetaCoq.Template.utils.All_Forall]
l:343 [in MetaCoq.Template.utils.MCList]
l:343 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
l:345 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
l:345 [in MetaCoq.PCUIC.PCUICConversion]
l:348 [in MetaCoq.Template.TypingWf]
l:349 [in MetaCoq.Template.utils.All_Forall]
l:349 [in MetaCoq.PCUIC.PCUICSubstitution]
l:35 [in MetaCoq.PCUIC.Syntax.PCUICViews]
l:35 [in MetaCoq.PCUIC.PCUICWcbvEval]
L:35 [in MetaCoq.Erasure.ErasureProperties]
l:35 [in MetaCoq.PCUIC.PCUICCanonicity]
l:35 [in MetaCoq.Template.monad_utils]
l:35 [in MetaCoq.Erasure.EAstUtils]
l:35 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
l:35 [in MetaCoq.Template.AstUtils]
l:351 [in MetaCoq.Template.utils.MCList]
l:351 [in MetaCoq.PCUIC.PCUICWcbvEval]
l:353 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
l:353 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
l:354 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
l:355 [in MetaCoq.PCUIC.PCUICConversion]
l:356 [in MetaCoq.Template.common.uGraph]
l:357 [in MetaCoq.Template.utils.All_Forall]
l:357 [in MetaCoq.Template.utils.MCList]
l:357 [in MetaCoq.PCUIC.PCUICSubstitution]
l:357 [in MetaCoq.SafeChecker.PCUICEqualityDec]
l:358 [in MetaCoq.Erasure.EWcbvEval]
l:36 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
l:36 [in MetaCoq.Erasure.Prelim]
l:360 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
l:360 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
l:361 [in MetaCoq.PCUIC.PCUICConversion]
l:361 [in MetaCoq.Erasure.EWcbvEval]
l:362 [in MetaCoq.Template.utils.All_Forall]
l:363 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
l:364 [in MetaCoq.Template.utils.MCList]
l:364 [in MetaCoq.PCUIC.PCUICNormal]
l:364 [in MetaCoq.Template.common.uGraph]
l:365 [in MetaCoq.PCUIC.PCUICSubstitution]
l:369 [in MetaCoq.PCUIC.PCUICConversion]
l:370 [in MetaCoq.Template.utils.MCList]
l:373 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
l:373 [in MetaCoq.SafeChecker.PCUICEqualityDec]
l:374 [in MetaCoq.Template.EtaExpand]
l:375 [in MetaCoq.Template.utils.MCList]
l:375 [in MetaCoq.SafeChecker.PCUICSafeChecker]
l:376 [in MetaCoq.Template.utils.All_Forall]
l:376 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
l:376 [in MetaCoq.PCUIC.PCUICConversion]
l:378 [in MetaCoq.SafeChecker.PCUICEqualityDec]
l:379 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
l:379 [in MetaCoq.PCUIC.PCUICConversion]
l:38 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
l:38 [in MetaCoq.PCUIC.Conversion.PCUICOnFreeVarsConv]
l:38 [in MetaCoq.Erasure.ESpineView]
L:38 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
l:38 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
l:38 [in MetaCoq.Erasure.ECSubst]
l:380 [in MetaCoq.Template.utils.MCList]
l:381 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
l:382 [in MetaCoq.Template.EtaExpand]
l:383 [in MetaCoq.SafeChecker.PCUICEqualityDec]
l:384 [in MetaCoq.Template.utils.MCList]
l:387 [in MetaCoq.Template.EtaExpand]
l:388 [in MetaCoq.Template.utils.All_Forall]
l:388 [in MetaCoq.SafeChecker.PCUICSafeChecker]
l:39 [in MetaCoq.SafeChecker.PCUICSafeChecker]
l:39 [in MetaCoq.Erasure.Prelim]
l:390 [in MetaCoq.Template.EtaExpand]
l:390 [in MetaCoq.Template.utils.MCList]
l:391 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
L:391 [in MetaCoq.PCUIC.PCUICConfluence]
l:391 [in MetaCoq.PCUIC.PCUICConversion]
l:393 [in MetaCoq.Template.utils.MCList]
l:398 [in MetaCoq.Template.utils.All_Forall]
l:398 [in MetaCoq.Template.Typing]
l:4 [in MetaCoq.Template.utils.MCList]
l:4 [in MetaCoq.Template.TemplateCheckWf]
l:4 [in MetaCoq.PCUIC.PCUICInductives]
l:4 [in MetaCoq.Template.utils.MCString]
l:4 [in MetaCoq.PCUIC.utils.PCUICSize]
l:4 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
l:40 [in MetaCoq.Template.utils.MCList]
l:40 [in MetaCoq.PCUIC.Syntax.PCUICViews]
L:40 [in MetaCoq.Erasure.ErasureProperties]
l:40 [in MetaCoq.Erasure.ESpineView]
l:40 [in MetaCoq.Examples.tauto]
l:40 [in MetaCoq.PCUIC.PCUICConfluence]
l:40 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
l:40 [in MetaCoq.Template.AstUtils]
L:400 [in MetaCoq.PCUIC.PCUICConfluence]
l:401 [in MetaCoq.Template.utils.MCList]
l:401 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
l:401 [in MetaCoq.PCUIC.PCUICConversion]
l:401 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
l:404 [in MetaCoq.PCUIC.PCUICReduction]
l:405 [in MetaCoq.Erasure.EEtaExpandedFix]
l:405 [in MetaCoq.Template.utils.MCList]
l:405 [in MetaCoq.PCUIC.PCUICReduction]
l:406 [in MetaCoq.Template.utils.All_Forall]
l:407 [in MetaCoq.Template.utils.MCList]
l:408 [in MetaCoq.Template.common.uGraph]
l:41 [in MetaCoq.PCUIC.PCUICParallelReduction]
l:41 [in MetaCoq.SafeChecker.PCUICSafeChecker]
l:411 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
l:411 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
L:412 [in MetaCoq.PCUIC.PCUICConfluence]
l:415 [in MetaCoq.Template.utils.All_Forall]
l:417 [in MetaCoq.Template.utils.MCList]
l:417 [in MetaCoq.PCUIC.PCUICNormal]
l:419 [in MetaCoq.Template.utils.MCList]
l:42 [in MetaCoq.Template.utils.All_Forall]
l:42 [in MetaCoq.Erasure.EGenericMapEnv]
l:421 [in MetaCoq.Template.utils.MCList]
L:421 [in MetaCoq.PCUIC.PCUICConfluence]
l:423 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
l:425 [in MetaCoq.Template.utils.All_Forall]
l:427 [in MetaCoq.PCUIC.PCUICEquality]
l:427 [in MetaCoq.Template.utils.wGraph]
l:429 [in MetaCoq.Template.utils.MCList]
l:429 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
l:43 [in MetaCoq.Erasure.EInduction]
l:43 [in MetaCoq.Template.utils.MCOption]
l:43 [in MetaCoq.PCUIC.PCUICCanonicity]
l:43 [in MetaCoq.Template.AstUtils]
l:430 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
l:432 [in MetaCoq.Template.utils.All_Forall]
l:432 [in MetaCoq.Template.utils.MCList]
l:432 [in MetaCoq.PCUIC.PCUICInductiveInversion]
l:432 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
l:434 [in MetaCoq.PCUIC.PCUICAst]
l:437 [in MetaCoq.Template.common.uGraph]
l:437 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
l:438 [in MetaCoq.Template.utils.All_Forall]
l:438 [in MetaCoq.PCUIC.PCUICAst]
l:439 [in MetaCoq.Template.utils.MCList]
l:439 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
l:44 [in MetaCoq.Template.WcbvEval]
L:44 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
l:44 [in MetaCoq.Erasure.EAstUtils]
l:44 [in MetaCoq.Template.Induction]
l:442 [in MetaCoq.Template.utils.All_Forall]
l:442 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
l:443 [in MetaCoq.PCUIC.PCUICAst]
l:444 [in MetaCoq.Template.utils.MCList]
l:444 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
l:445 [in MetaCoq.Template.utils.All_Forall]
l:445 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
l:446 [in MetaCoq.Template.utils.MCList]
l:448 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
l:449 [in MetaCoq.Template.utils.All_Forall]
l:449 [in MetaCoq.Template.utils.MCList]
l:449 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
l:45 [in MetaCoq.Erasure.EInduction]
l:45 [in MetaCoq.PCUIC.Syntax.PCUICViews]
l:45 [in MetaCoq.Template.monad_utils]
l:45 [in MetaCoq.Template.AstUtils]
l:452 [in MetaCoq.Template.utils.MCList]
l:452 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
l:453 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
l:454 [in MetaCoq.Template.utils.All_Forall]
l:454 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
l:454 [in MetaCoq.PCUIC.PCUICAst]
l:455 [in MetaCoq.Template.utils.MCList]
l:457 [in MetaCoq.Template.utils.wGraph]
l:459 [in MetaCoq.Template.utils.MCList]
l:459 [in MetaCoq.Template.utils.wGraph]
l:46 [in MetaCoq.Template.utils.bytestring]
l:46 [in MetaCoq.PCUIC.PCUICNormal]
l:46 [in MetaCoq.Examples.tauto]
l:46 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
l:46 [in MetaCoq.Template.TypingWf]
l:46 [in MetaCoq.Erasure.Prelim]
l:461 [in MetaCoq.PCUIC.PCUICAst]
l:462 [in MetaCoq.Template.utils.All_Forall]
l:462 [in MetaCoq.PCUIC.PCUICEquality]
L:463 [in MetaCoq.PCUIC.PCUICConfluence]
l:465 [in MetaCoq.Template.utils.MCList]
l:465 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
l:468 [in MetaCoq.Template.utils.All_Forall]
l:468 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
l:469 [in MetaCoq.Template.utils.wGraph]
l:47 [in MetaCoq.Translations.translation_utils]
l:47 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
l:470 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
l:471 [in MetaCoq.Template.Universes]
l:471 [in MetaCoq.Template.utils.MCList]
l:471 [in MetaCoq.Template.EnvironmentTyping]
l:471 [in MetaCoq.PCUIC.PCUICSR]
l:472 [in MetaCoq.Template.utils.All_Forall]
l:472 [in MetaCoq.Erasure.ErasureFunction]
L:472 [in MetaCoq.PCUIC.PCUICConfluence]
l:473 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
l:474 [in MetaCoq.Template.Universes]
l:474 [in MetaCoq.Erasure.EEtaExpandedFix]
l:475 [in MetaCoq.Template.utils.MCList]
l:475 [in MetaCoq.PCUIC.PCUICEquality]
l:476 [in MetaCoq.Template.utils.All_Forall]
l:477 [in MetaCoq.Erasure.ErasureFunction]
l:478 [in MetaCoq.Template.utils.MCList]
l:478 [in MetaCoq.Template.EnvironmentTyping]
l:478 [in MetaCoq.Template.common.uGraph]
l:478 [in MetaCoq.Template.utils.wGraph]
l:478 [in MetaCoq.PCUIC.PCUICReduction]
l:479 [in MetaCoq.Template.utils.wGraph]
l:48 [in MetaCoq.Template.utils.All_Forall]
l:48 [in MetaCoq.Template.utils.MCOption]
l:48 [in MetaCoq.Erasure.EAstUtils]
l:48 [in MetaCoq.Template.LiftSubst]
l:48 [in MetaCoq.Erasure.Prelim]
l:480 [in MetaCoq.Erasure.EEtaExpandedFix]
l:480 [in MetaCoq.Template.utils.MCList]
l:480 [in MetaCoq.Template.common.uGraph]
l:481 [in MetaCoq.Erasure.ErasureFunction]
l:481 [in MetaCoq.PCUIC.PCUICReduction]
l:482 [in MetaCoq.PCUIC.PCUICInductiveInversion]
l:482 [in MetaCoq.Template.common.uGraph]
l:482 [in MetaCoq.PCUIC.PCUICEquality]
l:483 [in MetaCoq.Erasure.EEtaExpandedFix]
l:483 [in MetaCoq.Template.utils.All_Forall]
l:483 [in MetaCoq.Template.utils.MCList]
L:484 [in MetaCoq.PCUIC.PCUICConfluence]
l:485 [in MetaCoq.Erasure.ErasureFunction]
l:485 [in MetaCoq.SafeChecker.PCUICSafeChecker]
l:486 [in MetaCoq.Erasure.EEtaExpandedFix]
l:487 [in MetaCoq.Template.utils.MCList]
l:488 [in MetaCoq.Template.utils.MCList]
l:489 [in MetaCoq.Template.Universes]
l:489 [in MetaCoq.Template.utils.All_Forall]
l:49 [in MetaCoq.PCUIC.PCUICWfUniverses]
l:49 [in MetaCoq.Erasure.ESpineView]
l:49 [in MetaCoq.PCUIC.PCUICConfluence]
l:49 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
l:49 [in MetaCoq.Template.AstUtils]
l:491 [in MetaCoq.PCUIC.PCUICInductiveInversion]
l:492 [in MetaCoq.Template.utils.MCList]
l:493 [in MetaCoq.Template.utils.MCList]
L:493 [in MetaCoq.PCUIC.PCUICConfluence]
l:494 [in MetaCoq.PCUIC.PCUICInductiveInversion]
l:495 [in MetaCoq.Template.utils.MCList]
l:495 [in MetaCoq.PCUIC.PCUICParallelReduction]
l:495 [in MetaCoq.Erasure.ErasureFunction]
l:496 [in MetaCoq.Template.utils.All_Forall]
l:499 [in MetaCoq.Template.utils.MCList]
l:499 [in MetaCoq.Template.common.uGraph]
l:5 [in MetaCoq.Erasure.EInduction]
l:5 [in MetaCoq.Template.utils.MCString]
l:5 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
l:5 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
l:5 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
l:5 [in MetaCoq.Template.Induction]
l:50 [in MetaCoq.Erasure.EArities]
l:50 [in MetaCoq.Template.utils.MCList]
l:50 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
l:50 [in MetaCoq.PCUIC.PCUICSR]
l:50 [in MetaCoq.Erasure.EAstUtils]
l:501 [in MetaCoq.Template.utils.All_Forall]
l:501 [in MetaCoq.Erasure.ErasureFunction]
l:503 [in MetaCoq.Template.EnvironmentTyping]
l:505 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
l:505 [in MetaCoq.Template.common.uGraph]
l:506 [in MetaCoq.Template.utils.All_Forall]
l:506 [in MetaCoq.Template.EnvironmentTyping]
l:506 [in MetaCoq.Erasure.ErasureFunction]
l:507 [in MetaCoq.Template.utils.MCList]
l:507 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
l:51 [in MetaCoq.Template.monad_utils]
l:51 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
l:511 [in MetaCoq.PCUIC.PCUICInductiveInversion]
l:511 [in MetaCoq.PCUIC.PCUICEquality]
l:511 [in MetaCoq.Erasure.ErasureFunction]
l:512 [in MetaCoq.Template.utils.All_Forall]
l:512 [in MetaCoq.Template.utils.MCList]
l:514 [in MetaCoq.Template.utils.MCList]
l:517 [in MetaCoq.Template.utils.MCList]
l:518 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
l:52 [in MetaCoq.Erasure.EInduction]
l:52 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
l:52 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
l:52 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
l:520 [in MetaCoq.Template.utils.All_Forall]
l:520 [in MetaCoq.PCUIC.PCUICEquality]
l:521 [in MetaCoq.Template.utils.MCList]
l:522 [in MetaCoq.Erasure.ErasureFunction]
l:526 [in MetaCoq.Template.utils.All_Forall]
l:527 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
l:528 [in MetaCoq.Erasure.ErasureFunction]
l:53 [in MetaCoq.Template.Universes]
l:53 [in MetaCoq.PCUIC.PCUICWfUniverses]
l:53 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
l:53 [in MetaCoq.PCUIC.PCUICGlobalEnv]
l:53 [in MetaCoq.Template.TypingWf]
l:53 [in MetaCoq.Template.LiftSubst]
l:530 [in MetaCoq.Template.utils.MCList]
l:531 [in MetaCoq.Template.utils.All_Forall]
l:533 [in MetaCoq.Template.utils.MCList]
l:533 [in MetaCoq.Erasure.ErasureFunction]
l:534 [in MetaCoq.PCUIC.PCUICInductiveInversion]
l:535 [in MetaCoq.PCUIC.PCUICEquality]
l:536 [in MetaCoq.Template.utils.All_Forall]
l:536 [in MetaCoq.Template.utils.MCList]
l:538 [in MetaCoq.Erasure.ErasureFunction]
l:539 [in MetaCoq.PCUIC.PCUICInductiveInversion]
l:539 [in MetaCoq.PCUIC.PCUICAst]
l:54 [in MetaCoq.PCUIC.PCUICWfUniverses]
l:54 [in MetaCoq.PCUIC.PCUICCumulProp]
l:54 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
l:540 [in MetaCoq.Template.utils.All_Forall]
l:543 [in MetaCoq.Template.utils.MCList]
l:543 [in MetaCoq.PCUIC.PCUICEquality]
l:543 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
l:544 [in MetaCoq.Template.utils.All_Forall]
l:549 [in MetaCoq.Template.utils.MCList]
l:549 [in MetaCoq.PCUIC.PCUICAst]
l:55 [in MetaCoq.Erasure.EInduction]
l:55 [in MetaCoq.Template.utils.All_Forall]
l:55 [in MetaCoq.PCUIC.PCUICValidity]
l:55 [in MetaCoq.Erasure.EAstUtils]
l:55 [in MetaCoq.Erasure.EOptimizePropDiscr]
l:551 [in MetaCoq.Template.utils.All_Forall]
l:552 [in MetaCoq.Template.utils.MCList]
l:553 [in MetaCoq.Erasure.EEtaExpandedFix]
l:553 [in MetaCoq.Template.common.uGraph]
l:554 [in MetaCoq.Template.utils.MCList]
l:555 [in MetaCoq.Template.utils.MCList]
l:555 [in MetaCoq.PCUIC.PCUICInductives]
l:556 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
l:557 [in MetaCoq.Template.utils.All_Forall]
l:557 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
l:558 [in MetaCoq.Template.common.uGraph]
l:56 [in MetaCoq.Template.utils.MCList]
l:56 [in MetaCoq.PCUIC.PCUICCumulProp]
l:56 [in MetaCoq.Template.WcbvEval]
l:56 [in MetaCoq.PCUIC.PCUICConfluence]
l:56 [in MetaCoq.Template.monad_utils]
l:56 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
l:56 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
l:560 [in MetaCoq.Erasure.ErasureFunction]
l:561 [in MetaCoq.Template.utils.MCList]
l:561 [in MetaCoq.PCUIC.PCUICAst]
l:562 [in MetaCoq.PCUIC.PCUICInductiveInversion]
l:563 [in MetaCoq.Template.utils.MCList]
l:563 [in MetaCoq.Template.common.uGraph]
l:564 [in MetaCoq.Template.utils.All_Forall]
l:565 [in MetaCoq.Erasure.ErasureFunction]
l:566 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
l:568 [in MetaCoq.Template.utils.MCList]
l:568 [in MetaCoq.Template.common.uGraph]
l:569 [in MetaCoq.Erasure.ErasureFunction]
l:57 [in MetaCoq.Erasure.EInduction]
l:57 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
l:570 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
l:572 [in MetaCoq.Template.utils.MCList]
l:573 [in MetaCoq.PCUIC.PCUICInductiveInversion]
l:573 [in MetaCoq.Erasure.ErasureFunction]
l:575 [in MetaCoq.Template.utils.MCList]
l:576 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
l:578 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
l:578 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
l:58 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
l:58 [in MetaCoq.Erasure.EAstUtils]
L:58 [in MetaCoq.Erasure.Prelim]
l:580 [in MetaCoq.Template.utils.All_Forall]
l:580 [in MetaCoq.Template.utils.MCList]
l:580 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
l:581 [in MetaCoq.Template.common.uGraph]
l:581 [in MetaCoq.Erasure.ErasureFunction]
l:584 [in MetaCoq.Template.utils.MCList]
l:584 [in MetaCoq.PCUIC.PCUICConversion]
l:586 [in MetaCoq.Template.utils.All_Forall]
l:586 [in MetaCoq.Template.common.uGraph]
l:586 [in MetaCoq.Erasure.ErasureFunction]
l:587 [in MetaCoq.PCUIC.PCUICInductiveInversion]
l:587 [in MetaCoq.Template.utils.wGraph]
l:589 [in MetaCoq.Template.utils.MCList]
l:589 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
l:59 [in MetaCoq.Template.utils.MCList]
l:59 [in MetaCoq.PCUIC.PCUICCasesContexts]
l:59 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
L:59 [in MetaCoq.Erasure.Prelim]
l:590 [in MetaCoq.Erasure.ErasureFunction]
l:590 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
l:591 [in MetaCoq.Template.utils.All_Forall]
l:591 [in MetaCoq.Template.common.uGraph]
l:591 [in MetaCoq.PCUIC.PCUICConversion]
l:592 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
l:594 [in MetaCoq.Template.utils.MCList]
l:594 [in MetaCoq.Erasure.ErasureFunction]
l:596 [in MetaCoq.Template.utils.All_Forall]
l:596 [in MetaCoq.Template.common.uGraph]
l:597 [in MetaCoq.Template.utils.MCList]
l:6 [in MetaCoq.Template.utils.All_Forall]
l:6 [in MetaCoq.PCUIC.Syntax.PCUICCases]
l:6 [in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
l:60 [in MetaCoq.Template.utils.MCList]
l:60 [in MetaCoq.Template.TypingWf]
l:60 [in MetaCoq.Template.Induction]
l:600 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
l:601 [in MetaCoq.Template.utils.All_Forall]
l:606 [in MetaCoq.Template.utils.MCList]
l:607 [in MetaCoq.Template.utils.All_Forall]
l:609 [in MetaCoq.PCUIC.PCUICInductiveInversion]
l:609 [in MetaCoq.Erasure.ErasureFunction]
l:612 [in MetaCoq.Template.utils.All_Forall]
l:614 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
l:614 [in MetaCoq.Erasure.ErasureFunction]
l:617 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
l:618 [in MetaCoq.Template.utils.MCList]
l:619 [in MetaCoq.Template.utils.All_Forall]
l:62 [in MetaCoq.Erasure.EInduction]
l:62 [in MetaCoq.Template.utils.All_Forall]
l:62 [in MetaCoq.Erasure.EAstUtils]
l:620 [in MetaCoq.Erasure.ErasureFunction]
l:622 [in MetaCoq.PCUIC.PCUICEquality]
l:623 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
l:625 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
l:626 [in MetaCoq.Erasure.ErasureFunction]
L:627 [in MetaCoq.Template.utils.All_Forall]
l:628 [in MetaCoq.Template.utils.All_Forall]
l:628 [in MetaCoq.Template.common.uGraph]
l:629 [in MetaCoq.Template.Typing]
l:63 [in MetaCoq.Template.Kernames]
l:63 [in MetaCoq.Template.monad_utils]
l:63 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
L:631 [in MetaCoq.Template.utils.All_Forall]
l:632 [in MetaCoq.Template.common.uGraph]
l:633 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
l:634 [in MetaCoq.Template.utils.All_Forall]
L:636 [in MetaCoq.Template.utils.All_Forall]
l:636 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
l:636 [in MetaCoq.Erasure.ErasureFunction]
l:638 [in MetaCoq.Template.utils.All_Forall]
l:64 [in MetaCoq.Template.Universes]
l:64 [in MetaCoq.Template.WfAst]
l:64 [in MetaCoq.PCUIC.PCUICConfluence]
l:64 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
l:641 [in MetaCoq.Template.utils.All_Forall]
l:641 [in MetaCoq.Template.common.uGraph]
l:641 [in MetaCoq.Erasure.ErasureFunction]
l:644 [in MetaCoq.SafeChecker.PCUICTypeChecker]
l:645 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
l:645 [in MetaCoq.SafeChecker.PCUICTypeChecker]
l:646 [in MetaCoq.SafeChecker.PCUICTypeChecker]
l:647 [in MetaCoq.Erasure.ErasureFunction]
l:647 [in MetaCoq.SafeChecker.PCUICTypeChecker]
l:65 [in MetaCoq.Template.Universes]
l:65 [in MetaCoq.PCUIC.PCUICWfUniverses]
l:65 [in MetaCoq.PCUIC.PCUICSR]
l:651 [in MetaCoq.SafeChecker.PCUICSafeConversion]
l:653 [in MetaCoq.Erasure.ErasureFunction]
l:654 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
l:659 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
l:66 [in MetaCoq.Erasure.EInduction]
l:66 [in MetaCoq.Template.utils.ReflectEq]
l:66 [in MetaCoq.PCUIC.Syntax.PCUICReflect]
l:66 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
l:66 [in MetaCoq.Template.TypingWf]
l:66 [in MetaCoq.Erasure.EOptimizePropDiscr]
l:660 [in MetaCoq.Template.Universes]
l:660 [in MetaCoq.PCUIC.PCUICSpine]
l:662 [in MetaCoq.Template.utils.MCList]
l:662 [in MetaCoq.PCUIC.PCUICSR]
l:664 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
l:667 [in MetaCoq.PCUIC.PCUICInductiveInversion]
l:668 [in MetaCoq.Template.utils.MCList]
l:669 [in MetaCoq.PCUIC.PCUICEquality]
l:669 [in MetaCoq.PCUIC.PCUICReduction]
l:67 [in MetaCoq.Template.WfAst]
l:67 [in MetaCoq.PCUIC.PCUICCasesContexts]
l:67 [in MetaCoq.Erasure.EAstUtils]
l:670 [in MetaCoq.Template.utils.All_Forall]
l:670 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
l:674 [in MetaCoq.Template.utils.MCList]
l:674 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
l:675 [in MetaCoq.PCUIC.PCUICSR]
l:675 [in MetaCoq.PCUIC.PCUICReduction]
l:677 [in MetaCoq.Template.Universes]
l:678 [in MetaCoq.Template.utils.MCList]
l:679 [in MetaCoq.Template.utils.All_Forall]
l:68 [in MetaCoq.Erasure.EInduction]
l:68 [in MetaCoq.Template.utils.MCList]
l:68 [in MetaCoq.Template.Normal]
l:68 [in MetaCoq.Template.Reflect]
l:681 [in MetaCoq.Template.Universes]
l:681 [in MetaCoq.PCUIC.PCUICReduction]
l:683 [in MetaCoq.Template.Universes]
l:684 [in MetaCoq.Template.utils.All_Forall]
l:688 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
l:689 [in MetaCoq.PCUIC.PCUICReduction]
l:69 [in MetaCoq.Template.utils.All_Forall]
l:69 [in MetaCoq.Template.utils.MCList]
l:69 [in MetaCoq.Erasure.EDeps]
l:69 [in MetaCoq.Template.utils.wGraph]
l:69 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
l:69 [in MetaCoq.Template.LiftSubst]
L:69 [in MetaCoq.Erasure.Prelim]
l:691 [in MetaCoq.Template.utils.All_Forall]
l:691 [in MetaCoq.Template.common.uGraph]
l:692 [in MetaCoq.Template.utils.MCList]
l:696 [in MetaCoq.Template.utils.MCList]
l:696 [in MetaCoq.Template.common.uGraph]
l:698 [in MetaCoq.Template.Universes]
l:698 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
l:698 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
l:7 [in MetaCoq.Template.utils.wGraph]
l:70 [in MetaCoq.Template.Universes]
l:70 [in MetaCoq.Template.utils.MCOption]
l:70 [in MetaCoq.PCUIC.PCUICConversion]
l:70 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
l:70 [in MetaCoq.Erasure.EAstUtils]
L:70 [in MetaCoq.Erasure.Prelim]
l:700 [in MetaCoq.Template.Universes]
l:700 [in MetaCoq.Template.utils.All_Forall]
l:700 [in MetaCoq.Template.utils.MCList]
l:702 [in MetaCoq.Template.utils.MCList]
l:705 [in MetaCoq.Template.utils.MCList]
l:706 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
l:71 [in MetaCoq.Template.Induction]
l:711 [in MetaCoq.Template.utils.MCList]
l:712 [in MetaCoq.Template.Universes]
l:714 [in MetaCoq.PCUIC.PCUICInductiveInversion]
l:718 [in MetaCoq.PCUIC.PCUICReduction]
l:72 [in MetaCoq.Erasure.EInduction]
l:72 [in MetaCoq.Translations.times_bool_fun]
l:72 [in MetaCoq.Template.utils.bytestring]
l:72 [in MetaCoq.Template.Reflect]
l:72 [in MetaCoq.Erasure.EAstUtils]
l:722 [in MetaCoq.Erasure.ErasureFunction]
l:726 [in MetaCoq.Template.utils.MCList]
l:726 [in MetaCoq.PCUIC.PCUICReduction]
l:728 [in MetaCoq.Erasure.ErasureFunction]
l:729 [in MetaCoq.Template.Universes]
l:73 [in MetaCoq.Template.utils.wGraph]
l:73 [in MetaCoq.Template.LiftSubst]
l:733 [in MetaCoq.Erasure.ErasureFunction]
l:737 [in MetaCoq.Template.Universes]
l:738 [in MetaCoq.Erasure.ErasureFunction]
l:738 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
l:738 [in MetaCoq.PCUIC.PCUICReduction]
l:739 [in MetaCoq.Template.utils.MCList]
l:74 [in MetaCoq.Template.WfAst]
l:741 [in MetaCoq.Template.utils.All_Forall]
l:742 [in MetaCoq.PCUIC.PCUICReduction]
l:746 [in MetaCoq.Template.Universes]
l:746 [in MetaCoq.PCUIC.PCUICReduction]
l:749 [in MetaCoq.Template.utils.All_Forall]
l:749 [in MetaCoq.Template.utils.MCList]
l:749 [in MetaCoq.Erasure.ErasureFunction]
l:75 [in MetaCoq.Translations.times_bool_fun]
l:75 [in MetaCoq.Template.utils.All_Forall]
l:75 [in MetaCoq.Template.utils.MCList]
l:750 [in MetaCoq.Template.Universes]
l:751 [in MetaCoq.PCUIC.PCUICReduction]
l:752 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
l:755 [in MetaCoq.Template.utils.All_Forall]
l:755 [in MetaCoq.Template.utils.MCList]
l:755 [in MetaCoq.Erasure.ErasureFunction]
l:756 [in MetaCoq.SafeChecker.PCUICSafeChecker]
l:756 [in MetaCoq.PCUIC.PCUICReduction]
l:76 [in MetaCoq.Template.Reflect]
l:76 [in MetaCoq.Template.utils.MCOption]
l:76 [in MetaCoq.PCUIC.PCUICConfluence]
l:760 [in MetaCoq.Template.utils.MCList]
l:760 [in MetaCoq.Erasure.ErasureFunction]
l:761 [in MetaCoq.Template.utils.All_Forall]
l:761 [in MetaCoq.PCUIC.PCUICReduction]
l:765 [in MetaCoq.Erasure.ErasureFunction]
l:765 [in MetaCoq.PCUIC.PCUICReduction]
l:766 [in MetaCoq.Template.utils.MCList]
l:767 [in MetaCoq.Template.utils.All_Forall]
l:767 [in MetaCoq.PCUIC.PCUICInductiveInversion]
l:77 [in MetaCoq.Template.Universes]
l:77 [in MetaCoq.Template.utils.MCList]
l:77 [in MetaCoq.Template.utils.wGraph]
l:77 [in MetaCoq.Template.monad_utils]
l:77 [in MetaCoq.Erasure.EAstUtils]
l:775 [in MetaCoq.Template.utils.All_Forall]
l:776 [in MetaCoq.PCUIC.PCUICReduction]
l:777 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
l:78 [in MetaCoq.Erasure.EInduction]
l:78 [in MetaCoq.PCUIC.PCUICAst]
l:78 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
l:78 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
l:780 [in MetaCoq.Template.utils.MCList]
l:782 [in MetaCoq.Template.utils.All_Forall]
l:785 [in MetaCoq.Template.utils.wGraph]
l:785 [in MetaCoq.PCUIC.PCUICReduction]
l:789 [in MetaCoq.Template.utils.wGraph]
l:79 [in MetaCoq.Template.utils.MCList]
l:79 [in MetaCoq.PCUIC.PCUICSubstitution]
l:791 [in MetaCoq.Template.utils.All_Forall]
l:791 [in MetaCoq.PCUIC.PCUICReduction]
l:792 [in MetaCoq.Template.utils.wGraph]
l:798 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
l:798 [in MetaCoq.Template.utils.wGraph]
l:8 [in MetaCoq.PCUIC.PCUICWeakeningEnv]
l:8 [in MetaCoq.PCUIC.Syntax.PCUICViews]
L:8 [in MetaCoq.PCUIC.PCUICCanonicity]
l:8 [in MetaCoq.PCUIC.utils.PCUICSize]
l:80 [in MetaCoq.Template.Universes]
l:80 [in MetaCoq.Template.utils.All_Forall]
l:80 [in MetaCoq.Erasure.Extract]
l:80 [in MetaCoq.Template.Reflect]
l:80 [in MetaCoq.Template.utils.MCOption]
L:800 [in MetaCoq.Template.utils.All_Forall]
l:801 [in MetaCoq.PCUIC.PCUICReduction]
l:802 [in MetaCoq.Template.utils.All_Forall]
l:804 [in MetaCoq.Template.utils.wGraph]
L:805 [in MetaCoq.Template.utils.All_Forall]
l:806 [in MetaCoq.PCUIC.PCUICReduction]
l:807 [in MetaCoq.Template.utils.wGraph]
l:809 [in MetaCoq.Template.utils.All_Forall]
l:81 [in MetaCoq.Template.utils.MCList]
l:81 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
l:81 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
l:81 [in MetaCoq.Erasure.EAstUtils]
L:811 [in MetaCoq.Template.utils.All_Forall]
l:811 [in MetaCoq.PCUIC.PCUICReduction]
l:812 [in MetaCoq.PCUIC.PCUICParallelReduction]
l:812 [in MetaCoq.Template.utils.wGraph]
l:814 [in MetaCoq.Template.utils.All_Forall]
l:815 [in MetaCoq.Template.utils.wGraph]
l:815 [in MetaCoq.PCUIC.PCUICConversion]
l:815 [in MetaCoq.PCUIC.PCUICReduction]
l:818 [in MetaCoq.Template.utils.All_Forall]
l:819 [in MetaCoq.Template.utils.wGraph]
l:82 [in MetaCoq.PCUIC.PCUICWeakeningEnv]
l:820 [in MetaCoq.PCUIC.PCUICInductiveInversion]
l:821 [in MetaCoq.PCUIC.PCUICReduction]
l:822 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
l:822 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
l:823 [in MetaCoq.PCUIC.PCUICReduction]
l:823 [in MetaCoq.SafeChecker.PCUICTypeChecker]
l:825 [in MetaCoq.Template.utils.MCList]
l:825 [in MetaCoq.PCUIC.PCUICReduction]
l:826 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
l:826 [in MetaCoq.PCUIC.PCUICReduction]
l:827 [in MetaCoq.PCUIC.PCUICReduction]
l:828 [in MetaCoq.PCUIC.PCUICReduction]
l:829 [in MetaCoq.Template.utils.MCList]
l:83 [in MetaCoq.Template.utils.MCList]
l:83 [in MetaCoq.PCUIC.PCUICParallelReduction]
l:83 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
l:83 [in MetaCoq.SafeChecker.PCUICSafeChecker]
l:830 [in MetaCoq.Template.utils.MCList]
l:832 [in MetaCoq.PCUIC.PCUICReduction]
l:84 [in MetaCoq.PCUIC.PCUICWeakeningEnv]
l:840 [in MetaCoq.Template.utils.MCList]
l:846 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
l:849 [in MetaCoq.PCUIC.PCUICReduction]
l:85 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
l:85 [in MetaCoq.Template.utils.All_Forall]
l:852 [in MetaCoq.Template.utils.All_Forall]
l:852 [in MetaCoq.PCUIC.PCUICReduction]
l:855 [in MetaCoq.SafeChecker.PCUICSafeChecker]
l:855 [in MetaCoq.PCUIC.PCUICReduction]
l:856 [in MetaCoq.Template.utils.MCList]
l:858 [in MetaCoq.Template.utils.MCList]
l:858 [in MetaCoq.PCUIC.PCUICReduction]
l:859 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
l:86 [in MetaCoq.PCUIC.PCUICNormal]
l:86 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
l:863 [in MetaCoq.Template.utils.All_Forall]
l:864 [in MetaCoq.PCUIC.PCUICReduction]
l:868 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
l:869 [in MetaCoq.Template.utils.All_Forall]
l:87 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
l:87 [in MetaCoq.Template.Typing]
l:872 [in MetaCoq.Template.utils.MCList]
l:872 [in MetaCoq.SafeChecker.PCUICSafeChecker]
l:877 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
l:878 [in MetaCoq.Template.utils.All_Forall]
l:878 [in MetaCoq.Template.utils.MCList]
l:88 [in MetaCoq.Template.utils.MCList]
l:88 [in MetaCoq.Erasure.ELiftSubst]
l:88 [in MetaCoq.Template.monad_utils]
l:88 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
l:884 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
l:886 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
l:887 [in MetaCoq.PCUIC.PCUICReduction]
l:888 [in MetaCoq.PCUIC.PCUICReduction]
l:889 [in MetaCoq.PCUIC.PCUICReduction]
l:89 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
l:89 [in MetaCoq.SafeChecker.PCUICEqualityDec]
l:890 [in MetaCoq.PCUIC.PCUICReduction]
l:892 [in MetaCoq.Template.utils.MCList]
l:899 [in MetaCoq.Template.utils.MCList]
l:9 [in MetaCoq.Template.WfAst]
l:9 [in MetaCoq.PCUIC.PCUICNormal]
l:9 [in MetaCoq.PCUIC.Syntax.PCUICCases]
l:9 [in MetaCoq.PCUIC.TemplateToPCUIC]
l:9 [in MetaCoq.Erasure.EAstUtils]
l:9 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
l:9 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
l:9 [in MetaCoq.Erasure.EWcbvEval]
l:90 [in MetaCoq.Template.utils.MCList]
l:90 [in MetaCoq.Template.WfAst]
l:903 [in MetaCoq.Template.utils.MCList]
l:904 [in MetaCoq.Template.utils.All_Forall]
l:907 [in MetaCoq.PCUIC.PCUICReduction]
l:908 [in MetaCoq.Template.utils.MCList]
l:91 [in MetaCoq.PCUIC.PCUICConfluence]
l:911 [in MetaCoq.Template.utils.MCList]
l:914 [in MetaCoq.Template.utils.All_Forall]
l:92 [in MetaCoq.Template.utils.MCList]
l:92 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
l:921 [in MetaCoq.PCUIC.PCUICReduction]
l:924 [in MetaCoq.Template.utils.All_Forall]
l:926 [in MetaCoq.Template.utils.MCList]
l:928 [in MetaCoq.PCUIC.PCUICReduction]
l:93 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
l:93 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
L:93 [in MetaCoq.PCUIC.PCUICNormal]
l:931 [in MetaCoq.Template.utils.All_Forall]
l:937 [in MetaCoq.Template.utils.All_Forall]
l:938 [in MetaCoq.PCUIC.PCUICTyping]
l:94 [in MetaCoq.Template.utils.MCList]
l:94 [in MetaCoq.PCUIC.Syntax.PCUICViews]
l:94 [in MetaCoq.PCUIC.PCUICAst]
l:94 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
l:944 [in MetaCoq.Template.utils.All_Forall]
l:944 [in MetaCoq.PCUIC.PCUICTyping]
l:95 [in MetaCoq.Template.Universes]
l:95 [in MetaCoq.Template.EnvironmentTyping]
l:95 [in MetaCoq.Template.monad_utils]
l:953 [in MetaCoq.Template.utils.All_Forall]
l:96 [in MetaCoq.Template.utils.MCList]
l:96 [in MetaCoq.Erasure.EInlineProjections]
l:96 [in MetaCoq.SafeChecker.PCUICEqualityDec]
l:961 [in MetaCoq.PCUIC.PCUICReduction]
l:963 [in MetaCoq.Template.utils.All_Forall]
l:97 [in MetaCoq.Template.Universes]
l:97 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
l:97 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
l:972 [in MetaCoq.Template.utils.All_Forall]
l:972 [in MetaCoq.PCUIC.PCUICTyping]
l:98 [in MetaCoq.Template.LiftSubst]
l:982 [in MetaCoq.Template.utils.All_Forall]
l:989 [in MetaCoq.Template.utils.wGraph]
l:99 [in MetaCoq.Erasure.EInduction]
l:99 [in MetaCoq.Template.utils.MCList]
L:99 [in MetaCoq.Translations.param_cheap_packed]
L:992 [in MetaCoq.Template.utils.All_Forall]
l:994 [in MetaCoq.Template.utils.All_Forall]
L:997 [in MetaCoq.Template.utils.All_Forall]
lΔ:927 [in MetaCoq.PCUIC.PCUICReduction]



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)