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)

E (binder)

eA:101 [in MetaCoq.PCUIC.utils.PCUICUtils]
ea:141 [in MetaCoq.SafeChecker.PCUICEqualityDec]
eA:18 [in MetaCoq.PCUIC.utils.PCUICUtils]
eA:59 [in MetaCoq.PCUIC.utils.PCUICUtils]
ecb:1254 [in MetaCoq.Erasure.ErasureFunction]
edges:201 [in MetaCoq.SafeChecker.PCUICErrors]
edges:209 [in MetaCoq.Template.common.uGraph]
edges:538 [in MetaCoq.Template.common.uGraph]
edges:539 [in MetaCoq.Template.common.uGraph]
efl:1 [in MetaCoq.Erasure.EInlineProjections]
efl:1 [in MetaCoq.Erasure.EProgram]
efl:1 [in MetaCoq.Erasure.EExtends]
efl:101 [in MetaCoq.Erasure.EOptimizePropDiscr]
efl:102 [in MetaCoq.Erasure.EInlineProjections]
efl:106 [in MetaCoq.Erasure.ETransform]
efl:109 [in MetaCoq.Erasure.EOptimizePropDiscr]
efl:11 [in MetaCoq.Erasure.EGenericMapEnv]
efl:111 [in MetaCoq.Erasure.EWellformed]
efl:112 [in MetaCoq.Erasure.EOptimizePropDiscr]
efl:113 [in MetaCoq.Erasure.EWellformed]
efl:115 [in MetaCoq.Erasure.EOptimizePropDiscr]
efl:118 [in MetaCoq.Erasure.EWellformed]
efl:118 [in MetaCoq.Erasure.EOptimizePropDiscr]
efl:1186 [in MetaCoq.Erasure.ErasureFunction]
efl:1195 [in MetaCoq.Erasure.ErasureFunction]
efl:1205 [in MetaCoq.Erasure.ErasureFunction]
efl:1217 [in MetaCoq.Erasure.ErasureFunction]
efl:124 [in MetaCoq.Erasure.EWellformed]
efl:128 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
efl:130 [in MetaCoq.Erasure.EWellformed]
efl:130 [in MetaCoq.Erasure.EOptimizePropDiscr]
efl:135 [in MetaCoq.Erasure.EWellformed]
efl:137 [in MetaCoq.Erasure.EInlineProjections]
efl:14 [in MetaCoq.Erasure.EProgram]
efl:140 [in MetaCoq.Erasure.EWellformed]
efl:140 [in MetaCoq.Erasure.EOptimizePropDiscr]
efl:142 [in MetaCoq.Erasure.EInlineProjections]
efl:144 [in MetaCoq.Erasure.EWellformed]
efl:145 [in MetaCoq.Erasure.EInlineProjections]
efl:148 [in MetaCoq.Erasure.EInlineProjections]
efl:15 [in MetaCoq.Erasure.ErasureCorrectness]
efl:150 [in MetaCoq.Erasure.EInlineProjections]
efl:152 [in MetaCoq.Erasure.EOptimizePropDiscr]
efl:153 [in MetaCoq.Erasure.EInlineProjections]
efl:1534 [in MetaCoq.Erasure.ErasureFunction]
efl:154 [in MetaCoq.Erasure.EInlineProjections]
efl:157 [in MetaCoq.Erasure.EOptimizePropDiscr]
efl:158 [in MetaCoq.Erasure.EInlineProjections]
efl:160 [in MetaCoq.Erasure.EOptimizePropDiscr]
efl:162 [in MetaCoq.Erasure.EInlineProjections]
efl:163 [in MetaCoq.Erasure.EOptimizePropDiscr]
efl:164 [in MetaCoq.Erasure.EEtaExpanded]
efl:165 [in MetaCoq.Erasure.EInlineProjections]
efl:165 [in MetaCoq.Erasure.EOptimizePropDiscr]
efl:167 [in MetaCoq.Erasure.EOptimizePropDiscr]
efl:170 [in MetaCoq.Erasure.EInlineProjections]
efl:170 [in MetaCoq.Erasure.EEtaExpanded]
efl:171 [in MetaCoq.Erasure.EOptimizePropDiscr]
efl:173 [in MetaCoq.Erasure.EInlineProjections]
efl:174 [in MetaCoq.Erasure.EEtaExpanded]
efl:175 [in MetaCoq.Erasure.EOptimizePropDiscr]
efl:177 [in MetaCoq.Erasure.EInlineProjections]
efl:178 [in MetaCoq.Erasure.EEtaExpanded]
efl:178 [in MetaCoq.Erasure.EOptimizePropDiscr]
efl:183 [in MetaCoq.Erasure.EOptimizePropDiscr]
efl:186 [in MetaCoq.Erasure.EOptimizePropDiscr]
efl:190 [in MetaCoq.Erasure.EOptimizePropDiscr]
efl:2 [in MetaCoq.Erasure.EInlineProjections]
efl:2 [in MetaCoq.Erasure.Erasure]
efl:23 [in MetaCoq.Erasure.EWellformed]
efl:3 [in MetaCoq.Erasure.EProgram]
efl:310 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
efl:312 [in MetaCoq.Erasure.EWcbvEval]
efl:351 [in MetaCoq.Erasure.EWcbvEval]
efl:365 [in MetaCoq.Erasure.ERemoveParams]
efl:369 [in MetaCoq.Erasure.ERemoveParams]
efl:38 [in MetaCoq.Erasure.ETransform]
efl:39 [in MetaCoq.Erasure.EWellformed]
efl:394 [in MetaCoq.Erasure.ERemoveParams]
efl:398 [in MetaCoq.Erasure.ERemoveParams]
efl:401 [in MetaCoq.Erasure.ERemoveParams]
efl:402 [in MetaCoq.Erasure.ERemoveParams]
efl:419 [in MetaCoq.Erasure.ERemoveParams]
efl:424 [in MetaCoq.Erasure.ERemoveParams]
efl:429 [in MetaCoq.Erasure.EEtaExpandedFix]
efl:429 [in MetaCoq.Erasure.ERemoveParams]
efl:433 [in MetaCoq.Erasure.ERemoveParams]
efl:435 [in MetaCoq.Erasure.EEtaExpandedFix]
efl:436 [in MetaCoq.Erasure.ERemoveParams]
efl:438 [in MetaCoq.Erasure.ERemoveParams]
efl:440 [in MetaCoq.Erasure.EEtaExpandedFix]
efl:440 [in MetaCoq.Erasure.ERemoveParams]
efl:444 [in MetaCoq.Erasure.EEtaExpandedFix]
efl:444 [in MetaCoq.Erasure.ERemoveParams]
efl:449 [in MetaCoq.Erasure.EEtaExpandedFix]
efl:449 [in MetaCoq.Erasure.ERemoveParams]
efl:451 [in MetaCoq.Erasure.ERemoveParams]
efl:46 [in MetaCoq.Erasure.EWellformed]
efl:48 [in MetaCoq.Erasure.EWellformed]
efl:48 [in MetaCoq.Erasure.ETransform]
efl:491 [in MetaCoq.Erasure.EEtaExpandedFix]
efl:496 [in MetaCoq.Erasure.EEtaExpandedFix]
efl:5 [in MetaCoq.Erasure.Erasure]
efl:52 [in MetaCoq.Erasure.ETransform]
efl:53 [in MetaCoq.Erasure.EWellformed]
efl:55 [in MetaCoq.Erasure.EInlineProjections]
efl:551 [in MetaCoq.Erasure.EEtaExpandedFix]
efl:560 [in MetaCoq.Erasure.EEtaExpandedFix]
efl:59 [in MetaCoq.Erasure.EWellformed]
efl:6 [in MetaCoq.Erasure.EInlineProjections]
efl:63 [in MetaCoq.Erasure.ETransform]
efl:68 [in MetaCoq.Erasure.EInlineProjections]
efl:74 [in MetaCoq.Erasure.ETransform]
efl:76 [in MetaCoq.Erasure.EInlineProjections]
efl:79 [in MetaCoq.Erasure.EInlineProjections]
efl:82 [in MetaCoq.Erasure.EInlineProjections]
efl:84 [in MetaCoq.Erasure.ETransform]
efl:85 [in MetaCoq.Erasure.EInlineProjections]
efl:88 [in MetaCoq.Erasure.EOptimizePropDiscr]
efl:96 [in MetaCoq.Erasure.ETransform]
efl:98 [in MetaCoq.Erasure.EInlineProjections]
ei:1477 [in MetaCoq.SafeChecker.PCUICSafeConversion]
ei:1950 [in MetaCoq.SafeChecker.PCUICSafeConversion]
ei:357 [in MetaCoq.Template.common.uGraph]
ei:373 [in MetaCoq.Template.common.uGraph]
ei:374 [in MetaCoq.Template.common.uGraph]
ei:377 [in MetaCoq.Template.common.uGraph]
ei:380 [in MetaCoq.Template.common.uGraph]
ei:384 [in MetaCoq.Template.common.uGraph]
ei:387 [in MetaCoq.Template.common.uGraph]
ei:389 [in MetaCoq.Template.common.uGraph]
ei:392 [in MetaCoq.Template.common.uGraph]
elims:69 [in MetaCoq.Erasure.EPretty]
elt:512 [in MetaCoq.Template.EnvironmentTyping]
embed:1003 [in MetaCoq.Template.utils.wGraph]
embed:1156 [in MetaCoq.Template.utils.wGraph]
empty:90 [in MetaCoq.Template.common.uGraph]
env:3 [in MetaCoq.Template.EnvMap]
env:352 [in MetaCoq.PCUIC.PCUICEquality]
env:372 [in MetaCoq.Template.Checker]
env:418 [in MetaCoq.Template.Checker]
env:54 [in MetaCoq.PCUIC.TemplateToPCUIC]
env:56 [in MetaCoq.PCUIC.TemplateToPCUIC]
env:6 [in MetaCoq.Template.EnvMap]
env:69 [in MetaCoq.SafeChecker.PCUICSafeChecker]
env:8 [in MetaCoq.Template.EnvMap]
eo:1102 [in MetaCoq.Template.utils.wGraph]
ep:202 [in MetaCoq.Erasure.ErasureFunction]
eqarglen:360 [in MetaCoq.SafeChecker.PCUICSafeChecker]
eqarglen:361 [in MetaCoq.SafeChecker.PCUICSafeChecker]
eqA:57 [in MetaCoq.Template.utils.ReflectEq]
eqA:65 [in MetaCoq.Template.utils.ReflectEq]
eqA:87 [in MetaCoq.Template.utils.ReflectEq]
eqA:97 [in MetaCoq.Template.utils.ReflectEq]
eqbindices:366 [in MetaCoq.SafeChecker.PCUICSafeChecker]
eqbpars:365 [in MetaCoq.SafeChecker.PCUICSafeChecker]
eqb_univ_instance:17 [in MetaCoq.Template.Ast]
eqb_univ_instance:252 [in MetaCoq.PCUIC.PCUICAst]
eqb:238 [in MetaCoq.SafeChecker.PCUICSafeChecker]
eqb:284 [in MetaCoq.SafeChecker.PCUICEqualityDec]
eqb:315 [in MetaCoq.SafeChecker.PCUICEqualityDec]
eqb:423 [in MetaCoq.Template.EnvironmentTyping]
eqB:88 [in MetaCoq.Template.utils.ReflectEq]
eqB:98 [in MetaCoq.Template.utils.ReflectEq]
eqci:2396 [in MetaCoq.SafeChecker.PCUICSafeConversion]
eqdecl:253 [in MetaCoq.PCUIC.PCUICAst]
eqhd:569 [in MetaCoq.SafeChecker.PCUICSafeChecker]
eqindices:990 [in MetaCoq.SafeChecker.PCUICSafeChecker]
eqlu':250 [in MetaCoq.SafeChecker.PCUICEqualityDec]
eqlu':263 [in MetaCoq.SafeChecker.PCUICEqualityDec]
eqlu':75 [in MetaCoq.SafeChecker.PCUICTypeChecker]
eqlu:249 [in MetaCoq.SafeChecker.PCUICEqualityDec]
eqlu:262 [in MetaCoq.SafeChecker.PCUICEqualityDec]
eqlu:74 [in MetaCoq.SafeChecker.PCUICTypeChecker]
eqna:237 [in MetaCoq.SafeChecker.PCUICSafeChecker]
eqna:242 [in MetaCoq.SafeChecker.PCUICSafeChecker]
eqna:414 [in MetaCoq.Template.EnvironmentTyping]
eqna:422 [in MetaCoq.Template.EnvironmentTyping]
eqpars:359 [in MetaCoq.SafeChecker.PCUICSafeChecker]
eqpars:989 [in MetaCoq.SafeChecker.PCUICSafeChecker]
eqr:334 [in MetaCoq.SafeChecker.PCUICSafeChecker]
eqr:551 [in MetaCoq.SafeChecker.PCUICSafeChecker]
eqsort:988 [in MetaCoq.SafeChecker.PCUICSafeChecker]
eqterm:18 [in MetaCoq.Template.Ast]
eqterm:254 [in MetaCoq.PCUIC.PCUICAst]
eqterm:257 [in MetaCoq.PCUIC.PCUICAst]
eqterm:379 [in MetaCoq.PCUIC.PCUICCumulProp]
eqterm:42 [in MetaCoq.Template.Reflect]
eqt:415 [in MetaCoq.Template.EnvironmentTyping]
eqt:424 [in MetaCoq.Template.EnvironmentTyping]
equ':248 [in MetaCoq.SafeChecker.PCUICEqualityDec]
equ':261 [in MetaCoq.SafeChecker.PCUICEqualityDec]
equ':363 [in MetaCoq.SafeChecker.PCUICEqualityDec]
equ':73 [in MetaCoq.SafeChecker.PCUICTypeChecker]
equ:11 [in MetaCoq.SafeChecker.PCUICEqualityDec]
equ:120 [in MetaCoq.SafeChecker.PCUICEqualityDec]
equ:149 [in MetaCoq.SafeChecker.PCUICEqualityDec]
equ:17 [in MetaCoq.SafeChecker.PCUICEqualityDec]
equ:187 [in MetaCoq.SafeChecker.PCUICEqualityDec]
equ:20 [in MetaCoq.SafeChecker.PCUICEqualityDec]
equ:201 [in MetaCoq.SafeChecker.PCUICEqualityDec]
equ:223 [in MetaCoq.SafeChecker.PCUICEqualityDec]
equ:247 [in MetaCoq.SafeChecker.PCUICEqualityDec]
equ:260 [in MetaCoq.SafeChecker.PCUICEqualityDec]
equ:30 [in MetaCoq.SafeChecker.PCUICEqualityDec]
equ:333 [in MetaCoq.SafeChecker.PCUICEqualityDec]
equ:344 [in MetaCoq.SafeChecker.PCUICEqualityDec]
equ:36 [in MetaCoq.SafeChecker.PCUICEqualityDec]
equ:362 [in MetaCoq.SafeChecker.PCUICEqualityDec]
equ:72 [in MetaCoq.SafeChecker.PCUICTypeChecker]
eq_levelalg:526 [in MetaCoq.Template.Universes]
eq_term:45 [in MetaCoq.Template.TermEquality]
eq_term':365 [in MetaCoq.PCUIC.PCUICEquality]
eq_term:364 [in MetaCoq.PCUIC.PCUICEquality]
eq_term:278 [in MetaCoq.PCUIC.PCUICEquality]
eq_term:257 [in MetaCoq.PCUIC.PCUICEquality]
eq_term:234 [in MetaCoq.PCUIC.PCUICEquality]
eq_term:111 [in MetaCoq.PCUIC.PCUICEquality]
eq_term:109 [in MetaCoq.PCUIC.PCUICEquality]
eq_term:107 [in MetaCoq.PCUIC.PCUICEquality]
eq_term:105 [in MetaCoq.PCUIC.PCUICEquality]
eq_term:103 [in MetaCoq.PCUIC.PCUICEquality]
eq_term:101 [in MetaCoq.PCUIC.PCUICEquality]
eq_term:99 [in MetaCoq.PCUIC.PCUICEquality]
eq_term:93 [in MetaCoq.PCUIC.PCUICEquality]
eq_term:83 [in MetaCoq.PCUIC.PCUICEquality]
eq_term':75 [in MetaCoq.PCUIC.PCUICEquality]
eq_term:73 [in MetaCoq.PCUIC.PCUICEquality]
eq_term':70 [in MetaCoq.PCUIC.PCUICEquality]
eq_term:68 [in MetaCoq.PCUIC.PCUICEquality]
eq_term':66 [in MetaCoq.PCUIC.PCUICEquality]
eq_term:64 [in MetaCoq.PCUIC.PCUICEquality]
eq_term:48 [in MetaCoq.PCUIC.PCUICEquality]
eq_npars:118 [in MetaCoq.PCUIC.PCUICInversion]
eq_npars:53 [in MetaCoq.PCUIC.PCUICTyping]
eq_params:1088 [in MetaCoq.SafeChecker.PCUICTypeChecker]
eq':39 [in MetaCoq.Examples.add_constructor]
eq':841 [in MetaCoq.SafeChecker.PCUICSafeConversion]
eq1:2164 [in MetaCoq.SafeChecker.PCUICSafeConversion]
eq2:2165 [in MetaCoq.SafeChecker.PCUICSafeConversion]
eq:1018 [in MetaCoq.PCUIC.PCUICTyping]
eq:1072 [in MetaCoq.SafeChecker.PCUICSafeChecker]
eq:1073 [in MetaCoq.SafeChecker.PCUICSafeChecker]
eq:1124 [in MetaCoq.PCUIC.PCUICConfluence]
eq:1128 [in MetaCoq.PCUIC.PCUICConfluence]
eq:1132 [in MetaCoq.PCUIC.PCUICConfluence]
eq:1235 [in MetaCoq.PCUIC.PCUICConfluence]
eq:1306 [in MetaCoq.Template.Typing]
eq:1329 [in MetaCoq.Template.Typing]
eq:187 [in MetaCoq.Template.utils.wGraph]
eq:24 [in MetaCoq.PCUIC.Syntax.PCUICViews]
eq:259 [in MetaCoq.Template.common.uGraph]
eq:282 [in MetaCoq.PCUIC.PCUICConfluence]
eq:381 [in MetaCoq.PCUIC.PCUICCumulProp]
eq:54 [in MetaCoq.SafeChecker.PCUICEqualityDec]
eq:58 [in MetaCoq.SafeChecker.PCUICEqualityDec]
eq:636 [in MetaCoq.SafeChecker.PCUICSafeConversion]
eq:840 [in MetaCoq.SafeChecker.PCUICSafeConversion]
eq:924 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
eq:957 [in MetaCoq.SafeChecker.PCUICSafeChecker]
eq:984 [in MetaCoq.SafeChecker.PCUICSafeChecker]
eq:997 [in MetaCoq.PCUIC.PCUICTyping]
eqΓ0:571 [in MetaCoq.PCUIC.PCUICSubstitution]
eqΓ0:581 [in MetaCoq.PCUIC.PCUICSubstitution]
es:267 [in MetaCoq.Template.Universes]
es:283 [in MetaCoq.Template.Universes]
es:777 [in MetaCoq.Template.utils.wGraph]
es:779 [in MetaCoq.Template.utils.wGraph]
es:782 [in MetaCoq.Template.utils.wGraph]
eta_args:8 [in MetaCoq.Template.EtaExpand]
etfl:101 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
etfl:105 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
etfl:107 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
etfl:115 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
etfl:3 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
etfl:307 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
etfl:33 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
etfl:39 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
etfl:46 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
etfl:55 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
etfl:6 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
etfl:62 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
etfl:70 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
etfl:97 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
et:1145 [in MetaCoq.Erasure.ErasureFunction]
et:1162 [in MetaCoq.Erasure.ErasureFunction]
et:1189 [in MetaCoq.Erasure.ErasureFunction]
et:1298 [in MetaCoq.Erasure.ErasureFunction]
et:152 [in MetaCoq.Erasure.EInlineProjections]
et:1527 [in MetaCoq.Erasure.ErasureFunction]
et:159 [in MetaCoq.Erasure.EDeps]
et:178 [in MetaCoq.Erasure.EDeps]
et:554 [in MetaCoq.Erasure.ErasureFunction]
et:856 [in MetaCoq.Erasure.ErasureFunction]
et:867 [in MetaCoq.Erasure.ErasureFunction]
eval'':49 [in MetaCoq.Template.Transform]
eval':13 [in MetaCoq.Template.Transform]
eval':40 [in MetaCoq.Template.Transform]
eval':48 [in MetaCoq.Template.Transform]
eval:12 [in MetaCoq.Template.Transform]
eval:39 [in MetaCoq.Template.Transform]
eval:47 [in MetaCoq.Template.Transform]
eva:432 [in MetaCoq.Erasure.EWcbvEval]
eva:445 [in MetaCoq.Erasure.EWcbvEval]
eva:467 [in MetaCoq.Erasure.EEtaExpandedFix]
even':43 [in MetaCoq.Examples.add_constructor]
even':45 [in MetaCoq.Examples.add_constructor]
evf:429 [in MetaCoq.Erasure.EWcbvEval]
evf:442 [in MetaCoq.Erasure.EWcbvEval]
evres:433 [in MetaCoq.Erasure.EWcbvEval]
ev':230 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
ev':285 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
ev':288 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
ev':456 [in MetaCoq.Erasure.EWcbvEval]
ev':9 [in MetaCoq.Erasure.EWcbvEvalInd]
ev':95 [in MetaCoq.Erasure.EWcbvEvalInd]
ev1:289 [in MetaCoq.Erasure.EWcbvEval]
ev1:293 [in MetaCoq.Erasure.EWcbvEval]
ev1:380 [in MetaCoq.PCUIC.PCUICWcbvEval]
ev1:387 [in MetaCoq.PCUIC.PCUICWcbvEval]
ev2:290 [in MetaCoq.Erasure.EWcbvEval]
ev2:294 [in MetaCoq.Erasure.EWcbvEval]
ev2:381 [in MetaCoq.PCUIC.PCUICWcbvEval]
ev2:388 [in MetaCoq.PCUIC.PCUICWcbvEval]
ev:1144 [in MetaCoq.PCUIC.PCUICReduction]
ev:1157 [in MetaCoq.PCUIC.PCUICReduction]
ev:116 [in MetaCoq.PCUIC.PCUICReduction]
ev:1225 [in MetaCoq.PCUIC.PCUICConversion]
ev:1228 [in MetaCoq.PCUIC.PCUICConversion]
ev:13 [in MetaCoq.Erasure.EWcbvEvalInd]
ev:13 [in MetaCoq.Template.Checker]
ev:16 [in MetaCoq.Erasure.EEtaExpandedFix]
ev:16 [in MetaCoq.PCUIC.PCUICEtaExpand]
ev:160 [in MetaCoq.Template.EtaExpand]
ev:166 [in MetaCoq.SafeChecker.PCUICErrors]
ev:181 [in MetaCoq.Template.Ast]
ev:187 [in MetaCoq.Erasure.EEtaExpanded]
ev:20 [in MetaCoq.Erasure.EWcbvEvalInd]
ev:210 [in MetaCoq.Template.Typing]
ev:220 [in MetaCoq.Erasure.EEtaExpanded]
ev:227 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
ev:258 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
ev:289 [in MetaCoq.PCUIC.PCUICParallelReduction]
ev:290 [in MetaCoq.PCUIC.PCUICReduction]
ev:321 [in MetaCoq.Erasure.EWcbvEval]
ev:397 [in MetaCoq.Template.Typing]
ev:422 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
ev:426 [in MetaCoq.Erasure.EWcbvEval]
ev:440 [in MetaCoq.Erasure.EWcbvEval]
ev:452 [in MetaCoq.Erasure.EWcbvEval]
ev:470 [in MetaCoq.PCUIC.PCUICSR]
ev:494 [in MetaCoq.PCUIC.PCUICParallelReduction]
ev:57 [in MetaCoq.Erasure.EEtaExpandedFix]
ev:6 [in MetaCoq.Erasure.EWcbvEvalInd]
ev:74 [in MetaCoq.Erasure.EWcbvEvalInd]
ev:76 [in MetaCoq.PCUIC.PCUICEtaExpand]
ev:84 [in MetaCoq.Erasure.EWcbvEvalInd]
ev:94 [in MetaCoq.Erasure.EWcbvEvalInd]
ev:95 [in MetaCoq.Template.EtaExpand]
exprs:111 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
exprs:27 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
exprs:49 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
expr:19 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
ext:106 [in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
ext:1070 [in MetaCoq.Template.utils.wGraph]
ext:1097 [in MetaCoq.Template.utils.wGraph]
ext:1124 [in MetaCoq.Template.utils.wGraph]
ext:255 [in MetaCoq.PCUIC.PCUICSpine]
ext:555 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
ext:74 [in MetaCoq.PCUIC.PCUICSpine]
ext:776 [in MetaCoq.SafeChecker.PCUICSafeChecker]
ext:91 [in MetaCoq.SafeChecker.PCUICSafeChecker]
ext:96 [in MetaCoq.SafeChecker.PCUICSafeChecker]
e'':303 [in MetaCoq.Erasure.EWcbvEval]
e'':306 [in MetaCoq.Erasure.EWcbvEval]
e':107 [in MetaCoq.Template.Universes]
E':116 [in MetaCoq.Translations.translation_utils]
E':124 [in MetaCoq.Translations.translation_utils]
E':132 [in MetaCoq.Translations.translation_utils]
E':150 [in MetaCoq.Translations.translation_utils]
E':152 [in MetaCoq.Translations.translation_utils]
E':157 [in MetaCoq.Translations.translation_utils]
E':159 [in MetaCoq.Translations.translation_utils]
e':210 [in MetaCoq.Erasure.EWcbvEval]
e':217 [in MetaCoq.Translations.times_bool_fun]
e':251 [in MetaCoq.PCUIC.PCUICWcbvEval]
e':293 [in MetaCoq.Template.WcbvEval]
e':302 [in MetaCoq.Erasure.EWcbvEval]
e':305 [in MetaCoq.Erasure.EWcbvEval]
e':310 [in MetaCoq.Template.utils.wGraph]
e':323 [in MetaCoq.Template.common.uGraph]
e':328 [in MetaCoq.Template.common.uGraph]
e':368 [in MetaCoq.Template.common.uGraph]
e':600 [in MetaCoq.Template.common.uGraph]
e':604 [in MetaCoq.Template.common.uGraph]
e':609 [in MetaCoq.Template.common.uGraph]
E':62 [in MetaCoq.Translations.translation_utils]
E':64 [in MetaCoq.Translations.translation_utils]
E':71 [in MetaCoq.Translations.translation_utils]
E':73 [in MetaCoq.Translations.translation_utils]
E':83 [in MetaCoq.Translations.translation_utils]
E':85 [in MetaCoq.Translations.translation_utils]
E':99 [in MetaCoq.Translations.translation_utils]
e0:124 [in MetaCoq.Erasure.EWcbvEvalInd]
e0:126 [in MetaCoq.Template.Universes]
e0:136 [in MetaCoq.Erasure.EWcbvEvalInd]
e0:153 [in MetaCoq.Erasure.EWcbvEvalInd]
e0:167 [in MetaCoq.Erasure.EWcbvEvalInd]
e0:169 [in MetaCoq.Template.Universes]
e0:171 [in MetaCoq.Template.Universes]
e0:177 [in MetaCoq.Template.Universes]
e0:177 [in MetaCoq.Erasure.EWcbvEvalInd]
e0:179 [in MetaCoq.Template.Universes]
e0:183 [in MetaCoq.Erasure.EWcbvEval]
e0:36 [in MetaCoq.Erasure.EWcbvEvalInd]
e0:52 [in MetaCoq.Erasure.EWcbvEvalInd]
e0:784 [in MetaCoq.Template.utils.wGraph]
e1:125 [in MetaCoq.Erasure.EWcbvEvalInd]
e1:128 [in MetaCoq.PCUIC.utils.PCUICUtils]
e1:137 [in MetaCoq.Erasure.EWcbvEvalInd]
e1:154 [in MetaCoq.Erasure.EWcbvEvalInd]
e1:169 [in MetaCoq.Erasure.EWcbvEvalInd]
e1:197 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
e1:206 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
e1:218 [in MetaCoq.Translations.times_bool_fun]
e1:219 [in MetaCoq.Translations.times_bool_fun]
e1:237 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
e1:246 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
e1:255 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
e1:262 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
e1:271 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
e1:278 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
e1:287 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
e1:294 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
e1:3004 [in MetaCoq.Translations.MiniHoTT]
e1:303 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
e1:310 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
e1:317 [in MetaCoq.Template.common.uGraph]
e1:332 [in MetaCoq.Template.common.uGraph]
e1:337 [in MetaCoq.Template.common.uGraph]
e1:37 [in MetaCoq.Erasure.EWcbvEvalInd]
e1:398 [in MetaCoq.Template.common.uGraph]
e1:406 [in MetaCoq.Template.common.uGraph]
e1:486 [in MetaCoq.Template.common.uGraph]
e1:53 [in MetaCoq.Erasure.EWcbvEvalInd]
e1:86 [in MetaCoq.PCUIC.utils.PCUICUtils]
e2:126 [in MetaCoq.Erasure.EWcbvEvalInd]
e2:129 [in MetaCoq.PCUIC.utils.PCUICUtils]
e2:138 [in MetaCoq.Erasure.EWcbvEvalInd]
e2:156 [in MetaCoq.Erasure.EWcbvEvalInd]
e2:170 [in MetaCoq.Erasure.EWcbvEvalInd]
e2:220 [in MetaCoq.Translations.times_bool_fun]
e2:221 [in MetaCoq.Translations.times_bool_fun]
e2:3005 [in MetaCoq.Translations.MiniHoTT]
e2:318 [in MetaCoq.Template.common.uGraph]
e2:335 [in MetaCoq.Template.common.uGraph]
e2:38 [in MetaCoq.Erasure.EWcbvEvalInd]
e2:54 [in MetaCoq.Erasure.EWcbvEvalInd]
e2:87 [in MetaCoq.PCUIC.utils.PCUICUtils]
e3:127 [in MetaCoq.Erasure.EWcbvEvalInd]
e3:139 [in MetaCoq.Erasure.EWcbvEvalInd]
e3:39 [in MetaCoq.Erasure.EWcbvEvalInd]
e3:55 [in MetaCoq.Erasure.EWcbvEvalInd]
e4:128 [in MetaCoq.Erasure.EWcbvEvalInd]
e4:140 [in MetaCoq.Erasure.EWcbvEvalInd]
e4:40 [in MetaCoq.Erasure.EWcbvEvalInd]
e4:56 [in MetaCoq.Erasure.EWcbvEvalInd]
e5:41 [in MetaCoq.Erasure.EWcbvEvalInd]
e5:57 [in MetaCoq.Erasure.EWcbvEvalInd]
e:10 [in MetaCoq.Template.BasicAst]
e:10 [in MetaCoq.PCUIC.utils.PCUICPrimitive]
e:101 [in MetaCoq.Template.Universes]
E:101 [in MetaCoq.Template.monad_utils]
e:1012 [in MetaCoq.Template.utils.wGraph]
e:1015 [in MetaCoq.Template.utils.wGraph]
e:103 [in MetaCoq.Template.Universes]
e:1030 [in MetaCoq.Template.utils.wGraph]
e:1038 [in MetaCoq.Template.utils.wGraph]
e:105 [in MetaCoq.Template.Universes]
e:107 [in MetaCoq.Translations.translation_utils]
e:1073 [in MetaCoq.Template.utils.wGraph]
e:108 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
e:1080 [in MetaCoq.Template.utils.wGraph]
e:1083 [in MetaCoq.Template.utils.wGraph]
e:1084 [in MetaCoq.Erasure.ErasureFunction]
e:1088 [in MetaCoq.Template.utils.wGraph]
e:1088 [in MetaCoq.Erasure.ErasureFunction]
e:109 [in MetaCoq.Template.Universes]
e:1091 [in MetaCoq.Template.utils.wGraph]
e:1092 [in MetaCoq.Template.utils.wGraph]
e:1093 [in MetaCoq.Template.utils.wGraph]
e:1093 [in MetaCoq.Erasure.ErasureFunction]
e:1097 [in MetaCoq.Erasure.ErasureFunction]
E:11 [in MetaCoq.Translations.param_cheap_packed]
e:1101 [in MetaCoq.Erasure.ErasureFunction]
e:1105 [in MetaCoq.Erasure.ErasureFunction]
e:1109 [in MetaCoq.Erasure.ErasureFunction]
e:1114 [in MetaCoq.Erasure.ErasureFunction]
e:1118 [in MetaCoq.Erasure.ErasureFunction]
e:112 [in MetaCoq.Template.Universes]
e:1122 [in MetaCoq.Erasure.ErasureFunction]
e:114 [in MetaCoq.Template.Universes]
e:117 [in MetaCoq.Erasure.ErasureProperties]
e:117 [in MetaCoq.Template.Pretty]
e:118 [in MetaCoq.Template.Universes]
e:119 [in MetaCoq.PCUIC.utils.PCUICUtils]
e:120 [in MetaCoq.Template.Universes]
e:122 [in MetaCoq.PCUIC.PCUICEquality]
e:123 [in MetaCoq.Erasure.EWcbvEvalInd]
e:124 [in MetaCoq.PCUIC.utils.PCUICUtils]
e:125 [in MetaCoq.Template.Universes]
e:126 [in MetaCoq.PCUIC.PCUICCumulProp]
E:127 [in MetaCoq.Template.monad_utils]
e:13 [in MetaCoq.Examples.metacoq_tour]
e:13 [in MetaCoq.Template.EnvMap]
e:130 [in MetaCoq.PCUIC.PCUICCumulProp]
e:130 [in MetaCoq.Template.monad_utils]
e:133 [in MetaCoq.PCUIC.utils.PCUICUtils]
e:1333 [in MetaCoq.Template.Typing]
e:1335 [in MetaCoq.Template.Typing]
e:1337 [in MetaCoq.Template.Typing]
e:1339 [in MetaCoq.Template.Typing]
E:134 [in MetaCoq.Translations.param_cheap_packed]
e:135 [in MetaCoq.Erasure.EWcbvEvalInd]
E:135 [in MetaCoq.Template.monad_utils]
e:138 [in MetaCoq.SafeChecker.PCUICErrors]
e:139 [in MetaCoq.Template.monad_utils]
e:14 [in MetaCoq.SafeChecker.PCUICErrors]
E:140 [in MetaCoq.Translations.param_cheap_packed]
e:141 [in MetaCoq.PCUIC.PCUICCumulProp]
E:142 [in MetaCoq.Template.monad_utils]
E:145 [in MetaCoq.Translations.param_cheap_packed]
e:146 [in MetaCoq.Template.Universes]
E:147 [in MetaCoq.Translations.param_cheap_packed]
e:147 [in MetaCoq.Template.monad_utils]
e:149 [in MetaCoq.SafeChecker.PCUICErrors]
E:15 [in MetaCoq.Translations.times_bool_fun]
e:150 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
e:151 [in MetaCoq.Template.Universes]
e:152 [in MetaCoq.Erasure.EWcbvEvalInd]
e:153 [in MetaCoq.Erasure.ErasureProperties]
e:1545 [in MetaCoq.SafeChecker.PCUICSafeReduce]
e:156 [in MetaCoq.Template.Universes]
e:157 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
e:159 [in MetaCoq.Erasure.ErasureProperties]
e:16 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
e:1609 [in MetaCoq.SafeChecker.PCUICSafeReduce]
e:161 [in MetaCoq.Template.Universes]
e:163 [in MetaCoq.Erasure.ErasureProperties]
e:165 [in MetaCoq.Template.Universes]
e:166 [in MetaCoq.Erasure.EWcbvEvalInd]
e:168 [in MetaCoq.Template.Universes]
E:17 [in MetaCoq.Translations.param_cheap_packed]
e:17 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
E:17 [in MetaCoq.SafeChecker.PCUICSafeChecker]
e:172 [in MetaCoq.Erasure.ErasureProperties]
e:1731 [in MetaCoq.SafeChecker.PCUICSafeReduce]
e:175 [in MetaCoq.Erasure.EEtaExpandedFix]
e:175 [in MetaCoq.Erasure.EWcbvEvalInd]
e:176 [in MetaCoq.Template.Universes]
e:176 [in MetaCoq.Template.common.uGraph]
e:179 [in MetaCoq.SafeChecker.PCUICErrors]
e:179 [in MetaCoq.Erasure.ErasureProperties]
E:18 [in MetaCoq.Translations.param_generous_packed]
e:182 [in MetaCoq.Erasure.EWcbvEval]
E:183 [in MetaCoq.Translations.MiniHoTT]
e:184 [in MetaCoq.Template.Universes]
e:184 [in MetaCoq.SafeChecker.PCUICSafeConversion]
e:186 [in MetaCoq.Erasure.ErasureProperties]
e:188 [in MetaCoq.Template.Universes]
e:189 [in MetaCoq.Template.Universes]
e:191 [in MetaCoq.Template.Universes]
e:191 [in MetaCoq.Template.utils.wGraph]
E:191 [in MetaCoq.Translations.MiniHoTT_paths]
e:194 [in MetaCoq.Template.utils.wGraph]
e:196 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
E:198 [in MetaCoq.Template.common.uGraph]
e:201 [in MetaCoq.Template.common.uGraph]
e:202 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
e:205 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
e:206 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
e:207 [in MetaCoq.Translations.times_bool_fun]
e:207 [in MetaCoq.Erasure.EWcbvEval]
e:209 [in MetaCoq.Erasure.EWcbvEval]
E:21 [in MetaCoq.Translations.param_binary]
e:211 [in MetaCoq.Template.common.uGraph]
e:212 [in MetaCoq.SafeChecker.PCUICErrors]
E:214 [in MetaCoq.Template.common.uGraph]
e:216 [in MetaCoq.Translations.times_bool_fun]
e:216 [in MetaCoq.SafeChecker.PCUICErrors]
E:217 [in MetaCoq.Template.common.uGraph]
e:223 [in MetaCoq.Erasure.EConstructorsAsBlocks]
e:228 [in MetaCoq.Template.utils.wGraph]
e:236 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
E:238 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
E:24 [in MetaCoq.Translations.param_generous_packed]
e:240 [in MetaCoq.SafeChecker.PCUICErrors]
e:243 [in MetaCoq.Template.utils.wGraph]
e:245 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
e:246 [in MetaCoq.SafeChecker.PCUICSafeConversion]
e:247 [in MetaCoq.SafeChecker.PCUICErrors]
e:248 [in MetaCoq.SafeChecker.PCUICErrors]
e:25 [in MetaCoq.Translations.translation_utils]
E:25 [in MetaCoq.Translations.param_cheap_packed]
e:250 [in MetaCoq.PCUIC.PCUICWcbvEval]
e:251 [in MetaCoq.SafeChecker.PCUICSafeConversion]
e:254 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
e:256 [in MetaCoq.SafeChecker.PCUICErrors]
e:261 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
e:263 [in MetaCoq.Template.Universes]
e:264 [in MetaCoq.Template.Universes]
e:265 [in MetaCoq.SafeChecker.PCUICErrors]
e:270 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
e:274 [in MetaCoq.Template.common.uGraph]
e:277 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
e:282 [in MetaCoq.Template.Universes]
e:285 [in MetaCoq.Erasure.EWcbvEval]
e:286 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
e:287 [in MetaCoq.PCUIC.PCUICWcbvEval]
e:289 [in MetaCoq.Template.common.uGraph]
e:292 [in MetaCoq.Template.WcbvEval]
e:293 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
e:298 [in MetaCoq.Template.WcbvEval]
E:30 [in MetaCoq.Translations.translation_utils]
e:300 [in MetaCoq.Template.utils.wGraph]
e:301 [in MetaCoq.Erasure.EWcbvEval]
e:302 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
e:304 [in MetaCoq.Erasure.EWcbvEval]
e:306 [in MetaCoq.Template.utils.wGraph]
e:309 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
e:31 [in MetaCoq.SafeChecker.PCUICErrors]
e:31 [in MetaCoq.Erasure.EEtaExpanded]
E:31 [in MetaCoq.Translations.param_generous_packed]
e:318 [in MetaCoq.Template.utils.wGraph]
e:322 [in MetaCoq.Template.common.uGraph]
e:327 [in MetaCoq.Template.common.uGraph]
e:33 [in MetaCoq.Template.Checker]
e:34 [in MetaCoq.PCUIC.utils.PCUICUtils]
e:342 [in MetaCoq.Template.common.uGraph]
e:346 [in MetaCoq.Template.common.uGraph]
e:35 [in MetaCoq.Erasure.EWcbvEvalInd]
e:367 [in MetaCoq.Template.common.uGraph]
e:379 [in MetaCoq.Template.Checker]
e:380 [in MetaCoq.Template.Checker]
e:386 [in MetaCoq.Template.Checker]
e:39 [in MetaCoq.Template.EnvMap]
e:411 [in MetaCoq.Erasure.EWcbvEval]
e:412 [in MetaCoq.Template.common.uGraph]
e:414 [in MetaCoq.Template.common.uGraph]
e:419 [in MetaCoq.Erasure.EWcbvEval]
e:421 [in MetaCoq.Template.common.uGraph]
e:422 [in MetaCoq.Template.common.uGraph]
e:423 [in MetaCoq.Template.common.uGraph]
e:426 [in MetaCoq.Template.utils.wGraph]
e:428 [in MetaCoq.Template.utils.wGraph]
e:45 [in MetaCoq.Template.EnvMap]
e:451 [in MetaCoq.Erasure.EWcbvEval]
e:459 [in MetaCoq.Erasure.EWcbvEval]
E:47 [in MetaCoq.Translations.param_original]
e:477 [in MetaCoq.Template.utils.wGraph]
e:479 [in MetaCoq.Template.common.uGraph]
e:48 [in MetaCoq.Template.Checker]
e:483 [in MetaCoq.Template.common.uGraph]
e:49 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
e:491 [in MetaCoq.Erasure.ErasureFunction]
e:497 [in MetaCoq.PCUIC.PCUICInductiveInversion]
e:497 [in MetaCoq.Erasure.ErasureFunction]
e:5 [in MetaCoq.Template.utils.MCEquality]
e:503 [in MetaCoq.Erasure.ErasureFunction]
e:508 [in MetaCoq.Erasure.ErasureFunction]
E:51 [in MetaCoq.Translations.param_binary]
e:51 [in MetaCoq.Erasure.EWcbvEvalInd]
e:513 [in MetaCoq.Erasure.ErasureFunction]
e:518 [in MetaCoq.Erasure.ErasureFunction]
E:52 [in MetaCoq.Translations.param_original]
e:524 [in MetaCoq.Erasure.ErasureFunction]
e:530 [in MetaCoq.Erasure.ErasureFunction]
e:535 [in MetaCoq.Erasure.ErasureFunction]
e:540 [in MetaCoq.Erasure.ErasureFunction]
e:543 [in MetaCoq.Template.common.uGraph]
E:55 [in MetaCoq.Template.utils.ReflectEq]
e:556 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
e:558 [in MetaCoq.Erasure.ErasureFunction]
E:56 [in MetaCoq.Translations.param_binary]
E:56 [in MetaCoq.Translations.param_original]
e:562 [in MetaCoq.Erasure.ErasureFunction]
e:567 [in MetaCoq.Erasure.ErasureFunction]
e:5685 [in MetaCoq.SafeChecker.PCUICSafeConversion]
e:571 [in MetaCoq.Erasure.ErasureFunction]
e:5712 [in MetaCoq.SafeChecker.PCUICSafeConversion]
e:575 [in MetaCoq.Erasure.ErasureFunction]
e:579 [in MetaCoq.Erasure.ErasureFunction]
e:58 [in MetaCoq.Template.EnvMap]
e:583 [in MetaCoq.Erasure.ErasureFunction]
e:588 [in MetaCoq.Erasure.ErasureFunction]
E:59 [in MetaCoq.Translations.param_original]
e:592 [in MetaCoq.Erasure.ErasureFunction]
e:595 [in MetaCoq.Template.utils.wGraph]
e:596 [in MetaCoq.Erasure.ErasureFunction]
e:599 [in MetaCoq.Template.common.uGraph]
E:6 [in MetaCoq.Translations.translation_utils]
e:6 [in MetaCoq.Erasure.ESpineView]
E:60 [in MetaCoq.Translations.param_binary]
e:603 [in MetaCoq.Template.common.uGraph]
e:607 [in MetaCoq.Erasure.ErasureFunction]
e:608 [in MetaCoq.Template.common.uGraph]
E:61 [in MetaCoq.Translations.param_cheap_packed]
E:61 [in MetaCoq.Translations.param_original]
e:611 [in MetaCoq.Erasure.ErasureFunction]
e:616 [in MetaCoq.Erasure.ErasureFunction]
e:62 [in MetaCoq.Template.EnvMap]
e:622 [in MetaCoq.Erasure.ErasureFunction]
e:628 [in MetaCoq.Erasure.ErasureFunction]
E:63 [in MetaCoq.Translations.param_binary]
e:630 [in MetaCoq.Template.common.uGraph]
e:634 [in MetaCoq.Erasure.ErasureFunction]
e:636 [in MetaCoq.Template.common.uGraph]
e:638 [in MetaCoq.Erasure.ErasureFunction]
e:643 [in MetaCoq.Erasure.ErasureFunction]
e:649 [in MetaCoq.Erasure.ErasureFunction]
E:65 [in MetaCoq.Translations.param_binary]
e:655 [in MetaCoq.Erasure.ErasureFunction]
e:66 [in MetaCoq.Template.Universes]
e:67 [in MetaCoq.Template.Universes]
e:68 [in MetaCoq.Template.Universes]
e:68 [in MetaCoq.Template.EnvMap]
E:69 [in MetaCoq.Translations.param_generous_packed]
E:7 [in MetaCoq.Translations.param_original]
E:70 [in MetaCoq.Template.monad_utils]
e:70 [in MetaCoq.SafeChecker.PCUICTypeChecker]
e:71 [in MetaCoq.Template.Universes]
e:718 [in MetaCoq.Erasure.ErasureFunction]
e:72 [in MetaCoq.Template.Universes]
e:720 [in MetaCoq.Template.Universes]
e:722 [in MetaCoq.Template.utils.wGraph]
e:723 [in MetaCoq.Template.utils.wGraph]
e:724 [in MetaCoq.Template.Universes]
e:724 [in MetaCoq.Erasure.ErasureFunction]
e:728 [in MetaCoq.Template.utils.wGraph]
e:730 [in MetaCoq.Erasure.ErasureFunction]
e:734 [in MetaCoq.Template.utils.wGraph]
e:735 [in MetaCoq.Erasure.ErasureFunction]
e:739 [in MetaCoq.Template.Universes]
e:74 [in MetaCoq.Translations.translation_utils]
e:740 [in MetaCoq.Template.utils.wGraph]
e:740 [in MetaCoq.Erasure.ErasureFunction]
e:745 [in MetaCoq.Erasure.ErasureFunction]
e:745 [in MetaCoq.Translations.MiniHoTT]
e:747 [in MetaCoq.Template.Universes]
e:751 [in MetaCoq.Erasure.ErasureFunction]
e:752 [in MetaCoq.Template.Universes]
e:753 [in MetaCoq.Translations.MiniHoTT_paths]
e:757 [in MetaCoq.Erasure.ErasureFunction]
e:76 [in MetaCoq.Template.monad_utils]
e:762 [in MetaCoq.Erasure.ErasureFunction]
e:765 [in MetaCoq.Translations.MiniHoTT]
e:767 [in MetaCoq.Erasure.ErasureFunction]
e:77 [in MetaCoq.PCUIC.utils.PCUICUtils]
e:773 [in MetaCoq.Translations.MiniHoTT_paths]
e:78 [in MetaCoq.Template.TermEquality]
e:780 [in MetaCoq.Template.utils.wGraph]
e:783 [in MetaCoq.Template.utils.wGraph]
e:790 [in MetaCoq.Template.utils.wGraph]
E:8 [in MetaCoq.Template.monad_utils]
e:80 [in MetaCoq.Translations.times_bool_fun2]
e:816 [in MetaCoq.Template.utils.wGraph]
e:82 [in MetaCoq.PCUIC.utils.PCUICUtils]
E:83 [in MetaCoq.Translations.param_cheap_packed]
e:85 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
e:86 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
e:888 [in MetaCoq.Template.utils.wGraph]
E:89 [in MetaCoq.Translations.param_cheap_packed]
e:89 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
e:895 [in MetaCoq.Template.utils.wGraph]
e:9 [in MetaCoq.Template.EnvMap]
e:90 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
e:91 [in MetaCoq.PCUIC.utils.PCUICUtils]
e:917 [in MetaCoq.Template.utils.wGraph]
e:925 [in MetaCoq.Template.utils.wGraph]
e:934 [in MetaCoq.Template.utils.wGraph]
e:942 [in MetaCoq.Template.utils.wGraph]
e:97 [in MetaCoq.PCUIC.utils.PCUICUtils]
e:992 [in MetaCoq.Template.utils.wGraph]



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)