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)

S (binder)

scrut_ty:127 [in MetaCoq.PCUIC.PCUICInversion]
sc:793 [in MetaCoq.PCUIC.PCUICConfluence]
sep:14 [in MetaCoq.Template.utils.MCString]
sep:141 [in MetaCoq.Template.utils.bytestring]
sep:152 [in MetaCoq.Template.utils.bytestring]
sep:154 [in MetaCoq.Template.utils.bytestring]
sep:3 [in MetaCoq.Template.utils.MCString]
sep:66 [in MetaCoq.Template.utils.bytestring]
se:432 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
se:495 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
se:532 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
se:544 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
se:546 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
se:639 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
sg:100 [in MetaCoq.Examples.tauto]
sg:49 [in MetaCoq.Examples.tauto]
sg:94 [in MetaCoq.Examples.tauto]
sg:97 [in MetaCoq.Examples.tauto]
shiftn0:133 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
shift':152 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
shift':51 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
shift':62 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
shift:125 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
shift:137 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
shift:151 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
shift:164 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
shift:178 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
shift:19 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
shift:50 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
shift:61 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
shift:68 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
shift:74 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
shift:81 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
shift:84 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
shift:9 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
short:102 [in MetaCoq.PCUIC.utils.PCUICPretty]
short:106 [in MetaCoq.Template.Pretty]
short:112 [in MetaCoq.PCUIC.utils.PCUICPretty]
short:113 [in MetaCoq.Template.Pretty]
short:115 [in MetaCoq.PCUIC.utils.PCUICPretty]
short:121 [in MetaCoq.Template.Pretty]
short:127 [in MetaCoq.PCUIC.utils.PCUICPretty]
short:129 [in MetaCoq.Template.Pretty]
short:130 [in MetaCoq.PCUIC.utils.PCUICPretty]
short:134 [in MetaCoq.Template.Pretty]
short:144 [in MetaCoq.Template.Pretty]
short:148 [in MetaCoq.Template.Pretty]
short:153 [in MetaCoq.Template.Pretty]
short:156 [in MetaCoq.Template.Pretty]
short:160 [in MetaCoq.Template.Pretty]
short:163 [in MetaCoq.Template.Pretty]
short:98 [in MetaCoq.PCUIC.utils.PCUICPretty]
singleton:92 [in MetaCoq.Template.common.uGraph]
sizeA:557 [in MetaCoq.Template.utils.MCList]
sizeB:559 [in MetaCoq.Template.utils.MCList]
size:1 [in MetaCoq.PCUIC.utils.PCUICSize]
size:11 [in MetaCoq.PCUIC.utils.PCUICSize]
size:127 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
size:132 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
size:145 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
size:156 [in MetaCoq.Examples.tauto]
size:158 [in MetaCoq.Examples.tauto]
size:160 [in MetaCoq.Examples.tauto]
size:162 [in MetaCoq.Examples.tauto]
size:164 [in MetaCoq.Examples.tauto]
size:166 [in MetaCoq.Examples.tauto]
size:3 [in MetaCoq.PCUIC.utils.PCUICSize]
size:5 [in MetaCoq.PCUIC.utils.PCUICSize]
size:548 [in MetaCoq.Template.utils.MCList]
size:588 [in MetaCoq.Template.utils.MCList]
size:7 [in MetaCoq.PCUIC.utils.PCUICSize]
size:9 [in MetaCoq.PCUIC.utils.PCUICSize]
size:901 [in MetaCoq.Template.utils.MCList]
sl:50 [in MetaCoq.Examples.tauto]
sl:51 [in MetaCoq.Examples.tauto]
smaller:169 [in MetaCoq.SafeChecker.PCUICSafeReduce]
soft:42 [in MetaCoq.PCUIC.utils.PCUICPrimitive]
sorting_size:404 [in MetaCoq.Template.EnvironmentTyping]
sorting:201 [in MetaCoq.Template.EnvironmentTyping]
sorting:212 [in MetaCoq.Template.EnvironmentTyping]
sorting:252 [in MetaCoq.Template.EnvironmentTyping]
sorting:289 [in MetaCoq.Template.EnvironmentTyping]
sorting:361 [in MetaCoq.Template.EnvironmentTyping]
sorting:394 [in MetaCoq.Template.EnvironmentTyping]
sorts:147 [in MetaCoq.PCUIC.PCUICWfUniverses]
sproperty:261 [in MetaCoq.Template.EnvironmentTyping]
sproperty:295 [in MetaCoq.Template.EnvironmentTyping]
sp':595 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
sP:24 [in MetaCoq.PCUIC.Conversion.PCUICOnFreeVarsConv]
sP:30 [in MetaCoq.PCUIC.Conversion.PCUICOnFreeVarsConv]
sP:51 [in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
sp:562 [in MetaCoq.PCUIC.PCUICSpine]
sp:578 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
sP:59 [in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
sp:593 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
sp:617 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
sp:625 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
ssize:370 [in MetaCoq.Template.EnvironmentTyping]
ss':352 [in MetaCoq.Template.utils.wGraph]
stack:435 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
stack:98 [in MetaCoq.Template.Checker]
start:480 [in MetaCoq.PCUIC.PCUICInductiveInversion]
start:49 [in MetaCoq.Template.utils.bytestring]
sub:228 [in MetaCoq.PCUIC.PCUICSpine]
sub:234 [in MetaCoq.PCUIC.PCUICSpine]
sub:274 [in MetaCoq.PCUIC.PCUICSpine]
sub:283 [in MetaCoq.PCUIC.PCUICSpine]
sub:312 [in MetaCoq.PCUIC.PCUICSpine]
sub:570 [in MetaCoq.PCUIC.PCUICSubstitution]
sub:580 [in MetaCoq.PCUIC.PCUICSubstitution]
sub:604 [in MetaCoq.PCUIC.PCUICInductives]
suffix:1444 [in MetaCoq.Erasure.ErasureFunction]
suffix:1446 [in MetaCoq.Erasure.ErasureFunction]
suffix:1450 [in MetaCoq.Erasure.ErasureFunction]
suffix:1452 [in MetaCoq.Erasure.ErasureFunction]
symbol:12 [in MetaCoq.Translations.param_original]
symbol:26 [in MetaCoq.Translations.param_binary]
sym:109 [in MetaCoq.PCUIC.utils.PCUICUtils]
sym:559 [in MetaCoq.PCUIC.PCUICConfluence]
sym:67 [in MetaCoq.PCUIC.utils.PCUICUtils]
s'':130 [in MetaCoq.Template.utils.wGraph]
s'':146 [in MetaCoq.Template.utils.wGraph]
s'':152 [in MetaCoq.Template.utils.wGraph]
s'':156 [in MetaCoq.Template.utils.wGraph]
s'':417 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
s'0:840 [in MetaCoq.PCUIC.PCUICParallelReduction]
s'0:929 [in MetaCoq.PCUIC.PCUICConversion]
s'0:988 [in MetaCoq.PCUIC.PCUICConversion]
s'0:990 [in MetaCoq.PCUIC.PCUICConversion]
s':1007 [in MetaCoq.PCUIC.PCUICParallelReduction]
s':101 [in MetaCoq.Template.utils.wGraph]
s':1016 [in MetaCoq.PCUIC.PCUICParallelReduction]
s':102 [in MetaCoq.PCUIC.PCUICSpine]
s':1025 [in MetaCoq.PCUIC.PCUICParallelReduction]
s':1025 [in MetaCoq.Template.utils.wGraph]
s':1033 [in MetaCoq.Template.utils.wGraph]
s':107 [in MetaCoq.PCUIC.PCUICSpine]
s':110 [in MetaCoq.PCUIC.PCUICConversion]
s':111 [in MetaCoq.PCUIC.PCUICContexts]
s':112 [in MetaCoq.Erasure.ESubstitution]
s':1174 [in MetaCoq.PCUIC.PCUICConversion]
s':1186 [in MetaCoq.PCUIC.PCUICConversion]
s':119 [in MetaCoq.Erasure.Prelim]
s':1195 [in MetaCoq.PCUIC.PCUICConversion]
s':120 [in MetaCoq.Template.utils.wGraph]
S':126 [in MetaCoq.PCUIC.PCUICArities]
s':126 [in MetaCoq.PCUIC.PCUICSR]
s':127 [in MetaCoq.PCUIC.PCUICEquality]
s':127 [in MetaCoq.Template.utils.wGraph]
s':127 [in MetaCoq.Template.TypingWf]
s':128 [in MetaCoq.PCUIC.PCUICConversion]
s':129 [in MetaCoq.Template.utils.wGraph]
s':133 [in MetaCoq.PCUIC.PCUICConversion]
s':140 [in MetaCoq.Template.utils.wGraph]
s':142 [in MetaCoq.Erasure.ESubstitution]
s':142 [in MetaCoq.PCUIC.PCUICSpine]
s':145 [in MetaCoq.Template.utils.wGraph]
s':149 [in MetaCoq.PCUIC.PCUICConversion]
s':151 [in MetaCoq.Template.utils.wGraph]
s':155 [in MetaCoq.Template.utils.wGraph]
s':158 [in MetaCoq.PCUIC.PCUICSpine]
s':159 [in MetaCoq.Template.utils.wGraph]
s':160 [in MetaCoq.PCUIC.PCUICConversion]
s':165 [in MetaCoq.PCUIC.PCUICConversion]
s':171 [in MetaCoq.PCUIC.PCUICArities]
s':179 [in MetaCoq.PCUIC.PCUICSpine]
s':187 [in MetaCoq.PCUIC.PCUICSpine]
s':192 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
s':206 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
s':208 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
s':210 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
s':235 [in MetaCoq.SafeChecker.PCUICSafeConversion]
s':239 [in MetaCoq.PCUIC.PCUICCumulProp]
s':249 [in MetaCoq.Erasure.EArities]
s':25 [in MetaCoq.Template.Universes]
s':251 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
s':253 [in MetaCoq.Template.utils.wGraph]
s':254 [in MetaCoq.Erasure.EArities]
s':257 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
s':260 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
s':261 [in MetaCoq.PCUIC.PCUICCumulProp]
s':265 [in MetaCoq.PCUIC.PCUICElimination]
s':272 [in MetaCoq.PCUIC.PCUICElimination]
s':275 [in MetaCoq.PCUIC.PCUICCumulProp]
s':279 [in MetaCoq.PCUIC.PCUICElimination]
s':280 [in MetaCoq.PCUIC.PCUICSpine]
s':284 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
s':286 [in MetaCoq.PCUIC.PCUICElimination]
s':291 [in MetaCoq.PCUIC.PCUICSubstitution]
s':292 [in MetaCoq.PCUIC.PCUICInductiveInversion]
s':293 [in MetaCoq.PCUIC.PCUICElimination]
s':30 [in MetaCoq.PCUIC.PCUICProgress]
s':300 [in MetaCoq.PCUIC.PCUICElimination]
s':301 [in MetaCoq.Template.utils.wGraph]
s':306 [in MetaCoq.PCUIC.PCUICSpine]
s':307 [in MetaCoq.PCUIC.PCUICElimination]
s':307 [in MetaCoq.Template.utils.wGraph]
s':311 [in MetaCoq.Template.utils.wGraph]
s':319 [in MetaCoq.Template.utils.wGraph]
s':322 [in MetaCoq.Template.utils.wGraph]
s':326 [in MetaCoq.Template.utils.wGraph]
s':329 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
s':33 [in MetaCoq.PCUIC.PCUICContextSubst]
s':332 [in MetaCoq.Template.utils.wGraph]
s':334 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
s':334 [in MetaCoq.PCUIC.PCUICSpine]
s':34 [in MetaCoq.PCUIC.PCUICCumulProp]
s':346 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
s':347 [in MetaCoq.Template.utils.wGraph]
s':35 [in MetaCoq.SafeChecker.PCUICTypeChecker]
s':36 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
s':36 [in MetaCoq.PCUIC.PCUICContextSubst]
s':36 [in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
s':360 [in MetaCoq.PCUIC.PCUICInductives]
s':371 [in MetaCoq.PCUIC.PCUICInductives]
s':383 [in MetaCoq.PCUIC.PCUICConversion]
s':386 [in MetaCoq.PCUIC.PCUICConversion]
s':39 [in MetaCoq.PCUIC.PCUICCumulProp]
s':397 [in MetaCoq.PCUIC.PCUICSpine]
s':400 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
s':403 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
s':405 [in MetaCoq.Template.utils.wGraph]
s':406 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
s':408 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
s':410 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
s':410 [in MetaCoq.Template.utils.wGraph]
s':413 [in MetaCoq.Template.utils.wGraph]
s':414 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
s':416 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
s':423 [in MetaCoq.Template.utils.wGraph]
s':43 [in MetaCoq.PCUIC.PCUICContextSubst]
s':443 [in MetaCoq.SafeChecker.PCUICSafeChecker]
s':45 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
s':450 [in MetaCoq.Template.utils.wGraph]
s':46 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
s':467 [in MetaCoq.PCUIC.PCUICNormal]
s':467 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
s':473 [in MetaCoq.SafeChecker.PCUICSafeChecker]
s':48 [in MetaCoq.PCUIC.PCUICContextSubst]
s':482 [in MetaCoq.SafeChecker.PCUICSafeChecker]
s':494 [in MetaCoq.Template.utils.wGraph]
s':499 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
s':50 [in MetaCoq.Template.Universes]
s':50 [in MetaCoq.Template.Typing]
s':509 [in MetaCoq.Template.Universes]
s':51 [in MetaCoq.PCUIC.PCUICSpine]
s':515 [in MetaCoq.Template.Universes]
s':518 [in MetaCoq.PCUIC.PCUICSubstitution]
s':52 [in MetaCoq.PCUIC.PCUICCumulProp]
s':529 [in MetaCoq.Template.Universes]
s':54 [in MetaCoq.PCUIC.PCUICProgress]
s':542 [in MetaCoq.Template.common.uGraph]
s':544 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
s':5634 [in MetaCoq.SafeChecker.PCUICSafeConversion]
S':568 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
s':574 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
S':576 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
s':58 [in MetaCoq.PCUIC.PCUICCumulProp]
s':583 [in MetaCoq.PCUIC.PCUICInductives]
s':6 [in MetaCoq.PCUIC.PCUICSpine]
s':60 [in MetaCoq.PCUIC.PCUICCumulProp]
s':600 [in MetaCoq.PCUIC.PCUICInductiveInversion]
s':605 [in MetaCoq.PCUIC.PCUICInductiveInversion]
s':62 [in MetaCoq.Template.Typing]
s':62 [in MetaCoq.Template.Reflect]
s':62 [in MetaCoq.PCUIC.PCUICContextSubst]
s':620 [in MetaCoq.PCUIC.PCUICInductiveInversion]
s':634 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
s':648 [in MetaCoq.PCUIC.PCUICSpine]
s':65 [in MetaCoq.PCUIC.PCUICArities]
S':656 [in MetaCoq.Template.common.uGraph]
s':66 [in MetaCoq.PCUIC.PCUICSpine]
s':67 [in MetaCoq.PCUIC.PCUICContextSubst]
s':685 [in MetaCoq.Template.Universes]
s':685 [in MetaCoq.PCUIC.PCUICSR]
s':73 [in MetaCoq.SafeChecker.PCUICWfReduction]
s':742 [in MetaCoq.PCUIC.PCUICParallelReduction]
s':752 [in MetaCoq.PCUIC.PCUICParallelReduction]
s':765 [in MetaCoq.PCUIC.PCUICParallelReduction]
s':77 [in MetaCoq.Template.Typing]
s':77 [in MetaCoq.PCUIC.PCUICContextSubst]
s':772 [in MetaCoq.PCUIC.PCUICParallelReduction]
s':779 [in MetaCoq.PCUIC.PCUICParallelReduction]
s':795 [in MetaCoq.PCUIC.PCUICParallelReduction]
s':796 [in MetaCoq.PCUIC.PCUICSpine]
s':80 [in MetaCoq.SafeChecker.PCUICWfReduction]
s':80 [in MetaCoq.PCUIC.PCUICContextSubst]
s':805 [in MetaCoq.PCUIC.PCUICParallelReduction]
s':812 [in MetaCoq.PCUIC.PCUICSpine]
s':827 [in MetaCoq.PCUIC.PCUICInductiveInversion]
s':828 [in MetaCoq.PCUIC.PCUICParallelReduction]
s':829 [in MetaCoq.Template.utils.wGraph]
s':83 [in MetaCoq.Template.TermEquality]
s':83 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
s':84 [in MetaCoq.PCUIC.PCUICElimination]
s':862 [in MetaCoq.Template.utils.wGraph]
s':92 [in MetaCoq.Erasure.ESubstitution]
s':927 [in MetaCoq.PCUIC.PCUICConversion]
s':967 [in MetaCoq.PCUIC.PCUICConversion]
s':979 [in MetaCoq.PCUIC.PCUICConversion]
s':98 [in MetaCoq.Template.utils.wGraph]
s':985 [in MetaCoq.PCUIC.PCUICConversion]
s':997 [in MetaCoq.PCUIC.PCUICConversion]
s0:102 [in MetaCoq.Template.utils.wGraph]
s0:112 [in MetaCoq.Template.utils.wGraph]
s0:171 [in MetaCoq.PCUIC.PCUICElimination]
s0:175 [in MetaCoq.PCUIC.PCUICElimination]
s0:385 [in MetaCoq.Template.utils.wGraph]
s0:389 [in MetaCoq.Template.utils.wGraph]
s0:395 [in MetaCoq.Template.utils.wGraph]
s0:470 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
s0:839 [in MetaCoq.PCUIC.PCUICParallelReduction]
s0:845 [in MetaCoq.Template.utils.wGraph]
s0:849 [in MetaCoq.Template.utils.wGraph]
s0:853 [in MetaCoq.Template.utils.wGraph]
s0:928 [in MetaCoq.PCUIC.PCUICConversion]
s0:987 [in MetaCoq.PCUIC.PCUICConversion]
s0:989 [in MetaCoq.PCUIC.PCUICConversion]
s1':655 [in MetaCoq.Template.Universes]
s1:100 [in MetaCoq.PCUIC.PCUICProgress]
s1:1000 [in MetaCoq.Template.Typing]
s1:1010 [in MetaCoq.Template.Typing]
s1:103 [in MetaCoq.Template.utils.wGraph]
s1:103 [in MetaCoq.PCUIC.PCUICTyping]
S1:105 [in MetaCoq.Template.common.uGraph]
s1:1064 [in MetaCoq.SafeChecker.PCUICTypeChecker]
s1:110 [in MetaCoq.PCUIC.PCUICProgress]
s1:113 [in MetaCoq.Template.utils.wGraph]
s1:116 [in MetaCoq.SafeChecker.PCUICSafeConversion]
s1:130 [in MetaCoq.SafeChecker.PCUICSafeConversion]
s1:148 [in MetaCoq.SafeChecker.PCUICSafeConversion]
s1:148 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
s1:151 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
s1:162 [in MetaCoq.SafeChecker.PCUICSafeConversion]
s1:194 [in MetaCoq.Template.Universes]
s1:20 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
s1:244 [in MetaCoq.PCUIC.PCUICProgress]
s1:253 [in MetaCoq.PCUIC.PCUICProgress]
s1:263 [in MetaCoq.PCUIC.PCUICProgress]
s1:3 [in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
s1:321 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
s1:33 [in MetaCoq.Template.utils.bytestring]
s1:345 [in MetaCoq.Template.Universes]
s1:345 [in MetaCoq.Template.Checker]
s1:356 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
s1:386 [in MetaCoq.Template.utils.wGraph]
s1:39 [in MetaCoq.Template.utils.bytestring]
s1:392 [in MetaCoq.Template.utils.wGraph]
s1:396 [in MetaCoq.Template.utils.wGraph]
s1:42 [in MetaCoq.PCUIC.PCUICInversion]
s1:449 [in MetaCoq.Template.common.uGraph]
s1:466 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
s1:471 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
s1:484 [in MetaCoq.PCUIC.PCUICTyping]
s1:493 [in MetaCoq.PCUIC.PCUICTyping]
s1:50 [in MetaCoq.PCUIC.PCUICInversion]
s1:503 [in MetaCoq.PCUIC.PCUICTyping]
s1:588 [in MetaCoq.Template.Universes]
s1:590 [in MetaCoq.Template.Universes]
s1:594 [in MetaCoq.Template.Universes]
s1:615 [in MetaCoq.Template.Typing]
s1:620 [in MetaCoq.Template.Typing]
s1:626 [in MetaCoq.Template.Typing]
s1:654 [in MetaCoq.Template.Universes]
S1:657 [in MetaCoq.Template.common.uGraph]
s1:666 [in MetaCoq.Template.Universes]
s1:67 [in MetaCoq.PCUIC.PCUICInversion]
s1:686 [in MetaCoq.Template.Universes]
s1:690 [in MetaCoq.Template.Universes]
s1:692 [in MetaCoq.Template.Universes]
s1:694 [in MetaCoq.Template.Universes]
s1:696 [in MetaCoq.Template.Universes]
s1:702 [in MetaCoq.Template.Universes]
s1:704 [in MetaCoq.Template.Universes]
s1:706 [in MetaCoq.Template.Universes]
s1:812 [in MetaCoq.PCUIC.PCUICTyping]
s1:821 [in MetaCoq.PCUIC.PCUICTyping]
s1:831 [in MetaCoq.PCUIC.PCUICTyping]
s1:839 [in MetaCoq.Template.utils.wGraph]
s1:842 [in MetaCoq.Template.utils.wGraph]
s1:846 [in MetaCoq.Template.utils.wGraph]
s1:850 [in MetaCoq.Template.utils.wGraph]
s1:854 [in MetaCoq.Template.utils.wGraph]
s1:91 [in MetaCoq.PCUIC.PCUICProgress]
s1:92 [in MetaCoq.PCUIC.PCUICTyping]
s1:97 [in MetaCoq.PCUIC.PCUICTyping]
s1:991 [in MetaCoq.Template.Typing]
s2':657 [in MetaCoq.Template.Universes]
s2':786 [in MetaCoq.PCUIC.PCUICParallelReduction]
s2:104 [in MetaCoq.Template.utils.wGraph]
S2:106 [in MetaCoq.Template.common.uGraph]
s2:1065 [in MetaCoq.SafeChecker.PCUICTypeChecker]
s2:114 [in MetaCoq.Template.utils.wGraph]
s2:117 [in MetaCoq.SafeChecker.PCUICSafeConversion]
s2:131 [in MetaCoq.SafeChecker.PCUICSafeConversion]
s2:149 [in MetaCoq.SafeChecker.PCUICSafeConversion]
s2:149 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
s2:152 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
s2:163 [in MetaCoq.SafeChecker.PCUICSafeConversion]
s2:195 [in MetaCoq.Template.Universes]
s2:21 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
s2:245 [in MetaCoq.PCUIC.PCUICProgress]
s2:322 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
s2:34 [in MetaCoq.Template.utils.bytestring]
s2:346 [in MetaCoq.Template.Universes]
s2:346 [in MetaCoq.Template.Checker]
s2:357 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
s2:387 [in MetaCoq.Template.utils.wGraph]
s2:393 [in MetaCoq.Template.utils.wGraph]
s2:397 [in MetaCoq.Template.utils.wGraph]
s2:4 [in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
s2:40 [in MetaCoq.Template.utils.bytestring]
s2:43 [in MetaCoq.PCUIC.PCUICInversion]
s2:450 [in MetaCoq.Template.common.uGraph]
s2:472 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
s2:472 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
s2:485 [in MetaCoq.PCUIC.PCUICTyping]
s2:51 [in MetaCoq.PCUIC.PCUICInversion]
s2:587 [in MetaCoq.Template.Universes]
s2:592 [in MetaCoq.Template.Universes]
s2:595 [in MetaCoq.Template.Universes]
s2:616 [in MetaCoq.Template.Typing]
s2:656 [in MetaCoq.Template.Universes]
S2:658 [in MetaCoq.Template.common.uGraph]
s2:667 [in MetaCoq.Template.Universes]
s2:687 [in MetaCoq.Template.Universes]
s2:691 [in MetaCoq.Template.Universes]
s2:693 [in MetaCoq.Template.Universes]
s2:695 [in MetaCoq.Template.Universes]
s2:697 [in MetaCoq.Template.Universes]
s2:703 [in MetaCoq.Template.Universes]
s2:705 [in MetaCoq.Template.Universes]
s2:707 [in MetaCoq.Template.Universes]
s2:785 [in MetaCoq.PCUIC.PCUICParallelReduction]
s2:813 [in MetaCoq.PCUIC.PCUICTyping]
s2:840 [in MetaCoq.Template.utils.wGraph]
s2:843 [in MetaCoq.Template.utils.wGraph]
s2:847 [in MetaCoq.Template.utils.wGraph]
s2:851 [in MetaCoq.Template.utils.wGraph]
s2:855 [in MetaCoq.Template.utils.wGraph]
s2:92 [in MetaCoq.PCUIC.PCUICProgress]
s2:93 [in MetaCoq.PCUIC.PCUICTyping]
s2:992 [in MetaCoq.Template.Typing]
s3:473 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
s3:668 [in MetaCoq.Template.Universes]
s:1 [in MetaCoq.Examples.typing_correctness]
s:1 [in MetaCoq.Examples.metacoq_tour_prelude]
s:1 [in MetaCoq.PCUIC.PCUICContexts]
s:10 [in MetaCoq.Translations.param_binary]
s:10 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
s:10 [in MetaCoq.PCUIC.PCUICCasesContexts]
S:100 [in MetaCoq.Template.utils.MCRelations]
s:100 [in MetaCoq.PCUIC.PCUICSubstitution]
s:100 [in MetaCoq.Template.utils.wGraph]
s:1003 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
s:1006 [in MetaCoq.PCUIC.PCUICParallelReduction]
S:1008 [in MetaCoq.PCUIC.PCUICConfluence]
s:101 [in MetaCoq.PCUIC.PCUICSpine]
s:1015 [in MetaCoq.PCUIC.PCUICParallelReduction]
s:1016 [in MetaCoq.Template.utils.wGraph]
s:102 [in MetaCoq.Template.Universes]
s:1020 [in MetaCoq.Template.Typing]
s:1021 [in MetaCoq.Template.utils.wGraph]
s:1024 [in MetaCoq.PCUIC.PCUICParallelReduction]
s:103 [in MetaCoq.Erasure.ESubstitution]
s:103 [in MetaCoq.Template.EnvironmentTyping]
s:103 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
s:103 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
S:104 [in MetaCoq.Template.common.uGraph]
s:104 [in MetaCoq.Examples.tauto]
s:105 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
s:105 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
s:105 [in MetaCoq.Examples.tauto]
S:1054 [in MetaCoq.PCUIC.PCUICConfluence]
s:106 [in MetaCoq.Template.WfAst]
s:106 [in MetaCoq.PCUIC.PCUICSpine]
s:107 [in MetaCoq.PCUIC.PCUICInductives]
s:107 [in MetaCoq.Examples.tauto]
s:1072 [in MetaCoq.Template.utils.wGraph]
s:1074 [in MetaCoq.Template.utils.wGraph]
s:1075 [in MetaCoq.Template.utils.wGraph]
S:1077 [in MetaCoq.PCUIC.PCUICConfluence]
s:108 [in MetaCoq.PCUIC.PCUICSubstitution]
s:108 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
s:1086 [in MetaCoq.Template.utils.wGraph]
s:1089 [in MetaCoq.Template.utils.wGraph]
s:109 [in MetaCoq.Template.utils.wGraph]
s:109 [in MetaCoq.PCUIC.PCUICConversion]
s:109 [in MetaCoq.PCUIC.PCUICTyping]
s:1094 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
s:1096 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
s:1098 [in MetaCoq.Template.utils.wGraph]
s:11 [in MetaCoq.PCUIC.PCUICContextSubst]
s:11 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
s:110 [in MetaCoq.Erasure.ESubstitution]
s:110 [in MetaCoq.PCUIC.PCUICElimination]
s:110 [in MetaCoq.PCUIC.PCUICSubstitution]
s:110 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
s:110 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
s:110 [in MetaCoq.PCUIC.PCUICContexts]
s:1104 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
s:1106 [in MetaCoq.Template.Typing]
s:111 [in MetaCoq.Erasure.EInduction]
s:1110 [in MetaCoq.Template.utils.wGraph]
s:1119 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
s:1120 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
s:1127 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
s:113 [in MetaCoq.PCUIC.PCUICConversion]
s:1136 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
S:114 [in MetaCoq.PCUIC.PCUICArities]
s:114 [in MetaCoq.PCUIC.PCUICSR]
s:114 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
s:114 [in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
s:114 [in MetaCoq.PCUIC.PCUICContexts]
s:117 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
s:1173 [in MetaCoq.PCUIC.PCUICConversion]
s:118 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
s:1185 [in MetaCoq.PCUIC.PCUICConversion]
s:119 [in MetaCoq.PCUIC.PCUICSubstitution]
s:119 [in MetaCoq.Template.utils.wGraph]
s:119 [in MetaCoq.PCUIC.PCUICConversion]
s:1193 [in MetaCoq.Translations.MiniHoTT]
s:1194 [in MetaCoq.PCUIC.PCUICConversion]
s:1196 [in MetaCoq.Template.Typing]
s:1199 [in MetaCoq.Template.Typing]
s:12 [in MetaCoq.PCUIC.PCUICInversion]
s:12 [in MetaCoq.Erasure.ELiftSubst]
s:12 [in MetaCoq.PCUIC.Typing.PCUICWeakeningTyp]
s:12 [in MetaCoq.Translations.MiniHoTT_paths]
s:12 [in MetaCoq.PCUIC.Conversion.PCUICClosedConv]
s:120 [in MetaCoq.PCUIC.PCUICProgress]
s:1201 [in MetaCoq.Translations.MiniHoTT_paths]
s:1203 [in MetaCoq.Translations.MiniHoTT]
s:1205 [in MetaCoq.Template.Typing]
s:1208 [in MetaCoq.Template.Typing]
S:121 [in MetaCoq.PCUIC.PCUICArities]
s:121 [in MetaCoq.Erasure.EInlineProjections]
s:121 [in MetaCoq.PCUIC.PCUICSR]
s:1211 [in MetaCoq.Translations.MiniHoTT_paths]
s:122 [in MetaCoq.Erasure.EInduction]
s:1228 [in MetaCoq.Template.Typing]
s:123 [in MetaCoq.Erasure.EInlineProjections]
s:1231 [in MetaCoq.Template.Typing]
s:1237 [in MetaCoq.Template.Typing]
s:124 [in MetaCoq.Erasure.ESubstitution]
s:124 [in MetaCoq.PCUIC.PCUICSR]
s:1240 [in MetaCoq.Template.Typing]
S:125 [in MetaCoq.PCUIC.PCUICArities]
s:125 [in MetaCoq.PCUIC.PCUICConversion]
s:125 [in MetaCoq.Template.TypingWf]
s:126 [in MetaCoq.PCUIC.PCUICSubstitution]
s:126 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
s:126 [in MetaCoq.PCUIC.PCUICEquality]
s:126 [in MetaCoq.Template.utils.wGraph]
s:126 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
s:1269 [in MetaCoq.Translations.MiniHoTT]
s:127 [in MetaCoq.PCUIC.PCUICCumulProp]
s:127 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
s:1273 [in MetaCoq.PCUIC.PCUICConversion]
s:1277 [in MetaCoq.Translations.MiniHoTT_paths]
s:128 [in MetaCoq.PCUIC.PCUICSubstitution]
s:128 [in MetaCoq.Template.utils.wGraph]
s:129 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
s:129 [in MetaCoq.PCUIC.PCUICCumulProp]
s:129 [in MetaCoq.Template.TypingWf]
s:1296 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
s:1299 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
s:13 [in MetaCoq.Erasure.EInduction]
s:130 [in MetaCoq.PCUIC.PCUICElimination]
s:130 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
s:130 [in MetaCoq.PCUIC.PCUICConversion]
s:130 [in MetaCoq.Erasure.ERemoveParams]
s:1304 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
s:1309 [in MetaCoq.Translations.MiniHoTT]
s:131 [in MetaCoq.PCUIC.PCUICSafeLemmata]
s:131 [in MetaCoq.PCUIC.PCUICSubstitution]
s:1311 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
s:1317 [in MetaCoq.Translations.MiniHoTT_paths]
S:132 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
s:132 [in MetaCoq.PCUIC.PCUICCumulProp]
s:132 [in MetaCoq.PCUIC.PCUICSR]
s:132 [in MetaCoq.PCUIC.PCUICContexts]
s:133 [in MetaCoq.PCUIC.PCUICElimination]
S:133 [in MetaCoq.PCUIC.PCUICArities]
s:133 [in MetaCoq.Template.utils.wGraph]
s:133 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
s:1330 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
s:134 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
s:134 [in MetaCoq.Translations.MiniHoTT]
s:1344 [in MetaCoq.Translations.MiniHoTT]
s:1345 [in MetaCoq.Translations.MiniHoTT]
s:135 [in MetaCoq.Erasure.ESubstitution]
s:135 [in MetaCoq.PCUIC.PCUICInductiveInversion]
s:135 [in MetaCoq.Erasure.EEtaExpanded]
s:1352 [in MetaCoq.Translations.MiniHoTT]
s:1352 [in MetaCoq.Translations.MiniHoTT_paths]
s:1353 [in MetaCoq.Translations.MiniHoTT]
s:1353 [in MetaCoq.Translations.MiniHoTT_paths]
s:136 [in MetaCoq.PCUIC.PCUICWfUniverses]
s:136 [in MetaCoq.PCUIC.PCUICCumulProp]
s:136 [in MetaCoq.Template.utils.wGraph]
s:1360 [in MetaCoq.Translations.MiniHoTT_paths]
s:1361 [in MetaCoq.Translations.MiniHoTT_paths]
s:137 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
S:137 [in MetaCoq.PCUIC.PCUICArities]
s:139 [in MetaCoq.Template.utils.wGraph]
s:139 [in MetaCoq.PCUIC.PCUICConversion]
s:139 [in MetaCoq.PCUIC.PCUICSpine]
s:1394 [in MetaCoq.SafeChecker.PCUICSafeReduce]
s:14 [in MetaCoq.PCUIC.PCUICSubstitution]
s:14 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
s:140 [in MetaCoq.Erasure.ESubstitution]
s:140 [in MetaCoq.PCUIC.PCUICCumulProp]
s:140 [in MetaCoq.PCUIC.PCUICSR]
S:141 [in MetaCoq.PCUIC.PCUICArities]
s:142 [in MetaCoq.Translations.MiniHoTT_paths]
s:142 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
s:143 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
s:143 [in MetaCoq.PCUIC.PCUICConversion]
s:144 [in MetaCoq.Template.utils.wGraph]
s:145 [in MetaCoq.Template.LiftSubst]
s:146 [in MetaCoq.PCUIC.PCUICArities]
s:147 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
s:148 [in MetaCoq.Erasure.EConstructorsAsBlocks]
s:148 [in MetaCoq.Template.utils.wGraph]
s:148 [in MetaCoq.PCUIC.PCUICConversion]
s:149 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
s:150 [in MetaCoq.PCUIC.PCUICInductives]
s:150 [in MetaCoq.Template.utils.wGraph]
s:150 [in MetaCoq.PCUIC.PCUICTyping]
s:151 [in MetaCoq.PCUIC.PCUICArities]
s:151 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
s:151 [in MetaCoq.SafeChecker.PCUICSafeChecker]
s:152 [in MetaCoq.PCUIC.PCUICElimination]
s:153 [in MetaCoq.PCUIC.PCUICArities]
s:154 [in MetaCoq.Template.utils.wGraph]
s:154 [in MetaCoq.PCUIC.PCUICConversion]
s:1547 [in MetaCoq.SafeChecker.PCUICSafeReduce]
s:155 [in MetaCoq.Template.utils.bytestring]
s:156 [in MetaCoq.PCUIC.PCUICTyping]
s:156 [in MetaCoq.SafeChecker.PCUICSafeChecker]
s:157 [in MetaCoq.PCUIC.PCUICAlpha]
s:157 [in MetaCoq.Erasure.ErasureFunction]
s:157 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
s:158 [in MetaCoq.PCUIC.PCUICWfUniverses]
s:158 [in MetaCoq.PCUIC.PCUICInductives]
s:158 [in MetaCoq.Template.utils.wGraph]
s:159 [in MetaCoq.Template.utils.bytestring]
s:159 [in MetaCoq.PCUIC.PCUICConversion]
s:159 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
s:159 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
s:16 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
s:16 [in MetaCoq.Erasure.EDeps]
s:16 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
s:16 [in MetaCoq.PCUIC.Conversion.PCUICClosedConv]
s:160 [in MetaCoq.PCUIC.PCUICInductives]
s:161 [in MetaCoq.PCUIC.PCUICTyping]
s:162 [in MetaCoq.PCUIC.PCUICInductiveInversion]
s:163 [in MetaCoq.Template.EtaExpand]
s:163 [in MetaCoq.PCUIC.PCUICSpine]
s:164 [in MetaCoq.PCUIC.PCUICArities]
s:164 [in MetaCoq.PCUIC.PCUICConversion]
s:166 [in MetaCoq.PCUIC.PCUICContexts]
s:167 [in MetaCoq.PCUIC.PCUICContexts]
s:168 [in MetaCoq.PCUIC.PCUICAlpha]
s:168 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
s:169 [in MetaCoq.PCUIC.PCUICSpine]
s:17 [in MetaCoq.Template.utils.MCString]
s:17 [in MetaCoq.PCUIC.PCUICContextSubst]
s:170 [in MetaCoq.PCUIC.PCUICArities]
s:170 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
s:170 [in MetaCoq.PCUIC.PCUICConversion]
s:170 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
s:171 [in MetaCoq.Erasure.ELiftSubst]
s:171 [in MetaCoq.SafeChecker.PCUICSafeChecker]
s:171 [in MetaCoq.PCUIC.PCUICContexts]
s:172 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
s:173 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
s:1737 [in MetaCoq.SafeChecker.PCUICSafeReduce]
s:1745 [in MetaCoq.SafeChecker.PCUICSafeReduce]
s:1747 [in MetaCoq.SafeChecker.PCUICSafeReduce]
s:175 [in MetaCoq.PCUIC.PCUICAst]
s:175 [in MetaCoq.PCUIC.PCUICConversion]
s:175 [in MetaCoq.PCUIC.PCUICContexts]
s:176 [in MetaCoq.PCUIC.PCUICNormal]
s:176 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
s:177 [in MetaCoq.PCUIC.PCUICArities]
s:177 [in MetaCoq.PCUIC.PCUICSpine]
s:178 [in MetaCoq.PCUIC.PCUICFirstorder]
s:178 [in MetaCoq.Erasure.ELiftSubst]
s:179 [in MetaCoq.PCUIC.PCUICContexts]
s:18 [in MetaCoq.PCUIC.PCUICEtaExpand]
s:181 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
s:182 [in MetaCoq.Erasure.ELiftSubst]
s:183 [in MetaCoq.Template.Ast]
s:183 [in MetaCoq.PCUIC.PCUICContexts]
s:184 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
s:184 [in MetaCoq.PCUIC.PCUICSR]
s:186 [in MetaCoq.PCUIC.PCUICArities]
s:186 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
s:186 [in MetaCoq.PCUIC.PCUICSpine]
s:188 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
s:188 [in MetaCoq.SafeChecker.PCUICTypeChecker]
s:19 [in MetaCoq.PCUIC.PCUICValidity]
s:19 [in MetaCoq.PCUIC.PCUICNormal]
s:19 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
s:19 [in MetaCoq.PCUIC.Typing.PCUICWeakeningTyp]
s:19 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
s:19 [in MetaCoq.Erasure.ECSubst]
s:190 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
s:191 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
s:192 [in MetaCoq.Template.Universes]
s:192 [in MetaCoq.PCUIC.PCUICArities]
s:192 [in MetaCoq.PCUIC.PCUICContexts]
s:193 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
s:193 [in MetaCoq.SafeChecker.PCUICErrors]
s:194 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
s:194 [in MetaCoq.PCUIC.PCUICSpine]
s:195 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
s:196 [in MetaCoq.PCUIC.PCUICContexts]
s:197 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
s:201 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
s:201 [in MetaCoq.PCUIC.PCUICSpine]
s:202 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
s:205 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
s:205 [in MetaCoq.Template.EnvironmentTyping]
s:205 [in MetaCoq.PCUIC.PCUICTyping]
s:205 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
s:206 [in MetaCoq.PCUIC.PCUICArities]
s:207 [in MetaCoq.PCUIC.PCUICWfUniverses]
s:207 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
s:208 [in MetaCoq.Erasure.EInduction]
s:208 [in MetaCoq.PCUIC.PCUICSpine]
s:209 [in MetaCoq.Template.EnvironmentTyping]
s:209 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
s:21 [in MetaCoq.Erasure.EInduction]
s:21 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
s:211 [in MetaCoq.PCUIC.PCUICProgress]
s:211 [in MetaCoq.PCUIC.PCUICWfUniverses]
s:212 [in MetaCoq.PCUIC.PCUICContexts]
s:213 [in MetaCoq.PCUIC.PCUICSpine]
s:215 [in MetaCoq.PCUIC.PCUICContexts]
s:216 [in MetaCoq.SafeChecker.PCUICSafeConversion]
s:216 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
s:218 [in MetaCoq.Erasure.EInduction]
s:22 [in MetaCoq.Template.Universes]
s:22 [in MetaCoq.PCUIC.PCUICSubstitution]
s:22 [in MetaCoq.Template.EnvMap]
s:22 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
s:22 [in MetaCoq.PCUIC.Conversion.PCUICClosedConv]
s:22 [in MetaCoq.PCUIC.utils.PCUICPrimitive]
s:22 [in MetaCoq.Template.Induction]
s:222 [in MetaCoq.PCUIC.PCUICCumulProp]
S:2229 [in MetaCoq.Template.utils.All_Forall]
s:224 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
s:226 [in MetaCoq.PCUIC.PCUICSpine]
s:227 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
s:227 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
s:227 [in MetaCoq.PCUIC.PCUICContexts]
s:228 [in MetaCoq.SafeChecker.PCUICSafeConversion]
s:229 [in MetaCoq.Template.EnvironmentTyping]
s:23 [in MetaCoq.Template.utils.bytestring]
s:23 [in MetaCoq.PCUIC.PCUICInductives]
s:230 [in MetaCoq.PCUIC.PCUICCumulProp]
s:232 [in MetaCoq.Template.Ast]
s:232 [in MetaCoq.PCUIC.PCUICSpine]
s:233 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
s:234 [in MetaCoq.Template.common.uGraph]
s:235 [in MetaCoq.PCUIC.PCUICSpine]
s:236 [in MetaCoq.PCUIC.PCUICSubstitution]
s:236 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
s:237 [in MetaCoq.PCUIC.PCUICSubstitution]
s:238 [in MetaCoq.PCUIC.PCUICCumulProp]
s:24 [in MetaCoq.Template.Universes]
s:24 [in MetaCoq.PCUIC.PCUICContextSubst]
s:24 [in MetaCoq.PCUIC.utils.PCUICPrimitive]
s:24 [in MetaCoq.PCUIC.PCUICContexts]
s:240 [in MetaCoq.Template.EnvironmentTyping]
s:241 [in MetaCoq.PCUIC.PCUICSpine]
s:242 [in MetaCoq.PCUIC.PCUICInductives]
s:244 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
s:248 [in MetaCoq.Erasure.EArities]
s:25 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
s:25 [in MetaCoq.Examples.tauto]
s:250 [in MetaCoq.Template.utils.wGraph]
s:250 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
s:252 [in MetaCoq.Template.utils.wGraph]
s:253 [in MetaCoq.Erasure.EArities]
s:253 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
s:255 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
s:256 [in MetaCoq.Erasure.EArities]
s:256 [in MetaCoq.PCUIC.PCUICSubstitution]
s:256 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
s:257 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
s:257 [in MetaCoq.Template.utils.wGraph]
s:259 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
s:259 [in MetaCoq.PCUIC.PCUICSpine]
s:26 [in MetaCoq.Template.Universes]
s:26 [in MetaCoq.Erasure.EDeps]
s:26 [in MetaCoq.Examples.tauto]
s:260 [in MetaCoq.Template.Universes]
s:260 [in MetaCoq.PCUIC.PCUICCumulProp]
s:261 [in MetaCoq.PCUIC.PCUICSubstitution]
s:261 [in MetaCoq.PCUIC.PCUICAlpha]
s:262 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
s:262 [in MetaCoq.Erasure.EArities]
s:263 [in MetaCoq.Template.utils.wGraph]
s:263 [in MetaCoq.PCUIC.PCUICSpine]
s:264 [in MetaCoq.PCUIC.PCUICElimination]
s:264 [in MetaCoq.PCUIC.PCUICInductiveInversion]
s:267 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
s:268 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
s:268 [in MetaCoq.PCUIC.PCUICSubstitution]
s:269 [in MetaCoq.Template.utils.wGraph]
s:269 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
s:27 [in MetaCoq.PCUIC.PCUICRedTypeIrrelevance]
S:27 [in MetaCoq.Template.utils.MCRelations]
s:27 [in MetaCoq.PCUIC.PCUICWfUniverses]
s:27 [in MetaCoq.PCUIC.PCUICSubstitution]
s:27 [in MetaCoq.PCUIC.PCUICContextSubst]
s:27 [in MetaCoq.PCUIC.PCUICSpine]
s:271 [in MetaCoq.PCUIC.PCUICElimination]
s:2721 [in MetaCoq.Translations.MiniHoTT]
s:2729 [in MetaCoq.Translations.MiniHoTT_paths]
s:273 [in MetaCoq.PCUIC.PCUICProgress]
s:273 [in MetaCoq.PCUIC.PCUICInductiveInversion]
s:274 [in MetaCoq.PCUIC.PCUICCumulProp]
s:275 [in MetaCoq.PCUIC.PCUICInductives]
s:2753 [in MetaCoq.Translations.MiniHoTT]
s:2761 [in MetaCoq.Translations.MiniHoTT_paths]
s:278 [in MetaCoq.PCUIC.PCUICElimination]
s:279 [in MetaCoq.PCUIC.PCUICSpine]
s:28 [in MetaCoq.Template.utils.bytestring]
s:280 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
s:282 [in MetaCoq.PCUIC.PCUICSubstitution]
s:282 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
s:283 [in MetaCoq.PCUIC.PCUICWfUniverses]
s:285 [in MetaCoq.PCUIC.PCUICElimination]
s:285 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
s:2875 [in MetaCoq.Translations.MiniHoTT]
s:2883 [in MetaCoq.Translations.MiniHoTT_paths]
s:29 [in MetaCoq.Erasure.EInlineProjections]
s:29 [in MetaCoq.PCUIC.PCUICCasesContexts]
s:290 [in MetaCoq.PCUIC.PCUICSubstitution]
s:290 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
s:291 [in MetaCoq.PCUIC.PCUICInductiveInversion]
s:292 [in MetaCoq.PCUIC.PCUICElimination]
s:294 [in MetaCoq.Template.EnvironmentTyping]
s:295 [in MetaCoq.Template.utils.wGraph]
s:297 [in MetaCoq.PCUIC.PCUICInductiveInversion]
s:298 [in MetaCoq.PCUIC.PCUICSpine]
s:299 [in MetaCoq.PCUIC.PCUICElimination]
s:3 [in MetaCoq.PCUIC.PCUICCanonicity]
s:30 [in MetaCoq.PCUIC.PCUICWfUniverses]
s:30 [in MetaCoq.SafeChecker.PCUICSafeConversion]
s:30 [in MetaCoq.PCUIC.Syntax.PCUICUnivSubst]
s:30 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
s:30 [in MetaCoq.PCUIC.TemplateToPCUICExpanded]
s:30 [in MetaCoq.PCUIC.PCUICContextSubst]
s:30 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
s:30 [in MetaCoq.Erasure.EOptimizePropDiscr]
s:300 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
s:301 [in MetaCoq.PCUIC.PCUICSubstitution]
s:302 [in MetaCoq.PCUIC.PCUICSpine]
s:305 [in MetaCoq.PCUIC.PCUICSpine]
s:306 [in MetaCoq.PCUIC.PCUICElimination]
s:306 [in MetaCoq.PCUIC.PCUICSubstitution]
s:308 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
s:309 [in MetaCoq.Template.Environment]
s:31 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
s:31 [in MetaCoq.PCUIC.PCUICRedTypeIrrelevance]
s:31 [in MetaCoq.Erasure.EDeps]
s:31 [in MetaCoq.Erasure.Prelim]
s:313 [in MetaCoq.Template.utils.wGraph]
s:313 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
s:313 [in MetaCoq.PCUIC.PCUICSpine]
s:314 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
s:314 [in MetaCoq.PCUIC.PCUICSubstitution]
s:318 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
s:32 [in MetaCoq.PCUIC.PCUICInductiveInversion]
s:32 [in MetaCoq.Template.Checker]
s:320 [in MetaCoq.PCUIC.PCUICSpine]
s:321 [in MetaCoq.PCUIC.PCUICSubstitution]
s:321 [in MetaCoq.Template.utils.wGraph]
s:323 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
s:324 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
s:325 [in MetaCoq.Template.utils.wGraph]
s:328 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
s:328 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
s:33 [in MetaCoq.Erasure.EDeps]
s:33 [in MetaCoq.PCUIC.PCUICCumulProp]
s:33 [in MetaCoq.PCUIC.PCUICConvCumInversion]
s:33 [in MetaCoq.PCUIC.PCUICContexts]
s:33 [in MetaCoq.Template.Induction]
s:331 [in MetaCoq.PCUIC.PCUICSubstitution]
s:331 [in MetaCoq.Template.utils.wGraph]
s:333 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
s:333 [in MetaCoq.PCUIC.PCUICSpine]
s:335 [in MetaCoq.PCUIC.PCUICSubstitution]
s:34 [in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
s:34 [in MetaCoq.SafeChecker.PCUICTypeChecker]
s:340 [in MetaCoq.PCUIC.PCUICSubstitution]
s:341 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
s:342 [in MetaCoq.Template.Universes]
s:342 [in MetaCoq.PCUIC.PCUICSubstitution]
s:343 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
s:344 [in MetaCoq.Template.Universes]
s:345 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
s:346 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
s:346 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
s:346 [in MetaCoq.Template.utils.wGraph]
s:348 [in MetaCoq.Erasure.EEtaExpandedFix]
s:348 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
s:35 [in MetaCoq.Template.TemplateMonad.Core]
s:35 [in MetaCoq.PCUIC.PCUICSubstitution]
s:35 [in MetaCoq.PCUIC.PCUICInductives]
s:35 [in MetaCoq.PCUIC.PCUICInversion]
s:35 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
s:35 [in MetaCoq.Template.Environment]
s:35 [in MetaCoq.PCUIC.PCUICSR]
s:35 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
s:351 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
s:354 [in MetaCoq.Template.utils.wGraph]
s:357 [in MetaCoq.SafeChecker.PCUICSafeChecker]
s:359 [in MetaCoq.PCUIC.PCUICInductives]
s:360 [in MetaCoq.Template.utils.wGraph]
s:361 [in MetaCoq.PCUIC.PCUICProgress]
s:362 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
s:362 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
s:365 [in MetaCoq.PCUIC.PCUICInductives]
s:365 [in MetaCoq.Template.utils.wGraph]
s:366 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
s:367 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
s:369 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
s:37 [in MetaCoq.PCUIC.PCUICContextSubst]
s:370 [in MetaCoq.PCUIC.PCUICInductives]
s:370 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
s:371 [in MetaCoq.Template.utils.wGraph]
s:375 [in MetaCoq.Template.utils.wGraph]
s:376 [in MetaCoq.Template.EtaExpand]
s:376 [in MetaCoq.PCUIC.PCUICInductives]
s:379 [in MetaCoq.Template.utils.wGraph]
S:38 [in MetaCoq.Template.utils.MCRelations]
s:38 [in MetaCoq.PCUIC.PCUICCumulProp]
s:38 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
s:38 [in MetaCoq.PCUIC.PCUICContexts]
s:381 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
s:381 [in MetaCoq.PCUIC.PCUICInductives]
s:382 [in MetaCoq.PCUIC.PCUICConversion]
s:385 [in MetaCoq.Template.EnvironmentTyping]
s:385 [in MetaCoq.PCUIC.PCUICConversion]
s:387 [in MetaCoq.PCUIC.PCUICSpine]
s:39 [in MetaCoq.Template.Typing]
s:39 [in MetaCoq.Template.Environment]
s:39 [in MetaCoq.Erasure.EOptimizePropDiscr]
s:390 [in MetaCoq.PCUIC.PCUICSpine]
s:391 [in MetaCoq.PCUIC.PCUICNormal]
s:393 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
s:394 [in MetaCoq.PCUIC.PCUICSpine]
s:396 [in MetaCoq.PCUIC.PCUICSpine]
s:399 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
s:399 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
s:4 [in MetaCoq.PCUIC.PCUICArities]
s:4 [in MetaCoq.Examples.typing_correctness]
s:4 [in MetaCoq.Examples.metacoq_tour_prelude]
s:400 [in MetaCoq.Template.utils.wGraph]
s:402 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
s:403 [in MetaCoq.Template.EnvironmentTyping]
s:405 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
s:407 [in MetaCoq.Template.Universes]
s:407 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
s:408 [in MetaCoq.PCUIC.PCUICSpine]
s:409 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
S:41 [in MetaCoq.Template.utils.MCRelations]
s:41 [in MetaCoq.PCUIC.PCUICContextSubst]
s:413 [in MetaCoq.Template.EtaExpand]
s:413 [in MetaCoq.Template.Universes]
s:413 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
s:415 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
s:418 [in MetaCoq.Template.utils.wGraph]
s:418 [in MetaCoq.PCUIC.PCUICSpine]
s:42 [in MetaCoq.PCUIC.PCUICValidity]
s:42 [in MetaCoq.Template.Environment]
s:421 [in MetaCoq.PCUIC.PCUICProgress]
s:423 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
s:424 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
s:425 [in MetaCoq.Template.utils.MCList]
s:426 [in MetaCoq.SafeChecker.PCUICSafeChecker]
s:427 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
s:427 [in MetaCoq.PCUIC.PCUICConversion]
s:428 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
s:43 [in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
s:430 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
s:430 [in MetaCoq.Template.utils.wGraph]
s:431 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
s:433 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
s:435 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
s:437 [in MetaCoq.Template.Universes]
S:44 [in MetaCoq.Template.utils.MCRelations]
s:44 [in MetaCoq.PCUIC.PCUICWfUniverses]
s:44 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
s:440 [in MetaCoq.Template.utils.wGraph]
s:441 [in MetaCoq.Template.utils.wGraph]
s:441 [in MetaCoq.SafeChecker.PCUICSafeChecker]
s:449 [in MetaCoq.Template.utils.wGraph]
s:45 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
s:45 [in MetaCoq.Examples.tauto]
s:45 [in MetaCoq.Template.Environment]
s:45 [in MetaCoq.PCUIC.PCUICSpine]
s:45 [in MetaCoq.Template.Induction]
s:450 [in MetaCoq.SafeChecker.PCUICTypeChecker]
s:453 [in MetaCoq.Template.utils.wGraph]
s:458 [in MetaCoq.PCUIC.PCUICInductives]
s:46 [in MetaCoq.Template.Typing]
s:46 [in MetaCoq.PCUIC.PCUICContextSubst]
s:46 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
s:461 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
s:461 [in MetaCoq.Template.utils.wGraph]
s:466 [in MetaCoq.PCUIC.PCUICNormal]
s:466 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
s:466 [in MetaCoq.Template.utils.wGraph]
S:47 [in MetaCoq.Template.utils.MCRelations]
s:47 [in MetaCoq.Template.Normal]
s:47 [in MetaCoq.Template.Environment]
s:470 [in MetaCoq.PCUIC.PCUICSubstitution]
s:471 [in MetaCoq.SafeChecker.PCUICSafeChecker]
s:472 [in MetaCoq.PCUIC.PCUICInductives]
s:474 [in MetaCoq.PCUIC.PCUICInductiveInversion]
s:475 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
s:476 [in MetaCoq.PCUIC.PCUICSubstitution]
s:48 [in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
s:48 [in MetaCoq.Examples.tauto]
s:480 [in MetaCoq.SafeChecker.PCUICSafeChecker]
s:481 [in MetaCoq.Template.utils.wGraph]
s:482 [in MetaCoq.PCUIC.PCUICSubstitution]
s:484 [in MetaCoq.PCUIC.PCUICInductiveInversion]
s:485 [in MetaCoq.PCUIC.PCUICConversion]
s:488 [in MetaCoq.PCUIC.PCUICSubstitution]
s:49 [in MetaCoq.PCUIC.PCUICProgress]
s:49 [in MetaCoq.Template.Universes]
s:490 [in MetaCoq.PCUIC.PCUICConversion]
s:490 [in MetaCoq.PCUIC.PCUICSpine]
s:493 [in MetaCoq.Template.utils.wGraph]
s:494 [in MetaCoq.PCUIC.PCUICSubstitution]
s:497 [in MetaCoq.PCUIC.PCUICSubstitution]
s:497 [in MetaCoq.Template.utils.wGraph]
s:498 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
s:498 [in MetaCoq.PCUIC.PCUICSpine]
s:5 [in MetaCoq.PCUIC.PCUICContextSubst]
s:5 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
s:5 [in MetaCoq.Template.Transform]
s:5 [in MetaCoq.PCUIC.PCUICSpine]
s:50 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
s:50 [in MetaCoq.Template.AstUtils]
s:50 [in MetaCoq.PCUIC.PCUICSpine]
s:501 [in MetaCoq.Template.utils.wGraph]
s:504 [in MetaCoq.PCUIC.PCUICSpine]
s:508 [in MetaCoq.Template.Universes]
s:508 [in MetaCoq.Template.utils.wGraph]
s:508 [in MetaCoq.Examples.tauto]
s:508 [in MetaCoq.PCUIC.PCUICSpine]
s:509 [in MetaCoq.PCUIC.PCUICSubstitution]
s:51 [in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
s:51 [in MetaCoq.PCUIC.PCUICCumulProp]
s:51 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
s:511 [in MetaCoq.PCUIC.PCUICSpine]
s:514 [in MetaCoq.Template.Universes]
s:514 [in MetaCoq.PCUIC.PCUICTyping]
s:517 [in MetaCoq.PCUIC.PCUICSubstitution]
s:52 [in MetaCoq.Examples.tauto]
s:52 [in MetaCoq.Template.Environment]
s:520 [in MetaCoq.PCUIC.PCUICSpine]
s:521 [in MetaCoq.Template.Typing]
s:523 [in MetaCoq.PCUIC.PCUICSubstitution]
s:523 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
s:524 [in MetaCoq.PCUIC.PCUICSpine]
s:528 [in MetaCoq.Template.Universes]
s:529 [in MetaCoq.PCUIC.PCUICSubstitution]
s:531 [in MetaCoq.Template.utils.wGraph]
s:534 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
s:535 [in MetaCoq.Template.utils.wGraph]
s:536 [in MetaCoq.Translations.MiniHoTT]
s:54 [in MetaCoq.Template.Universes]
s:54 [in MetaCoq.PCUIC.PCUICContexts]
s:541 [in MetaCoq.Template.common.uGraph]
s:543 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
s:543 [in MetaCoq.Template.utils.wGraph]
s:544 [in MetaCoq.Translations.MiniHoTT_paths]
s:546 [in MetaCoq.PCUIC.PCUICInductives]
s:548 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
s:548 [in MetaCoq.PCUIC.PCUICSpine]
s:5482 [in MetaCoq.SafeChecker.PCUICSafeConversion]
s:549 [in MetaCoq.PCUIC.PCUICSR]
s:549 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
S:55 [in MetaCoq.Template.utils.MCRelations]
s:55 [in MetaCoq.PCUIC.PCUICSubstitution]
s:550 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
s:551 [in MetaCoq.PCUIC.PCUICSubstitution]
s:551 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
s:555 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
s:555 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
s:556 [in MetaCoq.PCUIC.PCUICSubstitution]
s:556 [in MetaCoq.PCUIC.PCUICInductives]
s:557 [in MetaCoq.Template.Typing]
s:557 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
s:558 [in MetaCoq.PCUIC.PCUICInductives]
s:558 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
s:558 [in MetaCoq.Translations.MiniHoTT]
s:559 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
s:56 [in MetaCoq.PCUIC.PCUICValidity]
s:56 [in MetaCoq.Template.Environment]
s:56 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
s:560 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
s:5608 [in MetaCoq.SafeChecker.PCUICSafeConversion]
s:562 [in MetaCoq.PCUIC.PCUICInductives]
s:564 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
s:566 [in MetaCoq.Translations.MiniHoTT_paths]
S:567 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
s:567 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
s:569 [in MetaCoq.PCUIC.PCUICSubstitution]
s:569 [in MetaCoq.Translations.MiniHoTT]
s:57 [in MetaCoq.Template.Typing]
s:57 [in MetaCoq.PCUIC.PCUICCumulProp]
s:57 [in MetaCoq.PCUIC.PCUICSpine]
s:571 [in MetaCoq.PCUIC.PCUICInductives]
s:573 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
S:575 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
s:577 [in MetaCoq.PCUIC.PCUICInductives]
s:577 [in MetaCoq.Translations.MiniHoTT_paths]
s:579 [in MetaCoq.PCUIC.PCUICSubstitution]
s:58 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
s:58 [in MetaCoq.PCUIC.PCUICContextSubst]
s:580 [in MetaCoq.PCUIC.PCUICInductives]
s:580 [in MetaCoq.Translations.MiniHoTT]
s:581 [in MetaCoq.Template.utils.wGraph]
s:583 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
s:584 [in MetaCoq.PCUIC.PCUICInductives]
s:586 [in MetaCoq.SafeChecker.PCUICSafeChecker]
s:587 [in MetaCoq.PCUIC.PCUICSubstitution]
s:587 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
s:587 [in MetaCoq.PCUIC.PCUICSpine]
s:588 [in MetaCoq.Translations.MiniHoTT_paths]
s:59 [in MetaCoq.PCUIC.PCUICCumulProp]
s:59 [in MetaCoq.PCUIC.PCUICInversion]
s:59 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
s:590 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
s:594 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
s:596 [in MetaCoq.PCUIC.PCUICSubstitution]
s:597 [in MetaCoq.PCUIC.PCUICInductiveInversion]
s:598 [in MetaCoq.PCUIC.PCUICInductives]
s:598 [in MetaCoq.PCUIC.PCUICInductiveInversion]
s:598 [in MetaCoq.Translations.MiniHoTT]
s:6 [in MetaCoq.PCUIC.Syntax.PCUICInstDef]
s:6 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
s:6 [in MetaCoq.PCUIC.Conversion.PCUICClosedConv]
s:6 [in MetaCoq.Template.Induction]
s:60 [in MetaCoq.PCUIC.PCUICCasesContexts]
s:60 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
s:60 [in MetaCoq.SafeChecker.PCUICTypeChecker]
s:602 [in MetaCoq.PCUIC.PCUICInductiveInversion]
s:603 [in MetaCoq.PCUIC.PCUICInductives]
s:603 [in MetaCoq.PCUIC.PCUICTyping]
s:604 [in MetaCoq.PCUIC.PCUICSubstitution]
s:606 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
s:606 [in MetaCoq.Translations.MiniHoTT_paths]
s:607 [in MetaCoq.Template.Typing]
s:607 [in MetaCoq.PCUIC.PCUICInductiveInversion]
s:608 [in MetaCoq.PCUIC.PCUICSpine]
s:61 [in MetaCoq.Template.Reflect]
s:61 [in MetaCoq.PCUIC.PCUICContextSubst]
s:61 [in MetaCoq.PCUIC.PCUICSpine]
s:61 [in MetaCoq.Template.Induction]
s:611 [in MetaCoq.Template.Typing]
s:613 [in MetaCoq.PCUIC.PCUICInductives]
s:616 [in MetaCoq.Translations.MiniHoTT]
s:619 [in MetaCoq.PCUIC.PCUICInductiveInversion]
s:62 [in MetaCoq.Examples.tauto]
s:62 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
s:62 [in MetaCoq.PCUIC.PCUICContexts]
s:621 [in MetaCoq.PCUIC.PCUICInductives]
s:624 [in MetaCoq.Translations.MiniHoTT_paths]
s:626 [in MetaCoq.PCUIC.PCUICInductives]
S:629 [in MetaCoq.Template.utils.wGraph]
s:63 [in MetaCoq.PCUIC.PCUICWfUniverses]
s:630 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
s:631 [in MetaCoq.PCUIC.PCUICSubstitution]
s:632 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
s:633 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
S:633 [in MetaCoq.Template.utils.wGraph]
s:638 [in MetaCoq.Template.Universes]
s:638 [in MetaCoq.Template.common.uGraph]
s:64 [in MetaCoq.PCUIC.PCUICInductives]
s:640 [in MetaCoq.PCUIC.PCUICSubstitution]
s:642 [in MetaCoq.Template.Universes]
s:643 [in MetaCoq.Template.Universes]
S:643 [in MetaCoq.Template.utils.wGraph]
s:646 [in MetaCoq.PCUIC.PCUICSpine]
S:647 [in MetaCoq.Template.utils.wGraph]
s:649 [in MetaCoq.PCUIC.PCUICSubstitution]
s:649 [in MetaCoq.Template.common.uGraph]
S:65 [in MetaCoq.Template.utils.MCRelations]
s:65 [in MetaCoq.PCUIC.PCUICSubstitution]
s:65 [in MetaCoq.PCUIC.PCUICSpine]
s:651 [in MetaCoq.Template.Universes]
S:655 [in MetaCoq.Template.common.uGraph]
s:657 [in MetaCoq.PCUIC.PCUICSpine]
s:659 [in MetaCoq.PCUIC.PCUICSpine]
s:66 [in MetaCoq.Template.Typing]
s:66 [in MetaCoq.Examples.tauto]
s:66 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
s:66 [in MetaCoq.PCUIC.PCUICContextSubst]
s:660 [in MetaCoq.Template.EnvironmentTyping]
s:661 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
s:663 [in MetaCoq.Template.Universes]
s:663 [in MetaCoq.PCUIC.PCUICSpine]
s:664 [in MetaCoq.Template.Universes]
s:665 [in MetaCoq.Template.Universes]
s:669 [in MetaCoq.PCUIC.PCUICSpine]
s:67 [in MetaCoq.Template.utils.bytestring]
s:67 [in MetaCoq.SafeChecker.PCUICWfEnv]
s:67 [in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
s:672 [in MetaCoq.Template.Universes]
s:673 [in MetaCoq.PCUIC.PCUICSR]
s:674 [in MetaCoq.PCUIC.PCUICSpine]
s:676 [in MetaCoq.Template.Typing]
s:676 [in MetaCoq.PCUIC.PCUICSpine]
S:677 [in MetaCoq.Template.utils.wGraph]
s:679 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
s:68 [in MetaCoq.PCUIC.PCUICContexts]
s:680 [in MetaCoq.PCUIC.PCUICSpine]
S:681 [in MetaCoq.Template.utils.wGraph]
s:682 [in MetaCoq.Template.Typing]
s:684 [in MetaCoq.Template.Universes]
s:684 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
s:684 [in MetaCoq.PCUIC.PCUICSR]
s:685 [in MetaCoq.PCUIC.PCUICInductiveInversion]
s:687 [in MetaCoq.Template.Typing]
s:69 [in MetaCoq.Template.TermEquality]
s:691 [in MetaCoq.PCUIC.PCUICSR]
s:694 [in MetaCoq.Template.Typing]
S:695 [in MetaCoq.Template.utils.wGraph]
S:699 [in MetaCoq.Template.utils.wGraph]
s:7 [in MetaCoq.PCUIC.PCUICSubstitution]
s:7 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
s:70 [in MetaCoq.Examples.tauto]
s:70 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
s:708 [in MetaCoq.Template.Typing]
s:71 [in MetaCoq.Erasure.EWellformed]
s:71 [in MetaCoq.PCUIC.PCUICContextSubst]
s:71 [in MetaCoq.PCUIC.PCUICSpine]
s:710 [in MetaCoq.PCUIC.PCUICTyping]
s:712 [in MetaCoq.Template.utils.wGraph]
s:714 [in MetaCoq.PCUIC.PCUICTyping]
s:717 [in MetaCoq.PCUIC.PCUICInductiveInversion]
s:717 [in MetaCoq.PCUIC.PCUICEquality]
s:719 [in MetaCoq.PCUIC.PCUICTyping]
s:72 [in MetaCoq.SafeChecker.PCUICWfReduction]
s:72 [in MetaCoq.Template.Induction]
s:720 [in MetaCoq.Template.Typing]
s:720 [in MetaCoq.PCUIC.PCUICInductiveInversion]
s:723 [in MetaCoq.PCUIC.PCUICTyping]
s:73 [in MetaCoq.PCUIC.PCUICArities]
s:73 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
s:731 [in MetaCoq.Template.Universes]
s:736 [in MetaCoq.PCUIC.PCUICSpine]
s:74 [in MetaCoq.PCUIC.PCUICContextSubst]
s:741 [in MetaCoq.Template.Universes]
s:741 [in MetaCoq.PCUIC.PCUICParallelReduction]
s:748 [in MetaCoq.Template.Universes]
s:749 [in MetaCoq.Template.utils.wGraph]
s:75 [in MetaCoq.Template.Typing]
s:75 [in MetaCoq.Template.WfAst]
s:75 [in MetaCoq.Erasure.EWellformed]
s:75 [in MetaCoq.PCUIC.PCUICContexts]
s:751 [in MetaCoq.PCUIC.PCUICParallelReduction]
s:752 [in MetaCoq.PCUIC.PCUICTyping]
s:756 [in MetaCoq.PCUIC.PCUICTyping]
s:761 [in MetaCoq.PCUIC.PCUICTyping]
s:764 [in MetaCoq.PCUIC.PCUICParallelReduction]
s:765 [in MetaCoq.PCUIC.PCUICTyping]
s:766 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
s:769 [in MetaCoq.PCUIC.PCUICSpine]
S:77 [in MetaCoq.PCUIC.utils.PCUICOnOne]
s:771 [in MetaCoq.PCUIC.PCUICParallelReduction]
s:778 [in MetaCoq.PCUIC.PCUICParallelReduction]
s:778 [in MetaCoq.PCUIC.PCUICSpine]
s:78 [in MetaCoq.Erasure.ESubstitution]
s:78 [in MetaCoq.PCUIC.PCUICArities]
s:784 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
s:787 [in MetaCoq.PCUIC.PCUICInductiveInversion]
S:789 [in MetaCoq.PCUIC.PCUICConfluence]
s:79 [in MetaCoq.PCUIC.PCUICEtaExpand]
s:79 [in MetaCoq.SafeChecker.PCUICWfReduction]
s:79 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
S:792 [in MetaCoq.PCUIC.PCUICConfluence]
s:794 [in MetaCoq.PCUIC.PCUICParallelReduction]
s:795 [in MetaCoq.PCUIC.PCUICSpine]
s:8 [in MetaCoq.Template.Normal]
s:80 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
s:800 [in MetaCoq.SafeChecker.PCUICTypeChecker]
s:804 [in MetaCoq.PCUIC.PCUICParallelReduction]
s:808 [in MetaCoq.PCUIC.PCUICParallelReduction]
s:81 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
s:81 [in MetaCoq.Erasure.ESubstitution]
s:81 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
s:81 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
s:81 [in MetaCoq.SafeChecker.PCUICSafeConversion]
s:811 [in MetaCoq.PCUIC.PCUICSpine]
S:814 [in MetaCoq.PCUIC.PCUICConfluence]
s:82 [in MetaCoq.PCUIC.PCUICElimination]
S:82 [in MetaCoq.Template.utils.MCRelations]
s:82 [in MetaCoq.Template.TermEquality]
s:822 [in MetaCoq.PCUIC.PCUICSpine]
s:825 [in MetaCoq.PCUIC.PCUICInductiveInversion]
s:826 [in MetaCoq.SafeChecker.PCUICTypeChecker]
s:827 [in MetaCoq.PCUIC.PCUICParallelReduction]
s:828 [in MetaCoq.Template.utils.wGraph]
s:829 [in MetaCoq.PCUIC.PCUICSR]
s:83 [in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
s:83 [in MetaCoq.PCUIC.PCUICSpine]
s:834 [in MetaCoq.Template.utils.wGraph]
s:84 [in MetaCoq.PCUIC.PCUICInversion]
s:84 [in MetaCoq.Template.Environment]
s:841 [in MetaCoq.PCUIC.PCUICParallelReduction]
s:842 [in MetaCoq.PCUIC.PCUICTyping]
S:85 [in MetaCoq.Template.utils.MCRelations]
s:854 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
s:857 [in MetaCoq.Template.utils.wGraph]
s:866 [in MetaCoq.Template.utils.wGraph]
s:87 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
s:875 [in MetaCoq.PCUIC.PCUICInductiveInversion]
s:88 [in MetaCoq.PCUIC.PCUICTyping]
s:883 [in MetaCoq.PCUIC.PCUICInductiveInversion]
s:888 [in MetaCoq.Translations.MiniHoTT]
s:889 [in MetaCoq.PCUIC.PCUICConversion]
s:893 [in MetaCoq.PCUIC.PCUICInductiveInversion]
s:893 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
s:894 [in MetaCoq.PCUIC.PCUICConversion]
s:895 [in MetaCoq.PCUIC.PCUICInductiveInversion]
s:896 [in MetaCoq.Translations.MiniHoTT_paths]
s:899 [in MetaCoq.PCUIC.PCUICInductiveInversion]
s:9 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
s:900 [in MetaCoq.Template.utils.wGraph]
s:900 [in MetaCoq.PCUIC.PCUICConversion]
s:903 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
s:907 [in MetaCoq.PCUIC.PCUICConversion]
s:91 [in MetaCoq.Erasure.ESubstitution]
s:91 [in MetaCoq.Template.WfAst]
s:914 [in MetaCoq.PCUIC.PCUICConversion]
s:919 [in MetaCoq.Template.utils.wGraph]
s:92 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
s:926 [in MetaCoq.PCUIC.PCUICConversion]
s:926 [in MetaCoq.PCUIC.PCUICTyping]
s:927 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
s:927 [in MetaCoq.Template.utils.wGraph]
s:93 [in MetaCoq.PCUIC.PCUICWfUniverses]
s:939 [in MetaCoq.PCUIC.PCUICParallelReduction]
s:94 [in MetaCoq.PCUIC.PCUICSpine]
s:942 [in MetaCoq.Template.Typing]
s:943 [in MetaCoq.SafeChecker.PCUICSafeChecker]
s:945 [in MetaCoq.Template.utils.wGraph]
S:946 [in MetaCoq.PCUIC.PCUICReduction]
s:95 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
s:95 [in MetaCoq.Examples.tauto]
S:950 [in MetaCoq.PCUIC.PCUICParallelReduction]
s:966 [in MetaCoq.PCUIC.PCUICConversion]
s:968 [in MetaCoq.PCUIC.PCUICConversion]
s:97 [in MetaCoq.Template.EtaExpand]
s:97 [in MetaCoq.Template.utils.wGraph]
s:970 [in MetaCoq.PCUIC.PCUICParallelReduction]
s:978 [in MetaCoq.PCUIC.PCUICConversion]
s:979 [in MetaCoq.Template.utils.wGraph]
s:98 [in MetaCoq.PCUIC.PCUICWfUniverses]
s:98 [in MetaCoq.Examples.tauto]
s:983 [in MetaCoq.Template.Typing]
s:983 [in MetaCoq.Template.utils.wGraph]
s:984 [in MetaCoq.PCUIC.PCUICConversion]
S:987 [in MetaCoq.PCUIC.PCUICConfluence]
S:989 [in MetaCoq.PCUIC.PCUICConfluence]
s:99 [in MetaCoq.PCUIC.PCUICCanonicity]
S:991 [in MetaCoq.PCUIC.PCUICConfluence]
S:993 [in MetaCoq.PCUIC.PCUICConfluence]
s:996 [in MetaCoq.PCUIC.PCUICConversion]



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)