| 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) |
K (binder)
kelim:319 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]kelim:620 [in MetaCoq.Template.EnvironmentTyping]
kelim:75 [in MetaCoq.Erasure.EPretty]
kelim:929 [in MetaCoq.SafeChecker.PCUICSafeChecker]
keys:50 [in MetaCoq.Template.utils.bytestring]
kind:166 [in MetaCoq.Template.EtaExpand]
kind:185 [in MetaCoq.Template.Ast]
kind:99 [in MetaCoq.Template.EtaExpand]
kn':11 [in MetaCoq.Template.EnvMap]
kn':13 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
kn':15 [in MetaCoq.Template.EnvMap]
kn':18 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
kn':29 [in MetaCoq.Erasure.EGlobalEnv]
kn':42 [in MetaCoq.Template.Kernames]
kn':51 [in MetaCoq.Translations.param_original]
kn':55 [in MetaCoq.Translations.param_binary]
kn':55 [in MetaCoq.Translations.param_original]
kn':56 [in MetaCoq.Template.Kernames]
kn':59 [in MetaCoq.Translations.param_binary]
kn':86 [in MetaCoq.Translations.param_cheap_packed]
kn':886 [in MetaCoq.Erasure.ErasureFunction]
kn':891 [in MetaCoq.Erasure.ErasureFunction]
kn':895 [in MetaCoq.Erasure.ErasureFunction]
kn':898 [in MetaCoq.Erasure.ErasureFunction]
kn':904 [in MetaCoq.Erasure.ErasureFunction]
kn':92 [in MetaCoq.Translations.param_cheap_packed]
kn':95 [in MetaCoq.Translations.times_bool_fun]
kn':99 [in MetaCoq.Translations.times_bool_fun]
kn:10 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
kn:10 [in MetaCoq.Template.EnvMap]
kn:1022 [in MetaCoq.Erasure.ErasureFunction]
kn:103 [in MetaCoq.Erasure.EOptimizePropDiscr]
kn:1037 [in MetaCoq.Erasure.ErasureFunction]
kn:104 [in MetaCoq.Erasure.Extract]
kn:1068 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
kn:108 [in MetaCoq.Erasure.Extract]
kn:108 [in MetaCoq.Erasure.EOptimizePropDiscr]
kn:11 [in MetaCoq.SafeChecker.PCUICConsistency]
kn:11 [in MetaCoq.Erasure.EEnvMap]
kn:111 [in MetaCoq.Erasure.EOptimizePropDiscr]
kn:112 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
kn:114 [in MetaCoq.Erasure.EOptimizePropDiscr]
kn:116 [in MetaCoq.Template.TypingWf]
kn:117 [in MetaCoq.Erasure.EGlobalEnv]
kn:119 [in MetaCoq.Erasure.ErasureProperties]
kn:124 [in MetaCoq.PCUIC.PCUICFirstorder]
kn:1260 [in MetaCoq.Erasure.ErasureFunction]
kn:13 [in MetaCoq.Erasure.ErasureCorrectness]
kn:13 [in MetaCoq.Template.Kernames]
kn:13 [in MetaCoq.Erasure.EEnvMap]
kn:130 [in MetaCoq.Erasure.EDeps]
kn:139 [in MetaCoq.Erasure.ErasureProperties]
kn:14 [in MetaCoq.Template.EnvMap]
kn:140 [in MetaCoq.Translations.translation_utils]
kn:140 [in MetaCoq.Erasure.ErasureProperties]
kn:141 [in MetaCoq.Erasure.ErasureProperties]
kn:1425 [in MetaCoq.Erasure.ErasureFunction]
kn:1442 [in MetaCoq.Erasure.ErasureFunction]
kn:1455 [in MetaCoq.Erasure.ErasureFunction]
kn:146 [in MetaCoq.PCUIC.PCUICFirstorder]
kn:146 [in MetaCoq.Erasure.EWellformed]
kn:147 [in MetaCoq.Erasure.EDeps]
kn:148 [in MetaCoq.PCUIC.PCUICFirstorder]
kn:1484 [in MetaCoq.Erasure.ErasureFunction]
kn:15 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
kn:151 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
kn:152 [in MetaCoq.PCUIC.PCUICFirstorder]
kn:156 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
kn:156 [in MetaCoq.SafeChecker.PCUICWfEnv]
kn:158 [in MetaCoq.Erasure.ERemoveParams]
kn:16 [in MetaCoq.Erasure.ESpineView]
kn:160 [in MetaCoq.Erasure.ERemoveParams]
kn:161 [in MetaCoq.Erasure.EEtaExpanded]
kn:167 [in MetaCoq.Template.Environment]
kn:168 [in MetaCoq.Template.TypingWf]
kn:169 [in MetaCoq.Erasure.EInlineProjections]
kn:17 [in MetaCoq.Erasure.EEnvMap]
kn:171 [in MetaCoq.Template.Environment]
kn:173 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
kn:174 [in MetaCoq.Erasure.Extract]
kn:175 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
kn:179 [in MetaCoq.Erasure.EConstructorsAsBlocks]
kn:179 [in MetaCoq.Erasure.Extract]
kn:180 [in MetaCoq.Erasure.EEtaExpanded]
kn:182 [in MetaCoq.Erasure.EConstructorsAsBlocks]
kn:182 [in MetaCoq.Erasure.EOptimizePropDiscr]
kn:19 [in MetaCoq.Erasure.ErasureCorrectness]
kn:19 [in MetaCoq.Erasure.EEnvMap]
kn:199 [in MetaCoq.Erasure.Extract]
kn:212 [in MetaCoq.Template.TypingWf]
kn:220 [in MetaCoq.Erasure.EConstructorsAsBlocks]
kn:23 [in MetaCoq.Template.EnvironmentTyping]
kn:23 [in MetaCoq.Erasure.EEnvMap]
kn:232 [in MetaCoq.Erasure.EConstructorsAsBlocks]
kn:25 [in MetaCoq.Erasure.EEnvMap]
kn:25 [in MetaCoq.Erasure.EExtends]
kn:26 [in MetaCoq.Erasure.EGlobalEnv]
kn:26 [in MetaCoq.Erasure.EGenericMapEnv]
kn:27 [in MetaCoq.Template.EnvMap]
kn:31 [in MetaCoq.Erasure.EGlobalEnv]
kn:31 [in MetaCoq.Erasure.EGenericMapEnv]
kn:32 [in MetaCoq.Erasure.EEnvMap]
kn:33 [in MetaCoq.Erasure.EGenericMapEnv]
kn:34 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
kn:34 [in MetaCoq.Template.EnvironmentTyping]
kn:34 [in MetaCoq.Erasure.EGlobalEnv]
kn:34 [in MetaCoq.Examples.demo]
kn:341 [in MetaCoq.Erasure.EWcbvEval]
kn:35 [in MetaCoq.Erasure.EGenericMapEnv]
kn:366 [in MetaCoq.PCUIC.PCUICNormal]
kn:37 [in MetaCoq.Template.EnvironmentTyping]
kn:37 [in MetaCoq.Erasure.EGlobalEnv]
kn:37 [in MetaCoq.Erasure.EExtends]
kn:38 [in MetaCoq.SafeChecker.PCUICWfEnv]
kn:4 [in MetaCoq.Erasure.EInlineProjections]
kn:4 [in MetaCoq.SafeChecker.PCUICWfEnv]
kn:40 [in MetaCoq.Erasure.EGlobalEnv]
kn:40 [in MetaCoq.Examples.demo]
kn:40 [in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
kn:406 [in MetaCoq.Erasure.ERemoveParams]
kn:408 [in MetaCoq.Erasure.EWcbvEval]
kn:41 [in MetaCoq.Erasure.Extract]
kn:41 [in MetaCoq.Template.Kernames]
kn:41 [in MetaCoq.Erasure.EEnvMap]
kn:412 [in MetaCoq.Template.Checker]
kn:415 [in MetaCoq.Erasure.EWcbvEval]
kn:42 [in MetaCoq.Erasure.EGlobalEnv]
kn:426 [in MetaCoq.Erasure.EEtaExpandedFix]
kn:43 [in MetaCoq.Erasure.Extract]
kn:43 [in MetaCoq.Erasure.EEnvMap]
kn:446 [in MetaCoq.Erasure.EEtaExpandedFix]
kn:448 [in MetaCoq.Erasure.EWcbvEval]
kn:46 [in MetaCoq.Erasure.EEnvMap]
kn:47 [in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
kn:48 [in MetaCoq.Erasure.EGlobalEnv]
kn:481 [in MetaCoq.Template.EtaExpand]
kn:485 [in MetaCoq.Template.EtaExpand]
kn:489 [in MetaCoq.Template.EtaExpand]
kn:49 [in MetaCoq.Translations.param_original]
kn:492 [in MetaCoq.Template.EtaExpand]
kn:494 [in MetaCoq.Template.EtaExpand]
kn:5 [in MetaCoq.PCUIC.PCUICFirstorder]
kn:509 [in MetaCoq.Erasure.EEtaExpandedFix]
kn:53 [in MetaCoq.Translations.param_binary]
kn:53 [in MetaCoq.Erasure.EEnvMap]
kn:542 [in MetaCoq.Template.EtaExpand]
kn:55 [in MetaCoq.Template.Kernames]
kn:56 [in MetaCoq.Erasure.EWellformed]
kn:57 [in MetaCoq.SafeChecker.PCUICSafeChecker]
kn:59 [in MetaCoq.Template.Kernames]
kn:61 [in MetaCoq.Template.Kernames]
kn:61 [in MetaCoq.Erasure.EGlobalEnv]
kn:61 [in MetaCoq.SafeChecker.PCUICSafeChecker]
kn:62 [in MetaCoq.Erasure.EEnvMap]
kn:64 [in MetaCoq.Template.EnvMap]
kn:657 [in MetaCoq.Template.EnvironmentTyping]
kn:667 [in MetaCoq.Template.EnvironmentTyping]
kn:67 [in MetaCoq.Erasure.EPretty]
kn:69 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
kn:693 [in MetaCoq.Erasure.ErasureFunction]
kn:7 [in MetaCoq.Template.TypingWf]
kn:70 [in MetaCoq.Erasure.EInlineProjections]
kn:75 [in MetaCoq.Erasure.EInlineProjections]
kn:78 [in MetaCoq.Erasure.EInlineProjections]
kn:79 [in MetaCoq.Translations.param_cheap_packed]
kn:8 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
kn:8 [in MetaCoq.SafeChecker.PCUICConsistency]
kn:81 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
kn:81 [in MetaCoq.Translations.param_binary]
kn:81 [in MetaCoq.Erasure.EDeps]
kn:81 [in MetaCoq.Erasure.EInlineProjections]
kn:826 [in MetaCoq.Erasure.ErasureFunction]
kn:83 [in MetaCoq.Erasure.EPretty]
kn:835 [in MetaCoq.Erasure.ErasureFunction]
kn:84 [in MetaCoq.Translations.param_original]
kn:850 [in MetaCoq.Erasure.ErasureFunction]
kn:863 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
kn:87 [in MetaCoq.Erasure.EGenericMapEnv]
kn:877 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
kn:879 [in MetaCoq.Erasure.ErasureFunction]
kn:88 [in MetaCoq.Erasure.EGlobalEnv]
kn:885 [in MetaCoq.Erasure.ErasureFunction]
kn:888 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
kn:890 [in MetaCoq.Erasure.ErasureFunction]
kn:894 [in MetaCoq.Erasure.ErasureFunction]
kn:897 [in MetaCoq.Erasure.ErasureFunction]
kn:9 [in MetaCoq.Erasure.EEnvMap]
kn:90 [in MetaCoq.Translations.times_bool_fun]
kn:903 [in MetaCoq.Erasure.ErasureFunction]
kn:95 [in MetaCoq.Translations.translation_utils]
kn:973 [in MetaCoq.Erasure.ErasureFunction]
kn:999 [in MetaCoq.SafeChecker.PCUICSafeChecker]
k':10 [in MetaCoq.PCUIC.PCUICCSubst]
k':10 [in MetaCoq.Erasure.ELiftSubst]
k':10 [in MetaCoq.Template.WcbvEval]
k':10 [in MetaCoq.Erasure.ECSubst]
k':101 [in MetaCoq.PCUIC.utils.PCUICOnOne]
k':105 [in MetaCoq.PCUIC.PCUICContexts]
k':107 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k':111 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
k':115 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k':12 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
k':1205 [in MetaCoq.PCUIC.PCUICConversion]
k':121 [in MetaCoq.Template.LiftSubst]
k':129 [in MetaCoq.Template.LiftSubst]
k':1325 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
k':140 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
k':149 [in MetaCoq.Template.utils.MCList]
k':151 [in MetaCoq.Erasure.ELiftSubst]
k':153 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
k':156 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
k':16 [in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
k':16 [in MetaCoq.Erasure.EReflect]
k':164 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
k':168 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k':171 [in MetaCoq.PCUIC.PCUICAst]
k':173 [in MetaCoq.PCUIC.PCUICAst]
k':176 [in MetaCoq.Erasure.ELiftSubst]
k':180 [in MetaCoq.Erasure.ELiftSubst]
k':182 [in MetaCoq.PCUIC.PCUICAst]
k':183 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
k':184 [in MetaCoq.PCUIC.PCUICAst]
k':186 [in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
k':186 [in MetaCoq.PCUIC.PCUICSubstitution]
k':19 [in MetaCoq.Template.Kernames]
k':19 [in MetaCoq.Erasure.ELiftSubst]
k':190 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
k':192 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
k':195 [in MetaCoq.PCUIC.PCUICAst]
k':196 [in MetaCoq.PCUIC.PCUICAst]
k':197 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
k':199 [in MetaCoq.PCUIC.PCUICSubstitution]
k':204 [in MetaCoq.PCUIC.PCUICWfUniverses]
k':204 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
k':208 [in MetaCoq.PCUIC.PCUICWfUniverses]
k':208 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
k':208 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k':21 [in MetaCoq.Erasure.ELiftSubst]
k':212 [in MetaCoq.PCUIC.PCUICWfUniverses]
k':215 [in MetaCoq.PCUIC.PCUICAst]
k':216 [in MetaCoq.PCUIC.PCUICWfUniverses]
k':219 [in MetaCoq.PCUIC.PCUICAst]
k':220 [in MetaCoq.PCUIC.PCUICWfUniverses]
k':220 [in MetaCoq.PCUIC.PCUICAst]
k':225 [in MetaCoq.Template.Ast]
k':228 [in MetaCoq.Template.Ast]
k':230 [in MetaCoq.Template.Ast]
k':233 [in MetaCoq.PCUIC.PCUICInductives]
k':237 [in MetaCoq.Template.Ast]
k':239 [in MetaCoq.PCUIC.PCUICInductives]
k':240 [in MetaCoq.Template.Ast]
k':242 [in MetaCoq.Template.BasicAst]
k':242 [in MetaCoq.Template.Ast]
k':243 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k':246 [in MetaCoq.Template.BasicAst]
k':247 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k':250 [in MetaCoq.PCUIC.PCUICInductives]
k':251 [in MetaCoq.PCUIC.PCUICWfUniverses]
k':251 [in MetaCoq.Template.Ast]
k':254 [in MetaCoq.Template.Ast]
k':255 [in MetaCoq.PCUIC.PCUICWfUniverses]
k':255 [in MetaCoq.Template.Ast]
k':26 [in MetaCoq.Template.Environment]
k':261 [in MetaCoq.Template.Ast]
k':265 [in MetaCoq.Template.Ast]
k':266 [in MetaCoq.Template.Ast]
k':27 [in MetaCoq.PCUIC.PCUICAst]
k':280 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k':29 [in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
k':29 [in MetaCoq.Erasure.EWellformed]
k':297 [in MetaCoq.PCUIC.PCUICAst]
k':30 [in MetaCoq.Template.Environment]
k':32 [in MetaCoq.Erasure.ELiftSubst]
k':33 [in MetaCoq.Erasure.ELiftSubst]
k':33 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
k':339 [in MetaCoq.PCUIC.PCUICAst]
k':361 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
k':364 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
k':369 [in MetaCoq.PCUIC.PCUICAst]
k':375 [in MetaCoq.PCUIC.PCUICAst]
k':38 [in MetaCoq.Template.Environment]
k':406 [in MetaCoq.Template.EtaExpand]
k':417 [in MetaCoq.PCUIC.PCUICAst]
k':44 [in MetaCoq.PCUIC.PCUICContextSubst]
k':459 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
k':464 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
k':49 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
k':50 [in MetaCoq.Template.Environment]
k':504 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
k':510 [in MetaCoq.PCUIC.PCUICAst]
k':513 [in MetaCoq.Template.Typing]
k':519 [in MetaCoq.PCUIC.PCUICAst]
k':52 [in MetaCoq.Template.EnvMap]
k':523 [in MetaCoq.Template.Typing]
k':526 [in MetaCoq.PCUIC.PCUICAst]
k':53 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
k':532 [in MetaCoq.Template.utils.All_Forall]
k':537 [in MetaCoq.Template.utils.All_Forall]
k':549 [in MetaCoq.Template.Typing]
k':559 [in MetaCoq.Template.Typing]
k':582 [in MetaCoq.PCUIC.PCUICAst]
k':59 [in MetaCoq.Template.Environment]
k':596 [in MetaCoq.PCUIC.PCUICInductiveInversion]
k':6 [in MetaCoq.Template.WcbvEval]
k':6 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
k':60 [in MetaCoq.Template.EnvMap]
k':60 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
k':604 [in MetaCoq.PCUIC.PCUICInductiveInversion]
k':63 [in MetaCoq.Template.Ast]
k':639 [in MetaCoq.PCUIC.PCUICSpine]
k':64 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
k':644 [in MetaCoq.PCUIC.PCUICSpine]
k':66 [in MetaCoq.Erasure.EWellformed]
k':673 [in MetaCoq.PCUIC.PCUICSpine]
k':68 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
k':69 [in MetaCoq.Erasure.EWellformed]
k':73 [in MetaCoq.Erasure.EWellformed]
k':73 [in MetaCoq.Translations.param_cheap_packed]
k':74 [in MetaCoq.Template.TypingWf]
k':75 [in MetaCoq.Translations.param_cheap_packed]
k':76 [in MetaCoq.PCUIC.PCUICSubstitution]
k':8 [in MetaCoq.PCUIC.PCUICCSubst]
k':8 [in MetaCoq.Erasure.ELiftSubst]
k':8 [in MetaCoq.Template.WcbvEval]
k':8 [in MetaCoq.Erasure.ECSubst]
k':915 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
k':96 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
k:1 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
k:1 [in MetaCoq.Template.LiftSubst]
k:100 [in MetaCoq.PCUIC.utils.PCUICOnOne]
k:100 [in MetaCoq.PCUIC.PCUICInductives]
k:100 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
k:100 [in MetaCoq.Template.Environment]
k:100 [in MetaCoq.Template.LiftSubst]
k:1000 [in MetaCoq.PCUIC.PCUICParallelReduction]
k:1007 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
k:101 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
k:101 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:101 [in MetaCoq.PCUIC.PCUICContexts]
k:102 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
k:1022 [in MetaCoq.PCUIC.PCUICConversion]
k:103 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:103 [in MetaCoq.PCUIC.PCUICContexts]
k:104 [in MetaCoq.Erasure.ESubstitution]
k:104 [in MetaCoq.PCUIC.PCUICElimination]
k:104 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
k:104 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
k:105 [in MetaCoq.Erasure.ELiftSubst]
k:105 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:106 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
k:106 [in MetaCoq.PCUIC.PCUICInductives]
k:106 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
k:107 [in MetaCoq.PCUIC.PCUICContexts]
k:108 [in MetaCoq.PCUIC.utils.PCUICOnOne]
k:108 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
k:108 [in MetaCoq.PCUIC.PCUICAst]
k:108 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
k:108 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:109 [in MetaCoq.Erasure.Extract]
k:109 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
k:11 [in MetaCoq.PCUIC.PCUICCasesContexts]
k:11 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
k:11 [in MetaCoq.Erasure.EReflect]
k:110 [in MetaCoq.PCUIC.PCUICAlpha]
k:111 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
k:111 [in MetaCoq.PCUIC.PCUICInductives]
k:111 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
k:112 [in MetaCoq.PCUIC.PCUICSubstitution]
k:112 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
k:112 [in MetaCoq.Erasure.ELiftSubst]
k:112 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:1120 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
k:113 [in MetaCoq.PCUIC.PCUICContexts]
k:1134 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
k:114 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
k:114 [in MetaCoq.PCUIC.PCUICInductives]
k:114 [in MetaCoq.PCUIC.PCUICFirstorder]
k:114 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:114 [in MetaCoq.Erasure.ERemoveParams]
k:115 [in MetaCoq.Erasure.ELiftSubst]
k:115 [in MetaCoq.PCUIC.PCUICContexts]
k:115 [in MetaCoq.Template.LiftSubst]
k:1164 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
k:1166 [in MetaCoq.Template.utils.wGraph]
k:117 [in MetaCoq.PCUIC.PCUICFirstorder]
k:117 [in MetaCoq.Template.LiftSubst]
k:1172 [in MetaCoq.Translations.MiniHoTT]
k:1179 [in MetaCoq.Template.utils.wGraph]
k:118 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
k:118 [in MetaCoq.Erasure.EInlineProjections]
k:118 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:118 [in MetaCoq.Erasure.ERemoveParams]
k:1180 [in MetaCoq.Translations.MiniHoTT_paths]
k:1183 [in MetaCoq.Translations.MiniHoTT]
k:119 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
k:119 [in MetaCoq.PCUIC.PCUICInductives]
k:119 [in MetaCoq.Template.LiftSubst]
k:1191 [in MetaCoq.Translations.MiniHoTT_paths]
k:12 [in MetaCoq.Template.WfAst]
k:12 [in MetaCoq.Erasure.EDeps]
k:12 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
k:12 [in MetaCoq.Template.LiftSubst]
k:120 [in MetaCoq.PCUIC.PCUICFirstorder]
k:120 [in MetaCoq.Erasure.ELiftSubst]
k:1203 [in MetaCoq.PCUIC.PCUICConversion]
k:1205 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
k:121 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
k:122 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
k:122 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:123 [in MetaCoq.Template.LiftSubst]
k:124 [in MetaCoq.Erasure.EInlineProjections]
k:124 [in MetaCoq.Erasure.ELiftSubst]
k:1241 [in MetaCoq.PCUIC.PCUICConversion]
k:125 [in MetaCoq.Erasure.EEtaExpandedFix]
k:125 [in MetaCoq.Erasure.EConstructorsAsBlocks]
k:125 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
k:125 [in MetaCoq.PCUIC.PCUICSR]
k:126 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
k:126 [in MetaCoq.PCUIC.PCUICInductives]
k:126 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:1265 [in MetaCoq.PCUIC.PCUICConfluence]
k:127 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
k:1274 [in MetaCoq.SafeChecker.PCUICSafeConversion]
k:1275 [in MetaCoq.SafeChecker.PCUICSafeConversion]
k:1276 [in MetaCoq.SafeChecker.PCUICSafeConversion]
k:1276 [in MetaCoq.PCUIC.PCUICConfluence]
k:1277 [in MetaCoq.SafeChecker.PCUICSafeConversion]
k:128 [in MetaCoq.Template.WfAst]
k:128 [in MetaCoq.Erasure.ELiftSubst]
k:128 [in MetaCoq.Erasure.ERemoveParams]
k:128 [in MetaCoq.Template.LiftSubst]
k:129 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
k:129 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
k:129 [in MetaCoq.PCUIC.PCUICSubstitution]
k:129 [in MetaCoq.PCUIC.utils.PCUICOnOne]
k:1297 [in MetaCoq.Template.utils.All_Forall]
k:13 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
k:13 [in MetaCoq.PCUIC.PCUICCSubst]
k:13 [in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
k:13 [in MetaCoq.Erasure.ELiftSubst]
k:130 [in MetaCoq.Erasure.ELiftSubst]
k:130 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
k:130 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:130 [in MetaCoq.Template.TypingWf]
k:131 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
k:132 [in MetaCoq.Template.WfAst]
k:1324 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
k:133 [in MetaCoq.PCUIC.PCUICSubstitution]
k:133 [in MetaCoq.PCUIC.PCUICInductives]
k:133 [in MetaCoq.Erasure.EEtaExpanded]
k:133 [in MetaCoq.Template.LiftSubst]
k:134 [in MetaCoq.Erasure.ELiftSubst]
k:134 [in MetaCoq.PCUIC.PCUICSR]
k:134 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:1346 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
k:135 [in MetaCoq.Template.WfAst]
k:135 [in MetaCoq.PCUIC.PCUICContexts]
k:136 [in MetaCoq.Erasure.EDeps]
k:136 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
k:136 [in MetaCoq.Template.Ast]
k:136 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
k:1361 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
k:137 [in MetaCoq.Template.WfAst]
k:137 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
k:1376 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
k:1377 [in MetaCoq.Template.utils.All_Forall]
k:138 [in MetaCoq.PCUIC.PCUICSubstitution]
k:138 [in MetaCoq.Template.LiftSubst]
k:139 [in MetaCoq.PCUIC.PCUICEquality]
k:139 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:14 [in MetaCoq.PCUIC.PCUICFirstorder]
k:14 [in MetaCoq.PCUIC.PCUICCanonicity]
k:14 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:140 [in MetaCoq.Template.WfAst]
k:140 [in MetaCoq.Erasure.EDeps]
k:140 [in MetaCoq.PCUIC.PCUICContexts]
k:141 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
k:142 [in MetaCoq.PCUIC.PCUICSR]
k:142 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
k:143 [in MetaCoq.Template.TypingWf]
k:143 [in MetaCoq.Template.LiftSubst]
k:144 [in MetaCoq.Template.WfAst]
k:144 [in MetaCoq.PCUIC.PCUICSubstitution]
k:144 [in MetaCoq.Erasure.EConstructorsAsBlocks]
k:144 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
k:144 [in MetaCoq.PCUIC.PCUICContexts]
k:145 [in MetaCoq.Erasure.ELiftSubst]
k:146 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
k:146 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
k:146 [in MetaCoq.Translations.param_cheap_packed]
k:146 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:146 [in MetaCoq.Template.LiftSubst]
k:147 [in MetaCoq.Erasure.ELiftSubst]
k:147 [in MetaCoq.Template.TypingWf]
k:148 [in MetaCoq.Template.utils.MCList]
k:148 [in MetaCoq.Erasure.EDeps]
k:148 [in MetaCoq.Translations.param_cheap_packed]
k:149 [in MetaCoq.Erasure.ELiftSubst]
k:15 [in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
k:15 [in MetaCoq.Template.utils.wGraph]
k:15 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
k:150 [in MetaCoq.PCUIC.PCUICSubstitution]
k:150 [in MetaCoq.Template.Ast]
k:150 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
k:150 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
k:150 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:1502 [in MetaCoq.SafeChecker.PCUICSafeConversion]
k:151 [in MetaCoq.Template.TypingWf]
k:151 [in MetaCoq.Template.LiftSubst]
k:1511 [in MetaCoq.Translations.MiniHoTT]
k:1519 [in MetaCoq.Translations.MiniHoTT_paths]
k:152 [in MetaCoq.Erasure.ELiftSubst]
k:152 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
k:152 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:1523 [in MetaCoq.Translations.MiniHoTT]
k:153 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
k:153 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
k:1531 [in MetaCoq.Translations.MiniHoTT_paths]
k:154 [in MetaCoq.Template.Ast]
k:154 [in MetaCoq.PCUIC.PCUICContexts]
k:155 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
k:155 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:155 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
k:156 [in MetaCoq.Template.utils.MCList]
k:156 [in MetaCoq.PCUIC.PCUICSubstitution]
k:157 [in MetaCoq.Erasure.ELiftSubst]
k:158 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
k:158 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
k:158 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:159 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
k:159 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
k:159 [in MetaCoq.Template.LiftSubst]
k:16 [in MetaCoq.Template.Kernames]
k:16 [in MetaCoq.PCUIC.PCUICCSubst]
k:16 [in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
k:160 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
k:160 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
k:161 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
k:161 [in MetaCoq.Erasure.ELiftSubst]
k:162 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:163 [in MetaCoq.PCUIC.PCUICSubstitution]
k:163 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
k:165 [in MetaCoq.PCUIC.PCUICWfUniverses]
k:165 [in MetaCoq.PCUIC.PCUICAst]
k:165 [in MetaCoq.Erasure.ELiftSubst]
k:166 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
k:166 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:1666 [in MetaCoq.Translations.MiniHoTT]
k:167 [in MetaCoq.Erasure.EEtaExpandedFix]
k:1672 [in MetaCoq.Translations.MiniHoTT]
k:1674 [in MetaCoq.Translations.MiniHoTT_paths]
k:168 [in MetaCoq.Template.utils.MCList]
k:168 [in MetaCoq.PCUIC.PCUICFirstorder]
k:168 [in MetaCoq.Erasure.EEtaExpanded]
k:1680 [in MetaCoq.Translations.MiniHoTT_paths]
k:169 [in MetaCoq.Erasure.ELiftSubst]
k:17 [in MetaCoq.Erasure.EDeps]
k:17 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
k:17 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:17 [in MetaCoq.Erasure.ECSubst]
k:170 [in MetaCoq.Erasure.EEtaExpandedFix]
k:170 [in MetaCoq.Template.utils.MCList]
k:170 [in MetaCoq.PCUIC.PCUICSubstitution]
k:170 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
k:170 [in MetaCoq.PCUIC.PCUICFirstorder]
k:171 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
k:171 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:171 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
k:172 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
k:172 [in MetaCoq.PCUIC.PCUICFirstorder]
k:172 [in MetaCoq.Erasure.ELiftSubst]
k:174 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
k:174 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
k:174 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
k:175 [in MetaCoq.Template.Universes]
k:175 [in MetaCoq.PCUIC.PCUICSubstitution]
k:175 [in MetaCoq.Erasure.ELiftSubst]
k:175 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:176 [in MetaCoq.PCUIC.PCUICAst]
k:177 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
k:177 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
k:178 [in MetaCoq.Template.utils.MCList]
k:178 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
k:178 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
k:179 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
k:179 [in MetaCoq.Erasure.ELiftSubst]
k:179 [in MetaCoq.PCUIC.PCUICSR]
k:179 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:179 [in MetaCoq.Template.LiftSubst]
k:18 [in MetaCoq.PCUIC.Syntax.PCUICUnivSubst]
k:18 [in MetaCoq.PCUIC.PCUICContexts]
k:18 [in MetaCoq.Erasure.EOptimizePropDiscr]
k:180 [in MetaCoq.PCUIC.PCUICEtaExpand]
k:180 [in MetaCoq.Examples.tauto]
k:181 [in MetaCoq.PCUIC.PCUICSubstitution]
k:181 [in MetaCoq.Template.monad_utils]
k:181 [in MetaCoq.PCUIC.PCUICSR]
k:181 [in MetaCoq.PCUIC.PCUICContexts]
k:182 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
k:182 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
k:183 [in MetaCoq.Template.Universes]
k:183 [in MetaCoq.Erasure.ELiftSubst]
k:183 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:184 [in MetaCoq.PCUIC.PCUICSubstitution]
k:185 [in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
k:185 [in MetaCoq.PCUIC.PCUICContexts]
k:186 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
k:187 [in MetaCoq.Template.Universes]
k:187 [in MetaCoq.PCUIC.PCUICAst]
k:187 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
k:188 [in MetaCoq.Examples.tauto]
k:189 [in MetaCoq.PCUIC.PCUICSubstitution]
k:189 [in MetaCoq.PCUIC.PCUICEtaExpand]
k:189 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
k:189 [in MetaCoq.PCUIC.PCUICAst]
k:189 [in MetaCoq.Examples.tauto]
k:19 [in MetaCoq.Template.LiftSubst]
k:190 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
k:190 [in MetaCoq.Examples.tauto]
k:190 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:191 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
k:192 [in MetaCoq.Examples.tauto]
k:193 [in MetaCoq.PCUIC.PCUICSubstitution]
k:193 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
k:194 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
k:195 [in MetaCoq.PCUIC.PCUICWfUniverses]
k:195 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
k:196 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
k:197 [in MetaCoq.PCUIC.PCUICSubstitution]
k:198 [in MetaCoq.PCUIC.PCUICWfUniverses]
k:199 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
k:199 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:2 [in MetaCoq.PCUIC.PCUICCSubst]
k:2 [in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
k:2 [in MetaCoq.Erasure.ELiftSubst]
k:2 [in MetaCoq.Template.EnvMap]
k:2 [in MetaCoq.Template.WcbvEval]
k:2 [in MetaCoq.Translations.standard_model]
k:2 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
k:2 [in MetaCoq.Erasure.ECSubst]
k:20 [in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
k:201 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
k:202 [in MetaCoq.PCUIC.PCUICWfUniverses]
k:202 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
k:203 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:204 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
k:204 [in MetaCoq.Template.Environment]
k:206 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
k:206 [in MetaCoq.PCUIC.PCUICWfUniverses]
k:206 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
k:206 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
k:207 [in MetaCoq.PCUIC.PCUICArities]
k:207 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:209 [in MetaCoq.Template.BasicAst]
k:21 [in MetaCoq.Template.Environment]
k:21 [in MetaCoq.Template.UnivSubst]
k:21 [in MetaCoq.PCUIC.PCUICContexts]
k:210 [in MetaCoq.PCUIC.PCUICWfUniverses]
k:210 [in MetaCoq.PCUIC.PCUICAst]
k:210 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
k:211 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
k:214 [in MetaCoq.PCUIC.PCUICWfUniverses]
k:214 [in MetaCoq.Template.Typing]
k:214 [in MetaCoq.Erasure.EConstructorsAsBlocks]
k:215 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:216 [in MetaCoq.Template.utils.MCList]
k:217 [in MetaCoq.PCUIC.PCUICAst]
k:2179 [in MetaCoq.Template.utils.All_Forall]
k:218 [in MetaCoq.PCUIC.PCUICWfUniverses]
k:218 [in MetaCoq.Template.Typing]
k:218 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
k:218 [in MetaCoq.Template.Environment]
k:2188 [in MetaCoq.Template.utils.All_Forall]
k:219 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:22 [in MetaCoq.Erasure.EDeps]
k:22 [in MetaCoq.PCUIC.PCUICCasesContexts]
k:22 [in MetaCoq.Erasure.ECSubst]
k:22 [in MetaCoq.PCUIC.PCUICContextReduction]
k:22 [in MetaCoq.Erasure.EOptimizePropDiscr]
k:220 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:221 [in MetaCoq.PCUIC.PCUICWfUniverses]
k:221 [in MetaCoq.PCUIC.PCUICInductives]
k:221 [in MetaCoq.Template.Ast]
k:222 [in MetaCoq.Template.BasicAst]
k:222 [in MetaCoq.Template.Typing]
k:222 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:224 [in MetaCoq.PCUIC.PCUICWfUniverses]
k:225 [in MetaCoq.PCUIC.PCUICInductives]
k:227 [in MetaCoq.PCUIC.PCUICWfUniverses]
k:228 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:228 [in MetaCoq.PCUIC.PCUICContexts]
k:229 [in MetaCoq.PCUIC.PCUICAst]
k:23 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
k:23 [in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
k:23 [in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
k:23 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
k:23 [in MetaCoq.Template.LiftSubst]
k:230 [in MetaCoq.Template.Environment]
k:232 [in MetaCoq.PCUIC.PCUICInductives]
k:232 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
k:232 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:233 [in MetaCoq.Template.Ast]
k:233 [in MetaCoq.Template.Environment]
k:235 [in MetaCoq.Template.TypingWf]
k:2355 [in MetaCoq.SafeChecker.PCUICSafeConversion]
k:2356 [in MetaCoq.SafeChecker.PCUICSafeConversion]
k:2357 [in MetaCoq.SafeChecker.PCUICSafeConversion]
k:2358 [in MetaCoq.SafeChecker.PCUICSafeConversion]
k:237 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:238 [in MetaCoq.PCUIC.PCUICSubstitution]
k:238 [in MetaCoq.PCUIC.PCUICInductives]
k:24 [in MetaCoq.Template.EtaExpand]
k:24 [in MetaCoq.Erasure.EInlineProjections]
k:24 [in MetaCoq.Erasure.ELiftSubst]
k:24 [in MetaCoq.Template.Environment]
k:24 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:24 [in MetaCoq.Template.UnivSubst]
k:240 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:242 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
k:242 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:245 [in MetaCoq.Template.Ast]
k:246 [in MetaCoq.PCUIC.PCUICInductives]
k:246 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:247 [in MetaCoq.Template.Ast]
k:249 [in MetaCoq.PCUIC.PCUICWfUniverses]
k:25 [in MetaCoq.Template.TermEquality]
k:25 [in MetaCoq.Erasure.ECSubst]
k:25 [in MetaCoq.Erasure.EOptimizePropDiscr]
k:250 [in MetaCoq.Template.BasicAst]
k:2501 [in MetaCoq.Translations.MiniHoTT]
k:2509 [in MetaCoq.Translations.MiniHoTT_paths]
k:251 [in MetaCoq.Template.BasicAst]
k:253 [in MetaCoq.PCUIC.PCUICWfUniverses]
k:256 [in MetaCoq.Template.Ast]
k:2570 [in MetaCoq.Translations.MiniHoTT]
k:2575 [in MetaCoq.Translations.MiniHoTT]
k:2578 [in MetaCoq.Translations.MiniHoTT_paths]
k:258 [in MetaCoq.PCUIC.PCUICInductives]
k:2583 [in MetaCoq.Translations.MiniHoTT_paths]
k:259 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
k:26 [in MetaCoq.Template.WfAst]
k:26 [in MetaCoq.Erasure.EInlineProjections]
k:26 [in MetaCoq.PCUIC.PCUICAst]
k:26 [in MetaCoq.Erasure.EWellformed]
k:26 [in MetaCoq.Erasure.ELiftSubst]
k:26 [in MetaCoq.PCUIC.PCUICCasesContexts]
k:26 [in MetaCoq.PCUIC.PCUICContexts]
k:261 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
k:261 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
k:262 [in MetaCoq.Template.BasicAst]
k:263 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
k:263 [in MetaCoq.Template.Ast]
k:265 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:266 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
k:268 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
k:268 [in MetaCoq.PCUIC.PCUICInductives]
k:269 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:27 [in MetaCoq.Erasure.EDeps]
k:27 [in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
k:27 [in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
k:27 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
k:27 [in MetaCoq.Erasure.EEtaExpanded]
k:271 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:272 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
k:273 [in MetaCoq.Template.Environment]
k:274 [in MetaCoq.PCUIC.PCUICAst]
k:275 [in MetaCoq.Template.Ast]
k:276 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
k:276 [in MetaCoq.PCUIC.PCUICInductives]
k:276 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:278 [in MetaCoq.Template.Environment]
k:278 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:28 [in MetaCoq.Template.Environment]
k:28 [in MetaCoq.Erasure.ECSubst]
k:28 [in MetaCoq.Erasure.EOptimizePropDiscr]
k:281 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
k:283 [in MetaCoq.PCUIC.PCUICSubstitution]
k:284 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
k:285 [in MetaCoq.PCUIC.PCUICInductives]
k:287 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
k:29 [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
k:29 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:290 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
k:291 [in MetaCoq.PCUIC.PCUICConfluence]
k:292 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
k:294 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
k:296 [in MetaCoq.PCUIC.PCUICAst]
k:296 [in MetaCoq.PCUIC.PCUICSpine]
k:298 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
k:299 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
k:299 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
k:299 [in MetaCoq.PCUIC.PCUICSpine]
k:30 [in MetaCoq.Template.EnvironmentTyping]
k:30 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
k:30 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
k:30 [in MetaCoq.PCUIC.PCUICCasesContexts]
k:301 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
k:301 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
k:302 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
k:302 [in MetaCoq.PCUIC.PCUICSubstitution]
k:302 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
k:303 [in MetaCoq.Template.utils.MCList]
k:303 [in MetaCoq.PCUIC.PCUICSpine]
k:304 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
k:305 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
k:307 [in MetaCoq.PCUIC.PCUICSubstitution]
k:307 [in MetaCoq.PCUIC.PCUICSpine]
k:308 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
k:308 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
k:308 [in MetaCoq.PCUIC.PCUICConversion]
k:31 [in MetaCoq.Template.WfAst]
k:31 [in MetaCoq.PCUIC.PCUICAst]
k:31 [in MetaCoq.PCUIC.Syntax.PCUICUnivSubst]
k:31 [in MetaCoq.PCUIC.TemplateToPCUICExpanded]
k:310 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
k:310 [in MetaCoq.Template.Environment]
k:311 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
k:313 [in MetaCoq.Template.Environment]
k:314 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
k:314 [in MetaCoq.PCUIC.PCUICSpine]
k:315 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
k:316 [in MetaCoq.Template.utils.MCList]
k:317 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
k:318 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
k:32 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
k:32 [in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
k:32 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
k:32 [in MetaCoq.Erasure.ECSubst]
k:320 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
k:321 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
k:324 [in MetaCoq.Template.utils.MCList]
k:324 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
k:325 [in MetaCoq.Template.utils.MCList]
k:325 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
k:326 [in MetaCoq.PCUIC.PCUICInductiveInversion]
k:326 [in MetaCoq.PCUIC.PCUICAst]
k:327 [in MetaCoq.Erasure.EWcbvEval]
k:329 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
k:33 [in MetaCoq.PCUIC.PCUICAst]
k:33 [in MetaCoq.Erasure.EWellformed]
k:33 [in MetaCoq.Template.Environment]
k:33 [in MetaCoq.PCUIC.Conversion.PCUICClosedConv]
k:330 [in MetaCoq.Erasure.EEtaExpandedFix]
k:330 [in MetaCoq.SafeChecker.PCUICSafeChecker]
k:331 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
k:331 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
k:334 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
k:336 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
k:338 [in MetaCoq.Erasure.EEtaExpandedFix]
k:338 [in MetaCoq.PCUIC.PCUICAst]
k:338 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
k:34 [in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
k:34 [in MetaCoq.Erasure.ELiftSubst]
k:34 [in MetaCoq.PCUIC.Syntax.PCUICUnivSubst]
k:34 [in MetaCoq.Erasure.EOptimizePropDiscr]
k:340 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
k:341 [in MetaCoq.Template.common.uGraph]
k:343 [in MetaCoq.PCUIC.PCUICSubstitution]
k:344 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
k:345 [in MetaCoq.Template.utils.MCList]
k:345 [in MetaCoq.Template.common.uGraph]
k:346 [in MetaCoq.Template.utils.MCList]
k:346 [in MetaCoq.PCUIC.PCUICAst]
k:347 [in MetaCoq.Template.EtaExpand]
k:348 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
k:348 [in MetaCoq.PCUIC.PCUICAst]
k:35 [in MetaCoq.PCUIC.PCUICAst]
k:35 [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
k:35 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:35 [in MetaCoq.Template.LiftSubst]
k:350 [in MetaCoq.PCUIC.PCUICSubstitution]
k:351 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
k:352 [in MetaCoq.Template.utils.MCList]
k:352 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
k:352 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
k:353 [in MetaCoq.PCUIC.PCUICAst]
k:355 [in MetaCoq.PCUIC.PCUICAst]
k:357 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
k:358 [in MetaCoq.PCUIC.PCUICSubstitution]
k:359 [in MetaCoq.Template.BasicAst]
k:359 [in MetaCoq.Template.utils.MCList]
k:36 [in MetaCoq.Erasure.ESubstitution]
k:36 [in MetaCoq.Template.Environment]
k:36 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
k:36 [in MetaCoq.Erasure.ECSubst]
k:360 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
k:365 [in MetaCoq.Template.utils.MCList]
k:365 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
k:367 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
k:367 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
k:368 [in MetaCoq.PCUIC.PCUICSubstitution]
k:368 [in MetaCoq.PCUIC.PCUICAst]
k:369 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
k:37 [in MetaCoq.PCUIC.PCUICAst]
k:37 [in MetaCoq.Erasure.ELiftSubst]
k:37 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
k:37 [in MetaCoq.Erasure.EOptimizePropDiscr]
k:371 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
k:373 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
k:374 [in MetaCoq.PCUIC.PCUICAst]
k:375 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
k:375 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
k:377 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
k:38 [in MetaCoq.Erasure.ESubstitution]
k:38 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
k:38 [in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
k:38 [in MetaCoq.PCUIC.PCUICContextSubst]
k:380 [in MetaCoq.PCUIC.PCUICAst]
k:382 [in MetaCoq.Template.utils.wGraph]
k:382 [in MetaCoq.PCUIC.PCUICAst]
K:383 [in MetaCoq.Template.common.uGraph]
k:384 [in MetaCoq.Erasure.ERemoveParams]
k:385 [in MetaCoq.PCUIC.PCUICAst]
K:386 [in MetaCoq.Template.common.uGraph]
k:387 [in MetaCoq.PCUIC.PCUICAst]
k:39 [in MetaCoq.PCUIC.PCUICAst]
k:39 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
k:39 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
K:390 [in MetaCoq.Template.common.uGraph]
k:391 [in MetaCoq.PCUIC.PCUICSpine]
k:392 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
K:393 [in MetaCoq.Template.common.uGraph]
k:394 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
k:396 [in MetaCoq.PCUIC.PCUICEquality]
k:398 [in MetaCoq.PCUIC.PCUICSpine]
k:4 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
k:4 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
k:4 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
k:4 [in MetaCoq.Template.EnvMap]
k:4 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
k:4 [in MetaCoq.Template.LiftSubst]
k:40 [in MetaCoq.Template.Environment]
k:40 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:40 [in MetaCoq.Erasure.ECSubst]
k:40 [in MetaCoq.Template.LiftSubst]
k:400 [in MetaCoq.PCUIC.PCUICEquality]
k:401 [in MetaCoq.PCUIC.PCUICSpine]
k:403 [in MetaCoq.Erasure.EEtaExpandedFix]
k:404 [in MetaCoq.Template.EtaExpand]
k:404 [in MetaCoq.Template.Typing]
k:405 [in MetaCoq.PCUIC.PCUICSpine]
k:406 [in MetaCoq.PCUIC.PCUICEquality]
k:409 [in MetaCoq.Template.Typing]
k:41 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
k:41 [in MetaCoq.Erasure.EWellformed]
k:41 [in MetaCoq.Erasure.ELiftSubst]
k:411 [in MetaCoq.PCUIC.PCUICSpine]
k:412 [in MetaCoq.PCUIC.PCUICEquality]
k:414 [in MetaCoq.Template.Typing]
k:414 [in MetaCoq.PCUIC.PCUICSpine]
k:416 [in MetaCoq.PCUIC.PCUICAst]
k:419 [in MetaCoq.PCUIC.PCUICSpine]
k:42 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
k:42 [in MetaCoq.PCUIC.PCUICContextSubst]
k:420 [in MetaCoq.PCUIC.PCUICEquality]
k:425 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
k:425 [in MetaCoq.PCUIC.PCUICAst]
k:429 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
k:43 [in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
k:43 [in MetaCoq.Erasure.ECSubst]
k:43 [in MetaCoq.Translations.param_original]
k:430 [in MetaCoq.PCUIC.PCUICEquality]
k:433 [in MetaCoq.Erasure.EEtaExpandedFix]
k:434 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
k:435 [in MetaCoq.PCUIC.PCUICEquality]
k:436 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
k:436 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
k:438 [in MetaCoq.Template.utils.MCList]
k:44 [in MetaCoq.Template.WfAst]
k:44 [in MetaCoq.Erasure.Extract]
k:44 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:44 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
k:44 [in MetaCoq.Translations.param_original]
k:44 [in MetaCoq.Template.LiftSubst]
k:442 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
k:442 [in MetaCoq.PCUIC.PCUICEquality]
k:442 [in MetaCoq.PCUIC.PCUICAst]
k:45 [in MetaCoq.Erasure.ELiftSubst]
k:451 [in MetaCoq.SafeChecker.PCUICTypeChecker]
k:453 [in MetaCoq.PCUIC.PCUICAst]
k:458 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
k:459 [in MetaCoq.PCUIC.PCUICInductives]
k:46 [in MetaCoq.PCUIC.PCUICAst]
k:46 [in MetaCoq.Template.EnvMap]
k:46 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:46 [in MetaCoq.Erasure.ECSubst]
k:465 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
k:47 [in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
k:47 [in MetaCoq.Template.WfAst]
k:47 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
k:47 [in MetaCoq.PCUIC.PCUICContextSubst]
k:47 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
k:473 [in MetaCoq.PCUIC.PCUICInductives]
k:476 [in MetaCoq.PCUIC.PCUICEquality]
k:477 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
k:479 [in MetaCoq.Template.EnvironmentTyping]
k:479 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
k:48 [in MetaCoq.Erasure.ELiftSubst]
k:48 [in MetaCoq.Template.EnvMap]
k:48 [in MetaCoq.Template.Environment]
k:48 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
k:48 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
k:481 [in MetaCoq.PCUIC.PCUICInductiveInversion]
k:482 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
k:483 [in MetaCoq.PCUIC.PCUICEquality]
k:484 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
k:486 [in MetaCoq.PCUIC.PCUICNormal]
k:486 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
k:489 [in MetaCoq.PCUIC.PCUICAst]
k:49 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:492 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
k:495 [in MetaCoq.PCUIC.PCUICAst]
k:498 [in MetaCoq.PCUIC.PCUICSubstitution]
k:499 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
k:499 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
k:50 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
k:50 [in MetaCoq.PCUIC.PCUICAst]
k:50 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
k:50 [in MetaCoq.Template.LiftSubst]
k:500 [in MetaCoq.Template.utils.All_Forall]
k:500 [in MetaCoq.PCUIC.PCUICAst]
k:502 [in MetaCoq.PCUIC.PCUICSubstitution]
k:503 [in MetaCoq.PCUIC.PCUICAst]
k:504 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
k:506 [in MetaCoq.PCUIC.PCUICSubstitution]
k:507 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
k:509 [in MetaCoq.PCUIC.PCUICAst]
k:51 [in MetaCoq.Template.EnvMap]
k:51 [in MetaCoq.PCUIC.TemplateToPCUICExpanded]
k:510 [in MetaCoq.PCUIC.PCUICSubstitution]
k:510 [in MetaCoq.PCUIC.PCUICSpine]
k:511 [in MetaCoq.Template.utils.All_Forall]
k:512 [in MetaCoq.PCUIC.PCUICSpine]
k:514 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
k:514 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
k:517 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
k:518 [in MetaCoq.PCUIC.PCUICAst]
k:519 [in MetaCoq.Template.utils.All_Forall]
k:519 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
k:52 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
k:52 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
k:522 [in MetaCoq.Template.Typing]
k:522 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
k:525 [in MetaCoq.Template.utils.All_Forall]
k:525 [in MetaCoq.PCUIC.PCUICAst]
k:527 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
k:529 [in MetaCoq.PCUIC.PCUICInductiveInversion]
k:529 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
k:53 [in MetaCoq.Template.Environment]
k:530 [in MetaCoq.Template.utils.All_Forall]
k:531 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
k:531 [in MetaCoq.PCUIC.PCUICAst]
k:532 [in MetaCoq.PCUIC.PCUICInductiveInversion]
k:533 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
k:534 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
k:535 [in MetaCoq.Template.utils.All_Forall]
k:536 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
k:54 [in MetaCoq.PCUIC.PCUICContextReduction]
k:540 [in MetaCoq.PCUIC.PCUICInductiveInversion]
k:542 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
k:545 [in MetaCoq.PCUIC.PCUICInductives]
k:548 [in MetaCoq.PCUIC.PCUICAst]
k:55 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
k:55 [in MetaCoq.PCUIC.PCUICSR]
k:55 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:550 [in MetaCoq.Template.utils.All_Forall]
k:550 [in MetaCoq.PCUIC.PCUICInductives]
k:553 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
k:554 [in MetaCoq.PCUIC.PCUICInductives]
k:554 [in MetaCoq.PCUIC.PCUICAst]
k:556 [in MetaCoq.Template.utils.All_Forall]
k:558 [in MetaCoq.Template.Typing]
k:56 [in MetaCoq.PCUIC.PCUICInductives]
k:56 [in MetaCoq.Template.EnvMap]
k:562 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
k:563 [in MetaCoq.Template.utils.All_Forall]
k:564 [in MetaCoq.PCUIC.PCUICInductives]
k:565 [in MetaCoq.Template.utils.All_Forall]
k:565 [in MetaCoq.Template.utils.MCList]
k:566 [in MetaCoq.Template.utils.wGraph]
k:568 [in MetaCoq.PCUIC.PCUICInductives]
k:57 [in MetaCoq.PCUIC.PCUICValidity]
k:57 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
k:57 [in MetaCoq.Template.Environment]
k:57 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
k:570 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
k:572 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
k:574 [in MetaCoq.PCUIC.PCUICInductives]
k:576 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
k:576 [in MetaCoq.PCUIC.PCUICAst]
k:577 [in MetaCoq.Template.utils.MCList]
k:577 [in MetaCoq.PCUIC.PCUICSR]
k:578 [in MetaCoq.PCUIC.PCUICSR]
k:579 [in MetaCoq.PCUIC.PCUICConversion]
k:580 [in MetaCoq.Template.common.uGraph]
k:580 [in MetaCoq.PCUIC.PCUICAst]
k:580 [in MetaCoq.PCUIC.PCUICConversion]
k:581 [in MetaCoq.Template.EnvironmentTyping]
k:582 [in MetaCoq.PCUIC.PCUICInductives]
k:585 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
k:585 [in MetaCoq.PCUIC.PCUICAst]
k:587 [in MetaCoq.PCUIC.PCUICInductives]
k:59 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
k:59 [in MetaCoq.Template.EnvMap]
k:59 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
k:594 [in MetaCoq.Template.EnvironmentTyping]
k:595 [in MetaCoq.PCUIC.PCUICInductiveInversion]
k:599 [in MetaCoq.PCUIC.PCUICInductiveInversion]
k:6 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:60 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
k:60 [in MetaCoq.Translations.param_original]
k:60 [in MetaCoq.Template.LiftSubst]
k:600 [in MetaCoq.PCUIC.PCUICInductives]
k:600 [in MetaCoq.PCUIC.PCUICConversion]
k:603 [in MetaCoq.PCUIC.PCUICInductiveInversion]
k:603 [in MetaCoq.PCUIC.PCUICSpine]
k:604 [in MetaCoq.PCUIC.PCUICSpine]
k:605 [in MetaCoq.PCUIC.PCUICInductives]
k:606 [in MetaCoq.PCUIC.PCUICSpine]
k:609 [in MetaCoq.Template.Typing]
k:61 [in MetaCoq.Erasure.EWellformed]
k:61 [in MetaCoq.PCUIC.PCUICCasesContexts]
k:61 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:610 [in MetaCoq.PCUIC.PCUICInductiveInversion]
k:612 [in MetaCoq.PCUIC.PCUICParallelReduction]
k:614 [in MetaCoq.PCUIC.PCUICParallelReduction]
K:615 [in MetaCoq.Template.utils.wGraph]
k:62 [in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
k:62 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
k:62 [in MetaCoq.Translations.param_original]
k:620 [in MetaCoq.PCUIC.PCUICParallelReduction]
k:627 [in MetaCoq.PCUIC.PCUICInductives]
k:63 [in MetaCoq.Template.TermEquality]
k:63 [in MetaCoq.PCUIC.Typing.PCUICWeakeningTyp]
k:63 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
k:63 [in MetaCoq.Erasure.EGenericMapEnv]
k:635 [in MetaCoq.PCUIC.PCUICConversion]
k:637 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
k:637 [in MetaCoq.PCUIC.PCUICSpine]
k:64 [in MetaCoq.Translations.param_binary]
k:64 [in MetaCoq.Erasure.EWellformed]
k:640 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
k:640 [in MetaCoq.PCUIC.PCUICSpine]
K:641 [in MetaCoq.Template.utils.wGraph]
K:642 [in MetaCoq.Template.utils.wGraph]
k:643 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
k:643 [in MetaCoq.PCUIC.PCUICSpine]
k:647 [in MetaCoq.PCUIC.PCUICSR]
k:647 [in MetaCoq.PCUIC.PCUICSpine]
k:65 [in MetaCoq.PCUIC.PCUICInductives]
k:65 [in MetaCoq.Template.utils.wGraph]
k:65 [in MetaCoq.PCUIC.PCUICAst]
k:651 [in MetaCoq.PCUIC.PCUICSpine]
k:654 [in MetaCoq.PCUIC.PCUICSpine]
k:66 [in MetaCoq.Translations.param_binary]
k:66 [in MetaCoq.Erasure.ELiftSubst]
k:662 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
K:662 [in MetaCoq.Template.utils.wGraph]
k:662 [in MetaCoq.PCUIC.PCUICSpine]
k:665 [in MetaCoq.PCUIC.PCUICSpine]
k:668 [in MetaCoq.PCUIC.PCUICSpine]
k:67 [in MetaCoq.Template.Ast]
k:67 [in MetaCoq.Translations.param_cheap_packed]
k:67 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
k:672 [in MetaCoq.PCUIC.PCUICSpine]
k:674 [in MetaCoq.PCUIC.PCUICSR]
k:68 [in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
k:68 [in MetaCoq.PCUIC.PCUICSubstitution]
k:68 [in MetaCoq.PCUIC.PCUICAlpha]
k:68 [in MetaCoq.Erasure.EWellformed]
k:68 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:680 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
k:689 [in MetaCoq.Template.utils.MCList]
k:689 [in MetaCoq.PCUIC.PCUICSpine]
k:69 [in MetaCoq.Template.Ast]
k:69 [in MetaCoq.PCUIC.PCUICAlpha]
k:69 [in MetaCoq.Template.EnvMap]
k:692 [in MetaCoq.PCUIC.PCUICSpine]
K:693 [in MetaCoq.Template.utils.wGraph]
K:694 [in MetaCoq.Template.utils.wGraph]
k:7 [in MetaCoq.Translations.param_binary]
k:7 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
k:7 [in MetaCoq.Template.EnvMap]
k:70 [in MetaCoq.Template.TermEquality]
k:70 [in MetaCoq.Erasure.ELiftSubst]
k:71 [in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
k:71 [in MetaCoq.PCUIC.PCUICSubstitution]
k:71 [in MetaCoq.Template.Ast]
k:71 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
k:71 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
k:71 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:71 [in MetaCoq.Template.LiftSubst]
K:710 [in MetaCoq.Template.utils.wGraph]
K:711 [in MetaCoq.Template.utils.wGraph]
k:718 [in MetaCoq.PCUIC.PCUICInductiveInversion]
k:718 [in MetaCoq.PCUIC.PCUICEquality]
k:72 [in MetaCoq.Erasure.EWellformed]
k:72 [in MetaCoq.Template.TypingWf]
k:721 [in MetaCoq.PCUIC.PCUICInductiveInversion]
k:722 [in MetaCoq.PCUIC.PCUICEquality]
k:728 [in MetaCoq.Template.Universes]
k:73 [in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
k:73 [in MetaCoq.Template.Ast]
k:74 [in MetaCoq.PCUIC.PCUICSubstitution]
k:74 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
k:746 [in MetaCoq.PCUIC.PCUICInductiveInversion]
k:75 [in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
k:75 [in MetaCoq.Template.Ast]
k:76 [in MetaCoq.Erasure.EWellformed]
k:76 [in MetaCoq.Template.Checker]
k:76 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
k:76 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:77 [in MetaCoq.Erasure.ELiftSubst]
k:77 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
k:770 [in MetaCoq.PCUIC.PCUICSpine]
k:779 [in MetaCoq.PCUIC.PCUICSpine]
k:78 [in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
k:78 [in MetaCoq.Template.utils.All_Forall]
k:78 [in MetaCoq.Template.LiftSubst]
k:785 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
k:79 [in MetaCoq.PCUIC.PCUICWfUniverses]
k:79 [in MetaCoq.Template.Ast]
k:79 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
k:79 [in MetaCoq.Erasure.EWellformed]
k:79 [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
k:79 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
k:79 [in MetaCoq.Template.TypingWf]
k:80 [in MetaCoq.PCUIC.PCUICWfUniverses]
k:80 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:80 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
k:804 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
k:809 [in MetaCoq.PCUIC.PCUICParallelReduction]
k:81 [in MetaCoq.PCUIC.PCUICSubstitution]
k:81 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
k:81 [in MetaCoq.Template.Checker]
k:81 [in MetaCoq.Erasure.ELiftSubst]
k:81 [in MetaCoq.Template.LiftSubst]
k:819 [in MetaCoq.PCUIC.PCUICInductiveInversion]
k:82 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
k:82 [in MetaCoq.Erasure.EWellformed]
k:829 [in MetaCoq.PCUIC.PCUICInductiveInversion]
k:83 [in MetaCoq.PCUIC.PCUICWfUniverses]
k:83 [in MetaCoq.PCUIC.PCUICAst]
k:83 [in MetaCoq.Erasure.ELiftSubst]
k:837 [in MetaCoq.SafeChecker.PCUICSafeChecker]
k:839 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
k:84 [in MetaCoq.PCUIC.PCUICWfUniverses]
k:84 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
k:84 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:842 [in MetaCoq.PCUIC.PCUICParallelReduction]
k:844 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
k:85 [in MetaCoq.PCUIC.PCUICAst]
k:856 [in MetaCoq.SafeChecker.PCUICSafeChecker]
k:86 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:86 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
k:86 [in MetaCoq.Template.LiftSubst]
k:860 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
k:869 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
k:87 [in MetaCoq.PCUIC.PCUICAst]
k:87 [in MetaCoq.Template.Checker]
k:88 [in MetaCoq.PCUIC.PCUICWfUniverses]
k:88 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
k:88 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
k:89 [in MetaCoq.PCUIC.PCUICInductives]
k:894 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
k:9 [in MetaCoq.PCUIC.Conversion.PCUICOnFreeVarsConv]
k:9 [in MetaCoq.PCUIC.PCUICFirstorder]
k:9 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:9 [in MetaCoq.Template.UnivSubst]
k:9 [in MetaCoq.Template.LiftSubst]
k:90 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
k:90 [in MetaCoq.Erasure.ELiftSubst]
k:90 [in MetaCoq.Template.Environment]
k:90 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
k:90 [in MetaCoq.Template.LiftSubst]
k:902 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
k:909 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
k:909 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
k:91 [in MetaCoq.PCUIC.PCUICWfUniverses]
k:91 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
k:914 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
k:919 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
k:92 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
k:92 [in MetaCoq.PCUIC.PCUICInductives]
k:92 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
k:92 [in MetaCoq.PCUIC.PCUICContexts]
k:926 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
k:928 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
k:93 [in MetaCoq.PCUIC.PCUICSubstitution]
k:93 [in MetaCoq.Erasure.ELiftSubst]
k:932 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
k:94 [in MetaCoq.PCUIC.PCUICWfUniverses]
k:94 [in MetaCoq.PCUIC.PCUICContexts]
k:94 [in MetaCoq.Template.LiftSubst]
k:947 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
k:95 [in MetaCoq.Template.TermEquality]
k:95 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
k:95 [in MetaCoq.Template.Environment]
k:96 [in MetaCoq.PCUIC.PCUICInductives]
k:96 [in MetaCoq.Template.LiftSubst]
k:963 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
k:97 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
k:97 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
k:974 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
k:98 [in MetaCoq.PCUIC.PCUICCanonicity]
k:98 [in MetaCoq.PCUIC.PCUICContexts]
k:981 [in MetaCoq.Template.Typing]
k:988 [in MetaCoq.PCUIC.PCUICParallelReduction]
k:99 [in MetaCoq.PCUIC.PCUICWfUniverses]
k:99 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
k:99 [in MetaCoq.Erasure.ELiftSubst]
k:991 [in MetaCoq.PCUIC.PCUICParallelReduction]
k:992 [in MetaCoq.PCUIC.PCUICParallelReduction]
k:993 [in MetaCoq.PCUIC.PCUICParallelReduction]
k:994 [in MetaCoq.PCUIC.PCUICParallelReduction]
k:995 [in MetaCoq.PCUIC.PCUICParallelReduction]
k:996 [in MetaCoq.PCUIC.PCUICParallelReduction]
k:997 [in MetaCoq.PCUIC.PCUICParallelReduction]
k:998 [in MetaCoq.PCUIC.PCUICParallelReduction]
k:999 [in MetaCoq.PCUIC.PCUICParallelReduction]
| 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) |