| 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) |
U (binder)
ua:11 [in MetaCoq.PCUIC.Syntax.PCUICUnivSubst]ua:2 [in MetaCoq.Template.UnivSubst]
ua:7 [in MetaCoq.PCUIC.Syntax.PCUICUnivSubst]
uctx':12 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
uctx':181 [in MetaCoq.Template.common.uGraph]
uctx':4 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
uctx':700 [in MetaCoq.Template.common.uGraph]
uctx':708 [in MetaCoq.Template.common.uGraph]
uctx':713 [in MetaCoq.Template.common.uGraph]
uctx':78 [in MetaCoq.SafeChecker.PCUICSafeChecker]
uctx1:660 [in MetaCoq.Template.common.uGraph]
uctx1:670 [in MetaCoq.Template.common.uGraph]
uctx2:661 [in MetaCoq.Template.common.uGraph]
uctx2:671 [in MetaCoq.Template.common.uGraph]
uctx:156 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
uctx:157 [in MetaCoq.Template.common.uGraph]
uctx:158 [in MetaCoq.Template.common.uGraph]
uctx:159 [in MetaCoq.Template.common.uGraph]
uctx:162 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
uctx:162 [in MetaCoq.SafeChecker.PCUICWfEnv]
uctx:163 [in MetaCoq.Template.common.uGraph]
uctx:164 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
uctx:166 [in MetaCoq.Template.common.uGraph]
uctx:167 [in MetaCoq.SafeChecker.PCUICWfEnv]
uctx:169 [in MetaCoq.Template.common.uGraph]
uctx:172 [in MetaCoq.SafeChecker.PCUICWfEnv]
uctx:180 [in MetaCoq.Template.common.uGraph]
uctx:207 [in MetaCoq.Template.common.uGraph]
uctx:210 [in MetaCoq.Template.common.uGraph]
uctx:222 [in MetaCoq.Template.common.uGraph]
uctx:236 [in MetaCoq.Template.common.uGraph]
uctx:245 [in MetaCoq.Template.common.uGraph]
uctx:247 [in MetaCoq.Template.common.uGraph]
uctx:263 [in MetaCoq.Template.common.uGraph]
uctx:3 [in MetaCoq.SafeChecker.PCUICEqualityDec]
uctx:433 [in MetaCoq.Template.Universes]
uctx:439 [in MetaCoq.Template.Checker]
uctx:441 [in MetaCoq.Template.Universes]
uctx:45 [in MetaCoq.SafeChecker.PCUICWfEnv]
uctx:471 [in MetaCoq.Template.common.uGraph]
uctx:472 [in MetaCoq.Template.common.uGraph]
uctx:474 [in MetaCoq.Template.common.uGraph]
uctx:535 [in MetaCoq.Template.common.uGraph]
uctx:548 [in MetaCoq.SafeChecker.PCUICTypeChecker]
uctx:615 [in MetaCoq.Template.common.uGraph]
uctx:618 [in MetaCoq.Template.common.uGraph]
uctx:674 [in MetaCoq.Template.common.uGraph]
uctx:678 [in MetaCoq.Template.common.uGraph]
uctx:681 [in MetaCoq.Template.common.uGraph]
uctx:686 [in MetaCoq.Template.common.uGraph]
uctx:689 [in MetaCoq.Template.common.uGraph]
uctx:694 [in MetaCoq.Template.common.uGraph]
uctx:698 [in MetaCoq.Template.common.uGraph]
uctx:706 [in MetaCoq.Template.common.uGraph]
uctx:712 [in MetaCoq.Template.common.uGraph]
uctx:72 [in MetaCoq.Template.Checker]
uctx:74 [in MetaCoq.SafeChecker.PCUICSafeChecker]
uctx:764 [in MetaCoq.Template.Universes]
uctx:85 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
uctx:87 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
uctx:91 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
uctx:92 [in MetaCoq.Template.EnvironmentTyping]
uctx:99 [in MetaCoq.SafeChecker.PCUICSafeChecker]
uc:102 [in MetaCoq.Template.common.uGraph]
uc:103 [in MetaCoq.Template.common.uGraph]
uc:110 [in MetaCoq.Template.common.uGraph]
uc:112 [in MetaCoq.Template.common.uGraph]
uc:89 [in MetaCoq.Template.common.uGraph]
udecl':728 [in MetaCoq.SafeChecker.PCUICSafeChecker]
udecl':733 [in MetaCoq.SafeChecker.PCUICSafeChecker]
udecl:1035 [in MetaCoq.SafeChecker.PCUICSafeChecker]
udecl:163 [in MetaCoq.SafeChecker.PCUICWfEnv]
udecl:165 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
udecl:168 [in MetaCoq.SafeChecker.PCUICWfEnv]
udecl:173 [in MetaCoq.SafeChecker.PCUICWfEnv]
udecl:214 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
udecl:22 [in MetaCoq.Erasure.ErasureCorrectness]
udecl:221 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
udecl:228 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
udecl:314 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
udecl:46 [in MetaCoq.SafeChecker.PCUICWfEnv]
udecl:467 [in MetaCoq.Template.EnvironmentTyping]
udecl:570 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
udecl:669 [in MetaCoq.Template.EnvironmentTyping]
udecl:673 [in MetaCoq.Template.common.uGraph]
udecl:681 [in MetaCoq.SafeChecker.PCUICSafeConversion]
udecl:727 [in MetaCoq.SafeChecker.PCUICSafeChecker]
udecl:732 [in MetaCoq.SafeChecker.PCUICSafeChecker]
udecl:77 [in MetaCoq.SafeChecker.PCUICSafeChecker]
udecl:78 [in MetaCoq.PCUIC.PCUICWeakeningEnv]
udecl:862 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
udecl:901 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
udecl:92 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
udecl:977 [in MetaCoq.Erasure.ErasureFunction]
uf:14 [in MetaCoq.PCUIC.PCUICAst]
uf:23 [in MetaCoq.Template.Ast]
uf:29 [in MetaCoq.PCUIC.PCUICAst]
uf:65 [in MetaCoq.Template.Ast]
uinst:8 [in MetaCoq.PCUIC.PCUICSafeLemmata]
ui':113 [in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
ui':1235 [in MetaCoq.PCUIC.PCUICConversion]
ui':1243 [in MetaCoq.PCUIC.PCUICConversion]
ui':195 [in MetaCoq.SafeChecker.PCUICEqualityDec]
ui':30 [in MetaCoq.PCUIC.PCUICPrincipality]
ui':371 [in MetaCoq.PCUIC.PCUICConversion]
ui':393 [in MetaCoq.PCUIC.PCUICConversion]
ui':400 [in MetaCoq.PCUIC.PCUICConversion]
ui':58 [in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
ui:109 [in MetaCoq.PCUIC.PCUICAst]
ui:111 [in MetaCoq.PCUIC.PCUICAst]
ui:111 [in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
ui:114 [in MetaCoq.PCUIC.PCUICAst]
ui:1234 [in MetaCoq.PCUIC.PCUICConversion]
ui:1242 [in MetaCoq.PCUIC.PCUICConversion]
ui:163 [in MetaCoq.PCUIC.PCUICFirstorder]
ui:171 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
ui:189 [in MetaCoq.SafeChecker.PCUICSafeReduce]
ui:194 [in MetaCoq.SafeChecker.PCUICEqualityDec]
ui:224 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
ui:301 [in MetaCoq.SafeChecker.PCUICSafeReduce]
ui:329 [in MetaCoq.SafeChecker.PCUICSafeReduce]
ui:368 [in MetaCoq.PCUIC.PCUICConversion]
ui:39 [in MetaCoq.PCUIC.PCUICFirstorder]
ui:390 [in MetaCoq.PCUIC.PCUICConversion]
ui:399 [in MetaCoq.PCUIC.PCUICConversion]
ui:446 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
ui:48 [in MetaCoq.PCUIC.PCUICFirstorder]
ui:55 [in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
unf:210 [in MetaCoq.Template.Checker]
unguarded:85 [in MetaCoq.Erasure.EWcbvEval]
unguarded:93 [in MetaCoq.Erasure.EWcbvEvalInd]
univs':643 [in MetaCoq.Template.EnvironmentTyping]
univs':73 [in MetaCoq.PCUIC.PCUICWeakeningEnv]
univs:100 [in MetaCoq.Template.EnvironmentTyping]
univs:1013 [in MetaCoq.SafeChecker.PCUICSafeChecker]
univs:1014 [in MetaCoq.SafeChecker.PCUICSafeChecker]
univs:1015 [in MetaCoq.SafeChecker.PCUICSafeChecker]
univs:102 [in MetaCoq.PCUIC.PCUICWfUniverses]
univs:1024 [in MetaCoq.SafeChecker.PCUICSafeChecker]
univs:1034 [in MetaCoq.PCUIC.PCUICConversion]
univs:104 [in MetaCoq.Erasure.ErasureProperties]
univs:108 [in MetaCoq.PCUIC.utils.PCUICPretty]
univs:11 [in MetaCoq.Erasure.ErasureCorrectness]
univs:1101 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
univs:1135 [in MetaCoq.Erasure.ErasureFunction]
univs:1151 [in MetaCoq.Erasure.ErasureFunction]
univs:1198 [in MetaCoq.Erasure.ErasureFunction]
univs:1210 [in MetaCoq.Erasure.ErasureFunction]
univs:1222 [in MetaCoq.Erasure.ErasureFunction]
univs:1235 [in MetaCoq.Erasure.ErasureFunction]
univs:1292 [in MetaCoq.Erasure.ErasureFunction]
univs:1317 [in MetaCoq.Erasure.ErasureFunction]
univs:1318 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
univs:1334 [in MetaCoq.Erasure.ErasureFunction]
univs:1349 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
univs:1355 [in MetaCoq.Erasure.ErasureFunction]
univs:1370 [in MetaCoq.Erasure.ErasureFunction]
univs:1392 [in MetaCoq.Erasure.ErasureFunction]
univs:1398 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
univs:14 [in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
univs:140 [in MetaCoq.Template.Pretty]
univs:1417 [in MetaCoq.Erasure.ErasureFunction]
univs:142 [in MetaCoq.PCUIC.PCUICWfUniverses]
univs:149 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
univs:151 [in MetaCoq.SafeChecker.PCUICWfEnv]
univs:1521 [in MetaCoq.Erasure.ErasureFunction]
univs:1539 [in MetaCoq.Erasure.ErasureFunction]
univs:163 [in MetaCoq.PCUIC.PCUICEtaExpand]
univs:168 [in MetaCoq.Erasure.Extract]
univs:17 [in MetaCoq.Erasure.ErasureCorrectness]
univs:189 [in MetaCoq.SafeChecker.PCUICWfEnv]
univs:2 [in MetaCoq.SafeChecker.PCUICWfEnv]
univs:20 [in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
univs:201 [in MetaCoq.PCUIC.PCUICWfUniverses]
univs:23 [in MetaCoq.SafeChecker.PCUICTypeChecker]
univs:231 [in MetaCoq.PCUIC.PCUICWfUniverses]
univs:235 [in MetaCoq.PCUIC.PCUICWfUniverses]
univs:235 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
univs:239 [in MetaCoq.PCUIC.PCUICWfUniverses]
univs:243 [in MetaCoq.PCUIC.PCUICWfUniverses]
univs:247 [in MetaCoq.PCUIC.PCUICWfUniverses]
univs:25 [in MetaCoq.PCUIC.PCUICWfUniverses]
univs:25 [in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
univs:263 [in MetaCoq.Template.EtaExpand]
univs:27 [in MetaCoq.SafeChecker.PCUICTypeChecker]
univs:29 [in MetaCoq.PCUIC.PCUICWfUniverses]
univs:294 [in MetaCoq.PCUIC.PCUICCumulProp]
univs:300 [in MetaCoq.PCUIC.PCUICCumulProp]
univs:310 [in MetaCoq.PCUIC.PCUICCumulProp]
univs:319 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
univs:32 [in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
univs:39 [in MetaCoq.PCUIC.PCUICWfUniverses]
univs:39 [in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
univs:4 [in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
univs:41 [in MetaCoq.PCUIC.PCUICGuardCondition]
univs:42 [in MetaCoq.PCUIC.PCUICWfUniverses]
univs:424 [in MetaCoq.Template.Checker]
univs:431 [in MetaCoq.Template.Checker]
univs:44 [in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
univs:45 [in MetaCoq.SafeChecker.PCUICSafeChecker]
univs:460 [in MetaCoq.Template.EnvironmentTyping]
univs:462 [in MetaCoq.Template.EnvironmentTyping]
univs:464 [in MetaCoq.Template.EnvironmentTyping]
univs:466 [in MetaCoq.Template.EnvironmentTyping]
univs:48 [in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
univs:483 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
univs:490 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
univs:493 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
univs:505 [in MetaCoq.Template.EtaExpand]
univs:51 [in MetaCoq.SafeChecker.PCUICWfEnv]
univs:511 [in MetaCoq.Template.EtaExpand]
univs:517 [in MetaCoq.Template.EtaExpand]
univs:525 [in MetaCoq.Template.EnvironmentTyping]
univs:531 [in MetaCoq.Template.Typing]
univs:537 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
univs:539 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
univs:54 [in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
univs:540 [in MetaCoq.Template.EnvironmentTyping]
univs:545 [in MetaCoq.Template.EnvironmentTyping]
univs:547 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
univs:567 [in MetaCoq.Template.Typing]
univs:58 [in MetaCoq.PCUIC.PCUICWfUniverses]
univs:61 [in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
univs:61 [in MetaCoq.PCUIC.TemplateToPCUIC]
univs:639 [in MetaCoq.Template.EnvironmentTyping]
univs:64 [in MetaCoq.PCUIC.TemplateToPCUICExpanded]
univs:647 [in MetaCoq.SafeChecker.PCUICSafeChecker]
univs:66 [in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
univs:663 [in MetaCoq.Template.EnvironmentTyping]
univs:68 [in MetaCoq.PCUIC.TemplateToPCUICExpanded]
univs:71 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
univs:71 [in MetaCoq.Template.TypingWf]
univs:72 [in MetaCoq.PCUIC.PCUICWeakeningEnv]
univs:72 [in MetaCoq.PCUIC.TemplateToPCUICExpanded]
univs:720 [in MetaCoq.SafeChecker.PCUICSafeChecker]
univs:73 [in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
univs:74 [in MetaCoq.Erasure.ErasureProperties]
univs:76 [in MetaCoq.Translations.translation_utils]
univs:80 [in MetaCoq.Template.EnvironmentTyping]
univs:82 [in MetaCoq.Template.EnvironmentTyping]
univs:86 [in MetaCoq.Erasure.ErasureProperties]
univs:945 [in MetaCoq.Erasure.ErasureFunction]
univs:956 [in MetaCoq.SafeChecker.PCUICSafeChecker]
univs:961 [in MetaCoq.Erasure.ErasureFunction]
univs:969 [in MetaCoq.Erasure.ErasureFunction]
univs:97 [in MetaCoq.Erasure.ErasureProperties]
univx:87 [in MetaCoq.PCUIC.Syntax.PCUICReflect]
univy:91 [in MetaCoq.PCUIC.Syntax.PCUICReflect]
univ:160 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
upars:103 [in MetaCoq.PCUIC.Syntax.PCUICCases]
upars:395 [in MetaCoq.Template.Ast]
us':24 [in MetaCoq.Translations.param_original]
us':38 [in MetaCoq.Translations.param_binary]
us:126 [in MetaCoq.PCUIC.PCUICAst]
us:152 [in MetaCoq.PCUIC.PCUICArities]
us:16 [in MetaCoq.Erasure.EAst]
us:162 [in MetaCoq.PCUIC.PCUICArities]
us:2 [in MetaCoq.Translations.translation_utils]
us:217 [in MetaCoq.Template.Ast]
us:439 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
us:453 [in MetaCoq.Template.EnvironmentTyping]
us:482 [in MetaCoq.PCUIC.PCUICNormal]
us:515 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
us:60 [in MetaCoq.Translations.times_bool_fun]
u'':106 [in MetaCoq.PCUIC.PCUICContextConversion]
u'':99 [in MetaCoq.PCUIC.PCUICContextConversion]
u'0:398 [in MetaCoq.PCUIC.PCUICConfluence]
u'0:419 [in MetaCoq.PCUIC.PCUICConfluence]
u'0:470 [in MetaCoq.PCUIC.PCUICConfluence]
u'0:491 [in MetaCoq.PCUIC.PCUICConfluence]
u':101 [in MetaCoq.Erasure.Extract]
u':104 [in MetaCoq.PCUIC.PCUICContextConversion]
u':105 [in MetaCoq.SafeChecker.PCUICWfEnv]
u':1058 [in MetaCoq.PCUIC.PCUICConversion]
u':1067 [in MetaCoq.PCUIC.PCUICConversion]
u':1079 [in MetaCoq.PCUIC.PCUICConversion]
u':1098 [in MetaCoq.PCUIC.PCUICConversion]
u':11 [in MetaCoq.PCUIC.PCUICWfUniverses]
u':110 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
u':1105 [in MetaCoq.PCUIC.PCUICConversion]
u':111 [in MetaCoq.PCUIC.Syntax.PCUICReflect]
u':117 [in MetaCoq.Template.TermEquality]
u':117 [in MetaCoq.PCUIC.PCUICCumulProp]
u':118 [in MetaCoq.Template.common.uGraph]
u':118 [in MetaCoq.PCUIC.PCUICContextConversion]
u':12 [in MetaCoq.PCUIC.PCUICEquality]
u':12 [in MetaCoq.PCUIC.Bidirectional.BDUnique]
u':122 [in MetaCoq.PCUIC.PCUICInductiveInversion]
u':122 [in MetaCoq.PCUIC.PCUICCumulProp]
u':123 [in MetaCoq.Template.common.uGraph]
u':124 [in MetaCoq.PCUIC.PCUICContextConversion]
u':126 [in MetaCoq.Template.common.uGraph]
u':126 [in MetaCoq.PCUIC.Bidirectional.BDUnique]
u':126 [in MetaCoq.SafeChecker.PCUICEqualityDec]
u':128 [in MetaCoq.SafeChecker.PCUICEqualityDec]
u':130 [in MetaCoq.Template.common.uGraph]
u':130 [in MetaCoq.PCUIC.PCUICContextConversion]
u':131 [in MetaCoq.PCUIC.PCUICEquality]
u':1326 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
u':134 [in MetaCoq.Template.common.uGraph]
u':134 [in MetaCoq.PCUIC.PCUICEquality]
u':136 [in MetaCoq.PCUIC.PCUICContextConversion]
u':136 [in MetaCoq.SafeChecker.PCUICEqualityDec]
u':137 [in MetaCoq.PCUIC.PCUICEquality]
u':138 [in MetaCoq.Template.common.uGraph]
u':139 [in MetaCoq.PCUIC.Bidirectional.BDUnique]
u':139 [in MetaCoq.SafeChecker.PCUICEqualityDec]
u':14 [in MetaCoq.Template.TermEquality]
u':141 [in MetaCoq.PCUIC.PCUICEquality]
u':142 [in MetaCoq.Template.common.uGraph]
u':147 [in MetaCoq.Template.common.uGraph]
u':149 [in MetaCoq.PCUIC.PCUICInductiveInversion]
u':15 [in MetaCoq.SafeChecker.PCUICEqualityDec]
u':151 [in MetaCoq.Template.common.uGraph]
u':155 [in MetaCoq.Template.common.uGraph]
u':157 [in MetaCoq.PCUIC.PCUICArities]
u':157 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
u':157 [in MetaCoq.SafeChecker.PCUICEqualityDec]
u':159 [in MetaCoq.PCUIC.PCUICSR]
u':159 [in MetaCoq.SafeChecker.PCUICEqualityDec]
u':160 [in MetaCoq.SafeChecker.PCUICTypeChecker]
u':161 [in MetaCoq.PCUIC.PCUICEquality]
u':163 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
u':163 [in MetaCoq.SafeChecker.PCUICEqualityDec]
u':165 [in MetaCoq.Erasure.EArities]
u':167 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
u':17 [in MetaCoq.PCUIC.PCUICSN]
u':171 [in MetaCoq.PCUIC.PCUICCanonicity]
u':175 [in MetaCoq.SafeChecker.PCUICEqualityDec]
U':176 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
u':178 [in MetaCoq.SafeChecker.PCUICErrors]
u':18 [in MetaCoq.PCUIC.PCUICEquality]
u':182 [in MetaCoq.SafeChecker.PCUICEqualityDec]
u':185 [in MetaCoq.SafeChecker.PCUICEqualityDec]
u':186 [in MetaCoq.Erasure.EArities]
u':19 [in MetaCoq.SafeChecker.PCUICEqualityDec]
u':192 [in MetaCoq.Erasure.EArities]
u':197 [in MetaCoq.SafeChecker.PCUICEqualityDec]
u':199 [in MetaCoq.SafeChecker.PCUICEqualityDec]
u':208 [in MetaCoq.Template.Universes]
u':210 [in MetaCoq.SafeChecker.PCUICEqualityDec]
u':212 [in MetaCoq.SafeChecker.PCUICEqualityDec]
u':216 [in MetaCoq.SafeChecker.PCUICEqualityDec]
u':22 [in MetaCoq.Template.Checker]
u':222 [in MetaCoq.PCUIC.PCUICElimination]
u':228 [in MetaCoq.PCUIC.PCUICElimination]
u':229 [in MetaCoq.Template.Universes]
u':229 [in MetaCoq.PCUIC.PCUICConversion]
u':230 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
u':231 [in MetaCoq.Template.Universes]
u':233 [in MetaCoq.SafeChecker.PCUICEqualityDec]
u':234 [in MetaCoq.PCUIC.PCUICElimination]
u':235 [in MetaCoq.PCUIC.PCUICConversion]
u':235 [in MetaCoq.SafeChecker.PCUICEqualityDec]
u':238 [in MetaCoq.Template.Universes]
u':239 [in MetaCoq.SafeChecker.PCUICEqualityDec]
u':24 [in MetaCoq.SafeChecker.PCUICEqualityDec]
u':240 [in MetaCoq.PCUIC.PCUICElimination]
u':242 [in MetaCoq.Template.Universes]
u':244 [in MetaCoq.PCUIC.PCUICAlpha]
u':246 [in MetaCoq.PCUIC.PCUICElimination]
u':25 [in MetaCoq.PCUIC.PCUICSN]
u':250 [in MetaCoq.PCUIC.PCUICAlpha]
u':252 [in MetaCoq.PCUIC.PCUICElimination]
u':252 [in MetaCoq.SafeChecker.PCUICEqualityDec]
u':253 [in MetaCoq.PCUIC.PCUICEquality]
u':254 [in MetaCoq.SafeChecker.PCUICEqualityDec]
u':256 [in MetaCoq.PCUIC.PCUICAlpha]
u':258 [in MetaCoq.PCUIC.PCUICElimination]
u':258 [in MetaCoq.Erasure.EArities]
u':26 [in MetaCoq.PCUIC.PCUICPrincipality]
u':266 [in MetaCoq.Erasure.EArities]
u':266 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
u':270 [in MetaCoq.SafeChecker.PCUICEqualityDec]
u':272 [in MetaCoq.SafeChecker.PCUICEqualityDec]
u':29 [in MetaCoq.Translations.standard_model]
u':29 [in MetaCoq.PCUIC.Bidirectional.BDUnique]
u':292 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
u':296 [in MetaCoq.PCUIC.PCUICCumulProp]
u':3 [in MetaCoq.Template.TermEquality]
u':30 [in MetaCoq.Translations.times_bool_fun]
u':30 [in MetaCoq.PCUIC.PCUICSN]
u':302 [in MetaCoq.PCUIC.PCUICCumulProp]
u':31 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
u':310 [in MetaCoq.PCUIC.PCUICConfluence]
u':312 [in MetaCoq.PCUIC.PCUICCumulProp]
u':316 [in MetaCoq.PCUIC.PCUICCumulProp]
u':320 [in MetaCoq.Template.TypingWf]
U':321 [in MetaCoq.PCUIC.PCUICConversion]
u':323 [in MetaCoq.Template.Checker]
u':324 [in MetaCoq.SafeChecker.PCUICEqualityDec]
u':328 [in MetaCoq.SafeChecker.PCUICEqualityDec]
u':330 [in MetaCoq.Template.Universes]
u':332 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
u':34 [in MetaCoq.Translations.times_bool_fun]
u':340 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
u':350 [in MetaCoq.SafeChecker.PCUICEqualityDec]
u':351 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
u':353 [in MetaCoq.PCUIC.PCUICCumulProp]
u':354 [in MetaCoq.SafeChecker.PCUICEqualityDec]
u':355 [in MetaCoq.PCUIC.PCUICConfluence]
u':357 [in MetaCoq.PCUIC.PCUICConversion]
u':363 [in MetaCoq.PCUIC.PCUICInductiveInversion]
u':363 [in MetaCoq.PCUIC.PCUICCumulProp]
u':363 [in MetaCoq.PCUIC.PCUICConversion]
u':369 [in MetaCoq.SafeChecker.PCUICEqualityDec]
u':372 [in MetaCoq.PCUIC.PCUICInductiveInversion]
u':379 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
u':381 [in MetaCoq.PCUIC.PCUICInductiveInversion]
u':389 [in MetaCoq.PCUIC.PCUICInductiveInversion]
u':39 [in MetaCoq.PCUIC.PCUICSN]
u':39 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
u':390 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
u':393 [in MetaCoq.PCUIC.PCUICProgress]
u':394 [in MetaCoq.SafeChecker.PCUICEqualityDec]
u':396 [in MetaCoq.PCUIC.PCUICConfluence]
u':396 [in MetaCoq.SafeChecker.PCUICEqualityDec]
u':40 [in MetaCoq.Erasure.Extract]
u':417 [in MetaCoq.PCUIC.PCUICConfluence]
u':429 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
u':43 [in MetaCoq.PCUIC.PCUICCumulProp]
u':43 [in MetaCoq.Translations.param_cheap_packed]
u':44 [in MetaCoq.Template.TermEquality]
u':44 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
u':445 [in MetaCoq.PCUIC.PCUICInductiveInversion]
u':45 [in MetaCoq.PCUIC.PCUICAlpha]
u':45 [in MetaCoq.Translations.param_cheap_packed]
u':450 [in MetaCoq.PCUIC.PCUICInductiveInversion]
u':452 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
u':459 [in MetaCoq.Template.common.uGraph]
u':46 [in MetaCoq.SafeChecker.PCUICEqualityDec]
u':462 [in MetaCoq.Template.common.uGraph]
u':465 [in MetaCoq.PCUIC.PCUICInductiveInversion]
u':468 [in MetaCoq.PCUIC.PCUICConfluence]
u':47 [in MetaCoq.PCUIC.PCUICCumulProp]
u':47 [in MetaCoq.PCUIC.PCUICEquality]
u':47 [in MetaCoq.SafeChecker.PCUICSafeChecker]
u':48 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
u':481 [in MetaCoq.PCUIC.PCUICConversion]
u':487 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
u':489 [in MetaCoq.PCUIC.PCUICConfluence]
u':490 [in MetaCoq.PCUIC.PCUICInductiveInversion]
u':493 [in MetaCoq.PCUIC.PCUICInductiveInversion]
u':494 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
u':496 [in MetaCoq.PCUIC.PCUICInductiveInversion]
u':498 [in MetaCoq.Template.Universes]
u':499 [in MetaCoq.PCUIC.PCUICInductiveInversion]
u':502 [in MetaCoq.PCUIC.PCUICInductiveInversion]
u':503 [in MetaCoq.Template.Universes]
u':503 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
u':51 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
u':513 [in MetaCoq.PCUIC.PCUICEquality]
u':519 [in MetaCoq.Template.EnvironmentTyping]
u':519 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u':52 [in MetaCoq.PCUIC.PCUICSN]
u':52 [in MetaCoq.Translations.param_generous_packed]
u':520 [in MetaCoq.Template.Universes]
u':521 [in MetaCoq.PCUIC.PCUICConfluence]
u':522 [in MetaCoq.PCUIC.PCUICEquality]
u':524 [in MetaCoq.Template.Universes]
u':530 [in MetaCoq.Template.EnvironmentTyping]
u':536 [in MetaCoq.Template.Universes]
u':536 [in MetaCoq.PCUIC.PCUICSubstitution]
u':537 [in MetaCoq.PCUIC.PCUICEquality]
u':539 [in MetaCoq.Template.Universes]
u':54 [in MetaCoq.Translations.param_generous_packed]
u':543 [in MetaCoq.PCUIC.PCUICSubstitution]
u':545 [in MetaCoq.PCUIC.PCUICEquality]
u':546 [in MetaCoq.PCUIC.PCUICInductiveInversion]
u':548 [in MetaCoq.PCUIC.PCUICEquality]
u':550 [in MetaCoq.PCUIC.PCUICConfluence]
u':557 [in MetaCoq.PCUIC.PCUICInductiveInversion]
u':56 [in MetaCoq.PCUIC.PCUICWfUniverses]
u':567 [in MetaCoq.Template.Universes]
u':57 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
u':570 [in MetaCoq.Template.Universes]
u':571 [in MetaCoq.PCUIC.PCUICConfluence]
u':573 [in MetaCoq.Template.Universes]
u':578 [in MetaCoq.PCUIC.PCUICInductiveInversion]
u':592 [in MetaCoq.PCUIC.PCUICInductiveInversion]
u':60 [in MetaCoq.PCUIC.PCUICWfUniverses]
u':60 [in MetaCoq.PCUIC.PCUICSN]
u':61 [in MetaCoq.PCUIC.PCUICPrincipality]
u':621 [in MetaCoq.Template.Universes]
u':627 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
u':634 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
u':650 [in MetaCoq.SafeChecker.PCUICSafeConversion]
u':652 [in MetaCoq.PCUIC.PCUICInductiveInversion]
u':654 [in MetaCoq.PCUIC.PCUICReduction]
u':657 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
u':660 [in MetaCoq.SafeChecker.PCUICSafeConversion]
u':666 [in MetaCoq.SafeChecker.PCUICSafeConversion]
u':670 [in MetaCoq.PCUIC.PCUICEquality]
u':672 [in MetaCoq.SafeChecker.PCUICSafeConversion]
u':7 [in MetaCoq.PCUIC.PCUICEquality]
u':7 [in MetaCoq.PCUIC.Syntax.PCUICReflect]
u':70 [in MetaCoq.PCUIC.Bidirectional.BDUnique]
u':702 [in MetaCoq.PCUIC.PCUICInductiveInversion]
u':708 [in MetaCoq.PCUIC.PCUICEquality]
u':714 [in MetaCoq.SafeChecker.PCUICSafeConversion]
u':727 [in MetaCoq.Template.Universes]
u':756 [in MetaCoq.PCUIC.PCUICInductiveInversion]
u':77 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
u':77 [in MetaCoq.SafeChecker.PCUICEqualityDec]
u':77 [in MetaCoq.SafeChecker.PCUICTypeChecker]
u':787 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
u':79 [in MetaCoq.SafeChecker.PCUICTypeChecker]
u':8 [in MetaCoq.PCUIC.PCUICWfUniverses]
u':8 [in MetaCoq.Template.TermEquality]
u':801 [in MetaCoq.PCUIC.PCUICConversion]
u':81 [in MetaCoq.SafeChecker.PCUICEqualityDec]
u':81 [in MetaCoq.SafeChecker.PCUICTypeChecker]
u':869 [in MetaCoq.PCUIC.PCUICParallelReduction]
u':87 [in MetaCoq.Template.TermEquality]
u':87 [in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
u':90 [in MetaCoq.Template.TermEquality]
u':93 [in MetaCoq.Template.TermEquality]
u':93 [in MetaCoq.SafeChecker.PCUICWfEnv]
u':93 [in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
u':962 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
u':97 [in MetaCoq.Template.TermEquality]
u':97 [in MetaCoq.PCUIC.PCUICContextConversion]
u':988 [in MetaCoq.Erasure.ErasureFunction]
u0:29 [in MetaCoq.Translations.param_original]
u0:377 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u1':582 [in MetaCoq.Template.Universes]
u1:103 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u1:106 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u1:109 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u1:112 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u1:113 [in MetaCoq.PCUIC.PCUICElimination]
u1:115 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u1:118 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u1:121 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u1:124 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u1:132 [in MetaCoq.SafeChecker.PCUICErrors]
u1:138 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u1:143 [in MetaCoq.SafeChecker.PCUICErrors]
u1:200 [in MetaCoq.Erasure.EArities]
u1:204 [in MetaCoq.Erasure.EArities]
u1:211 [in MetaCoq.Template.Universes]
u1:254 [in MetaCoq.Template.Universes]
u1:2798 [in MetaCoq.Translations.MiniHoTT]
u1:2806 [in MetaCoq.Translations.MiniHoTT_paths]
u1:2810 [in MetaCoq.Translations.MiniHoTT]
u1:2818 [in MetaCoq.Translations.MiniHoTT_paths]
u1:30 [in MetaCoq.Translations.param_original]
u1:307 [in MetaCoq.Template.Universes]
u1:332 [in MetaCoq.PCUIC.PCUICConfluence]
u1:338 [in MetaCoq.PCUIC.PCUICConfluence]
u1:345 [in MetaCoq.PCUIC.PCUICConfluence]
u1:4 [in MetaCoq.PCUIC.Syntax.PCUICUnivSubst]
u1:410 [in MetaCoq.Template.common.uGraph]
u1:424 [in MetaCoq.Template.common.uGraph]
u1:426 [in MetaCoq.Template.common.uGraph]
u1:430 [in MetaCoq.Template.common.uGraph]
u1:4405 [in MetaCoq.SafeChecker.PCUICSafeConversion]
u1:445 [in MetaCoq.Template.common.uGraph]
u1:451 [in MetaCoq.Template.common.uGraph]
u1:453 [in MetaCoq.Template.common.uGraph]
u1:465 [in MetaCoq.Template.common.uGraph]
u1:49 [in MetaCoq.Translations.param_binary]
u1:490 [in MetaCoq.Template.common.uGraph]
u1:492 [in MetaCoq.Template.common.uGraph]
u1:494 [in MetaCoq.Template.common.uGraph]
u1:496 [in MetaCoq.Template.common.uGraph]
u1:501 [in MetaCoq.PCUIC.PCUICEquality]
u1:527 [in MetaCoq.Template.common.uGraph]
u1:527 [in MetaCoq.PCUIC.PCUICEquality]
u1:529 [in MetaCoq.Template.common.uGraph]
u1:531 [in MetaCoq.Template.common.uGraph]
u1:533 [in MetaCoq.Template.common.uGraph]
u1:537 [in MetaCoq.SafeChecker.PCUICSafeConversion]
u1:542 [in MetaCoq.SafeChecker.PCUICSafeConversion]
u1:570 [in MetaCoq.PCUIC.PCUICConversion]
u1:575 [in MetaCoq.Template.Universes]
u1:578 [in MetaCoq.Template.Universes]
u1:581 [in MetaCoq.Template.Universes]
u1:586 [in MetaCoq.Template.Universes]
u1:61 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u1:66 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u1:74 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u1:81 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u1:813 [in MetaCoq.PCUIC.PCUICConversion]
u1:85 [in MetaCoq.PCUIC.PCUICCumulProp]
u1:854 [in MetaCoq.PCUIC.PCUICConversion]
u2':584 [in MetaCoq.Template.Universes]
u2:104 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u2:107 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u2:110 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u2:113 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u2:114 [in MetaCoq.PCUIC.PCUICElimination]
u2:116 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u2:119 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u2:122 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u2:125 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u2:136 [in MetaCoq.SafeChecker.PCUICErrors]
u2:139 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u2:147 [in MetaCoq.SafeChecker.PCUICErrors]
u2:201 [in MetaCoq.Erasure.EArities]
u2:205 [in MetaCoq.Erasure.EArities]
u2:212 [in MetaCoq.Template.Universes]
u2:255 [in MetaCoq.Template.Universes]
u2:2801 [in MetaCoq.Translations.MiniHoTT]
u2:2809 [in MetaCoq.Translations.MiniHoTT_paths]
u2:2812 [in MetaCoq.Translations.MiniHoTT]
u2:2820 [in MetaCoq.Translations.MiniHoTT_paths]
u2:308 [in MetaCoq.Template.Universes]
u2:333 [in MetaCoq.PCUIC.PCUICConfluence]
u2:339 [in MetaCoq.PCUIC.PCUICConfluence]
u2:346 [in MetaCoq.PCUIC.PCUICConfluence]
u2:411 [in MetaCoq.Template.common.uGraph]
u2:425 [in MetaCoq.Template.common.uGraph]
u2:427 [in MetaCoq.Template.common.uGraph]
u2:431 [in MetaCoq.Template.common.uGraph]
u2:4406 [in MetaCoq.SafeChecker.PCUICSafeConversion]
u2:446 [in MetaCoq.Template.common.uGraph]
u2:452 [in MetaCoq.Template.common.uGraph]
u2:454 [in MetaCoq.Template.common.uGraph]
u2:466 [in MetaCoq.Template.common.uGraph]
u2:491 [in MetaCoq.Template.common.uGraph]
u2:493 [in MetaCoq.Template.common.uGraph]
u2:495 [in MetaCoq.Template.common.uGraph]
u2:497 [in MetaCoq.Template.common.uGraph]
u2:5 [in MetaCoq.PCUIC.Syntax.PCUICUnivSubst]
u2:503 [in MetaCoq.PCUIC.PCUICEquality]
u2:528 [in MetaCoq.Template.common.uGraph]
u2:529 [in MetaCoq.PCUIC.PCUICEquality]
u2:530 [in MetaCoq.Template.common.uGraph]
u2:532 [in MetaCoq.Template.common.uGraph]
u2:534 [in MetaCoq.Template.common.uGraph]
u2:539 [in MetaCoq.SafeChecker.PCUICSafeConversion]
u2:544 [in MetaCoq.SafeChecker.PCUICSafeConversion]
u2:571 [in MetaCoq.PCUIC.PCUICConversion]
u2:576 [in MetaCoq.Template.Universes]
u2:579 [in MetaCoq.Template.Universes]
u2:583 [in MetaCoq.Template.Universes]
u2:591 [in MetaCoq.Template.Universes]
u2:62 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u2:67 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u2:75 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u2:814 [in MetaCoq.PCUIC.PCUICConversion]
u2:82 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u2:855 [in MetaCoq.PCUIC.PCUICConversion]
u2:86 [in MetaCoq.PCUIC.PCUICCumulProp]
u:1 [in MetaCoq.PCUIC.Syntax.PCUICReflect]
u:1 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:10 [in MetaCoq.PCUIC.PCUICProgress]
u:10 [in MetaCoq.PCUIC.PCUICWfUniverses]
u:10 [in MetaCoq.Template.WfAst]
u:10 [in MetaCoq.Template.utils.MCEquality]
u:10 [in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
u:10 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
u:10 [in MetaCoq.Template.UnivSubst]
u:10 [in MetaCoq.Template.LiftSubst]
u:100 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
u:100 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
u:100 [in MetaCoq.PCUIC.PCUICValidity]
u:101 [in MetaCoq.PCUIC.PCUICEtaExpand]
u:101 [in MetaCoq.Template.EnvironmentTyping]
u:101 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
u:101 [in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
u:101 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:1018 [in MetaCoq.Translations.MiniHoTT]
u:102 [in MetaCoq.PCUIC.PCUICInversion]
u:102 [in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
u:102 [in MetaCoq.PCUIC.PCUICContextConversion]
u:1026 [in MetaCoq.PCUIC.PCUICConversion]
u:1026 [in MetaCoq.Translations.MiniHoTT_paths]
u:1028 [in MetaCoq.Template.Typing]
u:1029 [in MetaCoq.PCUIC.PCUICConfluence]
u:103 [in MetaCoq.Erasure.EArities]
u:103 [in MetaCoq.PCUIC.PCUICInductives]
u:103 [in MetaCoq.PCUIC.PCUICFirstorder]
u:103 [in MetaCoq.Erasure.ErasureProperties]
u:1031 [in MetaCoq.PCUIC.PCUICConversion]
u:1033 [in MetaCoq.PCUIC.PCUICConfluence]
u:1035 [in MetaCoq.Template.Typing]
u:1039 [in MetaCoq.PCUIC.PCUICConfluence]
u:104 [in MetaCoq.Template.Universes]
u:104 [in MetaCoq.PCUIC.PCUICWfUniverses]
u:104 [in MetaCoq.Template.EnvironmentTyping]
u:104 [in MetaCoq.SafeChecker.PCUICWfEnv]
U:104 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
u:1045 [in MetaCoq.Template.Typing]
u:1045 [in MetaCoq.PCUIC.PCUICConfluence]
u:105 [in MetaCoq.Erasure.Extract]
u:105 [in MetaCoq.PCUIC.Syntax.PCUICReflect]
u:1055 [in MetaCoq.Template.utils.All_Forall]
u:1057 [in MetaCoq.PCUIC.PCUICConversion]
u:1057 [in MetaCoq.Translations.MiniHoTT]
u:106 [in MetaCoq.Template.Universes]
u:106 [in MetaCoq.PCUIC.PCUICInductiveInversion]
u:106 [in MetaCoq.PCUIC.PCUICAst]
u:1062 [in MetaCoq.PCUIC.PCUICConversion]
u:1065 [in MetaCoq.Translations.MiniHoTT_paths]
u:1066 [in MetaCoq.PCUIC.PCUICConversion]
u:1068 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
u:107 [in MetaCoq.PCUIC.PCUICAlpha]
u:107 [in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
u:107 [in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
u:1072 [in MetaCoq.PCUIC.PCUICConversion]
u:1076 [in MetaCoq.Template.Typing]
u:1076 [in MetaCoq.SafeChecker.PCUICTypeChecker]
u:1078 [in MetaCoq.PCUIC.PCUICConversion]
u:108 [in MetaCoq.Template.Universes]
u:108 [in MetaCoq.PCUIC.PCUICFirstorder]
u:109 [in MetaCoq.PCUIC.PCUICElimination]
u:109 [in MetaCoq.Erasure.EInduction]
u:109 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
u:109 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
u:1097 [in MetaCoq.PCUIC.PCUICConversion]
u:1099 [in MetaCoq.PCUIC.PCUICConfluence]
u:11 [in MetaCoq.PCUIC.PCUICInductives]
u:11 [in MetaCoq.PCUIC.PCUICEquality]
U:11 [in MetaCoq.PCUIC.PCUICInversion]
u:11 [in MetaCoq.PCUIC.PCUICPrincipality]
u:11 [in MetaCoq.PCUIC.Bidirectional.BDUnique]
u:11 [in MetaCoq.SafeChecker.PCUICTypeChecker]
u:110 [in MetaCoq.Erasure.EArities]
U:110 [in MetaCoq.PCUIC.PCUICCumulProp]
u:110 [in MetaCoq.SafeChecker.PCUICWfEnv]
u:110 [in MetaCoq.PCUIC.PCUICTyping]
u:1101 [in MetaCoq.SafeChecker.PCUICTypeChecker]
u:1104 [in MetaCoq.PCUIC.PCUICConversion]
u:1107 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
u:111 [in MetaCoq.Template.Universes]
u:111 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
u:111 [in MetaCoq.PCUIC.PCUICValidity]
U:111 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
u:111 [in MetaCoq.Template.AstUtils]
u:1110 [in MetaCoq.PCUIC.PCUICConfluence]
u:112 [in MetaCoq.PCUIC.PCUICAlpha]
u:112 [in MetaCoq.PCUIC.PCUICFirstorder]
u:112 [in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
u:112 [in MetaCoq.Erasure.ErasureProperties]
u:112 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
u:112 [in MetaCoq.PCUIC.PCUICTyping]
u:113 [in MetaCoq.Template.Universes]
u:113 [in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
u:114 [in MetaCoq.Template.EtaExpand]
u:114 [in MetaCoq.PCUIC.Syntax.PCUICViews]
u:1149 [in MetaCoq.PCUIC.PCUICConfluence]
u:115 [in MetaCoq.Template.Universes]
u:115 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
u:115 [in MetaCoq.SafeChecker.PCUICWfEnv]
u:115 [in MetaCoq.PCUIC.PCUICTyping]
u:115 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
u:1153 [in MetaCoq.PCUIC.PCUICConfluence]
u:1158 [in MetaCoq.PCUIC.PCUICConfluence]
u:116 [in MetaCoq.Template.EtaExpand]
u:116 [in MetaCoq.Template.Universes]
u:116 [in MetaCoq.Template.TermEquality]
u:116 [in MetaCoq.PCUIC.PCUICCumulProp]
u:116 [in MetaCoq.SafeChecker.PCUICErrors]
u:116 [in MetaCoq.PCUIC.PCUICContextConversion]
u:116 [in MetaCoq.Erasure.EEtaExpanded]
u:1164 [in MetaCoq.PCUIC.PCUICConfluence]
u:117 [in MetaCoq.Template.Universes]
u:117 [in MetaCoq.PCUIC.PCUICValidity]
u:117 [in MetaCoq.Template.common.uGraph]
u:117 [in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
u:117 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:1187 [in MetaCoq.PCUIC.PCUICConfluence]
u:119 [in MetaCoq.Template.EtaExpand]
u:119 [in MetaCoq.Template.Universes]
u:119 [in MetaCoq.PCUIC.PCUICInductiveInversion]
U:119 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
U:1191 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
u:1191 [in MetaCoq.PCUIC.PCUICConfluence]
u:1194 [in MetaCoq.PCUIC.PCUICReduction]
u:1195 [in MetaCoq.PCUIC.PCUICConfluence]
U:1197 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
u:1199 [in MetaCoq.PCUIC.PCUICReduction]
u:12 [in MetaCoq.Erasure.EInduction]
u:12 [in MetaCoq.PCUIC.Syntax.PCUICUnivSubst]
u:12 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
u:12 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
u:120 [in MetaCoq.PCUIC.PCUICTyping]
u:120 [in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
u:120 [in MetaCoq.PCUIC.PCUICReduction]
u:1203 [in MetaCoq.PCUIC.PCUICReduction]
u:1207 [in MetaCoq.PCUIC.PCUICReduction]
u:121 [in MetaCoq.Erasure.EArities]
u:121 [in MetaCoq.PCUIC.PCUICInductives]
u:121 [in MetaCoq.PCUIC.PCUICCumulProp]
u:1211 [in MetaCoq.PCUIC.PCUICReduction]
u:1215 [in MetaCoq.PCUIC.PCUICReduction]
U:1216 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
u:1219 [in MetaCoq.PCUIC.PCUICReduction]
u:122 [in MetaCoq.Template.Universes]
u:122 [in MetaCoq.PCUIC.PCUICSafeLemmata]
u:122 [in MetaCoq.Template.WfAst]
u:122 [in MetaCoq.Template.common.uGraph]
u:122 [in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
u:122 [in MetaCoq.PCUIC.PCUICContextConversion]
u:122 [in MetaCoq.Erasure.EEtaExpanded]
u:1225 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
u:1227 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
u:1230 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
u:1231 [in MetaCoq.PCUIC.PCUICConfluence]
U:1237 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
u:1239 [in MetaCoq.PCUIC.PCUICConfluence]
u:124 [in MetaCoq.Template.Universes]
u:124 [in MetaCoq.Translations.param_cheap_packed]
u:124 [in MetaCoq.PCUIC.PCUICCanonicity]
u:124 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
u:124 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
U:1243 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
U:1249 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
u:125 [in MetaCoq.PCUIC.PCUICProgress]
u:125 [in MetaCoq.Template.WfAst]
u:125 [in MetaCoq.PCUIC.PCUICCumulProp]
u:125 [in MetaCoq.Template.common.uGraph]
u:125 [in MetaCoq.PCUIC.Bidirectional.BDUnique]
u:125 [in MetaCoq.PCUIC.PCUICReduction]
u:125 [in MetaCoq.SafeChecker.PCUICEqualityDec]
u:1252 [in MetaCoq.PCUIC.PCUICConfluence]
U:1255 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
u:1255 [in MetaCoq.PCUIC.PCUICConfluence]
u:126 [in MetaCoq.PCUIC.PCUICElimination]
u:126 [in MetaCoq.PCUIC.PCUICSafeLemmata]
u:126 [in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
u:126 [in MetaCoq.Erasure.Prelim]
u:1261 [in MetaCoq.SafeChecker.PCUICSafeReduce]
U:1263 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
u:1265 [in MetaCoq.SafeChecker.PCUICSafeReduce]
u:127 [in MetaCoq.Template.Universes]
u:127 [in MetaCoq.PCUIC.PCUICWfUniverses]
u:127 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:127 [in MetaCoq.SafeChecker.PCUICEqualityDec]
U:1270 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
u:1271 [in MetaCoq.PCUIC.PCUICConfluence]
U:1277 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
u:128 [in MetaCoq.Template.Typing]
u:128 [in MetaCoq.PCUIC.PCUICWcbvEval]
u:128 [in MetaCoq.PCUIC.PCUICInductives]
U:128 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
u:128 [in MetaCoq.PCUIC.PCUICContextConversion]
u:128 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
u:1283 [in MetaCoq.PCUIC.PCUICConfluence]
u:1287 [in MetaCoq.Template.Typing]
u:129 [in MetaCoq.Template.Universes]
u:129 [in MetaCoq.PCUIC.PCUICCumulativity]
u:129 [in MetaCoq.PCUIC.PCUICNormal]
u:129 [in MetaCoq.Template.common.uGraph]
u:129 [in MetaCoq.Erasure.ELiftSubst]
u:1290 [in MetaCoq.PCUIC.PCUICConfluence]
u:1299 [in MetaCoq.PCUIC.PCUICConfluence]
u:13 [in MetaCoq.PCUIC.PCUICCumulativity]
u:13 [in MetaCoq.Template.TermEquality]
u:13 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
u:13 [in MetaCoq.Erasure.ErasureFunction]
u:13 [in MetaCoq.SafeChecker.PCUICSafeConversion]
u:13 [in MetaCoq.Template.UnivSubst]
u:13 [in MetaCoq.Template.LiftSubst]
u:130 [in MetaCoq.Template.Universes]
u:130 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
u:130 [in MetaCoq.Template.Typing]
u:130 [in MetaCoq.PCUIC.PCUICEquality]
u:130 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
u:130 [in MetaCoq.Translations.param_cheap_packed]
u:130 [in MetaCoq.Template.WcbvEval]
u:131 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
u:1317 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
u:132 [in MetaCoq.Template.Universes]
u:132 [in MetaCoq.PCUIC.PCUICReduction]
u:1325 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
u:133 [in MetaCoq.PCUIC.PCUICProgress]
u:133 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
u:133 [in MetaCoq.Template.common.uGraph]
u:133 [in MetaCoq.PCUIC.PCUICEquality]
u:133 [in MetaCoq.Erasure.ELiftSubst]
u:133 [in MetaCoq.SafeChecker.PCUICSafeChecker]
u:134 [in MetaCoq.Template.Universes]
u:134 [in MetaCoq.PCUIC.PCUICEtaExpand]
U:134 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
u:134 [in MetaCoq.PCUIC.PCUICContextConversion]
u:134 [in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
u:135 [in MetaCoq.PCUIC.PCUICCumulativity]
u:135 [in MetaCoq.PCUIC.PCUICInductives]
u:135 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:135 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
u:135 [in MetaCoq.SafeChecker.PCUICEqualityDec]
u:136 [in MetaCoq.Template.Universes]
u:136 [in MetaCoq.PCUIC.PCUICNormal]
u:136 [in MetaCoq.PCUIC.PCUICEquality]
u:136 [in MetaCoq.PCUIC.PCUICConversion]
u:1360 [in MetaCoq.Erasure.ErasureFunction]
u:137 [in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
u:137 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
u:137 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
u:137 [in MetaCoq.Template.common.uGraph]
u:1374 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
u:1378 [in MetaCoq.Erasure.ErasureFunction]
u:138 [in MetaCoq.Template.Universes]
U:138 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
u:138 [in MetaCoq.PCUIC.PCUICCanonicity]
u:138 [in MetaCoq.PCUIC.Bidirectional.BDUnique]
u:138 [in MetaCoq.SafeChecker.PCUICEqualityDec]
u:1384 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
u:1386 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
U:139 [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
u:139 [in MetaCoq.PCUIC.PCUICReduction]
u:14 [in MetaCoq.PCUIC.PCUICElimination]
u:14 [in MetaCoq.PCUIC.PCUICCSubst]
u:14 [in MetaCoq.Erasure.ELiftSubst]
u:14 [in MetaCoq.PCUIC.PCUICCasesContexts]
u:14 [in MetaCoq.SafeChecker.PCUICEqualityDec]
u:140 [in MetaCoq.PCUIC.PCUICProgress]
u:140 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
u:140 [in MetaCoq.PCUIC.PCUICEquality]
u:140 [in MetaCoq.PCUIC.PCUICTyping]
u:1400 [in MetaCoq.Erasure.ErasureFunction]
u:1406 [in MetaCoq.SafeChecker.PCUICSafeReduce]
u:141 [in MetaCoq.Template.Universes]
u:141 [in MetaCoq.Erasure.EArities]
u:141 [in MetaCoq.Template.WfAst]
u:141 [in MetaCoq.Template.common.uGraph]
U:141 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
U:141 [in MetaCoq.PCUIC.PCUICContextConversion]
u:141 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:1413 [in MetaCoq.SafeChecker.PCUICSafeReduce]
u:1416 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
u:1424 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
u:143 [in MetaCoq.Template.EtaExpand]
u:143 [in MetaCoq.Template.Universes]
u:143 [in MetaCoq.PCUIC.PCUICWfUniverses]
u:143 [in MetaCoq.PCUIC.PCUICInductives]
u:143 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
u:143 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:144 [in MetaCoq.PCUIC.PCUICCumulativity]
u:144 [in MetaCoq.PCUIC.PCUICArities]
u:145 [in MetaCoq.Erasure.EArities]
u:145 [in MetaCoq.Template.WfAst]
u:145 [in MetaCoq.PCUIC.PCUICConfluence]
u:145 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:146 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
u:146 [in MetaCoq.PCUIC.PCUICWcbvEval]
u:146 [in MetaCoq.PCUIC.PCUICInductiveInversion]
U:146 [in MetaCoq.PCUIC.PCUICCumulProp]
u:146 [in MetaCoq.Template.common.uGraph]
u:146 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
u:146 [in MetaCoq.PCUIC.PCUICContextConversion]
u:146 [in MetaCoq.PCUIC.PCUICReduction]
U:147 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
u:147 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
u:147 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:149 [in MetaCoq.Template.Universes]
u:149 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
u:149 [in MetaCoq.Erasure.EArities]
u:149 [in MetaCoq.PCUIC.PCUICArities]
u:149 [in MetaCoq.PCUIC.Bidirectional.BDUnique]
U:149 [in MetaCoq.PCUIC.PCUICSpine]
u:1494 [in MetaCoq.SafeChecker.PCUICSafeReduce]
u:15 [in MetaCoq.Template.EtaExpand]
u:15 [in MetaCoq.PCUIC.PCUICCumulativity]
u:15 [in MetaCoq.PCUIC.PCUICInductives]
u:15 [in MetaCoq.PCUIC.PCUICInductiveInversion]
u:15 [in MetaCoq.Translations.sigma]
u:15 [in MetaCoq.PCUIC.PCUICSN]
u:15 [in MetaCoq.Erasure.ErasureProperties]
u:15 [in MetaCoq.PCUIC.Syntax.PCUICUnivSubst]
u:15 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
u:15 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:150 [in MetaCoq.PCUIC.PCUICProgress]
u:150 [in MetaCoq.Template.WfAst]
U:150 [in MetaCoq.PCUIC.PCUICCumulProp]
u:150 [in MetaCoq.Template.common.uGraph]
U:150 [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
u:150 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:150 [in MetaCoq.Template.AstUtils]
u:151 [in MetaCoq.PCUIC.PCUICWcbvEval]
u:151 [in MetaCoq.PCUIC.PCUICContextConversion]
u:151 [in MetaCoq.Template.AstUtils]
u:152 [in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
u:152 [in MetaCoq.Template.Universes]
u:152 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
u:152 [in MetaCoq.PCUIC.PCUICInversion]
u:1522 [in MetaCoq.SafeChecker.PCUICSafeConversion]
u:1528 [in MetaCoq.SafeChecker.PCUICSafeConversion]
u:153 [in MetaCoq.Template.Universes]
u:153 [in MetaCoq.Erasure.EArities]
u:153 [in MetaCoq.Template.WfAst]
u:153 [in MetaCoq.Template.TypingWf]
u:154 [in MetaCoq.Template.Universes]
u:154 [in MetaCoq.Template.common.uGraph]
u:155 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
u:155 [in MetaCoq.Template.TermEquality]
u:155 [in MetaCoq.PCUIC.PCUICSpine]
u:156 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
u:156 [in MetaCoq.PCUIC.PCUICArities]
u:156 [in MetaCoq.Template.WfAst]
u:156 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
u:156 [in MetaCoq.SafeChecker.PCUICEqualityDec]
u:157 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:158 [in MetaCoq.Erasure.EArities]
u:158 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
u:158 [in MetaCoq.PCUIC.PCUICCanonicity]
U:158 [in MetaCoq.PCUIC.PCUICContextConversion]
u:158 [in MetaCoq.PCUIC.PCUICSR]
u:158 [in MetaCoq.SafeChecker.PCUICEqualityDec]
u:159 [in MetaCoq.Template.Universes]
u:159 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
u:16 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
u:16 [in MetaCoq.PCUIC.PCUICCumulProp]
u:16 [in MetaCoq.PCUIC.PCUICPrincipality]
u:16 [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
u:16 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
u:16 [in MetaCoq.PCUIC.Typing.PCUICNamelessTyp]
u:16 [in MetaCoq.Template.UnivSubst]
u:16 [in MetaCoq.PCUIC.PCUICContexts]
u:160 [in MetaCoq.PCUIC.PCUICEquality]
u:160 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
u:160 [in MetaCoq.Template.WcbvEval]
u:160 [in MetaCoq.Template.AstUtils]
u:161 [in MetaCoq.PCUIC.PCUICAlpha]
u:162 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
u:162 [in MetaCoq.Erasure.EArities]
U:162 [in MetaCoq.PCUIC.PCUICAlpha]
u:162 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
u:162 [in MetaCoq.PCUIC.PCUICContextConversion]
u:162 [in MetaCoq.Template.LiftSubst]
u:162 [in MetaCoq.SafeChecker.PCUICEqualityDec]
u:1620 [in MetaCoq.SafeChecker.PCUICSafeReduce]
u:163 [in MetaCoq.Template.Universes]
u:164 [in MetaCoq.PCUIC.PCUICElimination]
u:164 [in MetaCoq.PCUIC.PCUICSafeLemmata]
U:164 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
u:164 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
u:165 [in MetaCoq.PCUIC.PCUICFirstorder]
u:165 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:165 [in MetaCoq.Template.TypingWf]
u:166 [in MetaCoq.Template.Universes]
u:166 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
u:166 [in MetaCoq.PCUIC.PCUICContextConversion]
u:167 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
u:168 [in MetaCoq.Template.WcbvEval]
u:168 [in MetaCoq.PCUIC.PCUICCanonicity]
u:168 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
U:169 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
u:169 [in MetaCoq.Erasure.ERemoveParams]
u:17 [in MetaCoq.PCUIC.PCUICWfUniverses]
u:17 [in MetaCoq.Template.Normal]
u:17 [in MetaCoq.PCUIC.PCUICEquality]
u:17 [in MetaCoq.PCUIC.PCUICCSubst]
u:17 [in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
u:17 [in MetaCoq.SafeChecker.PCUICSafeReduce]
u:17 [in MetaCoq.PCUIC.PCUICReduction]
u:171 [in MetaCoq.PCUIC.PCUICSafeLemmata]
U:171 [in MetaCoq.PCUIC.PCUICContextConversion]
u:172 [in MetaCoq.Examples.tauto]
u:173 [in MetaCoq.Template.Universes]
u:173 [in MetaCoq.PCUIC.PCUICAlpha]
u:1734 [in MetaCoq.SafeChecker.PCUICSafeReduce]
U:174 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
U:174 [in MetaCoq.PCUIC.PCUICAlpha]
u:174 [in MetaCoq.SafeChecker.PCUICSafeConversion]
u:174 [in MetaCoq.PCUIC.PCUICContexts]
u:174 [in MetaCoq.SafeChecker.PCUICEqualityDec]
U:175 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
u:175 [in MetaCoq.Erasure.EArities]
u:175 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
u:176 [in MetaCoq.SafeChecker.PCUICErrors]
u:176 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
u:176 [in MetaCoq.SafeChecker.PCUICSafeConversion]
u:176 [in MetaCoq.PCUIC.PCUICContextConversion]
u:176 [in MetaCoq.Template.TypingWf]
u:176 [in MetaCoq.PCUIC.PCUICReduction]
u:1762 [in MetaCoq.SafeChecker.PCUICSafeReduce]
u:177 [in MetaCoq.PCUIC.PCUICSafeLemmata]
u:177 [in MetaCoq.PCUIC.PCUICAst]
u:178 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
u:178 [in MetaCoq.Template.Checker]
u:178 [in MetaCoq.PCUIC.PCUICCanonicity]
u:178 [in MetaCoq.PCUIC.PCUICContexts]
u:1781 [in MetaCoq.SafeChecker.PCUICSafeConversion]
u:1786 [in MetaCoq.SafeChecker.PCUICSafeConversion]
u:179 [in MetaCoq.PCUIC.PCUICArities]
u:179 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
u:179 [in MetaCoq.SafeChecker.PCUICTypeChecker]
u:1792 [in MetaCoq.SafeChecker.PCUICSafeConversion]
u:18 [in MetaCoq.PCUIC.PCUICCumulativity]
u:18 [in MetaCoq.PCUIC.Syntax.PCUICViews]
u:18 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
u:18 [in MetaCoq.PCUIC.PCUICGeneration]
u:18 [in MetaCoq.PCUIC.PCUICConversion]
u:18 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
u:18 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
u:18 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:18 [in MetaCoq.Erasure.ECSubst]
u:18 [in MetaCoq.Template.UnivSubst]
u:18 [in MetaCoq.SafeChecker.PCUICEqualityDec]
u:180 [in MetaCoq.Erasure.EArities]
u:180 [in MetaCoq.PCUIC.PCUICInductives]
u:180 [in MetaCoq.PCUIC.PCUICFirstorder]
u:180 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
u:180 [in MetaCoq.Template.WcbvEval]
u:181 [in MetaCoq.PCUIC.PCUICProgress]
u:181 [in MetaCoq.Template.Universes]
u:181 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
u:181 [in MetaCoq.SafeChecker.PCUICEqualityDec]
u:182 [in MetaCoq.PCUIC.PCUICSubstitution]
U:183 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
u:184 [in MetaCoq.Template.TermEquality]
u:184 [in MetaCoq.SafeChecker.PCUICErrors]
u:184 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
u:184 [in MetaCoq.SafeChecker.PCUICEqualityDec]
u:185 [in MetaCoq.Template.Universes]
u:185 [in MetaCoq.Erasure.EArities]
u:185 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
u:185 [in MetaCoq.PCUIC.PCUICFirstorder]
u:185 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
u:186 [in MetaCoq.Template.EtaExpand]
u:186 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
u:187 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
u:187 [in MetaCoq.Template.TermEquality]
u:187 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
u:188 [in MetaCoq.PCUIC.PCUICAst]
u:189 [in MetaCoq.Template.EtaExpand]
u:189 [in MetaCoq.PCUIC.PCUICInductives]
u:19 [in MetaCoq.PCUIC.PCUICWfUniverses]
u:19 [in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
u:19 [in MetaCoq.PCUIC.PCUICInductives]
u:19 [in MetaCoq.Erasure.ErasureFunction]
u:19 [in MetaCoq.PCUIC.Syntax.PCUICUnivSubst]
u:19 [in MetaCoq.Translations.MiniHoTT]
u:19 [in MetaCoq.PCUIC.PCUICContexts]
u:19 [in MetaCoq.Template.AstUtils]
u:190 [in MetaCoq.PCUIC.PCUICEquality]
u:190 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
u:190 [in MetaCoq.PCUIC.PCUICContextConversion]
u:190 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
u:191 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
u:191 [in MetaCoq.Erasure.EArities]
u:191 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
u:191 [in MetaCoq.Template.Checker]
u:193 [in MetaCoq.Template.EtaExpand]
u:194 [in MetaCoq.PCUIC.PCUICParallelReduction]
u:194 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
u:194 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
u:194 [in MetaCoq.SafeChecker.PCUICSafeChecker]
u:195 [in MetaCoq.PCUIC.PCUICArities]
u:195 [in MetaCoq.Template.TermEquality]
u:195 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
u:195 [in MetaCoq.PCUIC.PCUICSR]
u:1952 [in MetaCoq.SafeChecker.PCUICSafeConversion]
u:196 [in MetaCoq.PCUIC.PCUICEquality]
u:196 [in MetaCoq.SafeChecker.PCUICEqualityDec]
u:197 [in MetaCoq.Template.Universes]
u:197 [in MetaCoq.PCUIC.PCUICCanonicity]
u:198 [in MetaCoq.Template.Universes]
u:198 [in MetaCoq.Template.TermEquality]
u:198 [in MetaCoq.SafeChecker.PCUICEqualityDec]
U:199 [in MetaCoq.PCUIC.PCUICArities]
u:2 [in MetaCoq.Template.TermEquality]
u:2 [in MetaCoq.Erasure.ErasureProperties]
u:20 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
u:20 [in MetaCoq.Template.Normal]
u:20 [in MetaCoq.PCUIC.PCUICSN]
u:20 [in MetaCoq.SafeChecker.PCUICSafeReduce]
u:20 [in MetaCoq.Erasure.EAst]
u:20 [in MetaCoq.Template.Checker]
u:20 [in MetaCoq.PCUIC.PCUICConversion]
u:20 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
u:20 [in MetaCoq.Erasure.ECSubst]
u:200 [in MetaCoq.Template.Ast]
u:201 [in MetaCoq.Template.TermEquality]
u:201 [in MetaCoq.PCUIC.PCUICCanonicity]
u:201 [in MetaCoq.PCUIC.PCUICContextConversion]
u:201 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:202 [in MetaCoq.Template.Ast]
u:202 [in MetaCoq.PCUIC.PCUICEquality]
u:202 [in MetaCoq.SafeChecker.PCUICWfEnv]
u:202 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
u:203 [in MetaCoq.PCUIC.PCUICWcbvEval]
u:203 [in MetaCoq.PCUIC.PCUICEtaExpand]
u:203 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:204 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
u:205 [in MetaCoq.PCUIC.PCUICArities]
u:205 [in MetaCoq.PCUIC.PCUICEtaExpand]
u:205 [in MetaCoq.Template.Ast]
u:206 [in MetaCoq.Erasure.EInduction]
u:207 [in MetaCoq.Template.Universes]
u:207 [in MetaCoq.PCUIC.PCUICEtaExpand]
u:207 [in MetaCoq.PCUIC.PCUICContextConversion]
u:207 [in MetaCoq.PCUIC.PCUICReduction]
u:2078 [in MetaCoq.Translations.MiniHoTT]
u:2086 [in MetaCoq.Translations.MiniHoTT]
u:2086 [in MetaCoq.Translations.MiniHoTT_paths]
u:209 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
u:209 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
u:209 [in MetaCoq.PCUIC.PCUICEtaExpand]
u:209 [in MetaCoq.SafeChecker.PCUICEqualityDec]
u:2094 [in MetaCoq.Translations.MiniHoTT]
u:2094 [in MetaCoq.Translations.MiniHoTT_paths]
u:2101 [in MetaCoq.Translations.MiniHoTT]
u:2102 [in MetaCoq.Translations.MiniHoTT_paths]
u:2108 [in MetaCoq.Translations.MiniHoTT]
u:2109 [in MetaCoq.Translations.MiniHoTT_paths]
u:211 [in MetaCoq.PCUIC.PCUICReduction]
u:211 [in MetaCoq.SafeChecker.PCUICEqualityDec]
u:2116 [in MetaCoq.Translations.MiniHoTT]
u:2116 [in MetaCoq.Translations.MiniHoTT_paths]
u:212 [in MetaCoq.PCUIC.PCUICContextConversion]
u:2124 [in MetaCoq.Translations.MiniHoTT]
u:2124 [in MetaCoq.Translations.MiniHoTT_paths]
u:213 [in MetaCoq.PCUIC.PCUICEtaExpand]
u:2131 [in MetaCoq.Translations.MiniHoTT]
u:2132 [in MetaCoq.Translations.MiniHoTT_paths]
u:2138 [in MetaCoq.Translations.MiniHoTT]
u:2139 [in MetaCoq.Translations.MiniHoTT_paths]
u:214 [in MetaCoq.PCUIC.PCUICSafeLemmata]
u:214 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
u:2145 [in MetaCoq.Translations.MiniHoTT]
u:2146 [in MetaCoq.Translations.MiniHoTT_paths]
u:215 [in MetaCoq.Template.Universes]
u:215 [in MetaCoq.PCUIC.PCUICWcbvEval]
u:215 [in MetaCoq.SafeChecker.PCUICEqualityDec]
u:2152 [in MetaCoq.Translations.MiniHoTT]
u:2153 [in MetaCoq.Translations.MiniHoTT_paths]
u:2159 [in MetaCoq.Translations.MiniHoTT]
u:216 [in MetaCoq.PCUIC.PCUICCanonicity]
u:2160 [in MetaCoq.Translations.MiniHoTT_paths]
u:2167 [in MetaCoq.Translations.MiniHoTT_paths]
u:217 [in MetaCoq.Template.Universes]
u:217 [in MetaCoq.PCUIC.PCUICSafeLemmata]
u:217 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
u:217 [in MetaCoq.SafeChecker.PCUICSafeChecker]
u:218 [in MetaCoq.PCUIC.PCUICCanonicity]
u:219 [in MetaCoq.Template.Universes]
u:219 [in MetaCoq.PCUIC.PCUICAlpha]
u:219 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
u:219 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
u:22 [in MetaCoq.Examples.typing_correctness]
u:22 [in MetaCoq.PCUIC.Conversion.PCUICOnFreeVarsConv]
u:22 [in MetaCoq.PCUIC.Syntax.PCUICUnivSubst]
u:22 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
u:22 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
u:22 [in MetaCoq.Template.UnivSubst]
U:220 [in MetaCoq.PCUIC.PCUICContextConversion]
u:221 [in MetaCoq.Template.Universes]
u:221 [in MetaCoq.PCUIC.PCUICElimination]
u:221 [in MetaCoq.PCUIC.PCUICSafeLemmata]
u:221 [in MetaCoq.PCUIC.PCUICNormal]
u:221 [in MetaCoq.PCUIC.PCUICAst]
u:221 [in MetaCoq.SafeChecker.PCUICSafeReduce]
u:222 [in MetaCoq.PCUIC.PCUICEquality]
u:222 [in MetaCoq.PCUIC.PCUICCanonicity]
u:222 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
u:223 [in MetaCoq.Template.Universes]
u:224 [in MetaCoq.PCUIC.PCUICSafeLemmata]
u:224 [in MetaCoq.PCUIC.PCUICSubstitution]
u:224 [in MetaCoq.PCUIC.PCUICInductiveInversion]
u:224 [in MetaCoq.SafeChecker.PCUICWfEnv]
u:224 [in MetaCoq.Template.WcbvEval]
U:224 [in MetaCoq.PCUIC.PCUICContextConversion]
u:225 [in MetaCoq.PCUIC.PCUICWcbvEval]
u:225 [in MetaCoq.PCUIC.PCUICAlpha]
u:226 [in MetaCoq.PCUIC.PCUICCanonicity]
u:227 [in MetaCoq.PCUIC.PCUICElimination]
u:227 [in MetaCoq.PCUIC.PCUICSafeLemmata]
u:227 [in MetaCoq.Template.TermEquality]
u:228 [in MetaCoq.Template.EtaExpand]
u:228 [in MetaCoq.Template.Universes]
u:228 [in MetaCoq.PCUIC.PCUICConversion]
U:228 [in MetaCoq.PCUIC.PCUICContextConversion]
u:229 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
u:229 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
u:23 [in MetaCoq.Erasure.EArities]
u:23 [in MetaCoq.PCUIC.PCUICWfUniverses]
u:23 [in MetaCoq.Erasure.EDeps]
u:23 [in MetaCoq.PCUIC.PCUICSN]
u:23 [in MetaCoq.SafeChecker.PCUICSafeReduce]
u:23 [in MetaCoq.PCUIC.PCUICConversion]
u:23 [in MetaCoq.Erasure.ECSubst]
u:23 [in MetaCoq.Template.Induction]
u:23 [in MetaCoq.SafeChecker.PCUICEqualityDec]
u:230 [in MetaCoq.Template.Universes]
u:231 [in MetaCoq.PCUIC.PCUICSubstitution]
u:231 [in MetaCoq.PCUIC.PCUICContexts]
u:232 [in MetaCoq.PCUIC.PCUICWfUniverses]
u:232 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
U:232 [in MetaCoq.PCUIC.PCUICContextConversion]
u:232 [in MetaCoq.SafeChecker.PCUICEqualityDec]
u:233 [in MetaCoq.Template.Universes]
u:233 [in MetaCoq.PCUIC.PCUICElimination]
u:233 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
u:234 [in MetaCoq.Template.Universes]
u:234 [in MetaCoq.PCUIC.PCUICSafeLemmata]
u:234 [in MetaCoq.Erasure.EArities]
u:234 [in MetaCoq.Template.Ast]
u:234 [in MetaCoq.PCUIC.PCUICConversion]
u:234 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:234 [in MetaCoq.SafeChecker.PCUICEqualityDec]
u:235 [in MetaCoq.Template.Universes]
u:236 [in MetaCoq.PCUIC.PCUICProgress]
u:236 [in MetaCoq.PCUIC.PCUICWfUniverses]
u:236 [in MetaCoq.PCUIC.PCUICInductiveInversion]
u:237 [in MetaCoq.Template.Universes]
u:237 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
u:238 [in MetaCoq.PCUIC.PCUICSafeLemmata]
U:238 [in MetaCoq.PCUIC.PCUICContextConversion]
u:238 [in MetaCoq.SafeChecker.PCUICEqualityDec]
u:239 [in MetaCoq.PCUIC.PCUICElimination]
u:24 [in MetaCoq.PCUIC.PCUICElimination]
u:24 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
u:24 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
u:24 [in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
u:24 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
u:24 [in MetaCoq.PCUIC.PCUICContextConversion]
u:240 [in MetaCoq.PCUIC.PCUICWfUniverses]
u:240 [in MetaCoq.PCUIC.PCUICParallelReduction]
u:240 [in MetaCoq.PCUIC.PCUICAst]
U:2403 [in MetaCoq.Template.utils.All_Forall]
u:241 [in MetaCoq.Template.Universes]
u:242 [in MetaCoq.PCUIC.PCUICSafeLemmata]
u:242 [in MetaCoq.PCUIC.PCUICParallelReduction]
u:242 [in MetaCoq.PCUIC.PCUICAlpha]
u:242 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
u:243 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:244 [in MetaCoq.PCUIC.PCUICParallelReduction]
U:244 [in MetaCoq.PCUIC.PCUICContextConversion]
u:245 [in MetaCoq.PCUIC.PCUICElimination]
u:246 [in MetaCoq.Template.Universes]
u:246 [in MetaCoq.Template.Ast]
u:246 [in MetaCoq.PCUIC.PCUICInductiveInversion]
u:247 [in MetaCoq.Template.WcbvEval]
u:247 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
u:248 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
u:248 [in MetaCoq.PCUIC.PCUICAlpha]
u:248 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:25 [in MetaCoq.Template.WfAst]
u:25 [in MetaCoq.PCUIC.PCUICValidity]
u:25 [in MetaCoq.PCUIC.PCUICPrincipality]
u:25 [in MetaCoq.Erasure.ELiftSubst]
u:25 [in MetaCoq.PCUIC.Syntax.PCUICUnivSubst]
u:25 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
u:25 [in MetaCoq.Template.UnivSubst]
u:25 [in MetaCoq.Template.Induction]
u:251 [in MetaCoq.PCUIC.PCUICElimination]
u:251 [in MetaCoq.SafeChecker.PCUICEqualityDec]
u:252 [in MetaCoq.PCUIC.PCUICEquality]
u:252 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
u:253 [in MetaCoq.PCUIC.PCUICInductiveInversion]
u:253 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:253 [in MetaCoq.SafeChecker.PCUICEqualityDec]
U:254 [in MetaCoq.PCUIC.PCUICCumulProp]
u:254 [in MetaCoq.PCUIC.PCUICAlpha]
u:254 [in MetaCoq.Template.WcbvEval]
u:255 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
u:255 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
u:255 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
u:256 [in MetaCoq.PCUIC.PCUICSpine]
u:257 [in MetaCoq.PCUIC.PCUICElimination]
u:257 [in MetaCoq.Erasure.EArities]
U:257 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
u:257 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:258 [in MetaCoq.PCUIC.PCUICWcbvEval]
u:258 [in MetaCoq.PCUIC.PCUICAlpha]
u:259 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
U:259 [in MetaCoq.PCUIC.PCUICContextConversion]
u:26 [in MetaCoq.PCUIC.PCUICWfUniverses]
u:26 [in MetaCoq.PCUIC.PCUICConversion]
u:26 [in MetaCoq.PCUIC.Bidirectional.BDUnique]
u:26 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:26 [in MetaCoq.Erasure.ECSubst]
u:261 [in MetaCoq.PCUIC.PCUICInductives]
u:261 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:261 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
U:262 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
U:262 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
U:263 [in MetaCoq.PCUIC.PCUICElimination]
u:2637 [in MetaCoq.Translations.MiniHoTT]
U:264 [in MetaCoq.PCUIC.PCUICContextConversion]
u:264 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:2640 [in MetaCoq.Translations.MiniHoTT]
u:2645 [in MetaCoq.Translations.MiniHoTT_paths]
u:2647 [in MetaCoq.Translations.MiniHoTT]
u:2648 [in MetaCoq.Translations.MiniHoTT_paths]
u:265 [in MetaCoq.Template.Universes]
u:265 [in MetaCoq.Erasure.EArities]
u:265 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
u:2655 [in MetaCoq.Translations.MiniHoTT_paths]
u:2657 [in MetaCoq.Translations.MiniHoTT]
u:266 [in MetaCoq.Template.Typing]
u:266 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:2660 [in MetaCoq.Translations.MiniHoTT]
u:2665 [in MetaCoq.Translations.MiniHoTT_paths]
u:2666 [in MetaCoq.Translations.MiniHoTT]
u:2668 [in MetaCoq.Translations.MiniHoTT_paths]
u:267 [in MetaCoq.Template.Ast]
u:267 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
u:2672 [in MetaCoq.Translations.MiniHoTT]
u:2674 [in MetaCoq.Translations.MiniHoTT_paths]
u:268 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
u:268 [in MetaCoq.Template.Universes]
u:268 [in MetaCoq.PCUIC.PCUICInductiveInversion]
U:268 [in MetaCoq.PCUIC.PCUICContextConversion]
u:268 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
u:268 [in MetaCoq.SafeChecker.PCUICEqualityDec]
u:2680 [in MetaCoq.Translations.MiniHoTT_paths]
u:269 [in MetaCoq.SafeChecker.PCUICEqualityDec]
u:27 [in MetaCoq.Template.WfAst]
u:27 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
u:27 [in MetaCoq.PCUIC.PCUICSN]
u:27 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
u:27 [in MetaCoq.Translations.MiniHoTT_paths]
u:27 [in MetaCoq.Template.UnivSubst]
u:27 [in MetaCoq.PCUIC.PCUICContextReduction]
u:270 [in MetaCoq.Template.Universes]
U:270 [in MetaCoq.PCUIC.PCUICElimination]
u:270 [in MetaCoq.PCUIC.PCUICAlpha]
U:270 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
u:270 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
u:2700 [in MetaCoq.Translations.MiniHoTT]
u:2705 [in MetaCoq.Translations.MiniHoTT]
u:2708 [in MetaCoq.Translations.MiniHoTT_paths]
u:271 [in MetaCoq.SafeChecker.PCUICEqualityDec]
u:2711 [in MetaCoq.Translations.MiniHoTT]
u:2713 [in MetaCoq.Translations.MiniHoTT_paths]
u:2717 [in MetaCoq.Translations.MiniHoTT]
u:2719 [in MetaCoq.Translations.MiniHoTT_paths]
u:272 [in MetaCoq.Template.Universes]
u:272 [in MetaCoq.PCUIC.PCUICWcbvEval]
U:272 [in MetaCoq.PCUIC.PCUICContextConversion]
u:272 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
u:2724 [in MetaCoq.Translations.MiniHoTT]
u:2725 [in MetaCoq.Translations.MiniHoTT_paths]
u:2729 [in MetaCoq.Translations.MiniHoTT]
u:273 [in MetaCoq.Erasure.EArities]
u:273 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
u:273 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:2732 [in MetaCoq.Translations.MiniHoTT_paths]
u:2737 [in MetaCoq.Translations.MiniHoTT]
u:2737 [in MetaCoq.Translations.MiniHoTT_paths]
u:274 [in MetaCoq.Template.Universes]
u:274 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
u:2743 [in MetaCoq.Translations.MiniHoTT]
u:2745 [in MetaCoq.Translations.MiniHoTT_paths]
u:2749 [in MetaCoq.Translations.MiniHoTT]
u:275 [in MetaCoq.PCUIC.PCUICProgress]
u:275 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
u:2751 [in MetaCoq.Translations.MiniHoTT_paths]
u:2756 [in MetaCoq.Translations.MiniHoTT]
u:2757 [in MetaCoq.Translations.MiniHoTT_paths]
u:276 [in MetaCoq.Template.Universes]
u:276 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
u:276 [in MetaCoq.Template.common.uGraph]
u:276 [in MetaCoq.PCUIC.PCUICAlpha]
U:276 [in MetaCoq.PCUIC.PCUICContextConversion]
u:2761 [in MetaCoq.Translations.MiniHoTT]
u:2764 [in MetaCoq.Translations.MiniHoTT_paths]
u:2769 [in MetaCoq.Translations.MiniHoTT]
u:2769 [in MetaCoq.Translations.MiniHoTT_paths]
U:277 [in MetaCoq.PCUIC.PCUICElimination]
u:277 [in MetaCoq.PCUIC.PCUICInductiveInversion]
u:277 [in MetaCoq.Template.common.uGraph]
u:2775 [in MetaCoq.Translations.MiniHoTT]
u:2777 [in MetaCoq.Translations.MiniHoTT_paths]
u:278 [in MetaCoq.Template.Universes]
u:2780 [in MetaCoq.Translations.MiniHoTT]
u:2783 [in MetaCoq.Translations.MiniHoTT_paths]
u:2784 [in MetaCoq.Translations.MiniHoTT]
u:2788 [in MetaCoq.Translations.MiniHoTT_paths]
u:2789 [in MetaCoq.Translations.MiniHoTT]
u:279 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
u:279 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
u:2792 [in MetaCoq.Translations.MiniHoTT_paths]
u:2797 [in MetaCoq.Translations.MiniHoTT_paths]
u:28 [in MetaCoq.PCUIC.PCUICNormal]
u:28 [in MetaCoq.PCUIC.Syntax.PCUICUnivSubst]
u:28 [in MetaCoq.PCUIC.PCUICContextConversion]
u:28 [in MetaCoq.Template.Induction]
U:280 [in MetaCoq.PCUIC.PCUICContextConversion]
u:281 [in MetaCoq.PCUIC.PCUICAlpha]
u:281 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:2818 [in MetaCoq.Translations.MiniHoTT]
u:282 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
u:282 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
u:282 [in MetaCoq.PCUIC.PCUICCumulProp]
u:2821 [in MetaCoq.Translations.MiniHoTT]
u:2826 [in MetaCoq.Translations.MiniHoTT_paths]
u:2828 [in MetaCoq.Translations.MiniHoTT]
u:2829 [in MetaCoq.Translations.MiniHoTT_paths]
u:283 [in MetaCoq.PCUIC.PCUICProgress]
u:283 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
u:2836 [in MetaCoq.Translations.MiniHoTT_paths]
U:284 [in MetaCoq.PCUIC.PCUICElimination]
u:284 [in MetaCoq.PCUIC.PCUICSafeLemmata]
u:284 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
u:284 [in MetaCoq.PCUIC.PCUICInductiveInversion]
u:284 [in MetaCoq.PCUIC.PCUICSR]
u:285 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
u:285 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
U:285 [in MetaCoq.PCUIC.PCUICContextConversion]
u:286 [in MetaCoq.Template.Universes]
u:286 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
u:286 [in MetaCoq.Template.Ast]
u:286 [in MetaCoq.PCUIC.PCUICCumulProp]
u:286 [in MetaCoq.PCUIC.PCUICConversion]
u:2860 [in MetaCoq.Translations.MiniHoTT]
u:2868 [in MetaCoq.Translations.MiniHoTT_paths]
u:2869 [in MetaCoq.Translations.MiniHoTT]
u:287 [in MetaCoq.Template.Checker]
u:2877 [in MetaCoq.Translations.MiniHoTT_paths]
u:288 [in MetaCoq.Template.EtaExpand]
u:288 [in MetaCoq.SafeChecker.PCUICEqualityDec]
u:289 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
u:289 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
u:289 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:289 [in MetaCoq.SafeChecker.PCUICEqualityDec]
u:29 [in MetaCoq.Template.WfAst]
u:29 [in MetaCoq.PCUIC.Conversion.PCUICOnFreeVarsConv]
u:29 [in MetaCoq.PCUIC.PCUICConversion]
u:290 [in MetaCoq.PCUIC.PCUICProgress]
u:290 [in MetaCoq.Template.Universes]
u:290 [in MetaCoq.SafeChecker.PCUICEqualityDec]
U:291 [in MetaCoq.PCUIC.PCUICElimination]
u:291 [in MetaCoq.PCUIC.PCUICSafeLemmata]
u:291 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
u:2919 [in MetaCoq.Translations.MiniHoTT]
u:292 [in MetaCoq.PCUIC.PCUICConversion]
u:2927 [in MetaCoq.Translations.MiniHoTT]
u:2927 [in MetaCoq.Translations.MiniHoTT_paths]
u:293 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
u:293 [in MetaCoq.PCUIC.PCUICInductives]
u:293 [in MetaCoq.Template.Ast]
u:2935 [in MetaCoq.Translations.MiniHoTT_paths]
u:294 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
u:294 [in MetaCoq.PCUIC.PCUICConversion]
u:295 [in MetaCoq.Template.Universes]
u:295 [in MetaCoq.Erasure.EArities]
U:295 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
u:295 [in MetaCoq.PCUIC.PCUICCumulProp]
u:296 [in MetaCoq.Template.Universes]
u:297 [in MetaCoq.PCUIC.PCUICSR]
U:298 [in MetaCoq.PCUIC.PCUICElimination]
u:298 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
u:298 [in MetaCoq.Template.Typing]
u:299 [in MetaCoq.Template.Universes]
u:299 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
u:299 [in MetaCoq.PCUIC.PCUICConversion]
u:3 [in MetaCoq.PCUIC.PCUICCSubst]
u:3 [in MetaCoq.PCUIC.Syntax.PCUICCases]
u:3 [in MetaCoq.Template.WcbvEval]
u:3 [in MetaCoq.PCUIC.Syntax.PCUICUnivSubst]
u:3 [in MetaCoq.Erasure.ECSubst]
u:3 [in MetaCoq.Template.UnivSubst]
u:30 [in MetaCoq.SafeChecker.PCUICWfReduction]
u:30 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
u:300 [in MetaCoq.PCUIC.PCUICProgress]
u:301 [in MetaCoq.Erasure.EArities]
u:301 [in MetaCoq.PCUIC.PCUICCumulProp]
U:301 [in MetaCoq.PCUIC.PCUICContextConversion]
u:302 [in MetaCoq.Template.Typing]
u:303 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
u:304 [in MetaCoq.PCUIC.PCUICConversion]
u:304 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
u:304 [in MetaCoq.PCUIC.PCUICContextConversion]
u:305 [in MetaCoq.Template.Universes]
U:305 [in MetaCoq.PCUIC.PCUICElimination]
u:305 [in MetaCoq.PCUIC.PCUICWcbvEval]
u:305 [in MetaCoq.SafeChecker.PCUICEqualityDec]
u:306 [in MetaCoq.PCUIC.PCUICConfluence]
u:306 [in MetaCoq.PCUIC.PCUICConversion]
u:306 [in MetaCoq.SafeChecker.PCUICEqualityDec]
u:307 [in MetaCoq.Template.Environment]
u:308 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
u:308 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:309 [in MetaCoq.Template.Universes]
u:309 [in MetaCoq.PCUIC.PCUICWcbvEval]
u:309 [in MetaCoq.PCUIC.PCUICSR]
u:31 [in MetaCoq.PCUIC.PCUICWfUniverses]
u:31 [in MetaCoq.PCUIC.PCUICValidity]
u:31 [in MetaCoq.Template.Normal]
u:31 [in MetaCoq.PCUIC.PCUICNormal]
u:31 [in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
u:31 [in MetaCoq.Erasure.EAstUtils]
u:310 [in MetaCoq.PCUIC.PCUICConversion]
u:311 [in MetaCoq.Template.Universes]
u:311 [in MetaCoq.PCUIC.PCUICCumulProp]
u:311 [in MetaCoq.SafeChecker.PCUICEqualityDec]
u:312 [in MetaCoq.PCUIC.PCUICElimination]
U:312 [in MetaCoq.PCUIC.PCUICContextConversion]
u:312 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:312 [in MetaCoq.Template.TypingWf]
u:312 [in MetaCoq.SafeChecker.PCUICEqualityDec]
u:313 [in MetaCoq.Template.Universes]
u:314 [in MetaCoq.PCUIC.PCUICInductiveInversion]
u:314 [in MetaCoq.Template.WcbvEval]
u:315 [in MetaCoq.Template.Universes]
u:315 [in MetaCoq.PCUIC.PCUICWcbvEval]
u:315 [in MetaCoq.PCUIC.PCUICCumulProp]
u:316 [in MetaCoq.Template.TypingWf]
u:317 [in MetaCoq.Template.Universes]
u:317 [in MetaCoq.PCUIC.PCUICElimination]
u:317 [in MetaCoq.PCUIC.PCUICInductives]
u:318 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:318 [in MetaCoq.Template.TypingWf]
U:319 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
u:32 [in MetaCoq.Template.WfAst]
u:32 [in MetaCoq.PCUIC.PCUICEtaExpand]
u:32 [in MetaCoq.SafeChecker.PCUICWfReduction]
u:32 [in MetaCoq.PCUIC.Syntax.PCUICUnivSubst]
u:32 [in MetaCoq.PCUIC.PCUICConversion]
u:32 [in MetaCoq.PCUIC.PCUICContextReduction]
u:320 [in MetaCoq.Template.Universes]
U:320 [in MetaCoq.PCUIC.PCUICConversion]
u:320 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:321 [in MetaCoq.Template.Checker]
u:321 [in MetaCoq.SafeChecker.PCUICEqualityDec]
u:322 [in MetaCoq.PCUIC.PCUICElimination]
u:322 [in MetaCoq.PCUIC.PCUICConfluence]
u:322 [in MetaCoq.SafeChecker.PCUICEqualityDec]
u:323 [in MetaCoq.Template.Universes]
u:323 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:323 [in MetaCoq.PCUIC.PCUICReduction]
u:323 [in MetaCoq.SafeChecker.PCUICEqualityDec]
U:324 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
u:325 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
u:325 [in MetaCoq.Template.Universes]
u:325 [in MetaCoq.Template.Ast]
u:325 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:325 [in MetaCoq.Template.TypingWf]
U:326 [in MetaCoq.PCUIC.PCUICConversion]
u:327 [in MetaCoq.PCUIC.PCUICElimination]
u:327 [in MetaCoq.SafeChecker.PCUICEqualityDec]
u:328 [in MetaCoq.PCUIC.PCUICInductives]
u:328 [in MetaCoq.Template.Ast]
u:328 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:329 [in MetaCoq.Template.Universes]
u:329 [in MetaCoq.Erasure.EArities]
u:329 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:33 [in MetaCoq.Translations.times_bool_fun]
U:33 [in MetaCoq.PCUIC.PCUICArities]
u:33 [in MetaCoq.PCUIC.PCUICWfUniverses]
u:330 [in MetaCoq.Erasure.ERemoveParams]
u:331 [in MetaCoq.PCUIC.PCUICProgress]
u:331 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
u:331 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:332 [in MetaCoq.PCUIC.PCUICNormal]
u:332 [in MetaCoq.PCUIC.PCUICSR]
u:333 [in MetaCoq.Template.common.uGraph]
u:333 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:335 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:336 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
u:336 [in MetaCoq.Template.TypingWf]
u:338 [in MetaCoq.Template.common.uGraph]
u:338 [in MetaCoq.PCUIC.PCUICSR]
u:338 [in MetaCoq.Template.TypingWf]
u:339 [in MetaCoq.PCUIC.PCUICInductives]
u:339 [in MetaCoq.Template.common.uGraph]
u:339 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
u:339 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:34 [in MetaCoq.PCUIC.PCUICElimination]
u:34 [in MetaCoq.PCUIC.PCUICEtaExpand]
u:34 [in MetaCoq.SafeChecker.PCUICSafeReduce]
u:34 [in MetaCoq.Erasure.EAstUtils]
u:34 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:341 [in MetaCoq.Template.Universes]
u:342 [in MetaCoq.PCUIC.PCUICConversion]
u:342 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:343 [in MetaCoq.Template.Universes]
u:343 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
u:343 [in MetaCoq.Template.common.uGraph]
u:344 [in MetaCoq.PCUIC.PCUICWcbvEval]
u:345 [in MetaCoq.PCUIC.PCUICWcbvEval]
u:346 [in MetaCoq.PCUIC.PCUICInductiveInversion]
u:346 [in MetaCoq.Erasure.EWcbvEval]
u:347 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
u:347 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:349 [in MetaCoq.PCUIC.PCUICConversion]
u:349 [in MetaCoq.SafeChecker.PCUICEqualityDec]
u:35 [in MetaCoq.PCUIC.Syntax.PCUICUnivSubst]
u:35 [in MetaCoq.PCUIC.PCUICConversion]
u:35 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
u:350 [in MetaCoq.PCUIC.PCUICCumulProp]
u:350 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
U:351 [in MetaCoq.Erasure.EArities]
u:351 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
u:351 [in MetaCoq.PCUIC.PCUICInductives]
u:351 [in MetaCoq.Template.common.uGraph]
u:351 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
U:352 [in MetaCoq.PCUIC.PCUICSubstitution]
u:352 [in MetaCoq.Template.TypingWf]
u:353 [in MetaCoq.Template.common.uGraph]
u:353 [in MetaCoq.PCUIC.PCUICConfluence]
u:353 [in MetaCoq.SafeChecker.PCUICEqualityDec]
u:354 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
u:354 [in MetaCoq.PCUIC.PCUICConversion]
u:355 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:355 [in MetaCoq.Template.TypingWf]
u:356 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
u:356 [in MetaCoq.PCUIC.PCUICSR]
u:356 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:356 [in MetaCoq.Erasure.EWcbvEval]
u:36 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
u:36 [in MetaCoq.PCUIC.PCUICWfUniverses]
u:36 [in MetaCoq.PCUIC.TemplateToPCUICExpanded]
u:360 [in MetaCoq.PCUIC.PCUICCumulProp]
u:360 [in MetaCoq.PCUIC.PCUICConversion]
u:362 [in MetaCoq.PCUIC.PCUICInductiveInversion]
u:363 [in MetaCoq.PCUIC.PCUICWcbvEval]
u:364 [in MetaCoq.PCUIC.PCUICInductiveInversion]
u:364 [in MetaCoq.Template.utils.wGraph]
u:365 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:366 [in MetaCoq.Template.common.uGraph]
u:366 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
u:367 [in MetaCoq.PCUIC.PCUICNormal]
u:368 [in MetaCoq.SafeChecker.PCUICEqualityDec]
u:369 [in MetaCoq.Erasure.EEtaExpandedFix]
u:369 [in MetaCoq.Template.utils.wGraph]
u:369 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:37 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
u:37 [in MetaCoq.PCUIC.PCUICCumulativity]
u:37 [in MetaCoq.PCUIC.PCUICAlpha]
u:37 [in MetaCoq.PCUIC.Syntax.PCUICUnivSubst]
u:37 [in MetaCoq.PCUIC.PCUICCanonicity]
u:370 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
u:370 [in MetaCoq.PCUIC.PCUICParallelReduction]
u:370 [in MetaCoq.Translations.MiniHoTT]
u:371 [in MetaCoq.PCUIC.PCUICInductiveInversion]
U:372 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
u:373 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:375 [in MetaCoq.PCUIC.PCUICProgress]
U:375 [in MetaCoq.PCUIC.PCUICCumulProp]
u:375 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
u:376 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
u:377 [in MetaCoq.Translations.MiniHoTT]
u:378 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
u:378 [in MetaCoq.Translations.MiniHoTT_paths]
u:379 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
u:379 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
u:379 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:379 [in MetaCoq.PCUIC.PCUICReduction]
u:38 [in MetaCoq.Erasure.Extract]
u:38 [in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
u:38 [in MetaCoq.PCUIC.PCUICSN]
u:38 [in MetaCoq.PCUIC.PCUICConversion]
u:38 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
u:380 [in MetaCoq.PCUIC.PCUICInductives]
u:380 [in MetaCoq.PCUIC.PCUICInductiveInversion]
u:382 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
u:383 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
u:383 [in MetaCoq.PCUIC.PCUICReduction]
u:384 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
u:384 [in MetaCoq.Translations.MiniHoTT]
u:384 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:385 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
u:385 [in MetaCoq.Translations.MiniHoTT_paths]
u:386 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:387 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
u:387 [in MetaCoq.PCUIC.PCUICSR]
u:388 [in MetaCoq.PCUIC.PCUICInductiveInversion]
u:388 [in MetaCoq.PCUIC.PCUICReduction]
u:388 [in MetaCoq.PCUIC.PCUICSpine]
u:389 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
u:389 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
u:389 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
u:389 [in MetaCoq.PCUIC.PCUICInductives]
u:389 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:39 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
u:39 [in MetaCoq.SafeChecker.PCUICSafeReduce]
u:390 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
U:391 [in MetaCoq.PCUIC.PCUICSubstitution]
u:391 [in MetaCoq.Translations.MiniHoTT]
u:391 [in MetaCoq.PCUIC.PCUICSR]
u:392 [in MetaCoq.PCUIC.PCUICProgress]
u:392 [in MetaCoq.Translations.MiniHoTT_paths]
u:393 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
u:393 [in MetaCoq.SafeChecker.PCUICEqualityDec]
u:394 [in MetaCoq.PCUIC.PCUICInductives]
u:394 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:395 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
u:395 [in MetaCoq.SafeChecker.PCUICEqualityDec]
u:396 [in MetaCoq.PCUIC.PCUICWcbvEval]
u:397 [in MetaCoq.PCUIC.PCUICConfluence]
u:398 [in MetaCoq.Translations.MiniHoTT]
u:399 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
U:399 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
u:399 [in MetaCoq.Template.common.uGraph]
u:399 [in MetaCoq.Translations.MiniHoTT_paths]
u:4 [in MetaCoq.SafeChecker.PCUICEqualityDec]
U:40 [in MetaCoq.PCUIC.PCUICProgress]
u:40 [in MetaCoq.PCUIC.PCUICArities]
u:40 [in MetaCoq.PCUIC.PCUICWfUniverses]
u:40 [in MetaCoq.PCUIC.PCUICFirstorder]
u:40 [in MetaCoq.PCUIC.Syntax.PCUICUnivSubst]
u:40 [in MetaCoq.PCUIC.PCUICConversion]
u:40 [in MetaCoq.PCUIC.PCUICGuardCondition]
u:40 [in MetaCoq.SafeChecker.PCUICEqualityDec]
u:401 [in MetaCoq.SafeChecker.PCUICEqualityDec]
U:402 [in MetaCoq.PCUIC.PCUICSubstitution]
u:403 [in MetaCoq.PCUIC.PCUICInductives]
u:404 [in MetaCoq.PCUIC.PCUICProgress]
U:404 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
u:404 [in MetaCoq.PCUIC.PCUICNormal]
u:405 [in MetaCoq.SafeChecker.PCUICEqualityDec]
u:406 [in MetaCoq.PCUIC.PCUICNormal]
u:406 [in MetaCoq.Translations.MiniHoTT]
u:406 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
u:406 [in MetaCoq.Translations.MiniHoTT_paths]
U:407 [in MetaCoq.PCUIC.PCUICSubstitution]
u:408 [in MetaCoq.Template.EtaExpand]
u:408 [in MetaCoq.SafeChecker.PCUICEqualityDec]
u:41 [in MetaCoq.PCUIC.PCUICAlpha]
u:41 [in MetaCoq.PCUIC.PCUICSN]
U:41 [in MetaCoq.PCUIC.PCUICContextConversion]
u:41 [in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
u:410 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
u:410 [in MetaCoq.SafeChecker.PCUICEqualityDec]
u:412 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
u:412 [in MetaCoq.SafeChecker.PCUICEqualityDec]
u:414 [in MetaCoq.Erasure.EEtaExpandedFix]
u:414 [in MetaCoq.Translations.MiniHoTT]
u:414 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
u:414 [in MetaCoq.Translations.MiniHoTT_paths]
u:414 [in MetaCoq.SafeChecker.PCUICEqualityDec]
u:415 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
u:417 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
u:417 [in MetaCoq.PCUIC.PCUICInductives]
u:418 [in MetaCoq.PCUIC.PCUICConfluence]
u:418 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
u:419 [in MetaCoq.Template.EtaExpand]
u:419 [in MetaCoq.SafeChecker.PCUICEqualityDec]
u:42 [in MetaCoq.Erasure.Extract]
u:42 [in MetaCoq.PCUIC.PCUICCumulProp]
u:42 [in MetaCoq.PCUIC.PCUICAlpha]
u:42 [in MetaCoq.PCUIC.Syntax.PCUICUnivSubst]
u:42 [in MetaCoq.PCUIC.PCUICConversion]
u:42 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:42 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
u:42 [in MetaCoq.Template.TypingWf]
u:420 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
u:420 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:422 [in MetaCoq.Translations.MiniHoTT]
u:422 [in MetaCoq.Translations.MiniHoTT_paths]
u:423 [in MetaCoq.PCUIC.PCUICParallelReduction]
U:427 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
u:427 [in MetaCoq.PCUIC.PCUICParallelReduction]
u:428 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
u:428 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:429 [in MetaCoq.PCUIC.PCUICInductiveInversion]
u:429 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:43 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
u:43 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
u:43 [in MetaCoq.PCUIC.PCUICWfUniverses]
u:43 [in MetaCoq.Template.TermEquality]
u:43 [in MetaCoq.PCUIC.PCUICInductives]
u:43 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
u:43 [in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
u:43 [in MetaCoq.SafeChecker.PCUICSafeReduce]
u:43 [in MetaCoq.Erasure.ELiftSubst]
u:43 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
u:43 [in MetaCoq.PCUIC.PCUICContexts]
u:430 [in MetaCoq.Template.Universes]
u:430 [in MetaCoq.Translations.MiniHoTT_paths]
u:431 [in MetaCoq.PCUIC.PCUICInductiveInversion]
u:431 [in MetaCoq.PCUIC.PCUICParallelReduction]
u:431 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
U:432 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
u:433 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:434 [in MetaCoq.PCUIC.PCUICInductives]
u:435 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
u:436 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
U:437 [in MetaCoq.PCUIC.PCUICEquality]
u:44 [in MetaCoq.PCUIC.PCUICElimination]
u:44 [in MetaCoq.PCUIC.PCUICSN]
u:44 [in MetaCoq.PCUIC.Conversion.PCUICClosedConv]
u:444 [in MetaCoq.PCUIC.PCUICInductiveInversion]
U:444 [in MetaCoq.PCUIC.PCUICEquality]
u:444 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:446 [in MetaCoq.PCUIC.PCUICSubstitution]
u:447 [in MetaCoq.Template.EnvironmentTyping]
u:447 [in MetaCoq.PCUIC.PCUICConversion]
u:447 [in MetaCoq.PCUIC.PCUICTyping]
u:448 [in MetaCoq.PCUIC.PCUICSubstitution]
u:449 [in MetaCoq.PCUIC.PCUICInductiveInversion]
u:449 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
u:45 [in MetaCoq.PCUIC.PCUICSafeLemmata]
u:45 [in MetaCoq.PCUIC.PCUICInductives]
u:45 [in MetaCoq.SafeChecker.PCUICWfReduction]
u:45 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:45 [in MetaCoq.PCUIC.PCUICReduction]
u:45 [in MetaCoq.SafeChecker.PCUICEqualityDec]
u:450 [in MetaCoq.PCUIC.PCUICTyping]
u:451 [in MetaCoq.PCUIC.PCUICSubstitution]
u:451 [in MetaCoq.PCUIC.PCUICConversion]
u:451 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
u:454 [in MetaCoq.Template.Typing]
u:455 [in MetaCoq.Template.common.uGraph]
u:456 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:457 [in MetaCoq.Template.Universes]
u:458 [in MetaCoq.Template.common.uGraph]
u:459 [in MetaCoq.Template.Typing]
u:459 [in MetaCoq.PCUIC.PCUICEquality]
u:46 [in MetaCoq.PCUIC.PCUICCumulProp]
u:46 [in MetaCoq.PCUIC.PCUICEquality]
u:46 [in MetaCoq.SafeChecker.PCUICSafeConversion]
u:46 [in MetaCoq.Erasure.ELiftSubst]
u:46 [in MetaCoq.SafeChecker.PCUICSafeChecker]
u:460 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:461 [in MetaCoq.Template.common.uGraph]
u:461 [in MetaCoq.PCUIC.PCUICConversion]
u:463 [in MetaCoq.Template.Universes]
u:463 [in MetaCoq.PCUIC.PCUICInductives]
u:463 [in MetaCoq.Template.common.uGraph]
u:463 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
u:464 [in MetaCoq.PCUIC.PCUICInductiveInversion]
u:464 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:465 [in MetaCoq.Template.Universes]
U:466 [in MetaCoq.PCUIC.PCUICSubstitution]
u:466 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
u:466 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:467 [in MetaCoq.Template.Typing]
u:467 [in MetaCoq.PCUIC.PCUICInductives]
u:467 [in MetaCoq.PCUIC.PCUICEquality]
u:468 [in MetaCoq.PCUIC.PCUICConversion]
u:469 [in MetaCoq.Template.Typing]
u:469 [in MetaCoq.PCUIC.PCUICConfluence]
u:469 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:47 [in MetaCoq.PCUIC.PCUICProgress]
u:47 [in MetaCoq.PCUIC.PCUICSafeLemmata]
u:47 [in MetaCoq.PCUIC.PCUICInductives]
u:47 [in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
u:47 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
u:471 [in MetaCoq.PCUIC.PCUICInductives]
u:471 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
u:472 [in MetaCoq.Template.Typing]
u:472 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
u:473 [in MetaCoq.PCUIC.PCUICInductiveInversion]
u:474 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:475 [in MetaCoq.PCUIC.PCUICProgress]
u:475 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
u:475 [in MetaCoq.PCUIC.PCUICConversion]
u:476 [in MetaCoq.PCUIC.PCUICTyping]
u:478 [in MetaCoq.PCUIC.PCUICInductiveInversion]
U:478 [in MetaCoq.PCUIC.PCUICEquality]
u:48 [in MetaCoq.PCUIC.PCUICInductives]
u:48 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:48 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
u:48 [in MetaCoq.PCUIC.PCUICReduction]
u:480 [in MetaCoq.PCUIC.PCUICInductives]
u:480 [in MetaCoq.PCUIC.PCUICConversion]
u:480 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:481 [in MetaCoq.Template.common.uGraph]
u:481 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
u:483 [in MetaCoq.PCUIC.PCUICProgress]
u:484 [in MetaCoq.Template.common.uGraph]
u:485 [in MetaCoq.PCUIC.PCUICInductiveInversion]
U:485 [in MetaCoq.PCUIC.PCUICEquality]
u:486 [in MetaCoq.Template.Typing]
u:486 [in MetaCoq.PCUIC.PCUICInductives]
u:486 [in MetaCoq.PCUIC.PCUICInductiveInversion]
u:486 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
u:487 [in MetaCoq.Template.common.uGraph]
u:487 [in MetaCoq.PCUIC.PCUICConversion]
u:487 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:488 [in MetaCoq.PCUIC.PCUICInductiveInversion]
u:488 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
u:489 [in MetaCoq.PCUIC.PCUICInductives]
u:489 [in MetaCoq.PCUIC.PCUICInductiveInversion]
u:49 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
u:49 [in MetaCoq.Erasure.EArities]
u:49 [in MetaCoq.PCUIC.PCUICFirstorder]
u:49 [in MetaCoq.SafeChecker.PCUICWfReduction]
u:49 [in MetaCoq.Erasure.ELiftSubst]
u:49 [in MetaCoq.SafeChecker.PCUICTypeChecker]
u:490 [in MetaCoq.PCUIC.PCUICConfluence]
u:492 [in MetaCoq.PCUIC.PCUICInductiveInversion]
u:492 [in MetaCoq.PCUIC.PCUICConversion]
u:493 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
u:493 [in MetaCoq.PCUIC.PCUICSpine]
u:495 [in MetaCoq.PCUIC.PCUICInductiveInversion]
u:495 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:497 [in MetaCoq.Template.Universes]
u:498 [in MetaCoq.PCUIC.PCUICInductiveInversion]
U:499 [in MetaCoq.PCUIC.PCUICConversion]
u:5 [in MetaCoq.PCUIC.PCUICCumulativity]
u:5 [in MetaCoq.PCUIC.PCUICWfUniverses]
u:5 [in MetaCoq.Erasure.Extract]
u:5 [in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
u:5 [in MetaCoq.PCUIC.Syntax.PCUICCases]
u:5 [in MetaCoq.PCUIC.PCUICConvCumInversion]
u:50 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
u:50 [in MetaCoq.PCUIC.PCUICInductiveInversion]
u:50 [in MetaCoq.PCUIC.PCUICSN]
u:50 [in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
u:501 [in MetaCoq.PCUIC.PCUICInductives]
u:501 [in MetaCoq.PCUIC.PCUICInductiveInversion]
u:502 [in MetaCoq.Template.Universes]
u:502 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
u:505 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:506 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:507 [in MetaCoq.Erasure.EEtaExpandedFix]
u:509 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:51 [in MetaCoq.PCUIC.PCUICCumulativity]
U:51 [in MetaCoq.PCUIC.PCUICValidity]
u:51 [in MetaCoq.SafeChecker.PCUICSafeConversion]
u:51 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:510 [in MetaCoq.PCUIC.PCUICEquality]
U:511 [in MetaCoq.PCUIC.PCUICSR]
u:512 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:513 [in MetaCoq.PCUIC.PCUICInductives]
u:513 [in MetaCoq.PCUIC.PCUICTyping]
u:514 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
U:517 [in MetaCoq.PCUIC.PCUICSR]
u:517 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:518 [in MetaCoq.Template.EnvironmentTyping]
u:519 [in MetaCoq.Template.Universes]
u:519 [in MetaCoq.PCUIC.PCUICEquality]
u:52 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
u:52 [in MetaCoq.Erasure.EArities]
u:52 [in MetaCoq.PCUIC.PCUICWfUniverses]
u:52 [in MetaCoq.PCUIC.PCUICNormal]
u:520 [in MetaCoq.PCUIC.PCUICConfluence]
u:521 [in MetaCoq.PCUIC.PCUICInductiveInversion]
U:522 [in MetaCoq.PCUIC.PCUICConversion]
u:522 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:523 [in MetaCoq.Template.Universes]
u:524 [in MetaCoq.Template.common.uGraph]
u:524 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
U:524 [in MetaCoq.PCUIC.PCUICSR]
u:525 [in MetaCoq.PCUIC.PCUICInductives]
u:525 [in MetaCoq.PCUIC.PCUICTyping]
u:525 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:526 [in MetaCoq.Template.common.uGraph]
u:527 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
u:527 [in MetaCoq.PCUIC.PCUICInductiveInversion]
u:53 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
u:53 [in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
u:53 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
u:53 [in MetaCoq.PCUIC.PCUICContexts]
u:53 [in MetaCoq.Template.AstUtils]
u:530 [in MetaCoq.Template.Typing]
u:531 [in MetaCoq.Template.EnvironmentTyping]
U:531 [in MetaCoq.PCUIC.PCUICSR]
u:532 [in MetaCoq.PCUIC.PCUICTyping]
u:534 [in MetaCoq.PCUIC.PCUICEquality]
u:535 [in MetaCoq.Template.Universes]
u:535 [in MetaCoq.PCUIC.PCUICSubstitution]
u:536 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
U:537 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
u:538 [in MetaCoq.Template.Universes]
U:538 [in MetaCoq.PCUIC.PCUICSR]
u:538 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:539 [in MetaCoq.PCUIC.PCUICConfluence]
u:54 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
u:54 [in MetaCoq.PCUIC.PCUICSafeLemmata]
u:54 [in MetaCoq.Template.Checker]
u:54 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
u:540 [in MetaCoq.Template.common.uGraph]
u:542 [in MetaCoq.PCUIC.PCUICSubstitution]
u:542 [in MetaCoq.PCUIC.PCUICEquality]
u:542 [in MetaCoq.PCUIC.PCUICTyping]
u:545 [in MetaCoq.PCUIC.PCUICInductiveInversion]
U:547 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
u:547 [in MetaCoq.PCUIC.PCUICEquality]
u:547 [in MetaCoq.SafeChecker.PCUICTypeChecker]
u:548 [in MetaCoq.PCUIC.PCUICInductiveInversion]
u:548 [in MetaCoq.PCUIC.PCUICConfluence]
u:548 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:55 [in MetaCoq.Translations.times_bool_fun]
u:55 [in MetaCoq.PCUIC.PCUICWfUniverses]
u:55 [in MetaCoq.PCUIC.PCUICNormal]
u:55 [in MetaCoq.SafeChecker.PCUICSafeConversion]
u:55 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:55 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
u:552 [in MetaCoq.SafeChecker.PCUICTypeChecker]
u:556 [in MetaCoq.PCUIC.PCUICInductiveInversion]
U:558 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
u:558 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:559 [in MetaCoq.PCUIC.PCUICInductiveInversion]
u:56 [in MetaCoq.PCUIC.PCUICCumulativity]
u:56 [in MetaCoq.Template.Normal]
u:56 [in MetaCoq.SafeChecker.PCUICWfReduction]
u:56 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
u:560 [in MetaCoq.PCUIC.PCUICEquality]
u:563 [in MetaCoq.PCUIC.PCUICInductiveInversion]
u:5642 [in MetaCoq.SafeChecker.PCUICSafeConversion]
u:5649 [in MetaCoq.SafeChecker.PCUICSafeConversion]
u:565 [in MetaCoq.PCUIC.PCUICEquality]
u:565 [in MetaCoq.PCUIC.PCUICConversion]
u:566 [in MetaCoq.Template.Universes]
u:566 [in MetaCoq.Template.Typing]
U:566 [in MetaCoq.PCUIC.PCUICConfluence]
u:567 [in MetaCoq.PCUIC.PCUICInductiveInversion]
u:567 [in MetaCoq.PCUIC.PCUICParallelReduction]
u:569 [in MetaCoq.Template.Universes]
u:569 [in MetaCoq.PCUIC.PCUICConfluence]
u:57 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
u:57 [in MetaCoq.PCUIC.Syntax.PCUICViews]
u:57 [in MetaCoq.PCUIC.PCUICEtaExpand]
u:57 [in MetaCoq.SafeChecker.PCUICSafeConversion]
u:57 [in MetaCoq.Template.Checker]
u:57 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
u:57 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:571 [in MetaCoq.PCUIC.PCUICEquality]
u:571 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
u:572 [in MetaCoq.Template.Universes]
u:573 [in MetaCoq.PCUIC.PCUICTyping]
u:576 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:577 [in MetaCoq.PCUIC.PCUICInductiveInversion]
u:577 [in MetaCoq.SafeChecker.PCUICSafeConversion]
u:579 [in MetaCoq.SafeChecker.PCUICSafeConversion]
u:58 [in MetaCoq.Erasure.EInduction]
u:58 [in MetaCoq.Template.utils.ReflectEq]
u:58 [in MetaCoq.PCUIC.PCUICSN]
u:58 [in MetaCoq.Erasure.ErasureProperties]
u:580 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:584 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:586 [in MetaCoq.Template.EnvironmentTyping]
u:587 [in MetaCoq.PCUIC.PCUICSR]
u:588 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:59 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
u:59 [in MetaCoq.PCUIC.PCUICWfUniverses]
u:59 [in MetaCoq.Template.Normal]
u:59 [in MetaCoq.Template.Checker]
u:591 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
u:591 [in MetaCoq.PCUIC.PCUICInductiveInversion]
u:592 [in MetaCoq.PCUIC.PCUICSR]
u:596 [in MetaCoq.PCUIC.PCUICSR]
u:596 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:6 [in MetaCoq.PCUIC.PCUICElimination]
U:6 [in MetaCoq.PCUIC.PCUICInductiveInversion]
u:6 [in MetaCoq.Template.utils.MCEquality]
u:6 [in MetaCoq.PCUIC.PCUICEquality]
u:6 [in MetaCoq.PCUIC.Syntax.PCUICReflect]
u:6 [in MetaCoq.Template.monad_utils]
u:6 [in MetaCoq.Template.UnivSubst]
u:6 [in MetaCoq.Translations.param_generous_packed]
u:60 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
u:60 [in MetaCoq.PCUIC.PCUICSafeLemmata]
u:60 [in MetaCoq.PCUIC.PCUICInductives]
u:60 [in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
u:60 [in MetaCoq.PCUIC.PCUICPrincipality]
u:601 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:604 [in MetaCoq.PCUIC.PCUICSR]
u:606 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:609 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:61 [in MetaCoq.Erasure.EInduction]
u:61 [in MetaCoq.PCUIC.PCUICCumulativity]
u:61 [in MetaCoq.PCUIC.PCUICCumulProp]
u:61 [in MetaCoq.SafeChecker.PCUICSafeConversion]
u:61 [in MetaCoq.Template.Environment]
u:61 [in MetaCoq.PCUIC.PCUICContexts]
u:610 [in MetaCoq.PCUIC.PCUICSR]
u:611 [in MetaCoq.PCUIC.PCUICSubstitution]
U:612 [in MetaCoq.PCUIC.PCUICSubstitution]
u:613 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
u:617 [in MetaCoq.Template.utils.wGraph]
u:619 [in MetaCoq.PCUIC.PCUICEquality]
u:62 [in MetaCoq.PCUIC.PCUICWeakeningEnv]
u:62 [in MetaCoq.PCUIC.PCUICSN]
u:62 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
u:62 [in MetaCoq.Template.Pretty]
u:62 [in MetaCoq.Erasure.EOptimizePropDiscr]
u:62 [in MetaCoq.Template.Induction]
u:620 [in MetaCoq.Template.Universes]
u:620 [in MetaCoq.PCUIC.PCUICSubstitution]
u:620 [in MetaCoq.Template.utils.wGraph]
U:621 [in MetaCoq.PCUIC.PCUICSubstitution]
U:622 [in MetaCoq.PCUIC.PCUICInductiveInversion]
u:622 [in MetaCoq.PCUIC.PCUICSR]
u:623 [in MetaCoq.Template.Universes]
u:623 [in MetaCoq.PCUIC.PCUICInductiveInversion]
u:623 [in MetaCoq.Template.utils.wGraph]
u:625 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
u:625 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
u:626 [in MetaCoq.PCUIC.PCUICInductiveInversion]
u:626 [in MetaCoq.Template.utils.wGraph]
u:628 [in MetaCoq.Template.Universes]
u:628 [in MetaCoq.PCUIC.PCUICSR]
u:628 [in MetaCoq.PCUIC.PCUICSpine]
u:630 [in MetaCoq.Template.utils.wGraph]
u:630 [in MetaCoq.PCUIC.PCUICConversion]
u:632 [in MetaCoq.Template.Universes]
u:632 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
u:632 [in MetaCoq.PCUIC.PCUICConversion]
u:633 [in MetaCoq.Template.Typing]
u:633 [in MetaCoq.PCUIC.PCUICSpine]
u:634 [in MetaCoq.Template.utils.wGraph]
u:636 [in MetaCoq.Template.Universes]
u:636 [in MetaCoq.PCUIC.PCUICInductives]
u:637 [in MetaCoq.Template.Typing]
u:637 [in MetaCoq.SafeChecker.PCUICSafeConversion]
u:639 [in MetaCoq.SafeChecker.PCUICSafeConversion]
u:64 [in MetaCoq.Erasure.EInduction]
u:64 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
u:64 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
u:64 [in MetaCoq.Template.Induction]
u:642 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
u:643 [in MetaCoq.Template.Typing]
u:644 [in MetaCoq.PCUIC.PCUICInductives]
u:644 [in MetaCoq.Template.utils.wGraph]
u:647 [in MetaCoq.PCUIC.PCUICConversion]
u:648 [in MetaCoq.Template.utils.wGraph]
u:648 [in MetaCoq.SafeChecker.PCUICTypeChecker]
u:649 [in MetaCoq.SafeChecker.PCUICSafeConversion]
u:65 [in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
u:65 [in MetaCoq.Template.Checker]
u:65 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
U:650 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
u:651 [in MetaCoq.PCUIC.PCUICInductiveInversion]
u:653 [in MetaCoq.PCUIC.PCUICConversion]
u:653 [in MetaCoq.PCUIC.PCUICReduction]
u:654 [in MetaCoq.PCUIC.PCUICInductives]
u:656 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
u:657 [in MetaCoq.PCUIC.PCUICReduction]
u:659 [in MetaCoq.SafeChecker.PCUICSafeConversion]
u:66 [in MetaCoq.PCUIC.PCUICWfUniverses]
u:66 [in MetaCoq.SafeChecker.PCUICWfReduction]
U:66 [in MetaCoq.PCUIC.PCUICContextConversion]
u:660 [in MetaCoq.PCUIC.PCUICReduction]
u:661 [in MetaCoq.Template.Universes]
u:662 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
u:663 [in MetaCoq.PCUIC.PCUICEquality]
u:663 [in MetaCoq.Template.utils.wGraph]
u:664 [in MetaCoq.PCUIC.PCUICConfluence]
u:665 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
u:665 [in MetaCoq.Template.Typing]
u:665 [in MetaCoq.SafeChecker.PCUICSafeConversion]
u:666 [in MetaCoq.Template.utils.wGraph]
u:668 [in MetaCoq.PCUIC.PCUICEquality]
u:668 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
u:669 [in MetaCoq.Template.utils.wGraph]
u:67 [in MetaCoq.PCUIC.PCUICCumulativity]
u:67 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
u:67 [in MetaCoq.Translations.param_original]
u:67 [in MetaCoq.Template.Induction]
u:670 [in MetaCoq.PCUIC.PCUICParallelReduction]
u:671 [in MetaCoq.Template.Universes]
u:671 [in MetaCoq.SafeChecker.PCUICSafeConversion]
u:672 [in MetaCoq.Template.utils.wGraph]
u:674 [in MetaCoq.Template.utils.All_Forall]
u:674 [in MetaCoq.PCUIC.PCUICEquality]
u:674 [in MetaCoq.PCUIC.PCUICConfluence]
u:674 [in MetaCoq.PCUIC.PCUICReduction]
u:675 [in MetaCoq.SafeChecker.PCUICSafeConversion]
u:677 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
u:678 [in MetaCoq.PCUIC.PCUICEquality]
u:678 [in MetaCoq.Template.utils.wGraph]
u:679 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
u:679 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
u:68 [in MetaCoq.PCUIC.PCUICWcbvEval]
u:68 [in MetaCoq.PCUIC.PCUICFirstorder]
u:68 [in MetaCoq.PCUIC.PCUICConvCumInversion]
u:68 [in MetaCoq.Translations.param_cheap_packed]
u:68 [in MetaCoq.Template.WcbvEval]
u:68 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
u:68 [in MetaCoq.PCUIC.PCUICCasesContexts]
u:680 [in MetaCoq.Template.EnvironmentTyping]
u:680 [in MetaCoq.PCUIC.PCUICReduction]
u:682 [in MetaCoq.PCUIC.PCUICEquality]
u:682 [in MetaCoq.Template.utils.wGraph]
u:682 [in MetaCoq.SafeChecker.PCUICSafeConversion]
u:686 [in MetaCoq.PCUIC.PCUICEquality]
u:686 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
u:687 [in MetaCoq.SafeChecker.PCUICSafeConversion]
u:687 [in MetaCoq.PCUIC.PCUICConfluence]
U:687 [in MetaCoq.PCUIC.PCUICSR]
u:689 [in MetaCoq.Template.EnvironmentTyping]
u:689 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
u:689 [in MetaCoq.PCUIC.PCUICConversion]
u:69 [in MetaCoq.PCUIC.PCUICWeakeningEnv]
u:69 [in MetaCoq.Erasure.EArities]
u:69 [in MetaCoq.PCUIC.PCUICInductiveInversion]
u:69 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
u:69 [in MetaCoq.Template.Checker]
u:69 [in MetaCoq.Translations.MiniHoTT]
u:69 [in MetaCoq.PCUIC.Bidirectional.BDUnique]
u:692 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
u:692 [in MetaCoq.SafeChecker.PCUICSafeConversion]
u:694 [in MetaCoq.PCUIC.PCUICEquality]
u:696 [in MetaCoq.Template.utils.wGraph]
u:696 [in MetaCoq.PCUIC.PCUICConversion]
u:698 [in MetaCoq.SafeChecker.PCUICSafeConversion]
U:699 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
u:699 [in MetaCoq.PCUIC.PCUICReduction]
u:7 [in MetaCoq.PCUIC.PCUICWfUniverses]
u:7 [in MetaCoq.Template.TermEquality]
u:7 [in MetaCoq.PCUIC.PCUICTyping]
u:7 [in MetaCoq.Template.LiftSubst]
u:70 [in MetaCoq.Template.Normal]
u:70 [in MetaCoq.PCUIC.PCUICInversion]
u:70 [in MetaCoq.Translations.param_original]
u:700 [in MetaCoq.Template.utils.wGraph]
u:700 [in MetaCoq.PCUIC.PCUICSR]
u:701 [in MetaCoq.PCUIC.PCUICInductiveInversion]
u:703 [in MetaCoq.PCUIC.PCUICEquality]
U:704 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
u:705 [in MetaCoq.SafeChecker.PCUICSafeConversion]
u:707 [in MetaCoq.PCUIC.PCUICEquality]
U:708 [in MetaCoq.PCUIC.PCUICSR]
u:71 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
u:71 [in MetaCoq.Translations.param_binary]
u:71 [in MetaCoq.PCUIC.PCUICInductiveInversion]
u:71 [in MetaCoq.PCUIC.PCUICCumulProp]
u:71 [in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
u:71 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
u:710 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
u:710 [in MetaCoq.SafeChecker.PCUICSafeConversion]
u:710 [in MetaCoq.PCUIC.PCUICConversion]
u:711 [in MetaCoq.Template.Universes]
u:712 [in MetaCoq.Translations.MiniHoTT]
u:714 [in MetaCoq.Template.Universes]
u:716 [in MetaCoq.Template.Universes]
U:716 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
u:716 [in MetaCoq.PCUIC.PCUICConversion]
u:719 [in MetaCoq.Template.Universes]
U:719 [in MetaCoq.Template.Typing]
u:72 [in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
u:720 [in MetaCoq.Translations.MiniHoTT]
u:720 [in MetaCoq.Translations.MiniHoTT_paths]
u:722 [in MetaCoq.Template.Universes]
u:723 [in MetaCoq.Template.Universes]
u:723 [in MetaCoq.PCUIC.PCUICConversion]
u:725 [in MetaCoq.PCUIC.PCUICSR]
u:726 [in MetaCoq.Template.Universes]
U:727 [in MetaCoq.Template.EnvironmentTyping]
u:727 [in MetaCoq.PCUIC.PCUICEquality]
u:727 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
u:728 [in MetaCoq.Translations.MiniHoTT_paths]
u:729 [in MetaCoq.PCUIC.PCUICInductiveInversion]
u:729 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
u:73 [in MetaCoq.PCUIC.PCUICCumulativity]
u:73 [in MetaCoq.PCUIC.PCUICCumulProp]
U:73 [in MetaCoq.PCUIC.PCUICContextConversion]
u:73 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:730 [in MetaCoq.SafeChecker.PCUICSafeChecker]
u:732 [in MetaCoq.Template.Universes]
u:732 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
u:732 [in MetaCoq.PCUIC.PCUICConversion]
u:733 [in MetaCoq.Template.Universes]
u:735 [in MetaCoq.Template.Universes]
u:735 [in MetaCoq.PCUIC.PCUICConversion]
u:735 [in MetaCoq.SafeChecker.PCUICSafeChecker]
u:736 [in MetaCoq.Template.Universes]
u:737 [in MetaCoq.PCUIC.PCUICConversion]
u:738 [in MetaCoq.Template.Universes]
U:738 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
u:74 [in MetaCoq.Translations.param_binary]
u:74 [in MetaCoq.PCUIC.PCUICConvCumInversion]
u:74 [in MetaCoq.Translations.MiniHoTT]
u:740 [in MetaCoq.Template.Universes]
u:740 [in MetaCoq.PCUIC.PCUICConversion]
u:742 [in MetaCoq.Template.Universes]
u:742 [in MetaCoq.PCUIC.PCUICInductiveInversion]
u:742 [in MetaCoq.PCUIC.PCUICConversion]
U:743 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
u:744 [in MetaCoq.Template.Universes]
u:744 [in MetaCoq.PCUIC.PCUICConversion]
u:744 [in MetaCoq.Translations.MiniHoTT]
u:746 [in MetaCoq.PCUIC.PCUICConversion]
u:748 [in MetaCoq.PCUIC.PCUICConversion]
u:75 [in MetaCoq.PCUIC.PCUICWfUniverses]
u:75 [in MetaCoq.Erasure.ErasureProperties]
u:75 [in MetaCoq.PCUIC.PCUICSpine]
u:750 [in MetaCoq.PCUIC.PCUICConversion]
u:752 [in MetaCoq.PCUIC.PCUICConversion]
u:752 [in MetaCoq.Translations.MiniHoTT_paths]
u:754 [in MetaCoq.PCUIC.PCUICConversion]
u:755 [in MetaCoq.Template.Universes]
u:755 [in MetaCoq.PCUIC.PCUICInductiveInversion]
u:757 [in MetaCoq.Template.Universes]
u:757 [in MetaCoq.PCUIC.PCUICConversion]
u:758 [in MetaCoq.PCUIC.PCUICSR]
u:759 [in MetaCoq.PCUIC.PCUICConversion]
u:76 [in MetaCoq.PCUIC.PCUICWeakeningEnv]
u:76 [in MetaCoq.PCUIC.PCUICWcbvEval]
u:76 [in MetaCoq.PCUIC.PCUICInductiveInversion]
u:76 [in MetaCoq.PCUIC.PCUICCumulProp]
u:76 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
u:76 [in MetaCoq.Template.WcbvEval]
u:76 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
u:76 [in MetaCoq.SafeChecker.PCUICEqualityDec]
u:76 [in MetaCoq.SafeChecker.PCUICTypeChecker]
U:761 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
u:762 [in MetaCoq.Template.Universes]
u:762 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
u:762 [in MetaCoq.PCUIC.PCUICConversion]
u:763 [in MetaCoq.Translations.MiniHoTT]
u:763 [in MetaCoq.PCUIC.PCUICSR]
u:764 [in MetaCoq.PCUIC.PCUICConversion]
u:766 [in MetaCoq.PCUIC.PCUICInductiveInversion]
U:767 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
u:768 [in MetaCoq.Template.Universes]
u:77 [in MetaCoq.PCUIC.PCUICSafeLemmata]
u:77 [in MetaCoq.PCUIC.PCUICInversion]
u:77 [in MetaCoq.Erasure.ErasureProperties]
u:77 [in MetaCoq.Translations.MiniHoTT_paths]
u:77 [in MetaCoq.PCUIC.Bidirectional.BDUnique]
u:770 [in MetaCoq.PCUIC.PCUICConversion]
u:770 [in MetaCoq.PCUIC.PCUICSR]
u:771 [in MetaCoq.Translations.MiniHoTT]
u:771 [in MetaCoq.Translations.MiniHoTT_paths]
u:776 [in MetaCoq.PCUIC.PCUICConversion]
u:778 [in MetaCoq.PCUIC.PCUICSR]
u:779 [in MetaCoq.Translations.MiniHoTT_paths]
u:78 [in MetaCoq.PCUIC.PCUICCumulativity]
u:78 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
u:78 [in MetaCoq.SafeChecker.PCUICTypeChecker]
u:780 [in MetaCoq.PCUIC.PCUICInductiveInversion]
U:781 [in MetaCoq.PCUIC.PCUICConversion]
u:784 [in MetaCoq.PCUIC.PCUICSR]
u:786 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
u:79 [in MetaCoq.PCUIC.PCUICFirstorder]
u:79 [in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
U:79 [in MetaCoq.PCUIC.PCUICConvCumInversion]
u:79 [in MetaCoq.PCUIC.PCUICReduction]
u:790 [in MetaCoq.PCUIC.PCUICSR]
u:795 [in MetaCoq.PCUIC.PCUICConfluence]
u:796 [in MetaCoq.PCUIC.PCUICSR]
u:799 [in MetaCoq.PCUIC.PCUICConfluence]
u:8 [in MetaCoq.PCUIC.PCUICCumulProp]
u:8 [in MetaCoq.PCUIC.Syntax.PCUICCases]
u:8 [in MetaCoq.Erasure.EWcbvEvalInd]
u:8 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
u:8 [in MetaCoq.PCUIC.Syntax.PCUICUnivSubst]
u:80 [in MetaCoq.PCUIC.PCUICSafeLemmata]
u:80 [in MetaCoq.Erasure.EArities]
u:80 [in MetaCoq.Erasure.EWellformed]
u:80 [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
u:80 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
u:80 [in MetaCoq.SafeChecker.PCUICEqualityDec]
u:80 [in MetaCoq.SafeChecker.PCUICTypeChecker]
u:800 [in MetaCoq.PCUIC.PCUICConversion]
u:801 [in MetaCoq.PCUIC.PCUICSpine]
u:803 [in MetaCoq.PCUIC.PCUICConfluence]
u:804 [in MetaCoq.PCUIC.PCUICConversion]
u:804 [in MetaCoq.PCUIC.PCUICTyping]
u:81 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
u:817 [in MetaCoq.PCUIC.PCUICSpine]
u:82 [in MetaCoq.PCUIC.PCUICCumulProp]
u:82 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
u:82 [in MetaCoq.Template.Checker]
u:82 [in MetaCoq.Translations.MiniHoTT_paths]
u:83 [in MetaCoq.PCUIC.PCUICProgress]
u:83 [in MetaCoq.PCUIC.PCUICWeakeningEnv]
u:83 [in MetaCoq.PCUIC.PCUICCumulativity]
U:83 [in MetaCoq.PCUIC.PCUICArities]
u:83 [in MetaCoq.Erasure.EWellformed]
u:83 [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
u:830 [in MetaCoq.PCUIC.PCUICSpine]
u:838 [in MetaCoq.PCUIC.PCUICConversion]
u:839 [in MetaCoq.PCUIC.PCUICConfluence]
u:84 [in MetaCoq.PCUIC.PCUICSafeLemmata]
u:84 [in MetaCoq.PCUIC.PCUICInductives]
u:84 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
u:841 [in MetaCoq.PCUIC.PCUICTyping]
u:842 [in MetaCoq.PCUIC.PCUICReduction]
u:843 [in MetaCoq.SafeChecker.PCUICSafeChecker]
u:845 [in MetaCoq.PCUIC.PCUICConversion]
u:848 [in MetaCoq.PCUIC.PCUICTyping]
u:85 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
u:85 [in MetaCoq.PCUIC.PCUICWcbvEval]
u:85 [in MetaCoq.Erasure.ErasureProperties]
u:85 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
u:85 [in MetaCoq.SafeChecker.PCUICTypeChecker]
u:851 [in MetaCoq.PCUIC.PCUICConfluence]
u:854 [in MetaCoq.PCUIC.PCUICConfluence]
u:855 [in MetaCoq.PCUIC.PCUICTyping]
u:857 [in MetaCoq.Template.utils.All_Forall]
u:857 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
u:857 [in MetaCoq.PCUIC.PCUICReduction]
u:86 [in MetaCoq.Template.TermEquality]
u:86 [in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
u:86 [in MetaCoq.Template.WcbvEval]
u:86 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
u:86 [in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
u:863 [in MetaCoq.PCUIC.PCUICReduction]
u:865 [in MetaCoq.PCUIC.PCUICTyping]
u:866 [in MetaCoq.PCUIC.PCUICConfluence]
u:868 [in MetaCoq.PCUIC.PCUICParallelReduction]
u:87 [in MetaCoq.PCUIC.PCUICSafeLemmata]
u:87 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
u:87 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
u:872 [in MetaCoq.PCUIC.PCUICConfluence]
u:879 [in MetaCoq.PCUIC.PCUICConfluence]
u:88 [in MetaCoq.PCUIC.PCUICCumulativity]
u:88 [in MetaCoq.PCUIC.PCUICFirstorder]
u:88 [in MetaCoq.SafeChecker.PCUICSafeConversion]
u:88 [in MetaCoq.Template.Checker]
u:883 [in MetaCoq.PCUIC.PCUICConfluence]
U:883 [in MetaCoq.PCUIC.PCUICSR]
u:889 [in MetaCoq.PCUIC.PCUICConfluence]
u:89 [in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
u:89 [in MetaCoq.Template.TermEquality]
u:89 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
u:896 [in MetaCoq.PCUIC.PCUICTyping]
u:897 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
u:897 [in MetaCoq.PCUIC.PCUICConfluence]
u:9 [in MetaCoq.Template.Typing]
u:9 [in MetaCoq.PCUIC.PCUICPrincipality]
u:90 [in MetaCoq.PCUIC.PCUICSafeLemmata]
u:90 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
u:90 [in MetaCoq.PCUIC.PCUICInversion]
u:90 [in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
u:90 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
u:902 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
u:906 [in MetaCoq.PCUIC.PCUICConfluence]
u:91 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
u:91 [in MetaCoq.Erasure.EArities]
u:91 [in MetaCoq.SafeChecker.PCUICSafeConversion]
u:915 [in MetaCoq.PCUIC.PCUICConfluence]
u:92 [in MetaCoq.Template.WfAst]
u:92 [in MetaCoq.Template.TermEquality]
u:92 [in MetaCoq.SafeChecker.PCUICWfEnv]
u:92 [in MetaCoq.PCUIC.PCUICConversion]
u:92 [in MetaCoq.PCUIC.PCUICCanonicity]
u:922 [in MetaCoq.Template.Typing]
u:922 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
u:924 [in MetaCoq.PCUIC.PCUICConfluence]
u:925 [in MetaCoq.Template.Typing]
u:928 [in MetaCoq.PCUIC.PCUICConfluence]
u:93 [in MetaCoq.Template.EnvironmentTyping]
u:93 [in MetaCoq.PCUIC.PCUICCumulProp]
u:93 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
U:933 [in MetaCoq.Template.Typing]
u:933 [in MetaCoq.PCUIC.PCUICConfluence]
u:94 [in MetaCoq.PCUIC.PCUICSafeLemmata]
u:94 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
u:94 [in MetaCoq.Template.WfAst]
u:94 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
u:94 [in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
u:95 [in MetaCoq.PCUIC.PCUICInversion]
u:95 [in MetaCoq.PCUIC.PCUICAst]
u:95 [in MetaCoq.PCUIC.PCUICContextConversion]
u:95 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
u:95 [in MetaCoq.Template.LiftSubst]
u:955 [in MetaCoq.PCUIC.PCUICConfluence]
u:96 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
u:96 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
u:96 [in MetaCoq.Template.TermEquality]
u:96 [in MetaCoq.SafeChecker.PCUICErrors]
u:96 [in MetaCoq.Erasure.ErasureProperties]
u:96 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
u:961 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
u:961 [in MetaCoq.PCUIC.PCUICConfluence]
u:97 [in MetaCoq.Template.WfAst]
u:97 [in MetaCoq.PCUIC.PCUICCumulProp]
u:972 [in MetaCoq.PCUIC.PCUICConfluence]
u:973 [in MetaCoq.PCUIC.PCUICTyping]
u:975 [in MetaCoq.Template.Typing]
u:975 [in MetaCoq.PCUIC.PCUICReduction]
u:978 [in MetaCoq.PCUIC.PCUICReduction]
u:98 [in MetaCoq.PCUIC.PCUICEtaExpand]
u:98 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
u:98 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
u:98 [in MetaCoq.PCUIC.PCUICReduction]
u:981 [in MetaCoq.PCUIC.PCUICReduction]
u:984 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
u:984 [in MetaCoq.PCUIC.PCUICReduction]
u:987 [in MetaCoq.Erasure.ErasureFunction]
u:99 [in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
u:99 [in MetaCoq.Template.Typing]
u:99 [in MetaCoq.Erasure.Extract]
u:99 [in MetaCoq.Template.LiftSubst]
U:999 [in MetaCoq.PCUIC.PCUICConversion]
| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (75519 entries) |
| Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (245 entries) |
| Binder Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (61331 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (144 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (89 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (236 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (6913 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1141 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (34 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (269 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (443 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (296 entries) |
| Instance Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (604 entries) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (248 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (3386 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (140 entries) |