| 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) |
V (binder)
value'':46 [in MetaCoq.Template.Transform]value':11 [in MetaCoq.Template.Transform]
value':45 [in MetaCoq.Template.Transform]
value:10 [in MetaCoq.Template.Transform]
value:38 [in MetaCoq.Template.Transform]
value:44 [in MetaCoq.Template.Transform]
val:195 [in MetaCoq.Erasure.Extract]
val:482 [in MetaCoq.Template.Universes]
val:75 [in MetaCoq.Erasure.EDeps]
variances:640 [in MetaCoq.Template.EnvironmentTyping]
variances:648 [in MetaCoq.SafeChecker.PCUICSafeChecker]
var:818 [in MetaCoq.SafeChecker.PCUICSafeChecker]
vi:53 [in MetaCoq.Erasure.ESpineView]
vn:55 [in MetaCoq.Erasure.ESpineView]
vset:507 [in MetaCoq.Template.common.uGraph]
vset:510 [in MetaCoq.Template.common.uGraph]
vsub:931 [in MetaCoq.Template.utils.wGraph]
vx:1190 [in MetaCoq.Template.utils.wGraph]
Vx:613 [in MetaCoq.Template.utils.wGraph]
Vx:659 [in MetaCoq.Template.utils.wGraph]
vy:1191 [in MetaCoq.Template.utils.wGraph]
Vy:614 [in MetaCoq.Template.utils.wGraph]
Vy:660 [in MetaCoq.Template.utils.wGraph]
Vy:744 [in MetaCoq.Template.utils.wGraph]
v'':61 [in MetaCoq.Template.Transform]
v':10 [in MetaCoq.PCUIC.PCUICCumulProp]
v':10 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
v':105 [in MetaCoq.Erasure.ETransform]
v':112 [in MetaCoq.PCUIC.Syntax.PCUICReflect]
v':115 [in MetaCoq.Erasure.ETransform]
v':119 [in MetaCoq.PCUIC.PCUICContextConversion]
v':125 [in MetaCoq.PCUIC.PCUICContextConversion]
v':126 [in MetaCoq.PCUIC.PCUICConfluence]
v':1292 [in MetaCoq.PCUIC.PCUICConfluence]
v':1301 [in MetaCoq.PCUIC.PCUICConfluence]
v':131 [in MetaCoq.PCUIC.PCUICContextConversion]
v':132 [in MetaCoq.PCUIC.PCUICNormal]
v':137 [in MetaCoq.PCUIC.PCUICContextConversion]
v':1387 [in MetaCoq.Erasure.ErasureFunction]
v':139 [in MetaCoq.PCUIC.PCUICNormal]
v':1409 [in MetaCoq.Erasure.ErasureFunction]
v':146 [in MetaCoq.PCUIC.PCUICCumulativity]
v':147 [in MetaCoq.PCUIC.PCUICConfluence]
v':148 [in MetaCoq.PCUIC.PCUICContextConversion]
v':149 [in MetaCoq.PCUIC.PCUICNormal]
v':152 [in MetaCoq.PCUIC.PCUICConfluence]
v':153 [in MetaCoq.PCUIC.PCUICContextConversion]
v':155 [in MetaCoq.PCUIC.PCUICConfluence]
v':159 [in MetaCoq.PCUIC.PCUICArities]
v':162 [in MetaCoq.PCUIC.PCUICNormal]
v':162 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
V':177 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
v':18 [in MetaCoq.PCUIC.PCUICTransform]
v':18 [in MetaCoq.PCUIC.PCUICSN]
v':184 [in MetaCoq.Erasure.EArities]
v':185 [in MetaCoq.PCUIC.PCUICContextConversion]
v':190 [in MetaCoq.Erasure.EArities]
v':190 [in MetaCoq.PCUIC.PCUICConfluence]
v':195 [in MetaCoq.PCUIC.PCUICConfluence]
v':197 [in MetaCoq.PCUIC.PCUICContextConversion]
v':20 [in MetaCoq.PCUIC.PCUICCumulProp]
v':200 [in MetaCoq.PCUIC.PCUICConfluence]
v':203 [in MetaCoq.PCUIC.PCUICContextConversion]
v':209 [in MetaCoq.PCUIC.PCUICContextConversion]
v':21 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
v':214 [in MetaCoq.PCUIC.PCUICConfluence]
v':22 [in MetaCoq.Template.Transform]
v':220 [in MetaCoq.PCUIC.PCUICElimination]
v':226 [in MetaCoq.PCUIC.PCUICElimination]
v':232 [in MetaCoq.PCUIC.PCUICElimination]
v':238 [in MetaCoq.PCUIC.PCUICElimination]
v':240 [in MetaCoq.Template.Universes]
v':244 [in MetaCoq.Template.Universes]
v':244 [in MetaCoq.PCUIC.PCUICElimination]
v':248 [in MetaCoq.PCUIC.PCUICConfluence]
v':253 [in MetaCoq.PCUIC.PCUICConfluence]
v':258 [in MetaCoq.PCUIC.PCUICConfluence]
v':272 [in MetaCoq.PCUIC.PCUICConfluence]
v':288 [in MetaCoq.Erasure.EWcbvEval]
v':29 [in MetaCoq.PCUIC.PCUICSN]
v':29 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
v':297 [in MetaCoq.Erasure.EWcbvEval]
v':300 [in MetaCoq.Erasure.EWcbvEval]
v':313 [in MetaCoq.PCUIC.PCUICConfluence]
v':32 [in MetaCoq.Erasure.ETransform]
v':356 [in MetaCoq.PCUIC.PCUICConfluence]
v':37 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
v':379 [in MetaCoq.PCUIC.PCUICWcbvEval]
v':384 [in MetaCoq.PCUIC.PCUICWcbvEval]
v':39 [in MetaCoq.PCUIC.PCUICCumulativity]
v':399 [in MetaCoq.PCUIC.PCUICConfluence]
v':4 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
v':420 [in MetaCoq.PCUIC.PCUICConfluence]
v':47 [in MetaCoq.Erasure.ETransform]
v':471 [in MetaCoq.PCUIC.PCUICConfluence]
v':472 [in MetaCoq.PCUIC.PCUICProgress]
v':480 [in MetaCoq.PCUIC.PCUICProgress]
v':488 [in MetaCoq.PCUIC.PCUICProgress]
v':488 [in MetaCoq.Template.Universes]
v':492 [in MetaCoq.PCUIC.PCUICConfluence]
v':53 [in MetaCoq.PCUIC.PCUICSN]
v':541 [in MetaCoq.PCUIC.PCUICConfluence]
v':551 [in MetaCoq.PCUIC.PCUICConfluence]
v':572 [in MetaCoq.PCUIC.PCUICConfluence]
v':59 [in MetaCoq.PCUIC.PCUICConvCumInversion]
v':59 [in MetaCoq.Template.Transform]
v':6 [in MetaCoq.PCUIC.PCUICTransform]
v':60 [in MetaCoq.Erasure.ETransform]
v':628 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
v':635 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
v':71 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
v':71 [in MetaCoq.Erasure.ETransform]
v':8 [in MetaCoq.Erasure.ErasureCorrectness]
v':81 [in MetaCoq.Erasure.ETransform]
v':93 [in MetaCoq.Erasure.ETransform]
v':959 [in MetaCoq.Erasure.ErasureFunction]
v':97 [in MetaCoq.PCUIC.PCUICConvCumInversion]
v':986 [in MetaCoq.Erasure.ErasureFunction]
v1:1001 [in MetaCoq.Template.utils.wGraph]
v1:1064 [in MetaCoq.Template.utils.wGraph]
v1:178 [in MetaCoq.PCUIC.PCUICSafeLemmata]
v1:2799 [in MetaCoq.Translations.MiniHoTT]
v1:2807 [in MetaCoq.Translations.MiniHoTT_paths]
v1:2811 [in MetaCoq.Translations.MiniHoTT]
v1:2819 [in MetaCoq.Translations.MiniHoTT_paths]
v1:538 [in MetaCoq.SafeChecker.PCUICSafeConversion]
v1:843 [in MetaCoq.PCUIC.PCUICReduction]
v2:1002 [in MetaCoq.Template.utils.wGraph]
v2:1065 [in MetaCoq.Template.utils.wGraph]
v2:179 [in MetaCoq.PCUIC.PCUICSafeLemmata]
v2:2802 [in MetaCoq.Translations.MiniHoTT]
v2:2810 [in MetaCoq.Translations.MiniHoTT_paths]
v2:2813 [in MetaCoq.Translations.MiniHoTT]
v2:2821 [in MetaCoq.Translations.MiniHoTT_paths]
v2:540 [in MetaCoq.SafeChecker.PCUICSafeConversion]
v2:844 [in MetaCoq.PCUIC.PCUICReduction]
v:1 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
v:10 [in MetaCoq.PCUIC.PCUICEquality]
v:100 [in MetaCoq.Template.EtaExpand]
v:100 [in MetaCoq.SafeChecker.PCUICErrors]
v:101 [in MetaCoq.Template.common.uGraph]
v:104 [in MetaCoq.Erasure.ETransform]
v:1056 [in MetaCoq.Template.utils.All_Forall]
v:106 [in MetaCoq.PCUIC.Syntax.PCUICReflect]
v:107 [in MetaCoq.PCUIC.PCUICSubstitution]
v:107 [in MetaCoq.PCUIC.PCUICAst]
v:1071 [in MetaCoq.Template.utils.wGraph]
v:108 [in MetaCoq.Template.common.uGraph]
v:108 [in MetaCoq.PCUIC.PCUICAlpha]
v:108 [in MetaCoq.Erasure.EEtaExpanded]
v:1085 [in MetaCoq.Template.utils.wGraph]
v:109 [in MetaCoq.PCUIC.PCUICNormal]
v:11 [in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
v:11 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
v:110 [in MetaCoq.Erasure.EEtaExpanded]
v:111 [in MetaCoq.PCUIC.PCUICSubstitution]
v:113 [in MetaCoq.PCUIC.PCUICAlpha]
v:113 [in MetaCoq.Erasure.EEtaExpanded]
v:114 [in MetaCoq.Erasure.ETransform]
v:117 [in MetaCoq.PCUIC.PCUICContextConversion]
v:118 [in MetaCoq.PCUIC.PCUICSubstitution]
v:1188 [in MetaCoq.Template.utils.wGraph]
v:119 [in MetaCoq.Template.common.uGraph]
v:1195 [in MetaCoq.PCUIC.PCUICReduction]
v:12 [in MetaCoq.Template.TermEquality]
v:120 [in MetaCoq.SafeChecker.PCUICErrors]
v:120 [in MetaCoq.Erasure.ERemoveParams]
v:122 [in MetaCoq.Erasure.ERemoveParams]
v:1228 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
v:123 [in MetaCoq.PCUIC.PCUICSafeLemmata]
v:123 [in MetaCoq.PCUIC.PCUICContextConversion]
v:1231 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
v:125 [in MetaCoq.PCUIC.PCUICSubstitution]
v:1261 [in MetaCoq.Translations.MiniHoTT]
v:1262 [in MetaCoq.SafeChecker.PCUICSafeReduce]
v:1266 [in MetaCoq.SafeChecker.PCUICSafeReduce]
v:1269 [in MetaCoq.Translations.MiniHoTT_paths]
v:127 [in MetaCoq.Erasure.EConstructorsAsBlocks]
v:127 [in MetaCoq.Template.common.uGraph]
v:128 [in MetaCoq.Template.Universes]
v:129 [in MetaCoq.PCUIC.PCUICContextConversion]
v:1291 [in MetaCoq.PCUIC.PCUICConfluence]
v:13 [in MetaCoq.Template.Universes]
v:13 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
v:13 [in MetaCoq.SafeChecker.PCUICEqualityDec]
v:130 [in MetaCoq.PCUIC.PCUICCumulativity]
v:130 [in MetaCoq.Erasure.EInlineProjections]
v:130 [in MetaCoq.PCUIC.PCUICNormal]
v:1300 [in MetaCoq.PCUIC.PCUICConfluence]
v:131 [in MetaCoq.Template.Universes]
v:131 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
v:1312 [in MetaCoq.Erasure.ErasureFunction]
v:1320 [in MetaCoq.Erasure.ErasureFunction]
v:133 [in MetaCoq.Template.Universes]
v:1337 [in MetaCoq.Erasure.ErasureFunction]
v:135 [in MetaCoq.Template.Universes]
v:135 [in MetaCoq.PCUIC.PCUICContextConversion]
v:136 [in MetaCoq.PCUIC.PCUICCumulativity]
v:137 [in MetaCoq.Template.Universes]
v:137 [in MetaCoq.PCUIC.PCUICNormal]
v:1373 [in MetaCoq.Erasure.ErasureFunction]
v:139 [in MetaCoq.Template.Universes]
v:1395 [in MetaCoq.Erasure.ErasureFunction]
v:14 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
v:1425 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
v:145 [in MetaCoq.PCUIC.PCUICCumulativity]
v:145 [in MetaCoq.Erasure.EOptimizePropDiscr]
v:146 [in MetaCoq.PCUIC.PCUICConfluence]
v:147 [in MetaCoq.PCUIC.PCUICNormal]
v:147 [in MetaCoq.PCUIC.PCUICContextConversion]
v:148 [in MetaCoq.Template.Universes]
V:151 [in MetaCoq.PCUIC.PCUICCumulProp]
v:152 [in MetaCoq.PCUIC.PCUICContextConversion]
v:1523 [in MetaCoq.SafeChecker.PCUICSafeConversion]
v:1529 [in MetaCoq.SafeChecker.PCUICSafeConversion]
v:155 [in MetaCoq.Template.Universes]
v:157 [in MetaCoq.Template.Universes]
v:158 [in MetaCoq.PCUIC.PCUICArities]
v:16 [in MetaCoq.PCUIC.PCUICCumulativity]
v:16 [in MetaCoq.PCUIC.PCUICEquality]
v:16 [in MetaCoq.PCUIC.PCUICSN]
v:160 [in MetaCoq.Template.Universes]
v:160 [in MetaCoq.PCUIC.PCUICNormal]
v:161 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
v:161 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
v:162 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
v:164 [in MetaCoq.Template.Universes]
v:166 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
v:167 [in MetaCoq.Template.EtaExpand]
v:167 [in MetaCoq.Template.Universes]
v:169 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
v:17 [in MetaCoq.PCUIC.PCUICTransform]
v:17 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
v:17 [in MetaCoq.PCUIC.PCUICCumulProp]
v:17 [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
v:173 [in MetaCoq.Examples.tauto]
v:174 [in MetaCoq.Template.Universes]
v:176 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
v:1763 [in MetaCoq.SafeChecker.PCUICSafeReduce]
v:177 [in MetaCoq.PCUIC.PCUICContextConversion]
v:1782 [in MetaCoq.SafeChecker.PCUICSafeConversion]
v:1787 [in MetaCoq.SafeChecker.PCUICSafeConversion]
v:179 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
v:1793 [in MetaCoq.SafeChecker.PCUICSafeConversion]
v:18 [in MetaCoq.Template.Normal]
v:18 [in MetaCoq.SafeChecker.PCUICSafeReduce]
v:181 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
v:182 [in MetaCoq.Template.Universes]
v:182 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
v:183 [in MetaCoq.Erasure.EArities]
v:1849 [in MetaCoq.Template.utils.All_Forall]
v:186 [in MetaCoq.Template.Universes]
v:186 [in MetaCoq.Template.Ast]
v:186 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
v:186 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
v:189 [in MetaCoq.Erasure.EArities]
v:19 [in MetaCoq.PCUIC.PCUICCumulativity]
v:19 [in MetaCoq.Template.Transform]
v:190 [in MetaCoq.Template.Universes]
v:191 [in MetaCoq.PCUIC.PCUICContextConversion]
v:193 [in MetaCoq.Template.Universes]
v:1953 [in MetaCoq.SafeChecker.PCUICSafeConversion]
v:2 [in MetaCoq.PCUIC.PCUICTransform]
v:2 [in MetaCoq.PCUIC.Syntax.PCUICReflect]
v:20 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
v:202 [in MetaCoq.PCUIC.PCUICContextConversion]
v:207 [in MetaCoq.Template.TermEquality]
v:2079 [in MetaCoq.Translations.MiniHoTT]
v:208 [in MetaCoq.PCUIC.PCUICContextConversion]
v:2087 [in MetaCoq.Translations.MiniHoTT]
v:2087 [in MetaCoq.Translations.MiniHoTT_paths]
v:2095 [in MetaCoq.Translations.MiniHoTT]
v:2095 [in MetaCoq.Translations.MiniHoTT_paths]
v:21 [in MetaCoq.Template.Normal]
v:21 [in MetaCoq.PCUIC.PCUICSN]
v:21 [in MetaCoq.SafeChecker.PCUICSafeReduce]
v:21 [in MetaCoq.Template.AstUtils]
v:2102 [in MetaCoq.Translations.MiniHoTT]
v:2103 [in MetaCoq.Translations.MiniHoTT_paths]
v:2109 [in MetaCoq.Translations.MiniHoTT]
v:2110 [in MetaCoq.Translations.MiniHoTT_paths]
v:2117 [in MetaCoq.Translations.MiniHoTT]
v:2117 [in MetaCoq.Translations.MiniHoTT_paths]
v:2125 [in MetaCoq.Translations.MiniHoTT]
v:2125 [in MetaCoq.Translations.MiniHoTT_paths]
v:213 [in MetaCoq.PCUIC.PCUICContextConversion]
v:213 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
v:2132 [in MetaCoq.Translations.MiniHoTT]
v:2133 [in MetaCoq.Translations.MiniHoTT_paths]
v:2139 [in MetaCoq.Translations.MiniHoTT]
v:2140 [in MetaCoq.Translations.MiniHoTT_paths]
v:2146 [in MetaCoq.Translations.MiniHoTT]
v:2147 [in MetaCoq.Translations.MiniHoTT_paths]
v:215 [in MetaCoq.PCUIC.PCUICSafeLemmata]
v:2153 [in MetaCoq.Translations.MiniHoTT]
v:2154 [in MetaCoq.Translations.MiniHoTT_paths]
v:216 [in MetaCoq.Erasure.EArities]
v:2160 [in MetaCoq.Translations.MiniHoTT]
v:2161 [in MetaCoq.Translations.MiniHoTT_paths]
v:2168 [in MetaCoq.Translations.MiniHoTT_paths]
v:218 [in MetaCoq.PCUIC.PCUICSafeLemmata]
v:218 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
v:219 [in MetaCoq.PCUIC.PCUICElimination]
v:219 [in MetaCoq.Erasure.EArities]
v:22 [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
v:22 [in MetaCoq.SafeChecker.PCUICEqualityDec]
v:222 [in MetaCoq.PCUIC.PCUICSafeLemmata]
v:222 [in MetaCoq.Erasure.EArities]
v:222 [in MetaCoq.PCUIC.PCUICAlpha]
v:225 [in MetaCoq.PCUIC.PCUICElimination]
v:225 [in MetaCoq.PCUIC.PCUICSafeLemmata]
v:225 [in MetaCoq.SafeChecker.PCUICWfEnv]
v:226 [in MetaCoq.PCUIC.PCUICNormal]
v:226 [in MetaCoq.PCUIC.PCUICAlpha]
v:228 [in MetaCoq.PCUIC.PCUICSafeLemmata]
v:228 [in MetaCoq.PCUIC.PCUICNormal]
v:23 [in MetaCoq.Translations.param_original]
v:230 [in MetaCoq.Template.common.uGraph]
v:230 [in MetaCoq.Erasure.EWcbvEval]
v:231 [in MetaCoq.PCUIC.PCUICElimination]
v:235 [in MetaCoq.Erasure.EWcbvEval]
v:236 [in MetaCoq.PCUIC.PCUICNormal]
v:237 [in MetaCoq.PCUIC.PCUICElimination]
v:239 [in MetaCoq.Template.Universes]
v:24 [in MetaCoq.PCUIC.PCUICSN]
v:24 [in MetaCoq.SafeChecker.PCUICSafeReduce]
v:240 [in MetaCoq.PCUIC.PCUICNormal]
v:241 [in MetaCoq.Template.common.uGraph]
v:243 [in MetaCoq.Template.Universes]
v:243 [in MetaCoq.PCUIC.PCUICElimination]
v:246 [in MetaCoq.Template.Environment]
v:248 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
v:249 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
v:249 [in MetaCoq.Template.Environment]
v:249 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
v:25 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
v:25 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
v:256 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
v:256 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
v:259 [in MetaCoq.PCUIC.PCUICAlpha]
v:262 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
v:2661 [in MetaCoq.Translations.MiniHoTT]
v:2667 [in MetaCoq.Translations.MiniHoTT]
v:2669 [in MetaCoq.Translations.MiniHoTT_paths]
v:2673 [in MetaCoq.Translations.MiniHoTT]
v:2675 [in MetaCoq.Translations.MiniHoTT_paths]
v:2681 [in MetaCoq.Translations.MiniHoTT_paths]
v:269 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
v:27 [in MetaCoq.Template.Normal]
v:27 [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
v:2701 [in MetaCoq.Translations.MiniHoTT]
v:2706 [in MetaCoq.Translations.MiniHoTT]
v:2709 [in MetaCoq.Translations.MiniHoTT_paths]
v:271 [in MetaCoq.PCUIC.PCUICAlpha]
v:2712 [in MetaCoq.Translations.MiniHoTT]
v:2714 [in MetaCoq.Translations.MiniHoTT_paths]
v:2718 [in MetaCoq.Translations.MiniHoTT]
v:2720 [in MetaCoq.Translations.MiniHoTT_paths]
v:2725 [in MetaCoq.Translations.MiniHoTT]
v:2726 [in MetaCoq.Translations.MiniHoTT_paths]
v:2730 [in MetaCoq.Translations.MiniHoTT]
v:2733 [in MetaCoq.Translations.MiniHoTT_paths]
v:2738 [in MetaCoq.Translations.MiniHoTT]
v:2738 [in MetaCoq.Translations.MiniHoTT_paths]
v:2744 [in MetaCoq.Translations.MiniHoTT]
v:2746 [in MetaCoq.Translations.MiniHoTT_paths]
v:2750 [in MetaCoq.Translations.MiniHoTT]
v:2752 [in MetaCoq.Translations.MiniHoTT_paths]
v:2757 [in MetaCoq.Translations.MiniHoTT]
v:2758 [in MetaCoq.Translations.MiniHoTT_paths]
v:2762 [in MetaCoq.Translations.MiniHoTT]
v:2765 [in MetaCoq.Translations.MiniHoTT_paths]
v:277 [in MetaCoq.PCUIC.PCUICAlpha]
v:2770 [in MetaCoq.Translations.MiniHoTT]
v:2770 [in MetaCoq.Translations.MiniHoTT_paths]
v:2776 [in MetaCoq.Translations.MiniHoTT]
v:2778 [in MetaCoq.Translations.MiniHoTT_paths]
v:2781 [in MetaCoq.Translations.MiniHoTT]
v:2784 [in MetaCoq.Translations.MiniHoTT_paths]
v:2785 [in MetaCoq.Translations.MiniHoTT]
v:2789 [in MetaCoq.Translations.MiniHoTT_paths]
v:279 [in MetaCoq.Template.common.uGraph]
v:2790 [in MetaCoq.Translations.MiniHoTT]
v:2793 [in MetaCoq.Translations.MiniHoTT_paths]
v:2798 [in MetaCoq.Translations.MiniHoTT_paths]
v:28 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
v:28 [in MetaCoq.PCUIC.PCUICSN]
v:28 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
v:281 [in MetaCoq.Template.common.uGraph]
v:282 [in MetaCoq.PCUIC.PCUICAlpha]
v:2822 [in MetaCoq.Translations.MiniHoTT]
v:2829 [in MetaCoq.Translations.MiniHoTT]
v:283 [in MetaCoq.Template.common.uGraph]
v:2830 [in MetaCoq.Translations.MiniHoTT_paths]
v:2837 [in MetaCoq.Translations.MiniHoTT_paths]
v:284 [in MetaCoq.Template.Environment]
v:2861 [in MetaCoq.Translations.MiniHoTT]
v:2869 [in MetaCoq.Translations.MiniHoTT_paths]
v:287 [in MetaCoq.Template.Universes]
v:287 [in MetaCoq.Template.Environment]
v:287 [in MetaCoq.Erasure.EWcbvEval]
v:2870 [in MetaCoq.Translations.MiniHoTT]
v:2878 [in MetaCoq.Translations.MiniHoTT_paths]
v:29 [in MetaCoq.PCUIC.PCUICNormal]
v:29 [in MetaCoq.Template.common.uGraph]
v:29 [in MetaCoq.PCUIC.PCUICEquality]
v:290 [in MetaCoq.PCUIC.PCUICCumulProp]
v:291 [in MetaCoq.Template.Environment]
v:292 [in MetaCoq.Erasure.EWcbvEval]
v:2928 [in MetaCoq.Translations.MiniHoTT]
v:2936 [in MetaCoq.Translations.MiniHoTT_paths]
v:295 [in MetaCoq.PCUIC.PCUICConversion]
v:296 [in MetaCoq.Erasure.EWcbvEval]
v:297 [in MetaCoq.Template.Environment]
v:298 [in MetaCoq.Template.Universes]
v:299 [in MetaCoq.Erasure.EWcbvEval]
v:3 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
v:3 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
v:300 [in MetaCoq.PCUIC.PCUICConversion]
v:301 [in MetaCoq.Template.Universes]
v:303 [in MetaCoq.Erasure.EEtaExpandedFix]
v:305 [in MetaCoq.PCUIC.PCUICConversion]
v:306 [in MetaCoq.Template.Universes]
v:307 [in MetaCoq.PCUIC.PCUICConfluence]
v:307 [in MetaCoq.PCUIC.PCUICConversion]
v:309 [in MetaCoq.Erasure.EWcbvEval]
v:31 [in MetaCoq.SafeChecker.PCUICWfReduction]
v:31 [in MetaCoq.Erasure.ETransform]
v:310 [in MetaCoq.Template.Universes]
v:311 [in MetaCoq.Template.WcbvEval]
v:311 [in MetaCoq.PCUIC.PCUICConversion]
v:312 [in MetaCoq.Template.Universes]
v:312 [in MetaCoq.Erasure.EEtaExpandedFix]
v:314 [in MetaCoq.Template.Universes]
v:315 [in MetaCoq.Template.WcbvEval]
v:315 [in MetaCoq.Erasure.EWcbvEval]
v:316 [in MetaCoq.Template.Universes]
v:318 [in MetaCoq.Template.Universes]
v:32 [in MetaCoq.Template.TermEquality]
v:32 [in MetaCoq.PCUIC.PCUICNormal]
v:320 [in MetaCoq.Erasure.EEtaExpandedFix]
v:321 [in MetaCoq.Template.Universes]
v:326 [in MetaCoq.Template.Universes]
v:33 [in MetaCoq.SafeChecker.PCUICWfReduction]
v:331 [in MetaCoq.Erasure.EArities]
v:331 [in MetaCoq.Erasure.ERemoveParams]
v:334 [in MetaCoq.PCUIC.PCUICEquality]
v:34 [in MetaCoq.Template.Normal]
v:340 [in MetaCoq.Template.common.uGraph]
v:343 [in MetaCoq.PCUIC.PCUICConversion]
v:344 [in MetaCoq.Template.common.uGraph]
v:35 [in MetaCoq.PCUIC.PCUICNormal]
v:35 [in MetaCoq.SafeChecker.PCUICSafeReduce]
v:354 [in MetaCoq.PCUIC.PCUICConfluence]
v:356 [in MetaCoq.PCUIC.PCUICWcbvEval]
v:36 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
v:365 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
v:367 [in MetaCoq.Erasure.EWcbvEval]
v:369 [in MetaCoq.Template.common.uGraph]
v:37 [in MetaCoq.Translations.param_binary]
v:370 [in MetaCoq.Template.common.uGraph]
v:371 [in MetaCoq.Erasure.EEtaExpandedFix]
v:371 [in MetaCoq.Template.common.uGraph]
v:371 [in MetaCoq.Translations.MiniHoTT]
v:372 [in MetaCoq.Template.common.uGraph]
v:374 [in MetaCoq.Erasure.ERemoveParams]
v:378 [in MetaCoq.PCUIC.PCUICWcbvEval]
v:378 [in MetaCoq.Translations.MiniHoTT]
v:378 [in MetaCoq.Erasure.EWcbvEval]
v:379 [in MetaCoq.Translations.MiniHoTT_paths]
v:38 [in MetaCoq.PCUIC.PCUICCumulativity]
v:38 [in MetaCoq.Erasure.ErasureCorrectness]
v:38 [in MetaCoq.PCUIC.PCUICNormal]
v:383 [in MetaCoq.PCUIC.PCUICWcbvEval]
v:384 [in MetaCoq.PCUIC.PCUICReduction]
v:385 [in MetaCoq.Translations.MiniHoTT]
v:386 [in MetaCoq.PCUIC.PCUICWcbvEval]
v:386 [in MetaCoq.Translations.MiniHoTT_paths]
v:386 [in MetaCoq.Erasure.EWcbvEval]
v:389 [in MetaCoq.PCUIC.PCUICReduction]
v:392 [in MetaCoq.Translations.MiniHoTT]
v:393 [in MetaCoq.PCUIC.PCUICWcbvEval]
v:393 [in MetaCoq.Translations.MiniHoTT_paths]
v:394 [in MetaCoq.PCUIC.PCUICEquality]
v:397 [in MetaCoq.PCUIC.PCUICWcbvEval]
v:398 [in MetaCoq.PCUIC.PCUICEquality]
v:399 [in MetaCoq.Translations.MiniHoTT]
v:4 [in MetaCoq.Erasure.EEtaExpandedFix]
v:4 [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
v:40 [in MetaCoq.SafeChecker.PCUICSafeReduce]
v:400 [in MetaCoq.Translations.MiniHoTT_paths]
v:403 [in MetaCoq.Erasure.EWcbvEval]
v:407 [in MetaCoq.Translations.MiniHoTT]
v:407 [in MetaCoq.Translations.MiniHoTT_paths]
v:41 [in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
v:41 [in MetaCoq.SafeChecker.PCUICEqualityDec]
v:412 [in MetaCoq.PCUIC.PCUICSubstitution]
v:415 [in MetaCoq.Translations.MiniHoTT]
v:415 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
v:415 [in MetaCoq.Translations.MiniHoTT_paths]
v:417 [in MetaCoq.PCUIC.PCUICSubstitution]
v:418 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
v:421 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
v:423 [in MetaCoq.PCUIC.PCUICSubstitution]
v:423 [in MetaCoq.Translations.MiniHoTT]
v:423 [in MetaCoq.Translations.MiniHoTT_paths]
v:425 [in MetaCoq.Erasure.EWcbvEval]
v:429 [in MetaCoq.PCUIC.PCUICSubstitution]
v:43 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
v:431 [in MetaCoq.Translations.MiniHoTT_paths]
v:437 [in MetaCoq.PCUIC.PCUICSubstitution]
v:439 [in MetaCoq.Erasure.EWcbvEval]
v:44 [in MetaCoq.PCUIC.PCUICNormal]
v:44 [in MetaCoq.SafeChecker.PCUICSafeReduce]
v:44 [in MetaCoq.SafeChecker.PCUICSafeChecker]
v:442 [in MetaCoq.Template.common.uGraph]
v:444 [in MetaCoq.Template.common.uGraph]
v:446 [in MetaCoq.PCUIC.PCUICEquality]
v:449 [in MetaCoq.PCUIC.PCUICSubstitution]
v:45 [in MetaCoq.PCUIC.PCUICSN]
v:451 [in MetaCoq.PCUIC.PCUICEquality]
v:452 [in MetaCoq.PCUIC.PCUICSubstitution]
v:452 [in MetaCoq.PCUIC.PCUICConversion]
v:46 [in MetaCoq.PCUIC.PCUICSafeLemmata]
v:46 [in MetaCoq.Erasure.ETransform]
v:460 [in MetaCoq.PCUIC.PCUICProgress]
v:460 [in MetaCoq.PCUIC.PCUICEquality]
v:463 [in MetaCoq.PCUIC.PCUICProgress]
v:466 [in MetaCoq.Erasure.EEtaExpandedFix]
v:468 [in MetaCoq.Template.Universes]
v:468 [in MetaCoq.PCUIC.PCUICEquality]
v:47 [in MetaCoq.SafeChecker.PCUICSafeConversion]
v:47 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
v:470 [in MetaCoq.Template.Typing]
v:473 [in MetaCoq.Template.Typing]
v:476 [in MetaCoq.Template.Universes]
v:477 [in MetaCoq.Template.Universes]
v:479 [in MetaCoq.PCUIC.PCUICProgress]
v:48 [in MetaCoq.PCUIC.PCUICSafeLemmata]
v:482 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
v:484 [in MetaCoq.Template.Universes]
v:487 [in MetaCoq.PCUIC.PCUICProgress]
v:487 [in MetaCoq.Template.Universes]
v:489 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
v:489 [in MetaCoq.Examples.tauto]
v:49 [in MetaCoq.Template.EnvMap]
v:491 [in MetaCoq.Examples.tauto]
v:494 [in MetaCoq.PCUIC.PCUICSpine]
v:499 [in MetaCoq.Template.Universes]
v:5 [in MetaCoq.PCUIC.PCUICTransform]
v:50 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
v:506 [in MetaCoq.Examples.tauto]
v:508 [in MetaCoq.Erasure.EEtaExpandedFix]
v:51 [in MetaCoq.PCUIC.PCUICSN]
v:512 [in MetaCoq.PCUIC.PCUICInductiveInversion]
v:515 [in MetaCoq.Template.common.uGraph]
v:517 [in MetaCoq.Template.EnvironmentTyping]
V:518 [in MetaCoq.PCUIC.PCUICSR]
v:519 [in MetaCoq.Template.utils.MCList]
v:52 [in MetaCoq.Erasure.ESpineView]
v:52 [in MetaCoq.SafeChecker.PCUICSafeConversion]
v:521 [in MetaCoq.Template.Universes]
v:523 [in MetaCoq.Template.utils.MCList]
V:525 [in MetaCoq.PCUIC.PCUICSR]
v:526 [in MetaCoq.Template.EnvironmentTyping]
v:527 [in MetaCoq.PCUIC.PCUICInductives]
v:528 [in MetaCoq.PCUIC.PCUICInductiveInversion]
v:53 [in MetaCoq.Template.EnvMap]
v:53 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
V:532 [in MetaCoq.PCUIC.PCUICSR]
v:538 [in MetaCoq.Template.EnvironmentTyping]
V:539 [in MetaCoq.PCUIC.PCUICSR]
v:540 [in MetaCoq.PCUIC.PCUICConfluence]
v:542 [in MetaCoq.Template.Universes]
v:543 [in MetaCoq.Template.EnvironmentTyping]
v:549 [in MetaCoq.PCUIC.PCUICConfluence]
v:55 [in MetaCoq.PCUIC.PCUICSafeLemmata]
v:56 [in MetaCoq.SafeChecker.PCUICSafeConversion]
v:561 [in MetaCoq.PCUIC.PCUICEquality]
v:563 [in MetaCoq.Erasure.EEtaExpandedFix]
V:565 [in MetaCoq.PCUIC.PCUICConfluence]
v:566 [in MetaCoq.PCUIC.PCUICEquality]
v:566 [in MetaCoq.PCUIC.PCUICConversion]
v:57 [in MetaCoq.Template.Normal]
v:57 [in MetaCoq.PCUIC.PCUICNormal]
v:57 [in MetaCoq.Template.EnvMap]
v:570 [in MetaCoq.Template.EnvironmentTyping]
v:570 [in MetaCoq.PCUIC.PCUICConfluence]
v:572 [in MetaCoq.PCUIC.PCUICEquality]
v:572 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
v:573 [in MetaCoq.Template.common.uGraph]
v:574 [in MetaCoq.PCUIC.PCUICInductiveInversion]
v:578 [in MetaCoq.SafeChecker.PCUICSafeConversion]
v:58 [in MetaCoq.Erasure.EDeps]
v:58 [in MetaCoq.PCUIC.PCUICConvCumInversion]
v:58 [in MetaCoq.SafeChecker.PCUICSafeConversion]
v:58 [in MetaCoq.Template.Transform]
v:580 [in MetaCoq.SafeChecker.PCUICSafeConversion]
v:588 [in MetaCoq.PCUIC.PCUICInductiveInversion]
v:59 [in MetaCoq.Template.utils.ReflectEq]
v:59 [in MetaCoq.PCUIC.PCUICSN]
v:59 [in MetaCoq.Erasure.ETransform]
v:6 [in MetaCoq.Erasure.ErasureCorrectness]
v:6 [in MetaCoq.Template.TermEquality]
v:6 [in MetaCoq.Template.TemplateProgram]
v:6 [in MetaCoq.PCUIC.Conversion.PCUICWeakeningConv]
v:6 [in MetaCoq.PCUIC.PCUICConvCumInversion]
v:60 [in MetaCoq.Template.Normal]
v:605 [in MetaCoq.Template.common.uGraph]
v:61 [in MetaCoq.PCUIC.PCUICSafeLemmata]
v:61 [in MetaCoq.Template.EnvMap]
v:618 [in MetaCoq.Template.utils.wGraph]
v:62 [in MetaCoq.PCUIC.PCUICCumulativity]
v:62 [in MetaCoq.PCUIC.PCUICCumulProp]
v:62 [in MetaCoq.SafeChecker.PCUICSafeConversion]
v:620 [in MetaCoq.PCUIC.PCUICEquality]
v:621 [in MetaCoq.Template.utils.wGraph]
v:624 [in MetaCoq.Template.utils.wGraph]
v:626 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
v:627 [in MetaCoq.Template.utils.wGraph]
v:63 [in MetaCoq.Template.Universes]
v:63 [in MetaCoq.PCUIC.PCUICSN]
v:631 [in MetaCoq.Template.utils.wGraph]
v:631 [in MetaCoq.PCUIC.PCUICConversion]
v:633 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
v:633 [in MetaCoq.PCUIC.PCUICConversion]
v:635 [in MetaCoq.Template.utils.wGraph]
v:636 [in MetaCoq.Template.EnvironmentTyping]
v:638 [in MetaCoq.SafeChecker.PCUICSafeConversion]
v:640 [in MetaCoq.SafeChecker.PCUICSafeConversion]
v:645 [in MetaCoq.Template.utils.wGraph]
v:648 [in MetaCoq.PCUIC.PCUICConversion]
v:649 [in MetaCoq.Template.utils.wGraph]
v:654 [in MetaCoq.PCUIC.PCUICConversion]
v:66 [in MetaCoq.Template.Normal]
v:664 [in MetaCoq.PCUIC.PCUICEquality]
v:664 [in MetaCoq.Template.utils.wGraph]
v:664 [in MetaCoq.SafeChecker.PCUICSafeConversion]
v:667 [in MetaCoq.Template.utils.wGraph]
v:670 [in MetaCoq.Template.utils.wGraph]
v:670 [in MetaCoq.SafeChecker.PCUICSafeConversion]
v:671 [in MetaCoq.PCUIC.PCUICParallelReduction]
v:673 [in MetaCoq.Template.utils.wGraph]
v:675 [in MetaCoq.Template.utils.All_Forall]
v:675 [in MetaCoq.PCUIC.PCUICEquality]
v:676 [in MetaCoq.SafeChecker.PCUICSafeConversion]
v:679 [in MetaCoq.PCUIC.PCUICEquality]
v:679 [in MetaCoq.Template.utils.wGraph]
v:68 [in MetaCoq.PCUIC.PCUICCumulativity]
v:68 [in MetaCoq.Template.common.uGraph]
v:68 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
v:680 [in MetaCoq.Template.Universes]
v:680 [in MetaCoq.Template.utils.MCList]
v:682 [in MetaCoq.Template.Universes]
v:683 [in MetaCoq.Template.common.uGraph]
v:683 [in MetaCoq.PCUIC.PCUICEquality]
v:683 [in MetaCoq.Template.utils.wGraph]
v:687 [in MetaCoq.PCUIC.PCUICEquality]
v:69 [in MetaCoq.PCUIC.PCUICConvCumInversion]
v:69 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
v:690 [in MetaCoq.PCUIC.PCUICConversion]
v:693 [in MetaCoq.SafeChecker.PCUICSafeConversion]
v:695 [in MetaCoq.PCUIC.PCUICEquality]
v:697 [in MetaCoq.Template.utils.wGraph]
v:697 [in MetaCoq.PCUIC.PCUICConversion]
v:699 [in MetaCoq.SafeChecker.PCUICSafeConversion]
v:70 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
v:70 [in MetaCoq.Erasure.ETransform]
v:701 [in MetaCoq.Template.utils.wGraph]
v:704 [in MetaCoq.PCUIC.PCUICEquality]
v:71 [in MetaCoq.PCUIC.PCUICInversion]
v:711 [in MetaCoq.PCUIC.PCUICConversion]
v:717 [in MetaCoq.PCUIC.PCUICConversion]
v:719 [in MetaCoq.SafeChecker.PCUICSafeChecker]
v:72 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
v:724 [in MetaCoq.PCUIC.PCUICConversion]
v:73 [in MetaCoq.Template.Normal]
v:730 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
v:733 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
v:733 [in MetaCoq.PCUIC.PCUICConversion]
v:736 [in MetaCoq.PCUIC.PCUICConversion]
v:738 [in MetaCoq.PCUIC.PCUICConversion]
v:74 [in MetaCoq.PCUIC.PCUICCumulProp]
v:741 [in MetaCoq.PCUIC.PCUICConversion]
v:743 [in MetaCoq.PCUIC.PCUICConversion]
v:745 [in MetaCoq.PCUIC.PCUICConversion]
v:747 [in MetaCoq.PCUIC.PCUICConversion]
v:749 [in MetaCoq.PCUIC.PCUICConversion]
v:75 [in MetaCoq.PCUIC.PCUICConvCumInversion]
v:75 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
v:751 [in MetaCoq.PCUIC.PCUICConversion]
v:753 [in MetaCoq.PCUIC.PCUICConversion]
v:755 [in MetaCoq.PCUIC.PCUICConversion]
v:758 [in MetaCoq.PCUIC.PCUICConversion]
v:760 [in MetaCoq.Template.utils.wGraph]
v:760 [in MetaCoq.PCUIC.PCUICConversion]
v:761 [in MetaCoq.Template.utils.wGraph]
v:763 [in MetaCoq.PCUIC.PCUICConversion]
v:764 [in MetaCoq.Translations.MiniHoTT]
v:765 [in MetaCoq.PCUIC.PCUICConversion]
v:77 [in MetaCoq.PCUIC.PCUICCumulProp]
v:771 [in MetaCoq.PCUIC.PCUICConversion]
v:772 [in MetaCoq.Translations.MiniHoTT_paths]
v:777 [in MetaCoq.PCUIC.PCUICConversion]
v:78 [in MetaCoq.PCUIC.PCUICSafeLemmata]
v:78 [in MetaCoq.PCUIC.PCUICInversion]
v:781 [in MetaCoq.PCUIC.PCUICInductiveInversion]
v:796 [in MetaCoq.PCUIC.PCUICConfluence]
v:80 [in MetaCoq.Erasure.ETransform]
v:800 [in MetaCoq.PCUIC.PCUICConfluence]
v:804 [in MetaCoq.PCUIC.PCUICConfluence]
v:805 [in MetaCoq.PCUIC.PCUICConversion]
v:81 [in MetaCoq.PCUIC.PCUICSafeLemmata]
v:82 [in MetaCoq.Template.common.uGraph]
v:82 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
v:832 [in MetaCoq.PCUIC.PCUICSpine]
v:836 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
v:84 [in MetaCoq.Template.common.uGraph]
v:845 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
v:85 [in MetaCoq.PCUIC.PCUICSafeLemmata]
v:85 [in MetaCoq.Template.common.uGraph]
v:858 [in MetaCoq.Template.utils.All_Forall]
v:88 [in MetaCoq.PCUIC.PCUICSafeLemmata]
v:89 [in MetaCoq.SafeChecker.PCUICSafeConversion]
v:9 [in MetaCoq.PCUIC.PCUICCumulProp]
v:9 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
v:907 [in MetaCoq.PCUIC.PCUICConfluence]
v:91 [in MetaCoq.PCUIC.PCUICSafeLemmata]
v:91 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
v:91 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
v:92 [in MetaCoq.Erasure.ETransform]
v:929 [in MetaCoq.PCUIC.PCUICConfluence]
v:94 [in MetaCoq.Template.Universes]
v:948 [in MetaCoq.Erasure.ErasureFunction]
v:95 [in MetaCoq.PCUIC.PCUICSafeLemmata]
v:95 [in MetaCoq.PCUIC.PCUICConvCumInversion]
v:955 [in MetaCoq.SafeChecker.PCUICSafeChecker]
v:96 [in MetaCoq.Template.Universes]
v:97 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
v:976 [in MetaCoq.PCUIC.PCUICReduction]
v:979 [in MetaCoq.PCUIC.PCUICReduction]
v:982 [in MetaCoq.PCUIC.PCUICReduction]
v:985 [in MetaCoq.Erasure.ErasureFunction]
v:985 [in MetaCoq.PCUIC.PCUICReduction]
v:99 [in MetaCoq.Template.common.uGraph]
| 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) |