| 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) |
B (binder)
base:334 [in MetaCoq.Template.EnvironmentTyping]base:340 [in MetaCoq.Template.EnvironmentTyping]
base:352 [in MetaCoq.Template.EnvironmentTyping]
base:434 [in MetaCoq.Template.utils.wGraph]
base:444 [in MetaCoq.Template.utils.wGraph]
bbodyf:93 [in MetaCoq.Template.Ast]
bbody:146 [in MetaCoq.Template.AstUtils]
bbody:31 [in MetaCoq.PCUIC.TemplateToPCUIC]
bbody:56 [in MetaCoq.PCUIC.TemplateToPCUICExpanded]
BB:385 [in MetaCoq.SafeChecker.PCUICSafeChecker]
bb:393 [in MetaCoq.SafeChecker.PCUICSafeChecker]
bb:396 [in MetaCoq.SafeChecker.PCUICSafeChecker]
BB:742 [in MetaCoq.SafeChecker.PCUICSafeChecker]
bb:752 [in MetaCoq.SafeChecker.PCUICSafeChecker]
bb:754 [in MetaCoq.SafeChecker.PCUICSafeChecker]
bb:758 [in MetaCoq.SafeChecker.PCUICSafeChecker]
bb:760 [in MetaCoq.SafeChecker.PCUICSafeChecker]
bb:764 [in MetaCoq.SafeChecker.PCUICSafeChecker]
bb:766 [in MetaCoq.SafeChecker.PCUICSafeChecker]
bb:768 [in MetaCoq.SafeChecker.PCUICSafeChecker]
bb:773 [in MetaCoq.SafeChecker.PCUICSafeChecker]
BB:849 [in MetaCoq.SafeChecker.PCUICSafeChecker]
bb:860 [in MetaCoq.SafeChecker.PCUICSafeChecker]
bb:863 [in MetaCoq.SafeChecker.PCUICSafeChecker]
bb:876 [in MetaCoq.SafeChecker.PCUICSafeChecker]
bb:879 [in MetaCoq.SafeChecker.PCUICSafeChecker]
bcontext':176 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
bcontext':181 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
bcontext:198 [in MetaCoq.PCUIC.PCUICAst]
bcontext:30 [in MetaCoq.PCUIC.TemplateToPCUIC]
bcontext:362 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
bctxd:18 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
bctx':127 [in MetaCoq.PCUIC.PCUICAlpha]
bctx:104 [in MetaCoq.Template.Typing]
bctx:110 [in MetaCoq.Template.Checker]
bctx:126 [in MetaCoq.PCUIC.PCUICAlpha]
bctx:143 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
bctx:147 [in MetaCoq.Template.AstUtils]
bctx:157 [in MetaCoq.PCUIC.Syntax.PCUICCases]
bctx:176 [in MetaCoq.Template.WcbvEval]
bctx:185 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
bctx:204 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
bctx:222 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
bctx:236 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
bctx:250 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
bctx:258 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
bctx:271 [in MetaCoq.Template.Typing]
bctx:3 [in MetaCoq.PCUIC.TemplateToPCUICExpanded]
bctx:32 [in MetaCoq.PCUIC.TemplateToPCUIC]
bctx:35 [in MetaCoq.Template.Typing]
bctx:356 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
bctx:362 [in MetaCoq.Template.Ast]
bctx:415 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
bctx:422 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
bctx:442 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
bctx:471 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
bctx:482 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
bctx:495 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
bctx:55 [in MetaCoq.PCUIC.TemplateToPCUICExpanded]
bctx:750 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
bctx:77 [in MetaCoq.PCUIC.Syntax.PCUICCases]
bctx:82 [in MetaCoq.Template.WcbvEval]
bctx:95 [in MetaCoq.PCUIC.Syntax.PCUICCases]
bctx:951 [in MetaCoq.PCUIC.PCUICInductiveInversion]
bds:166 [in MetaCoq.Erasure.Extract]
bds:677 [in MetaCoq.Erasure.ErasureFunction]
bd:16 [in MetaCoq.PCUIC.PCUICToTemplate]
bd:29 [in MetaCoq.PCUIC.PCUICExpandLets]
bd:50 [in MetaCoq.PCUIC.TemplateToPCUIC]
before:1421 [in MetaCoq.SafeChecker.PCUICSafeReduce]
Beq:1661 [in MetaCoq.Translations.MiniHoTT]
Beq:1669 [in MetaCoq.Translations.MiniHoTT_paths]
bf:478 [in MetaCoq.Examples.tauto]
bf:480 [in MetaCoq.Examples.tauto]
bf:482 [in MetaCoq.Examples.tauto]
bla:20 [in MetaCoq.Erasure.Prelim]
block_args:512 [in MetaCoq.Erasure.EEtaExpandedFix]
block_args:319 [in MetaCoq.Erasure.EEtaExpandedFix]
block_args:144 [in MetaCoq.Erasure.EEtaExpandedFix]
block_args:224 [in MetaCoq.Erasure.EConstructorsAsBlocks]
block_args:196 [in MetaCoq.Erasure.EConstructorsAsBlocks]
block_args:114 [in MetaCoq.Erasure.EEtaExpanded]
block_args:12 [in MetaCoq.Erasure.EEtaExpanded]
block_args:324 [in MetaCoq.Erasure.ERemoveParams]
block_args:320 [in MetaCoq.Erasure.ERemoveParams]
block_args:316 [in MetaCoq.Erasure.ERemoveParams]
bodies':50 [in MetaCoq.Translations.times_bool_fun]
bodies:128 [in MetaCoq.PCUIC.PCUICWfUniverses]
bodies:153 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
bodies:164 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
bodies:183 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
bodies:183 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
bodies:227 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
bodies:37 [in MetaCoq.PCUIC.TemplateToPCUICExpanded]
bodies:380 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
bodies:585 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
bodies:679 [in MetaCoq.Erasure.ErasureFunction]
bodies:95 [in MetaCoq.Translations.param_cheap_packed]
bodies:98 [in MetaCoq.Translations.param_cheap_packed]
bodyf:16 [in MetaCoq.PCUIC.Syntax.PCUICNamelessDef]
bodyf:54 [in MetaCoq.Template.BasicAst]
bodyf:69 [in MetaCoq.Template.BasicAst]
bodyf:89 [in MetaCoq.Template.Ast]
bodyx:86 [in MetaCoq.PCUIC.Syntax.PCUICReflect]
bodyy:90 [in MetaCoq.PCUIC.Syntax.PCUICReflect]
body':103 [in MetaCoq.Template.Checker]
body':1258 [in MetaCoq.SafeChecker.PCUICSafeReduce]
body':132 [in MetaCoq.PCUIC.PCUICParallelReduction]
body':139 [in MetaCoq.PCUIC.PCUICParallelReduction]
body':728 [in MetaCoq.PCUIC.PCUICParallelReduction]
body:103 [in MetaCoq.Template.EtaExpand]
body:105 [in MetaCoq.Erasure.EWcbvEval]
body:106 [in MetaCoq.Template.EtaExpand]
body:108 [in MetaCoq.PCUIC.PCUICNormal]
body:110 [in MetaCoq.Template.EtaExpand]
body:112 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
body:115 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
body:115 [in MetaCoq.Erasure.EWcbvEvalInd]
body:1211 [in MetaCoq.PCUIC.PCUICConversion]
body:1217 [in MetaCoq.PCUIC.PCUICConversion]
body:1240 [in MetaCoq.Erasure.ErasureFunction]
body:126 [in MetaCoq.Template.Typing]
body:13 [in MetaCoq.Template.WcbvEval]
body:13 [in MetaCoq.Erasure.ECSubst]
body:133 [in MetaCoq.PCUIC.PCUICParallelReduction]
body:138 [in MetaCoq.PCUIC.PCUICParallelReduction]
body:139 [in MetaCoq.Erasure.EDeps]
body:14 [in MetaCoq.PCUIC.PCUICReduction]
body:141 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
body:1417 [in MetaCoq.SafeChecker.PCUICSafeReduce]
body:159 [in MetaCoq.Template.WcbvEval]
body:161 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
body:171 [in MetaCoq.Template.EtaExpand]
body:172 [in MetaCoq.PCUIC.PCUICReduction]
body:175 [in MetaCoq.Template.EtaExpand]
body:180 [in MetaCoq.Template.EtaExpand]
body:189 [in MetaCoq.Template.Ast]
body:19 [in MetaCoq.Erasure.EEtaExpandedFix]
body:190 [in MetaCoq.PCUIC.PCUICParallelReduction]
body:190 [in MetaCoq.Erasure.EEtaExpanded]
body:192 [in MetaCoq.Template.Ast]
body:193 [in MetaCoq.Erasure.Extract]
body:193 [in MetaCoq.Erasure.EEtaExpanded]
body:196 [in MetaCoq.Erasure.Extract]
body:196 [in MetaCoq.Template.Ast]
body:197 [in MetaCoq.PCUIC.PCUICNormal]
body:197 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
body:201 [in MetaCoq.PCUIC.PCUICWcbvEval]
body:202 [in MetaCoq.Erasure.Extract]
body:206 [in MetaCoq.PCUIC.PCUICReduction]
body:21 [in MetaCoq.PCUIC.PCUICEtaExpand]
body:213 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
body:22 [in MetaCoq.Erasure.EEtaExpandedFix]
body:223 [in MetaCoq.Erasure.EEtaExpanded]
body:226 [in MetaCoq.Erasure.EEtaExpanded]
body:236 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
body:238 [in MetaCoq.PCUIC.PCUICParallelReduction]
body:24 [in MetaCoq.PCUIC.PCUICWcbvEval]
body:24 [in MetaCoq.PCUIC.PCUICEtaExpand]
body:248 [in MetaCoq.PCUIC.PCUICNormal]
body:259 [in MetaCoq.Template.Typing]
body:259 [in MetaCoq.PCUIC.PCUICNormal]
body:269 [in MetaCoq.PCUIC.PCUICNormal]
body:28 [in MetaCoq.PCUIC.PCUICEtaExpand]
body:297 [in MetaCoq.Template.Typing]
body:347 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
body:352 [in MetaCoq.PCUIC.PCUICSR]
body:362 [in MetaCoq.PCUIC.PCUICParallelReduction]
body:371 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
body:371 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
body:376 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
body:386 [in MetaCoq.PCUIC.PCUICSR]
body:40 [in MetaCoq.Template.TemplateMonad.Extractable]
body:405 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
body:416 [in MetaCoq.Template.Checker]
body:422 [in MetaCoq.PCUIC.PCUICParallelReduction]
body:43 [in MetaCoq.PCUIC.PCUICReduction]
body:50 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
body:515 [in MetaCoq.SafeChecker.PCUICTypeChecker]
body:62 [in MetaCoq.Erasure.EEtaExpandedFix]
body:63 [in MetaCoq.PCUIC.PCUICNormal]
body:66 [in MetaCoq.Erasure.EEtaExpandedFix]
body:66 [in MetaCoq.PCUIC.PCUICWcbvEval]
body:66 [in MetaCoq.Template.WcbvEval]
body:72 [in MetaCoq.Erasure.EPretty]
body:72 [in MetaCoq.Erasure.EDeps]
body:727 [in MetaCoq.PCUIC.PCUICParallelReduction]
body:76 [in MetaCoq.Erasure.EDeps]
body:829 [in MetaCoq.Erasure.ErasureFunction]
body:83 [in MetaCoq.PCUIC.PCUICEtaExpand]
body:84 [in MetaCoq.Erasure.EDeps]
body:85 [in MetaCoq.Erasure.EDeps]
body:87 [in MetaCoq.PCUIC.PCUICEtaExpand]
body:9 [in MetaCoq.PCUIC.Syntax.PCUICRenameDef]
body:90 [in MetaCoq.PCUIC.PCUICNormal]
body:92 [in MetaCoq.PCUIC.PCUICEtaExpand]
body:920 [in MetaCoq.Erasure.ErasureFunction]
body:93 [in MetaCoq.Template.Typing]
bod:1131 [in MetaCoq.Erasure.ErasureFunction]
bod:135 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
bod:136 [in MetaCoq.PCUIC.PCUICAst]
bod:14 [in MetaCoq.Template.WcbvEval]
bod:14 [in MetaCoq.Erasure.ECSubst]
bod:147 [in MetaCoq.Template.LiftSubst]
bod:173 [in MetaCoq.Erasure.ELiftSubst]
bod:25 [in MetaCoq.PCUIC.PCUICWcbvEval]
bod:50 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
bod:51 [in MetaCoq.Template.LiftSubst]
bod:660 [in MetaCoq.Erasure.ErasureFunction]
bod:663 [in MetaCoq.Erasure.ErasureFunction]
bod:91 [in MetaCoq.Erasure.ELiftSubst]
bod:94 [in MetaCoq.Erasure.ELiftSubst]
bo:1002 [in MetaCoq.PCUIC.PCUICReduction]
bo:1025 [in MetaCoq.PCUIC.PCUICReduction]
bo:1030 [in MetaCoq.PCUIC.PCUICReduction]
bo:1068 [in MetaCoq.PCUIC.PCUICReduction]
bo:1073 [in MetaCoq.PCUIC.PCUICReduction]
bo:1096 [in MetaCoq.PCUIC.PCUICReduction]
bo:1101 [in MetaCoq.PCUIC.PCUICReduction]
bo:997 [in MetaCoq.PCUIC.PCUICReduction]
branches:106 [in MetaCoq.PCUIC.PCUICEtaExpand]
branches:126 [in MetaCoq.Template.EtaExpand]
branches:200 [in MetaCoq.Erasure.EEtaExpanded]
branches:201 [in MetaCoq.Template.EtaExpand]
branches:209 [in MetaCoq.Template.Ast]
branches:233 [in MetaCoq.Erasure.EEtaExpanded]
branches:29 [in MetaCoq.Erasure.EEtaExpandedFix]
branches:38 [in MetaCoq.PCUIC.PCUICEtaExpand]
branches:76 [in MetaCoq.Erasure.EEtaExpandedFix]
brctxty':760 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
brctxty:1003 [in MetaCoq.PCUIC.PCUICInductiveInversion]
brctxty:1022 [in MetaCoq.PCUIC.PCUICInductiveInversion]
brctxty:1069 [in MetaCoq.Template.Typing]
brctxty:119 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
brctxty:134 [in MetaCoq.PCUIC.PCUICInversion]
brctxty:174 [in MetaCoq.PCUIC.PCUICProgress]
brctxty:221 [in MetaCoq.PCUIC.PCUICTyping]
brctxty:324 [in MetaCoq.PCUIC.PCUICProgress]
brctxty:408 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
brctxty:566 [in MetaCoq.PCUIC.PCUICTyping]
brctxty:66 [in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
brctxty:662 [in MetaCoq.Template.Typing]
brctxty:68 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
brctxty:700 [in MetaCoq.SafeChecker.PCUICTypeChecker]
brctxty:722 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
brctxty:744 [in MetaCoq.SafeChecker.PCUICTypeChecker]
brctxty:759 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
brctxty:766 [in MetaCoq.SafeChecker.PCUICTypeChecker]
brctxty:79 [in MetaCoq.PCUIC.PCUICTyping]
brctxty:889 [in MetaCoq.PCUIC.PCUICTyping]
brctxty:970 [in MetaCoq.PCUIC.PCUICInductiveInversion]
brctxty:986 [in MetaCoq.PCUIC.PCUICInductiveInversion]
brctx':1021 [in MetaCoq.PCUIC.PCUICInductiveInversion]
brctx':969 [in MetaCoq.PCUIC.PCUICInductiveInversion]
brctx:102 [in MetaCoq.PCUIC.Syntax.PCUICCases]
brctx:106 [in MetaCoq.PCUIC.PCUICSR]
brctx:190 [in MetaCoq.Template.Typing]
brctx:244 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
brctx:369 [in MetaCoq.Template.Typing]
brctx:394 [in MetaCoq.Template.Ast]
brctx:42 [in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
brctx:688 [in MetaCoq.PCUIC.PCUICReduction]
brctx:696 [in MetaCoq.PCUIC.PCUICReduction]
brctx:916 [in MetaCoq.PCUIC.PCUICReduction]
brctx:93 [in MetaCoq.PCUIC.PCUICSR]
brctx:99 [in MetaCoq.PCUIC.PCUICSR]
brs_ty:135 [in MetaCoq.PCUIC.PCUICInversion]
brs_ty:80 [in MetaCoq.PCUIC.PCUICTyping]
brs':10 [in MetaCoq.Template.TemplateCheckWf]
brs':118 [in MetaCoq.Erasure.Extract]
brs':1183 [in MetaCoq.Erasure.ErasureFunction]
brs':122 [in MetaCoq.PCUIC.PCUICConvCumInversion]
brs':124 [in MetaCoq.Template.TermEquality]
brs':124 [in MetaCoq.Erasure.ErasureProperties]
brs':1470 [in MetaCoq.SafeChecker.PCUICSafeConversion]
brs':149 [in MetaCoq.Template.AstUtils]
brs':155 [in MetaCoq.Template.Checker]
brs':168 [in MetaCoq.PCUIC.PCUICEquality]
brs':170 [in MetaCoq.PCUIC.PCUICAst]
brs':18 [in MetaCoq.Erasure.ELiftSubst]
brs':181 [in MetaCoq.PCUIC.PCUICAst]
brs':189 [in MetaCoq.Template.Typing]
brs':194 [in MetaCoq.PCUIC.PCUICAst]
brs':199 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
brs':2088 [in MetaCoq.SafeChecker.PCUICSafeConversion]
brs':209 [in MetaCoq.PCUIC.PCUICAst]
brs':218 [in MetaCoq.PCUIC.PCUICAst]
brs':226 [in MetaCoq.PCUIC.PCUICAst]
brs':227 [in MetaCoq.Template.Ast]
brs':234 [in MetaCoq.PCUIC.PCUICAst]
brs':2344 [in MetaCoq.SafeChecker.PCUICSafeConversion]
brs':239 [in MetaCoq.Template.Ast]
brs':253 [in MetaCoq.Template.Ast]
brs':26 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
brs':264 [in MetaCoq.Template.Ast]
brs':264 [in MetaCoq.PCUIC.PCUICReduction]
brs':266 [in MetaCoq.Erasure.ERemoveParams]
brs':272 [in MetaCoq.Template.Ast]
brs':280 [in MetaCoq.Template.Ast]
brs':29 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
brs':301 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
brs':308 [in MetaCoq.PCUIC.PCUICNormal]
brs':31 [in MetaCoq.Erasure.ELiftSubst]
brs':368 [in MetaCoq.Template.Typing]
brs':37 [in MetaCoq.PCUIC.TemplateToPCUIC]
brs':38 [in MetaCoq.Erasure.EWellformed]
brs':385 [in MetaCoq.PCUIC.PCUICNormal]
brs':40 [in MetaCoq.Translations.param_original]
brs':41 [in MetaCoq.Template.EtaExpand]
brs':414 [in MetaCoq.Erasure.ErasureFunction]
brs':439 [in MetaCoq.Erasure.ErasureFunction]
brs':444 [in MetaCoq.PCUIC.PCUICSR]
brs':460 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
brs':493 [in MetaCoq.PCUIC.PCUICNormal]
brs':5 [in MetaCoq.Erasure.EOptimizePropDiscr]
brs':51 [in MetaCoq.Erasure.Extract]
brs':564 [in MetaCoq.SafeChecker.PCUICSafeConversion]
brs':594 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
brs':597 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
brs':601 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
brs':604 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
brs':61 [in MetaCoq.SafeChecker.PCUICErrors]
brs':612 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
brs':646 [in MetaCoq.PCUIC.PCUICConversion]
brs':660 [in MetaCoq.PCUIC.PCUICConversion]
brs':670 [in MetaCoq.PCUIC.PCUICConversion]
brs':7 [in MetaCoq.PCUIC.PCUICExpandLets]
brs':7 [in MetaCoq.PCUIC.PCUICCSubst]
brs':7 [in MetaCoq.Erasure.ELiftSubst]
brs':7 [in MetaCoq.Template.WcbvEval]
brs':7 [in MetaCoq.Erasure.ECSubst]
brs':71 [in MetaCoq.SafeChecker.PCUICErrors]
brs':72 [in MetaCoq.Translations.param_cheap_packed]
brs':81 [in MetaCoq.SafeChecker.PCUICErrors]
brs':84 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
brs':85 [in MetaCoq.Template.AstUtils]
brs':9 [in MetaCoq.PCUIC.PCUICToTemplate]
brs':913 [in MetaCoq.PCUIC.PCUICReduction]
brs':933 [in MetaCoq.PCUIC.PCUICReduction]
brs':94 [in MetaCoq.PCUIC.PCUICReduction]
brs':940 [in MetaCoq.PCUIC.PCUICReduction]
brs':95 [in MetaCoq.Erasure.ERemoveParams]
brs':953 [in MetaCoq.PCUIC.PCUICReduction]
brs':958 [in MetaCoq.PCUIC.PCUICReduction]
brs':97 [in MetaCoq.Erasure.EConstructorsAsBlocks]
brs':973 [in MetaCoq.PCUIC.PCUICReduction]
brs0:199 [in MetaCoq.PCUIC.PCUICParallelReduction]
brs0:222 [in MetaCoq.PCUIC.PCUICParallelReduction]
brs0:269 [in MetaCoq.PCUIC.PCUICParallelReduction]
brs0:359 [in MetaCoq.PCUIC.PCUICConfluence]
brs0:364 [in MetaCoq.PCUIC.PCUICConfluence]
brs0:375 [in MetaCoq.PCUIC.PCUICParallelReduction]
brs0:402 [in MetaCoq.PCUIC.PCUICParallelReduction]
brs0:464 [in MetaCoq.PCUIC.PCUICParallelReduction]
brs1':1259 [in MetaCoq.SafeChecker.PCUICSafeConversion]
brs1':1288 [in MetaCoq.SafeChecker.PCUICSafeConversion]
brs1:1253 [in MetaCoq.SafeChecker.PCUICSafeConversion]
brs1:1282 [in MetaCoq.SafeChecker.PCUICSafeConversion]
brs1:200 [in MetaCoq.PCUIC.PCUICParallelReduction]
brs1:2149 [in MetaCoq.SafeChecker.PCUICSafeConversion]
brs1:223 [in MetaCoq.PCUIC.PCUICParallelReduction]
brs1:2371 [in MetaCoq.SafeChecker.PCUICSafeConversion]
brs1:2386 [in MetaCoq.SafeChecker.PCUICSafeConversion]
brs1:25 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
brs1:270 [in MetaCoq.PCUIC.PCUICParallelReduction]
brs1:376 [in MetaCoq.PCUIC.PCUICParallelReduction]
brs1:403 [in MetaCoq.PCUIC.PCUICParallelReduction]
brs1:426 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
brs1:465 [in MetaCoq.PCUIC.PCUICParallelReduction]
brs1:492 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
brs1:523 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
brs2':1260 [in MetaCoq.SafeChecker.PCUICSafeConversion]
brs2':1289 [in MetaCoq.SafeChecker.PCUICSafeConversion]
brs2:1254 [in MetaCoq.SafeChecker.PCUICSafeConversion]
brs2:1283 [in MetaCoq.SafeChecker.PCUICSafeConversion]
brs2:2155 [in MetaCoq.SafeChecker.PCUICSafeConversion]
brs2:2377 [in MetaCoq.SafeChecker.PCUICSafeConversion]
brs2:2392 [in MetaCoq.SafeChecker.PCUICSafeConversion]
brs2:424 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
brs2:490 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
brs2:521 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
brs:101 [in MetaCoq.Erasure.Prelim]
brs:1014 [in MetaCoq.PCUIC.PCUICInductiveInversion]
brs:102 [in MetaCoq.PCUIC.PCUICSafeLemmata]
brs:102 [in MetaCoq.Template.Typing]
brs:102 [in MetaCoq.Erasure.EDeps]
brs:103 [in MetaCoq.Erasure.EWcbvEvalInd]
brs:1032 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
brs:104 [in MetaCoq.Erasure.EWellformed]
brs:1057 [in MetaCoq.Template.Typing]
brs:111 [in MetaCoq.PCUIC.PCUICInversion]
brs:115 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
brs:116 [in MetaCoq.PCUIC.PCUICWcbvEval]
brs:116 [in MetaCoq.Erasure.Extract]
brs:117 [in MetaCoq.Template.Typing]
brs:118 [in MetaCoq.PCUIC.PCUICAst]
brs:118 [in MetaCoq.PCUIC.PCUICConvCumInversion]
brs:118 [in MetaCoq.Template.WcbvEval]
brs:118 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
brs:123 [in MetaCoq.Template.TermEquality]
brs:125 [in MetaCoq.Erasure.EOptimizePropDiscr]
brs:127 [in MetaCoq.PCUIC.PCUICTyping]
brs:128 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
brs:129 [in MetaCoq.Template.AstUtils]
brs:132 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
brs:140 [in MetaCoq.PCUIC.PCUICInversion]
brs:140 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
brs:1432 [in MetaCoq.SafeChecker.PCUICSafeReduce]
brs:1464 [in MetaCoq.SafeChecker.PCUICSafeConversion]
brs:156 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
brs:157 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
brs:159 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
brs:162 [in MetaCoq.PCUIC.PCUICProgress]
brs:163 [in MetaCoq.Template.Typing]
brs:164 [in MetaCoq.Erasure.ErasureProperties]
brs:166 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
brs:167 [in MetaCoq.PCUIC.PCUICEquality]
brs:171 [in MetaCoq.Template.WcbvEval]
brs:173 [in MetaCoq.PCUIC.Syntax.PCUICCases]
brs:173 [in MetaCoq.Erasure.ErasureProperties]
brs:174 [in MetaCoq.Template.Typing]
brs:175 [in MetaCoq.PCUIC.Syntax.PCUICCases]
brs:177 [in MetaCoq.PCUIC.Syntax.PCUICCases]
brs:179 [in MetaCoq.PCUIC.Syntax.PCUICCases]
brs:179 [in MetaCoq.PCUIC.PCUICReduction]
brs:180 [in MetaCoq.Erasure.ErasureProperties]
brs:181 [in MetaCoq.Template.Typing]
brs:188 [in MetaCoq.PCUIC.PCUICElimination]
brs:188 [in MetaCoq.Template.Typing]
brs:191 [in MetaCoq.Template.TypingWf]
brs:193 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
brs:195 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
brs:195 [in MetaCoq.PCUIC.PCUICReduction]
brs:199 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
brs:20 [in MetaCoq.PCUIC.PCUICReduction]
brs:201 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
brs:202 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
brs:204 [in MetaCoq.PCUIC.PCUICAst]
brs:205 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
brs:2062 [in MetaCoq.SafeChecker.PCUICSafeConversion]
brs:2087 [in MetaCoq.SafeChecker.PCUICSafeConversion]
brs:209 [in MetaCoq.PCUIC.PCUICWcbvEval]
brs:212 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
brs:212 [in MetaCoq.Template.WcbvEval]
brs:217 [in MetaCoq.Erasure.Extract]
brs:217 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
brs:217 [in MetaCoq.PCUIC.PCUICTyping]
brs:218 [in MetaCoq.PCUIC.PCUICWcbvEval]
brs:218 [in MetaCoq.Erasure.ErasureFunction]
brs:22 [in MetaCoq.Erasure.ESpineView]
brs:222 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
brs:223 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
brs:225 [in MetaCoq.PCUIC.PCUICInductiveInversion]
brs:226 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
brs:227 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
brs:23 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
brs:231 [in MetaCoq.PCUIC.PCUICTyping]
brs:233 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
brs:234 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
brs:2343 [in MetaCoq.SafeChecker.PCUICSafeConversion]
brs:237 [in MetaCoq.SafeChecker.PCUICSafeReduce]
brs:242 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
brs:246 [in MetaCoq.PCUIC.PCUICReduction]
brs:249 [in MetaCoq.PCUIC.PCUICWcbvEval]
brs:252 [in MetaCoq.PCUIC.PCUICReduction]
brs:258 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
brs:258 [in MetaCoq.PCUIC.PCUICReduction]
brs:263 [in MetaCoq.PCUIC.PCUICReduction]
brs:269 [in MetaCoq.Template.Typing]
brs:270 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
brs:279 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
brs:282 [in MetaCoq.Erasure.EArities]
brs:285 [in MetaCoq.PCUIC.PCUICSafeLemmata]
brs:286 [in MetaCoq.Template.Typing]
brs:289 [in MetaCoq.PCUIC.PCUICNormal]
brs:295 [in MetaCoq.PCUIC.PCUICNormal]
brs:300 [in MetaCoq.PCUIC.PCUICSafeLemmata]
brs:300 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
brs:301 [in MetaCoq.PCUIC.PCUICNormal]
brs:307 [in MetaCoq.PCUIC.PCUICNormal]
brs:312 [in MetaCoq.PCUIC.PCUICProgress]
brs:317 [in MetaCoq.PCUIC.PCUICWcbvEval]
brs:317 [in MetaCoq.PCUIC.PCUICNormal]
brs:32 [in MetaCoq.Erasure.EWcbvEvalInd]
brs:325 [in MetaCoq.Erasure.EArities]
brs:33 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
brs:334 [in MetaCoq.Erasure.EArities]
brs:34 [in MetaCoq.PCUIC.PCUICReduction]
brs:340 [in MetaCoq.Template.Typing]
brs:352 [in MetaCoq.Template.Typing]
brs:359 [in MetaCoq.Template.Typing]
brs:359 [in MetaCoq.PCUIC.PCUICSR]
brs:36 [in MetaCoq.Template.WfAst]
brs:367 [in MetaCoq.Template.Typing]
brs:37 [in MetaCoq.SafeChecker.PCUICWfReduction]
brs:374 [in MetaCoq.Template.Ast]
brs:375 [in MetaCoq.PCUIC.PCUICSR]
brs:378 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
brs:38 [in MetaCoq.Template.Normal]
brs:38 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
brs:380 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
brs:381 [in MetaCoq.Template.Ast]
brs:383 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
brs:384 [in MetaCoq.PCUIC.PCUICNormal]
brs:387 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
brs:394 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
brs:394 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
brs:397 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
brs:40 [in MetaCoq.Erasure.EWcbvEval]
brs:41 [in MetaCoq.SafeChecker.PCUICWfReduction]
brs:426 [in MetaCoq.PCUIC.PCUICSR]
brs:432 [in MetaCoq.PCUIC.PCUICSR]
brs:438 [in MetaCoq.PCUIC.PCUICSR]
brs:443 [in MetaCoq.PCUIC.PCUICSR]
brs:456 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
brs:459 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
brs:465 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
brs:4668 [in MetaCoq.SafeChecker.PCUICSafeConversion]
brs:48 [in MetaCoq.Erasure.EWcbvEvalInd]
brs:4866 [in MetaCoq.SafeChecker.PCUICSafeConversion]
brs:4875 [in MetaCoq.SafeChecker.PCUICSafeConversion]
brs:49 [in MetaCoq.Erasure.Extract]
brs:49 [in MetaCoq.Erasure.EWcbvEval]
brs:492 [in MetaCoq.PCUIC.PCUICNormal]
brs:52 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
brs:55 [in MetaCoq.Erasure.EWcbvEval]
brs:554 [in MetaCoq.PCUIC.PCUICTyping]
brs:56 [in MetaCoq.SafeChecker.PCUICErrors]
brs:560 [in MetaCoq.SafeChecker.PCUICSafeConversion]
brs:57 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
brs:58 [in MetaCoq.Erasure.EPretty]
brs:59 [in MetaCoq.Erasure.EPretty]
brs:599 [in MetaCoq.PCUIC.PCUICConversion]
brs:6 [in MetaCoq.PCUIC.PCUICProgress]
brs:604 [in MetaCoq.PCUIC.PCUICConversion]
brs:608 [in MetaCoq.PCUIC.PCUICConversion]
brs:61 [in MetaCoq.Erasure.EWcbvEvalInd]
brs:613 [in MetaCoq.PCUIC.PCUICConversion]
brs:623 [in MetaCoq.PCUIC.PCUICConversion]
brs:629 [in MetaCoq.PCUIC.PCUICConversion]
brs:645 [in MetaCoq.PCUIC.PCUICConversion]
brs:65 [in MetaCoq.PCUIC.PCUICElimination]
brs:651 [in MetaCoq.Template.Typing]
brs:659 [in MetaCoq.PCUIC.PCUICConversion]
brs:66 [in MetaCoq.SafeChecker.PCUICErrors]
brs:669 [in MetaCoq.PCUIC.PCUICConversion]
brs:69 [in MetaCoq.PCUIC.PCUICNormal]
brs:711 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
brs:711 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
brs:72 [in MetaCoq.PCUIC.PCUICTyping]
brs:73 [in MetaCoq.PCUIC.PCUICNormal]
brs:74 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
brs:747 [in MetaCoq.SafeChecker.PCUICTypeChecker]
brs:76 [in MetaCoq.SafeChecker.PCUICErrors]
brs:77 [in MetaCoq.Template.Normal]
brs:77 [in MetaCoq.PCUIC.PCUICReduction]
brs:79 [in MetaCoq.PCUIC.PCUICWcbvEval]
brs:79 [in MetaCoq.Template.WcbvEval]
brs:791 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
brs:815 [in MetaCoq.SafeChecker.PCUICSafeConversion]
brs:83 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
brs:84 [in MetaCoq.PCUIC.Syntax.PCUICCases]
brs:84 [in MetaCoq.PCUIC.PCUICReduction]
brs:843 [in MetaCoq.Erasure.ErasureFunction]
brs:877 [in MetaCoq.PCUIC.PCUICTyping]
brs:879 [in MetaCoq.PCUIC.PCUICReduction]
brs:88 [in MetaCoq.Template.Pretty]
brs:89 [in MetaCoq.PCUIC.Syntax.PCUICCases]
brs:89 [in MetaCoq.Template.Pretty]
brs:89 [in MetaCoq.PCUIC.PCUICReduction]
brs:89 [in MetaCoq.PCUIC.utils.PCUICPretty]
brs:894 [in MetaCoq.PCUIC.PCUICReduction]
brs:899 [in MetaCoq.PCUIC.PCUICReduction]
brs:90 [in MetaCoq.PCUIC.utils.PCUICPretty]
brs:904 [in MetaCoq.PCUIC.PCUICReduction]
brs:912 [in MetaCoq.PCUIC.PCUICReduction]
brs:92 [in MetaCoq.Erasure.EInlineProjections]
brs:921 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
brs:93 [in MetaCoq.Erasure.EWcbvEval]
brs:93 [in MetaCoq.PCUIC.PCUICReduction]
brs:932 [in MetaCoq.PCUIC.PCUICReduction]
brs:939 [in MetaCoq.PCUIC.PCUICReduction]
brs:952 [in MetaCoq.PCUIC.PCUICReduction]
brs:957 [in MetaCoq.PCUIC.PCUICReduction]
brs:960 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
brs:969 [in MetaCoq.PCUIC.PCUICReduction]
brs:99 [in MetaCoq.Erasure.EWellformed]
brs:997 [in MetaCoq.PCUIC.PCUICInductiveInversion]
br':1036 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
br':122 [in MetaCoq.Erasure.Extract]
br':1250 [in MetaCoq.SafeChecker.PCUICSafeConversion]
br':136 [in MetaCoq.PCUIC.PCUICAlpha]
br':1400 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
br':183 [in MetaCoq.Template.Checker]
br':192 [in MetaCoq.Template.Typing]
br':196 [in MetaCoq.Template.Checker]
br':203 [in MetaCoq.PCUIC.PCUICParallelReduction]
br':226 [in MetaCoq.PCUIC.PCUICParallelReduction]
br':251 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
br':266 [in MetaCoq.PCUIC.PCUICReduction]
br':269 [in MetaCoq.Template.Checker]
br':272 [in MetaCoq.PCUIC.PCUICParallelReduction]
br':299 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
br':306 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
br':308 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
br':310 [in MetaCoq.PCUIC.PCUICNormal]
br':316 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
br':361 [in MetaCoq.PCUIC.PCUICConfluence]
br':362 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
br':366 [in MetaCoq.PCUIC.PCUICConfluence]
br':371 [in MetaCoq.Template.Typing]
br':379 [in MetaCoq.PCUIC.PCUICParallelReduction]
br':387 [in MetaCoq.PCUIC.PCUICNormal]
br':406 [in MetaCoq.PCUIC.PCUICParallelReduction]
br':438 [in MetaCoq.Erasure.ErasureFunction]
br':439 [in MetaCoq.PCUIC.PCUICConversion]
br':44 [in MetaCoq.PCUIC.PCUICContextConversion]
br':446 [in MetaCoq.PCUIC.PCUICSR]
br':46 [in MetaCoq.PCUIC.PCUICContextConversion]
br':465 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
br':467 [in MetaCoq.PCUIC.PCUICParallelReduction]
br':467 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
br':488 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
br':495 [in MetaCoq.PCUIC.PCUICNormal]
br':501 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
br':503 [in MetaCoq.PCUIC.PCUICNormal]
br':505 [in MetaCoq.PCUIC.PCUICNormal]
br':519 [in MetaCoq.PCUIC.PCUICParallelReduction]
br':523 [in MetaCoq.PCUIC.PCUICParallelReduction]
br':527 [in MetaCoq.PCUIC.PCUICParallelReduction]
br':531 [in MetaCoq.PCUIC.PCUICParallelReduction]
br':535 [in MetaCoq.PCUIC.PCUICParallelReduction]
br':539 [in MetaCoq.PCUIC.PCUICParallelReduction]
br':543 [in MetaCoq.PCUIC.PCUICParallelReduction]
br':547 [in MetaCoq.PCUIC.PCUICParallelReduction]
br':551 [in MetaCoq.PCUIC.PCUICParallelReduction]
br':555 [in MetaCoq.PCUIC.PCUICParallelReduction]
br':559 [in MetaCoq.PCUIC.PCUICParallelReduction]
br':563 [in MetaCoq.PCUIC.PCUICParallelReduction]
br':687 [in MetaCoq.PCUIC.PCUICReduction]
br':695 [in MetaCoq.PCUIC.PCUICReduction]
br':710 [in MetaCoq.PCUIC.PCUICReduction]
br':713 [in MetaCoq.PCUIC.PCUICReduction]
br':756 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
br':794 [in MetaCoq.PCUIC.PCUICReduction]
br':80 [in MetaCoq.PCUIC.Syntax.PCUICReflect]
br':89 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
br':915 [in MetaCoq.PCUIC.PCUICReduction]
br':935 [in MetaCoq.PCUIC.PCUICReduction]
br':942 [in MetaCoq.PCUIC.PCUICReduction]
br':956 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
br':96 [in MetaCoq.PCUIC.PCUICReduction]
br0:518 [in MetaCoq.PCUIC.PCUICParallelReduction]
br0:526 [in MetaCoq.PCUIC.PCUICParallelReduction]
br0:534 [in MetaCoq.PCUIC.PCUICParallelReduction]
br0:542 [in MetaCoq.PCUIC.PCUICParallelReduction]
br0:550 [in MetaCoq.PCUIC.PCUICParallelReduction]
br0:558 [in MetaCoq.PCUIC.PCUICParallelReduction]
br:10 [in MetaCoq.PCUIC.utils.PCUICSize]
br:100 [in MetaCoq.Erasure.EWellformed]
br:1002 [in MetaCoq.PCUIC.PCUICInductiveInversion]
br:101 [in MetaCoq.Erasure.ESubstitution]
br:1019 [in MetaCoq.PCUIC.PCUICInductiveInversion]
br:103 [in MetaCoq.Template.Typing]
br:103 [in MetaCoq.Erasure.EDeps]
br:1033 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
br:104 [in MetaCoq.Erasure.EDeps]
br:1049 [in MetaCoq.Erasure.ErasureFunction]
br:105 [in MetaCoq.Template.WfAst]
br:105 [in MetaCoq.Erasure.EWellformed]
br:106 [in MetaCoq.Erasure.EWellformed]
br:106 [in MetaCoq.Erasure.Prelim]
br:1068 [in MetaCoq.Template.Typing]
br:107 [in MetaCoq.PCUIC.PCUICEtaExpand]
br:107 [in MetaCoq.Erasure.Prelim]
br:108 [in MetaCoq.PCUIC.PCUICEtaExpand]
br:118 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
br:118 [in MetaCoq.PCUIC.Syntax.PCUICCases]
br:119 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
br:121 [in MetaCoq.Erasure.Extract]
br:1249 [in MetaCoq.SafeChecker.PCUICSafeConversion]
br:126 [in MetaCoq.Erasure.EOptimizePropDiscr]
br:127 [in MetaCoq.Template.EtaExpand]
br:128 [in MetaCoq.Erasure.Prelim]
br:133 [in MetaCoq.PCUIC.PCUICInversion]
br:134 [in MetaCoq.Erasure.ERemoveParams]
br:135 [in MetaCoq.PCUIC.PCUICAlpha]
br:136 [in MetaCoq.PCUIC.PCUICSubstitution]
br:137 [in MetaCoq.Template.Checker]
br:139 [in MetaCoq.Erasure.EEtaExpanded]
br:1399 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
br:143 [in MetaCoq.Template.Checker]
br:144 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
br:145 [in MetaCoq.Template.AstUtils]
br:152 [in MetaCoq.Erasure.EConstructorsAsBlocks]
br:152 [in MetaCoq.Erasure.EGlobalEnv]
br:153 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
br:155 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
br:157 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
br:16 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
br:160 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
br:165 [in MetaCoq.Examples.tauto]
br:166 [in MetaCoq.Erasure.ErasureProperties]
br:168 [in MetaCoq.PCUIC.PCUICSR]
br:17 [in MetaCoq.Erasure.ELiftSubst]
br:172 [in MetaCoq.Template.WcbvEval]
br:173 [in MetaCoq.PCUIC.PCUICProgress]
br:174 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
br:180 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
br:180 [in MetaCoq.PCUIC.PCUICReduction]
br:182 [in MetaCoq.Template.Checker]
br:185 [in MetaCoq.Template.TypingWf]
br:186 [in MetaCoq.PCUIC.PCUICAlpha]
br:191 [in MetaCoq.Template.Typing]
br:195 [in MetaCoq.PCUIC.Syntax.PCUICCases]
br:195 [in MetaCoq.Template.Checker]
br:196 [in MetaCoq.PCUIC.PCUICAlpha]
br:198 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
br:199 [in MetaCoq.PCUIC.Syntax.PCUICCases]
br:2 [in MetaCoq.PCUIC.PCUICExpandLets]
br:201 [in MetaCoq.PCUIC.PCUICParallelReduction]
br:201 [in MetaCoq.Erasure.EEtaExpanded]
br:202 [in MetaCoq.Template.EtaExpand]
br:202 [in MetaCoq.PCUIC.PCUICParallelReduction]
br:203 [in MetaCoq.Template.EtaExpand]
br:204 [in MetaCoq.PCUIC.Syntax.PCUICCases]
br:206 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
br:209 [in MetaCoq.PCUIC.Syntax.PCUICCases]
br:21 [in MetaCoq.PCUIC.PCUICReduction]
br:216 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
br:218 [in MetaCoq.Erasure.Extract]
br:219 [in MetaCoq.PCUIC.PCUICWcbvEval]
br:220 [in MetaCoq.PCUIC.Syntax.PCUICCases]
br:220 [in MetaCoq.Erasure.ErasureFunction]
br:220 [in MetaCoq.PCUIC.PCUICTyping]
br:225 [in MetaCoq.PCUIC.PCUICParallelReduction]
br:227 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
br:228 [in MetaCoq.PCUIC.PCUICInductiveInversion]
br:231 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
br:234 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
br:234 [in MetaCoq.Erasure.EEtaExpanded]
br:235 [in MetaCoq.Erasure.EEtaExpanded]
br:24 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
br:241 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
br:241 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
br:243 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
br:244 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
br:247 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
br:248 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
br:250 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
br:250 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
br:256 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
br:257 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
br:265 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
br:265 [in MetaCoq.PCUIC.PCUICReduction]
br:268 [in MetaCoq.Template.Checker]
br:27 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
br:270 [in MetaCoq.Template.Typing]
br:271 [in MetaCoq.PCUIC.PCUICParallelReduction]
br:286 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
br:294 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
br:30 [in MetaCoq.Erasure.EEtaExpandedFix]
br:30 [in MetaCoq.Erasure.ELiftSubst]
br:302 [in MetaCoq.PCUIC.PCUICSafeLemmata]
br:305 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
br:307 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
br:309 [in MetaCoq.PCUIC.PCUICNormal]
br:309 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
br:309 [in MetaCoq.Template.TypingWf]
br:31 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
br:318 [in MetaCoq.PCUIC.PCUICWcbvEval]
br:32 [in MetaCoq.PCUIC.PCUICSafeLemmata]
br:32 [in MetaCoq.PCUIC.Syntax.PCUICCases]
br:323 [in MetaCoq.PCUIC.PCUICProgress]
br:33 [in MetaCoq.Erasure.EInlineProjections]
br:33 [in MetaCoq.Erasure.EWcbvEvalInd]
br:336 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
br:34 [in MetaCoq.PCUIC.Syntax.PCUICCases]
br:35 [in MetaCoq.Erasure.ESubstitution]
br:353 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
br:355 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
br:356 [in MetaCoq.Erasure.EEtaExpandedFix]
br:36 [in MetaCoq.Template.Typing]
br:360 [in MetaCoq.PCUIC.PCUICConfluence]
br:360 [in MetaCoq.PCUIC.PCUICSR]
br:365 [in MetaCoq.PCUIC.PCUICConfluence]
br:368 [in MetaCoq.Template.Ast]
br:37 [in MetaCoq.Erasure.EWellformed]
br:37 [in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
br:370 [in MetaCoq.Template.Typing]
br:375 [in MetaCoq.Template.Ast]
br:377 [in MetaCoq.PCUIC.PCUICParallelReduction]
br:378 [in MetaCoq.PCUIC.PCUICParallelReduction]
br:379 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
br:38 [in MetaCoq.PCUIC.Syntax.PCUICCases]
br:382 [in MetaCoq.Template.Ast]
br:386 [in MetaCoq.PCUIC.PCUICNormal]
br:388 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
br:39 [in MetaCoq.PCUIC.PCUICEtaExpand]
br:390 [in MetaCoq.Template.Ast]
br:393 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
br:396 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
br:40 [in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
br:40 [in MetaCoq.Template.WfAst]
br:40 [in MetaCoq.PCUIC.TemplateToPCUIC]
br:404 [in MetaCoq.Template.Ast]
br:405 [in MetaCoq.PCUIC.PCUICParallelReduction]
br:407 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
br:41 [in MetaCoq.Erasure.EWcbvEval]
br:423 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
br:425 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
br:43 [in MetaCoq.PCUIC.PCUICContextConversion]
br:43 [in MetaCoq.Erasure.EOptimizePropDiscr]
br:430 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
br:438 [in MetaCoq.PCUIC.PCUICConversion]
br:443 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
br:445 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
br:445 [in MetaCoq.PCUIC.PCUICSR]
br:45 [in MetaCoq.PCUIC.PCUICContextConversion]
br:450 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
br:459 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
br:462 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
br:464 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
br:464 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
br:466 [in MetaCoq.PCUIC.PCUICParallelReduction]
br:466 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
br:481 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
br:485 [in MetaCoq.PCUIC.PCUICNormal]
br:49 [in MetaCoq.Erasure.EWcbvEvalInd]
br:491 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
br:494 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
br:494 [in MetaCoq.PCUIC.PCUICNormal]
br:50 [in MetaCoq.Erasure.EPretty]
br:50 [in MetaCoq.Erasure.EWcbvEval]
br:502 [in MetaCoq.PCUIC.PCUICNormal]
br:504 [in MetaCoq.PCUIC.PCUICNormal]
br:522 [in MetaCoq.PCUIC.PCUICParallelReduction]
br:522 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
br:526 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
br:529 [in MetaCoq.Erasure.EEtaExpandedFix]
br:53 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
br:530 [in MetaCoq.PCUIC.PCUICParallelReduction]
br:538 [in MetaCoq.PCUIC.PCUICParallelReduction]
br:54 [in MetaCoq.Erasure.EPretty]
br:546 [in MetaCoq.PCUIC.PCUICParallelReduction]
br:55 [in MetaCoq.Template.WfAst]
br:554 [in MetaCoq.PCUIC.PCUICParallelReduction]
br:562 [in MetaCoq.PCUIC.PCUICParallelReduction]
br:565 [in MetaCoq.PCUIC.PCUICTyping]
br:578 [in MetaCoq.PCUIC.PCUICConversion]
br:6 [in MetaCoq.PCUIC.PCUICCSubst]
br:6 [in MetaCoq.Erasure.ELiftSubst]
br:6 [in MetaCoq.Erasure.ECSubst]
br:61 [in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
br:618 [in MetaCoq.PCUIC.PCUICParallelReduction]
br:649 [in MetaCoq.PCUIC.PCUICSR]
br:657 [in MetaCoq.PCUIC.PCUICSR]
br:661 [in MetaCoq.Template.Typing]
br:661 [in MetaCoq.PCUIC.PCUICConversion]
br:662 [in MetaCoq.PCUIC.PCUICConversion]
br:67 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
br:675 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
br:686 [in MetaCoq.PCUIC.PCUICReduction]
br:694 [in MetaCoq.PCUIC.PCUICReduction]
br:699 [in MetaCoq.SafeChecker.PCUICTypeChecker]
br:709 [in MetaCoq.PCUIC.PCUICReduction]
br:712 [in MetaCoq.PCUIC.PCUICReduction]
br:721 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
br:736 [in MetaCoq.SafeChecker.PCUICTypeChecker]
br:748 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
br:77 [in MetaCoq.Erasure.EEtaExpandedFix]
br:775 [in MetaCoq.SafeChecker.PCUICTypeChecker]
br:78 [in MetaCoq.Erasure.EEtaExpandedFix]
br:78 [in MetaCoq.PCUIC.PCUICTyping]
br:78 [in MetaCoq.PCUIC.PCUICCasesContexts]
br:79 [in MetaCoq.PCUIC.Syntax.PCUICReflect]
br:793 [in MetaCoq.PCUIC.PCUICReduction]
br:794 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
br:799 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
br:80 [in MetaCoq.PCUIC.PCUICWcbvEval]
br:80 [in MetaCoq.Template.WcbvEval]
br:859 [in MetaCoq.Erasure.ErasureFunction]
br:86 [in MetaCoq.Template.Pretty]
br:86 [in MetaCoq.PCUIC.utils.PCUICPretty]
br:861 [in MetaCoq.Erasure.ErasureFunction]
br:869 [in MetaCoq.Erasure.ErasureFunction]
br:871 [in MetaCoq.Erasure.ErasureFunction]
br:88 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
br:888 [in MetaCoq.PCUIC.PCUICTyping]
br:914 [in MetaCoq.PCUIC.PCUICReduction]
br:918 [in MetaCoq.PCUIC.PCUICInductiveInversion]
br:93 [in MetaCoq.Erasure.EInlineProjections]
br:934 [in MetaCoq.PCUIC.PCUICReduction]
br:941 [in MetaCoq.PCUIC.PCUICReduction]
br:95 [in MetaCoq.PCUIC.PCUICReduction]
br:953 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
br:961 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
br:967 [in MetaCoq.PCUIC.PCUICInductiveInversion]
br:985 [in MetaCoq.PCUIC.PCUICInductiveInversion]
bs:1007 [in MetaCoq.Template.utils.All_Forall]
bs:1125 [in MetaCoq.Template.utils.wGraph]
bs:890 [in MetaCoq.Template.utils.All_Forall]
bs:895 [in MetaCoq.Template.utils.All_Forall]
bs:93 [in MetaCoq.Template.utils.All_Forall]
bs:999 [in MetaCoq.Template.utils.All_Forall]
btys:457 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
btys:792 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
bty:1001 [in MetaCoq.Template.Typing]
bty:101 [in MetaCoq.PCUIC.PCUICProgress]
bty:254 [in MetaCoq.PCUIC.PCUICProgress]
bty:363 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
bty:460 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
bty:465 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
bty:494 [in MetaCoq.PCUIC.PCUICTyping]
bty:621 [in MetaCoq.Template.Typing]
bty:795 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
bty:800 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
bty:822 [in MetaCoq.PCUIC.PCUICTyping]
bypass_opacity:19 [in MetaCoq.Template.TemplateMonad.Extractable]
b_ty:261 [in MetaCoq.PCUIC.PCUICProgress]
b_ty:108 [in MetaCoq.PCUIC.PCUICProgress]
b_ty:1008 [in MetaCoq.Template.Typing]
b_ty:624 [in MetaCoq.Template.Typing]
b_ty:829 [in MetaCoq.PCUIC.PCUICTyping]
b_ty:501 [in MetaCoq.PCUIC.PCUICTyping]
b'_ty:264 [in MetaCoq.PCUIC.PCUICProgress]
b'_ty:111 [in MetaCoq.PCUIC.PCUICProgress]
b'_ty:1011 [in MetaCoq.Template.Typing]
b'_ty:627 [in MetaCoq.Template.Typing]
b'_ty:478 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
b'_ty:348 [in MetaCoq.Template.Checker]
b'_ty:832 [in MetaCoq.PCUIC.PCUICTyping]
b'_ty:504 [in MetaCoq.PCUIC.PCUICTyping]
b'_ty:1067 [in MetaCoq.SafeChecker.PCUICTypeChecker]
B'':22 [in MetaCoq.PCUIC.Bidirectional.BDUnique]
B'':92 [in MetaCoq.PCUIC.Bidirectional.BDUnique]
b':1001 [in MetaCoq.PCUIC.PCUICConfluence]
b':1005 [in MetaCoq.PCUIC.PCUICConfluence]
b':1009 [in MetaCoq.Template.Typing]
B':104 [in MetaCoq.PCUIC.Bidirectional.BDUnique]
B':104 [in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
b':109 [in MetaCoq.PCUIC.PCUICProgress]
b':109 [in MetaCoq.Template.TermEquality]
b':11 [in MetaCoq.Erasure.ESpineView]
b':110 [in MetaCoq.PCUIC.Syntax.PCUICViews]
B':110 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
b':110 [in MetaCoq.PCUIC.Syntax.PCUICReflect]
b':110 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
B':111 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
B':1127 [in MetaCoq.PCUIC.PCUICConversion]
B':1136 [in MetaCoq.PCUIC.PCUICConversion]
B':1138 [in MetaCoq.PCUIC.PCUICReduction]
B':1143 [in MetaCoq.PCUIC.PCUICReduction]
B':116 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
B':116 [in MetaCoq.PCUIC.Bidirectional.BDUnique]
b':1173 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
B':119 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
b':1194 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
b':12 [in MetaCoq.PCUIC.PCUICReduction]
B':121 [in MetaCoq.PCUIC.PCUICSpine]
B':127 [in MetaCoq.PCUIC.PCUICSpine]
B':131 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
b':1332 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
B':14 [in MetaCoq.PCUIC.PCUICGeneration]
B':1431 [in MetaCoq.Template.utils.All_Forall]
b':144 [in MetaCoq.Template.Typing]
b':148 [in MetaCoq.PCUIC.PCUICConfluence]
b':149 [in MetaCoq.Template.Typing]
b':149 [in MetaCoq.PCUIC.PCUICConfluence]
b':149 [in MetaCoq.Erasure.Prelim]
b':15 [in MetaCoq.PCUIC.PCUICContextConversion]
b':150 [in MetaCoq.Template.Checker]
b':153 [in MetaCoq.PCUIC.PCUICEquality]
b':154 [in MetaCoq.Template.Typing]
B':1609 [in MetaCoq.Template.utils.All_Forall]
b':169 [in MetaCoq.PCUIC.PCUICReduction]
B':1690 [in MetaCoq.Template.utils.All_Forall]
b':17 [in MetaCoq.Template.utils.MCUtils]
B':1725 [in MetaCoq.Template.utils.All_Forall]
b':18 [in MetaCoq.Template.BasicAst]
b':186 [in MetaCoq.PCUIC.PCUICWcbvEval]
b':190 [in MetaCoq.PCUIC.PCUICConversion]
b':192 [in MetaCoq.PCUIC.PCUICInductiveInversion]
b':193 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
B':197 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
B':20 [in MetaCoq.PCUIC.Bidirectional.BDUnique]
B':2068 [in MetaCoq.Template.utils.All_Forall]
b':21 [in MetaCoq.Template.BasicAst]
B':216 [in MetaCoq.PCUIC.PCUICCumulProp]
B':22 [in MetaCoq.Translations.standard_model]
b':227 [in MetaCoq.PCUIC.PCUICReduction]
b':23 [in MetaCoq.Template.WfAst]
b':233 [in MetaCoq.PCUIC.PCUICReduction]
b':239 [in MetaCoq.PCUIC.PCUICReduction]
B':24 [in MetaCoq.Translations.times_bool_fun]
b':24 [in MetaCoq.Erasure.EReflect]
B':2480 [in MetaCoq.Template.utils.All_Forall]
b':256 [in MetaCoq.Template.Typing]
B':26 [in MetaCoq.PCUIC.PCUICArities]
b':262 [in MetaCoq.PCUIC.PCUICProgress]
B':267 [in MetaCoq.PCUIC.PCUICConversion]
B':27 [in MetaCoq.Translations.times_bool_fun]
b':272 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
B':273 [in MetaCoq.PCUIC.PCUICConversion]
b':282 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
B':29 [in MetaCoq.PCUIC.PCUICProgress]
b':312 [in MetaCoq.Template.WcbvEval]
b':318 [in MetaCoq.Template.Typing]
b':324 [in MetaCoq.Template.Typing]
b':324 [in MetaCoq.Template.Environment]
b':325 [in MetaCoq.Template.common.uGraph]
b':330 [in MetaCoq.Template.Typing]
b':332 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
B':335 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
b':337 [in MetaCoq.Template.Environment]
b':343 [in MetaCoq.PCUIC.PCUICReduction]
b':349 [in MetaCoq.PCUIC.PCUICSR]
b':368 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
b':394 [in MetaCoq.PCUIC.PCUICWcbvEval]
B':396 [in MetaCoq.PCUIC.PCUICNormal]
b':398 [in MetaCoq.PCUIC.PCUICInductiveInversion]
B':401 [in MetaCoq.PCUIC.PCUICNormal]
b':407 [in MetaCoq.PCUIC.PCUICSR]
b':409 [in MetaCoq.Erasure.ErasureFunction]
b':411 [in MetaCoq.PCUIC.PCUICInductiveInversion]
B':412 [in MetaCoq.PCUIC.PCUICConversion]
b':413 [in MetaCoq.PCUIC.PCUICSR]
b':419 [in MetaCoq.PCUIC.PCUICSR]
b':420 [in MetaCoq.Template.EnvironmentTyping]
B':422 [in MetaCoq.PCUIC.PCUICConversion]
B':425 [in MetaCoq.PCUIC.PCUICInductiveInversion]
B':44 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
b':443 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
b':452 [in MetaCoq.PCUIC.PCUICInductives]
B':48 [in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
b':49 [in MetaCoq.Translations.times_bool_fun]
B':49 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
b':49 [in MetaCoq.Template.Reflect]
b':50 [in MetaCoq.Template.utils.MCProd]
B':501 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
b':502 [in MetaCoq.PCUIC.PCUICTyping]
b':52 [in MetaCoq.Template.utils.MCProd]
B':552 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
b':57 [in MetaCoq.Template.TermEquality]
B':58 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
b':59 [in MetaCoq.Template.Typing]
b':60 [in MetaCoq.PCUIC.PCUICEquality]
b':61 [in MetaCoq.PCUIC.PCUICReduction]
b':625 [in MetaCoq.Template.Typing]
B':63 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
b':66 [in MetaCoq.PCUIC.PCUICReduction]
b':669 [in MetaCoq.Erasure.ErasureFunction]
b':67 [in MetaCoq.PCUIC.utils.PCUICOnOne]
B':69 [in MetaCoq.PCUIC.PCUICSafeLemmata]
b':69 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
B':696 [in MetaCoq.Template.Typing]
B':71 [in MetaCoq.PCUIC.PCUICFirstorder]
b':71 [in MetaCoq.PCUIC.PCUICReduction]
B':734 [in MetaCoq.Template.utils.MCList]
b':770 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
b':788 [in MetaCoq.PCUIC.PCUICParallelReduction]
b':794 [in MetaCoq.PCUIC.PCUICConversion]
B':810 [in MetaCoq.PCUIC.PCUICConversion]
b':813 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
B':818 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
b':828 [in MetaCoq.SafeChecker.PCUICTypeChecker]
b':829 [in MetaCoq.SafeChecker.PCUICTypeChecker]
b':83 [in MetaCoq.Template.Universes]
b':830 [in MetaCoq.PCUIC.PCUICTyping]
b':85 [in MetaCoq.Template.Environment]
b':855 [in MetaCoq.PCUIC.PCUICParallelReduction]
b':86 [in MetaCoq.Template.Environment]
B':90 [in MetaCoq.PCUIC.Bidirectional.BDUnique]
b':91 [in MetaCoq.Template.Typing]
B':944 [in MetaCoq.Template.Typing]
b0':150 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
b0':153 [in MetaCoq.Template.WcbvEval]
b0':192 [in MetaCoq.PCUIC.PCUICWcbvEval]
b0':23 [in MetaCoq.Erasure.EWcbvEvalInd]
b0':31 [in MetaCoq.Erasure.EWcbvEval]
b0':60 [in MetaCoq.PCUIC.PCUICWcbvEval]
b0':60 [in MetaCoq.Template.WcbvEval]
b0:149 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
b0:152 [in MetaCoq.Template.WcbvEval]
b0:178 [in MetaCoq.PCUIC.PCUICParallelReduction]
b0:187 [in MetaCoq.PCUIC.PCUICParallelReduction]
b0:191 [in MetaCoq.PCUIC.PCUICWcbvEval]
b0:196 [in MetaCoq.PCUIC.PCUICWcbvEval]
B0:20 [in MetaCoq.Translations.param_original]
b0:22 [in MetaCoq.Erasure.EWcbvEvalInd]
b0:22 [in MetaCoq.SafeChecker.PCUICSafeChecker]
b0:23 [in MetaCoq.SafeChecker.PCUICSafeChecker]
b0:243 [in MetaCoq.PCUIC.PCUICConversion]
b0:259 [in MetaCoq.PCUIC.PCUICConversion]
b0:262 [in MetaCoq.PCUIC.PCUICParallelReduction]
b0:30 [in MetaCoq.Erasure.EWcbvEval]
B0:33 [in MetaCoq.Translations.param_binary]
b0:346 [in MetaCoq.PCUIC.PCUICParallelReduction]
b0:357 [in MetaCoq.PCUIC.PCUICParallelReduction]
b0:384 [in MetaCoq.PCUIC.PCUICSubstitution]
b0:455 [in MetaCoq.PCUIC.PCUICParallelReduction]
b0:59 [in MetaCoq.PCUIC.PCUICWcbvEval]
b0:59 [in MetaCoq.Template.WcbvEval]
b0:874 [in MetaCoq.PCUIC.PCUICReduction]
b0:900 [in MetaCoq.PCUIC.PCUICParallelReduction]
b1:151 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
b1:155 [in MetaCoq.Template.WcbvEval]
b1:179 [in MetaCoq.PCUIC.PCUICParallelReduction]
b1:18 [in MetaCoq.Template.utils.MCUtils]
b1:188 [in MetaCoq.PCUIC.PCUICParallelReduction]
b1:195 [in MetaCoq.PCUIC.PCUICWcbvEval]
b1:199 [in MetaCoq.PCUIC.PCUICWcbvEval]
B1:21 [in MetaCoq.Translations.param_original]
b1:24 [in MetaCoq.Erasure.EWcbvEvalInd]
b1:244 [in MetaCoq.PCUIC.PCUICConversion]
B1:26 [in MetaCoq.SafeChecker.PCUICErrors]
b1:260 [in MetaCoq.PCUIC.PCUICConversion]
b1:263 [in MetaCoq.PCUIC.PCUICParallelReduction]
b1:32 [in MetaCoq.Erasure.EWcbvEval]
b1:347 [in MetaCoq.PCUIC.PCUICParallelReduction]
B1:35 [in MetaCoq.Translations.param_binary]
B1:35 [in MetaCoq.SafeChecker.PCUICErrors]
b1:358 [in MetaCoq.PCUIC.PCUICParallelReduction]
B1:36 [in MetaCoq.Translations.param_cheap_packed]
b1:385 [in MetaCoq.PCUIC.PCUICSubstitution]
B1:44 [in MetaCoq.Translations.param_generous_packed]
b1:456 [in MetaCoq.PCUIC.PCUICParallelReduction]
B1:47 [in MetaCoq.Translations.param_generous_packed]
B1:515 [in MetaCoq.PCUIC.PCUICConversion]
b1:547 [in MetaCoq.SafeChecker.PCUICSafeConversion]
B1:553 [in MetaCoq.SafeChecker.PCUICSafeConversion]
b1:62 [in MetaCoq.PCUIC.PCUICWcbvEval]
b1:62 [in MetaCoq.Template.WcbvEval]
b1:73 [in MetaCoq.Template.utils.ReflectEq]
b1:865 [in MetaCoq.PCUIC.PCUICConversion]
b1:875 [in MetaCoq.PCUIC.PCUICConversion]
b1:875 [in MetaCoq.PCUIC.PCUICReduction]
b1:883 [in MetaCoq.PCUIC.PCUICConversion]
b1:901 [in MetaCoq.PCUIC.PCUICParallelReduction]
b2:19 [in MetaCoq.Template.utils.MCUtils]
B2:30 [in MetaCoq.SafeChecker.PCUICErrors]
B2:38 [in MetaCoq.Translations.param_cheap_packed]
B2:39 [in MetaCoq.SafeChecker.PCUICErrors]
B2:45 [in MetaCoq.Translations.param_generous_packed]
B2:516 [in MetaCoq.PCUIC.PCUICConversion]
b2:550 [in MetaCoq.SafeChecker.PCUICSafeConversion]
B2:556 [in MetaCoq.SafeChecker.PCUICSafeConversion]
b2:74 [in MetaCoq.Template.utils.ReflectEq]
b2:868 [in MetaCoq.PCUIC.PCUICConversion]
b2:876 [in MetaCoq.PCUIC.PCUICConversion]
b2:884 [in MetaCoq.PCUIC.PCUICConversion]
b:1 [in MetaCoq.Template.utils.bytestring]
b:1 [in MetaCoq.Template.common.uGraph]
B:10 [in MetaCoq.Erasure.EPretty]
b:10 [in MetaCoq.Erasure.Extract]
b:10 [in MetaCoq.PCUIC.PCUICNormal]
b:10 [in MetaCoq.Erasure.ESpineView]
B:10 [in MetaCoq.Template.utils.MCPrelude]
b:10 [in MetaCoq.PCUIC.PCUICReduction]
b:100 [in MetaCoq.PCUIC.Syntax.PCUICViews]
b:100 [in MetaCoq.Template.utils.ReflectEq]
b:100 [in MetaCoq.PCUIC.PCUICTyping]
b:1000 [in MetaCoq.PCUIC.PCUICConfluence]
B:1002 [in MetaCoq.Translations.MiniHoTT_paths]
b:1004 [in MetaCoq.PCUIC.PCUICConfluence]
B:1005 [in MetaCoq.Translations.MiniHoTT]
b:1006 [in MetaCoq.Template.utils.All_Forall]
b:1007 [in MetaCoq.Template.Typing]
B:1007 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
B:101 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
b:101 [in MetaCoq.Template.Ast]
B:101 [in MetaCoq.PCUIC.PCUICTyping]
B:101 [in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
B:1013 [in MetaCoq.Translations.MiniHoTT_paths]
B:1017 [in MetaCoq.Template.utils.All_Forall]
B:102 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
B:102 [in MetaCoq.PCUIC.PCUICCumulProp]
B:102 [in MetaCoq.Translations.param_generous_packed]
B:1020 [in MetaCoq.Translations.MiniHoTT]
b:1023 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
b:1026 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
B:1028 [in MetaCoq.Translations.MiniHoTT_paths]
b:103 [in MetaCoq.PCUIC.PCUICAst]
B:103 [in MetaCoq.Translations.MiniHoTT]
B:103 [in MetaCoq.PCUIC.Bidirectional.BDUnique]
B:1032 [in MetaCoq.Template.utils.All_Forall]
B:1032 [in MetaCoq.Translations.MiniHoTT]
B:1033 [in MetaCoq.PCUIC.PCUICConversion]
B:104 [in MetaCoq.Template.utils.All_Forall]
B:104 [in MetaCoq.PCUIC.PCUICAst]
b:104 [in MetaCoq.PCUIC.Syntax.PCUICReflect]
B:1040 [in MetaCoq.Translations.MiniHoTT_paths]
b:1046 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
B:1047 [in MetaCoq.Template.utils.All_Forall]
b:1047 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
B:1048 [in MetaCoq.Translations.MiniHoTT]
B:1049 [in MetaCoq.PCUIC.PCUICConfluence]
B:105 [in MetaCoq.Template.BasicAst]
B:105 [in MetaCoq.Template.utils.MCList]
B:105 [in MetaCoq.Template.Ast]
b:105 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
b:1056 [in MetaCoq.PCUIC.PCUICConfluence]
B:1056 [in MetaCoq.Translations.MiniHoTT_paths]
B:1058 [in MetaCoq.Template.utils.All_Forall]
B:106 [in MetaCoq.Translations.param_binary]
B:106 [in MetaCoq.PCUIC.PCUICArities]
B:106 [in MetaCoq.PCUIC.PCUICCumulProp]
B:106 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
B:106 [in MetaCoq.Template.monad_utils]
b:1061 [in MetaCoq.PCUIC.PCUICConfluence]
b:1064 [in MetaCoq.PCUIC.PCUICConfluence]
B:1065 [in MetaCoq.Translations.MiniHoTT]
B:1066 [in MetaCoq.SafeChecker.PCUICTypeChecker]
B:1068 [in MetaCoq.Template.utils.All_Forall]
b:1069 [in MetaCoq.PCUIC.PCUICConfluence]
b:107 [in MetaCoq.PCUIC.PCUICProgress]
b:107 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
B:1071 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
B:1071 [in MetaCoq.Translations.MiniHoTT]
B:1073 [in MetaCoq.PCUIC.PCUICConfluence]
B:1073 [in MetaCoq.Translations.MiniHoTT_paths]
B:1078 [in MetaCoq.Template.utils.All_Forall]
B:1079 [in MetaCoq.Translations.MiniHoTT_paths]
b:108 [in MetaCoq.Template.TermEquality]
B:108 [in MetaCoq.PCUIC.PCUICTyping]
b:108 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
B:108 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
B:1080 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
B:1088 [in MetaCoq.Template.utils.All_Forall]
B:109 [in MetaCoq.Template.BasicAst]
b:109 [in MetaCoq.PCUIC.Syntax.PCUICViews]
B:109 [in MetaCoq.Erasure.ERemoveParams]
B:1098 [in MetaCoq.Template.utils.All_Forall]
b:11 [in MetaCoq.Template.utils.MCReflect]
B:11 [in MetaCoq.Template.Normal]
b:11 [in MetaCoq.Template.utils.ReflectEq]
B:11 [in MetaCoq.SafeChecker.PCUICWfReduction]
B:11 [in MetaCoq.Template.utils.MCUtils]
B:11 [in MetaCoq.Template.utils.MCProd]
b:11 [in MetaCoq.Translations.param_generous_packed]
B:11 [in MetaCoq.PCUIC.utils.PCUICPretty]
b:110 [in MetaCoq.PCUIC.PCUICArities]
B:110 [in MetaCoq.PCUIC.PCUICValidity]
b:110 [in MetaCoq.PCUIC.Syntax.PCUICCases]
B:1105 [in MetaCoq.Template.Typing]
B:1108 [in MetaCoq.Template.utils.All_Forall]
B:111 [in MetaCoq.Translations.param_binary]
B:111 [in MetaCoq.PCUIC.PCUICArities]
b:111 [in MetaCoq.PCUIC.PCUICEtaExpand]
B:111 [in MetaCoq.Translations.MiniHoTT]
B:111 [in MetaCoq.Translations.MiniHoTT_paths]
B:1113 [in MetaCoq.Template.utils.All_Forall]
B:1118 [in MetaCoq.Template.utils.All_Forall]
B:1126 [in MetaCoq.PCUIC.PCUICConversion]
B:1127 [in MetaCoq.Template.utils.All_Forall]
B:113 [in MetaCoq.Template.utils.MCList]
B:113 [in MetaCoq.PCUIC.Bidirectional.BDUnique]
B:1133 [in MetaCoq.PCUIC.PCUICReduction]
B:1135 [in MetaCoq.PCUIC.PCUICConversion]
B:1136 [in MetaCoq.Template.utils.All_Forall]
B:1137 [in MetaCoq.PCUIC.PCUICReduction]
B:114 [in MetaCoq.Translations.param_binary]
b:114 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
B:1141 [in MetaCoq.PCUIC.PCUICReduction]
B:1145 [in MetaCoq.Template.utils.All_Forall]
b:115 [in MetaCoq.Template.EnvironmentTyping]
B:115 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
B:1154 [in MetaCoq.Template.utils.All_Forall]
B:116 [in MetaCoq.Template.utils.All_Forall]
B:116 [in MetaCoq.Translations.MiniHoTT]
B:1163 [in MetaCoq.Template.utils.All_Forall]
B:117 [in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
b:117 [in MetaCoq.PCUIC.PCUICArities]
b:117 [in MetaCoq.Erasure.ErasureFunction]
B:1172 [in MetaCoq.Template.utils.All_Forall]
b:1172 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
B:1174 [in MetaCoq.PCUIC.PCUICReduction]
B:118 [in MetaCoq.PCUIC.PCUICProgress]
B:118 [in MetaCoq.Translations.param_binary]
B:118 [in MetaCoq.Template.utils.MCList]
B:118 [in MetaCoq.PCUIC.PCUICArities]
B:118 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
B:1180 [in MetaCoq.PCUIC.PCUICReduction]
B:1182 [in MetaCoq.Template.utils.All_Forall]
b:1187 [in MetaCoq.PCUIC.PCUICConversion]
b:119 [in MetaCoq.Template.Ast]
b:119 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
B:119 [in MetaCoq.Translations.MiniHoTT_paths]
b:1193 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
B:1196 [in MetaCoq.Template.utils.All_Forall]
b:12 [in MetaCoq.Template.EtaExpand]
B:12 [in MetaCoq.Template.BasicAst]
b:12 [in MetaCoq.PCUIC.Syntax.PCUICViews]
B:12 [in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
B:12 [in MetaCoq.PCUIC.PCUICGeneration]
b:12 [in MetaCoq.Examples.demo]
b:12 [in MetaCoq.PCUIC.Syntax.PCUICNamelessDef]
B:12 [in MetaCoq.Template.utils.MCPrelude]
B:12 [in MetaCoq.Erasure.EOptimizePropDiscr]
B:120 [in MetaCoq.Template.BasicAst]
B:120 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
B:120 [in MetaCoq.PCUIC.PCUICSpine]
B:1202 [in MetaCoq.Template.utils.All_Forall]
B:121 [in MetaCoq.Template.Ast]
B:121 [in MetaCoq.Template.monad_utils]
B:123 [in MetaCoq.PCUIC.Syntax.PCUICCases]
b:123 [in MetaCoq.Erasure.EWellformed]
B:124 [in MetaCoq.Translations.param_binary]
b:124 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
B:124 [in MetaCoq.Translations.MiniHoTT]
B:124 [in MetaCoq.Translations.MiniHoTT_paths]
B:1244 [in MetaCoq.Template.utils.All_Forall]
b:1247 [in MetaCoq.Translations.MiniHoTT]
B:125 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
b:125 [in MetaCoq.PCUIC.PCUICFirstorder]
b:125 [in MetaCoq.Erasure.ErasureProperties]
B:1255 [in MetaCoq.Template.utils.All_Forall]
b:1255 [in MetaCoq.Translations.MiniHoTT_paths]
b:1259 [in MetaCoq.Translations.MiniHoTT]
b:126 [in MetaCoq.Erasure.EAstUtils]
B:126 [in MetaCoq.PCUIC.PCUICSpine]
b:1267 [in MetaCoq.Translations.MiniHoTT_paths]
B:1268 [in MetaCoq.Template.utils.All_Forall]
B:127 [in MetaCoq.Template.utils.All_Forall]
B:127 [in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
B:1272 [in MetaCoq.PCUIC.PCUICConversion]
b:1277 [in MetaCoq.PCUIC.PCUICConfluence]
B:1278 [in MetaCoq.Template.utils.All_Forall]
b:128 [in MetaCoq.Template.Ast]
b:128 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
B:1281 [in MetaCoq.Translations.MiniHoTT]
B:1289 [in MetaCoq.Translations.MiniHoTT]
B:1289 [in MetaCoq.Translations.MiniHoTT_paths]
b:129 [in MetaCoq.PCUIC.PCUICArities]
b:129 [in MetaCoq.Template.Ast]
b:129 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
b:129 [in MetaCoq.Erasure.EWellformed]
b:129 [in MetaCoq.Erasure.ERemoveParams]
B:1297 [in MetaCoq.Translations.MiniHoTT_paths]
B:1299 [in MetaCoq.Translations.MiniHoTT]
b:13 [in MetaCoq.Template.utils.MCReflect]
b:13 [in MetaCoq.PCUIC.PCUICContextSubst]
B:130 [in MetaCoq.PCUIC.PCUICArities]
B:130 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
B:130 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
B:1301 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
B:1304 [in MetaCoq.Template.utils.All_Forall]
B:1307 [in MetaCoq.Translations.MiniHoTT_paths]
b:131 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
B:1311 [in MetaCoq.Translations.MiniHoTT]
B:1319 [in MetaCoq.Translations.MiniHoTT_paths]
B:132 [in MetaCoq.Translations.MiniHoTT_paths]
B:1320 [in MetaCoq.Translations.MiniHoTT]
B:1327 [in MetaCoq.Template.utils.All_Forall]
B:1328 [in MetaCoq.Translations.MiniHoTT]
B:1328 [in MetaCoq.Translations.MiniHoTT_paths]
B:133 [in MetaCoq.Examples.tauto]
B:133 [in MetaCoq.Translations.MiniHoTT]
b:1331 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
B:1336 [in MetaCoq.Translations.MiniHoTT_paths]
B:1339 [in MetaCoq.Translations.MiniHoTT]
B:134 [in MetaCoq.PCUIC.PCUICSafeLemmata]
b:134 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
b:134 [in MetaCoq.Erasure.EWellformed]
b:134 [in MetaCoq.Erasure.EEtaExpanded]
B:1347 [in MetaCoq.Translations.MiniHoTT]
B:1347 [in MetaCoq.Translations.MiniHoTT_paths]
B:135 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
B:135 [in MetaCoq.PCUIC.PCUICFirstorder]
B:135 [in MetaCoq.Examples.tauto]
B:1353 [in MetaCoq.Template.utils.All_Forall]
B:1355 [in MetaCoq.Translations.MiniHoTT_paths]
b:1362 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
B:1363 [in MetaCoq.Template.utils.All_Forall]
B:137 [in MetaCoq.Examples.tauto]
B:1373 [in MetaCoq.Template.utils.All_Forall]
b:138 [in MetaCoq.Template.Ast]
B:138 [in MetaCoq.Translations.MiniHoTT]
b:138 [in MetaCoq.Template.monad_utils]
B:1388 [in MetaCoq.Template.utils.All_Forall]
B:139 [in MetaCoq.PCUIC.utils.PCUICUtils]
b:139 [in MetaCoq.Template.Ast]
b:139 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
b:14 [in MetaCoq.Template.BasicAst]
B:14 [in MetaCoq.PCUIC.PCUICRedTypeIrrelevance]
B:14 [in MetaCoq.Template.utils.MCRelations]
B:14 [in MetaCoq.Template.Normal]
b:14 [in MetaCoq.Template.utils.ReflectEq]
B:14 [in MetaCoq.PCUIC.PCUICPrincipality]
b:14 [in MetaCoq.PCUIC.PCUICContextConversion]
B:14 [in MetaCoq.Translations.times_bool_fun2]
b:14 [in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
B:14 [in MetaCoq.PCUIC.Syntax.PCUICNamelessDef]
B:140 [in MetaCoq.PCUIC.PCUICSafeLemmata]
B:140 [in MetaCoq.Erasure.EArities]
B:140 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
b:140 [in MetaCoq.PCUIC.PCUICConversion]
B:1405 [in MetaCoq.Template.utils.All_Forall]
B:141 [in MetaCoq.Template.Ast]
B:141 [in MetaCoq.Translations.MiniHoTT_paths]
B:1413 [in MetaCoq.Template.utils.All_Forall]
B:1414 [in MetaCoq.Translations.MiniHoTT]
B:1418 [in MetaCoq.Template.utils.All_Forall]
b:142 [in MetaCoq.Template.Typing]
B:1422 [in MetaCoq.Translations.MiniHoTT_paths]
B:1424 [in MetaCoq.Translations.MiniHoTT]
B:1429 [in MetaCoq.Template.utils.All_Forall]
b:143 [in MetaCoq.Erasure.Prelim]
B:1432 [in MetaCoq.Translations.MiniHoTT_paths]
B:1434 [in MetaCoq.Translations.MiniHoTT]
B:1439 [in MetaCoq.Translations.MiniHoTT]
B:144 [in MetaCoq.Erasure.EArities]
B:144 [in MetaCoq.Template.utils.MCList]
b:144 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
B:144 [in MetaCoq.Examples.tauto]
B:1440 [in MetaCoq.Template.utils.All_Forall]
B:1442 [in MetaCoq.Translations.MiniHoTT_paths]
B:1445 [in MetaCoq.Template.utils.All_Forall]
B:1446 [in MetaCoq.Translations.MiniHoTT]
B:1447 [in MetaCoq.Translations.MiniHoTT_paths]
B:145 [in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
B:145 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
b:145 [in MetaCoq.Erasure.EConstructorsAsBlocks]
B:145 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
B:1451 [in MetaCoq.Template.utils.All_Forall]
B:1453 [in MetaCoq.Translations.MiniHoTT]
B:1454 [in MetaCoq.Translations.MiniHoTT_paths]
b:1458 [in MetaCoq.Translations.MiniHoTT]
B:1459 [in MetaCoq.Template.utils.All_Forall]
B:146 [in MetaCoq.Examples.tauto]
b:146 [in MetaCoq.Template.WcbvEval]
B:146 [in MetaCoq.Translations.MiniHoTT_paths]
B:1461 [in MetaCoq.Translations.MiniHoTT_paths]
B:1462 [in MetaCoq.Translations.MiniHoTT]
b:1465 [in MetaCoq.Translations.MiniHoTT]
b:1466 [in MetaCoq.Translations.MiniHoTT_paths]
B:1467 [in MetaCoq.Template.utils.All_Forall]
b:147 [in MetaCoq.Template.Typing]
B:147 [in MetaCoq.Translations.MiniHoTT]
B:1470 [in MetaCoq.Translations.MiniHoTT_paths]
B:1473 [in MetaCoq.Translations.MiniHoTT]
b:1473 [in MetaCoq.Translations.MiniHoTT_paths]
B:1475 [in MetaCoq.Template.utils.All_Forall]
B:1475 [in MetaCoq.Translations.MiniHoTT]
B:148 [in MetaCoq.Erasure.EArities]
B:148 [in MetaCoq.Template.Ast]
B:148 [in MetaCoq.Examples.tauto]
b:148 [in MetaCoq.Erasure.Prelim]
b:1481 [in MetaCoq.Translations.MiniHoTT]
B:1481 [in MetaCoq.Translations.MiniHoTT_paths]
B:1482 [in MetaCoq.Template.utils.All_Forall]
B:1483 [in MetaCoq.Translations.MiniHoTT]
B:1483 [in MetaCoq.Translations.MiniHoTT_paths]
b:1489 [in MetaCoq.Translations.MiniHoTT_paths]
B:149 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
b:149 [in MetaCoq.PCUIC.PCUICFirstorder]
B:1490 [in MetaCoq.Translations.MiniHoTT]
B:1491 [in MetaCoq.Translations.MiniHoTT_paths]
B:1497 [in MetaCoq.Template.utils.All_Forall]
B:1498 [in MetaCoq.Translations.MiniHoTT]
B:1498 [in MetaCoq.Translations.MiniHoTT_paths]
B:15 [in MetaCoq.Template.utils.All_Forall]
B:15 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
b:15 [in MetaCoq.Template.utils.MCUtils]
B:15 [in MetaCoq.Template.TemplateMonad.Common]
B:15 [in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
b:150 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
b:150 [in MetaCoq.PCUIC.PCUICConversion]
B:1505 [in MetaCoq.Translations.MiniHoTT]
B:1506 [in MetaCoq.Translations.MiniHoTT_paths]
B:1512 [in MetaCoq.Template.utils.All_Forall]
B:1513 [in MetaCoq.Translations.MiniHoTT_paths]
B:1517 [in MetaCoq.Translations.MiniHoTT]
B:1519 [in MetaCoq.Template.utils.All_Forall]
B:152 [in MetaCoq.Erasure.EArities]
B:152 [in MetaCoq.Template.utils.MCList]
b:152 [in MetaCoq.Template.Typing]
b:152 [in MetaCoq.PCUIC.PCUICEquality]
B:152 [in MetaCoq.Translations.MiniHoTT]
B:1524 [in MetaCoq.Template.utils.All_Forall]
B:1525 [in MetaCoq.Translations.MiniHoTT_paths]
B:153 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
b:153 [in MetaCoq.PCUIC.PCUICFirstorder]
B:1534 [in MetaCoq.Translations.MiniHoTT]
B:1539 [in MetaCoq.Template.utils.All_Forall]
B:154 [in MetaCoq.PCUIC.PCUICElimination]
b:1541 [in MetaCoq.Translations.MiniHoTT]
b:1542 [in MetaCoq.Translations.MiniHoTT]
B:1542 [in MetaCoq.Translations.MiniHoTT_paths]
b:1543 [in MetaCoq.Translations.MiniHoTT]
b:1544 [in MetaCoq.Translations.MiniHoTT]
b:1545 [in MetaCoq.Translations.MiniHoTT]
b:1546 [in MetaCoq.Translations.MiniHoTT]
B:1547 [in MetaCoq.Template.utils.All_Forall]
b:1549 [in MetaCoq.Translations.MiniHoTT_paths]
B:155 [in MetaCoq.Translations.times_bool_fun]
b:155 [in MetaCoq.PCUIC.PCUICConversion]
B:155 [in MetaCoq.Translations.MiniHoTT_paths]
b:1550 [in MetaCoq.Translations.MiniHoTT_paths]
b:1551 [in MetaCoq.Translations.MiniHoTT_paths]
b:1552 [in MetaCoq.Translations.MiniHoTT_paths]
B:1553 [in MetaCoq.Template.utils.All_Forall]
b:1553 [in MetaCoq.Translations.MiniHoTT_paths]
B:1554 [in MetaCoq.Translations.MiniHoTT]
b:1554 [in MetaCoq.Translations.MiniHoTT_paths]
b:1555 [in MetaCoq.SafeChecker.PCUICSafeReduce]
B:1561 [in MetaCoq.Template.utils.All_Forall]
B:1561 [in MetaCoq.Translations.MiniHoTT]
B:1562 [in MetaCoq.Translations.MiniHoTT_paths]
B:1568 [in MetaCoq.Translations.MiniHoTT]
B:1569 [in MetaCoq.Translations.MiniHoTT_paths]
B:157 [in MetaCoq.Erasure.EArities]
B:157 [in MetaCoq.Template.Ast]
B:157 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
B:1575 [in MetaCoq.Translations.MiniHoTT]
B:1576 [in MetaCoq.Template.utils.All_Forall]
B:1576 [in MetaCoq.Translations.MiniHoTT_paths]
B:158 [in MetaCoq.PCUIC.PCUICCumulProp]
B:1582 [in MetaCoq.Translations.MiniHoTT]
B:1583 [in MetaCoq.Translations.MiniHoTT_paths]
B:1587 [in MetaCoq.Translations.MiniHoTT]
B:159 [in MetaCoq.Template.utils.MCList]
B:1590 [in MetaCoq.Translations.MiniHoTT_paths]
B:1591 [in MetaCoq.Translations.MiniHoTT]
B:1595 [in MetaCoq.Translations.MiniHoTT_paths]
B:1599 [in MetaCoq.Translations.MiniHoTT]
B:1599 [in MetaCoq.Translations.MiniHoTT_paths]
B:16 [in MetaCoq.Template.BasicAst]
B:16 [in MetaCoq.Template.utils.MCList]
B:16 [in MetaCoq.PCUIC.utils.PCUICUtils]
b:16 [in MetaCoq.Template.WfAst]
b:16 [in MetaCoq.Template.utils.bytestring]
b:16 [in MetaCoq.PCUIC.PCUICFirstorder]
b:16 [in MetaCoq.Template.utils.MCUtils]
b:16 [in MetaCoq.Erasure.EWcbvEvalInd]
b:16 [in MetaCoq.PCUIC.Syntax.PCUICReflect]
b:16 [in MetaCoq.Examples.demo]
b:16 [in MetaCoq.PCUIC.PCUICGuardCondition]
B:160 [in MetaCoq.PCUIC.PCUICTyping]
B:160 [in MetaCoq.Translations.MiniHoTT_paths]
B:1600 [in MetaCoq.Template.utils.All_Forall]
B:1604 [in MetaCoq.Translations.MiniHoTT]
B:1607 [in MetaCoq.Template.utils.All_Forall]
B:1607 [in MetaCoq.Translations.MiniHoTT_paths]
B:161 [in MetaCoq.Erasure.EDeps]
b:161 [in MetaCoq.PCUIC.Syntax.PCUICCases]
b:161 [in MetaCoq.PCUIC.PCUICConversion]
B:1612 [in MetaCoq.Translations.MiniHoTT_paths]
b:1613 [in MetaCoq.SafeChecker.PCUICSafeReduce]
B:1617 [in MetaCoq.Translations.MiniHoTT]
B:1618 [in MetaCoq.Template.utils.All_Forall]
B:1624 [in MetaCoq.Translations.MiniHoTT]
B:1625 [in MetaCoq.Translations.MiniHoTT_paths]
B:1627 [in MetaCoq.Template.utils.All_Forall]
b:163 [in MetaCoq.PCUIC.Syntax.PCUICCases]
b:163 [in MetaCoq.PCUIC.PCUICReduction]
B:1630 [in MetaCoq.Translations.MiniHoTT]
B:1632 [in MetaCoq.Translations.MiniHoTT_paths]
B:1635 [in MetaCoq.Template.utils.All_Forall]
B:1638 [in MetaCoq.Translations.MiniHoTT_paths]
B:164 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
B:164 [in MetaCoq.Template.utils.All_Forall]
B:164 [in MetaCoq.Template.utils.MCList]
B:164 [in MetaCoq.PCUIC.PCUICCumulProp]
B:164 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
B:164 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
B:1643 [in MetaCoq.Template.utils.All_Forall]
B:1643 [in MetaCoq.Translations.MiniHoTT]
B:165 [in MetaCoq.Template.Ast]
B:1650 [in MetaCoq.Translations.MiniHoTT]
B:1651 [in MetaCoq.Template.utils.All_Forall]
B:1651 [in MetaCoq.Translations.MiniHoTT_paths]
B:1655 [in MetaCoq.Translations.MiniHoTT]
B:1658 [in MetaCoq.Translations.MiniHoTT_paths]
B:1659 [in MetaCoq.Template.utils.All_Forall]
b:166 [in MetaCoq.PCUIC.PCUICConversion]
B:1663 [in MetaCoq.Translations.MiniHoTT_paths]
B:1667 [in MetaCoq.Template.utils.All_Forall]
B:167 [in MetaCoq.Translations.times_bool_fun]
b:167 [in MetaCoq.PCUIC.Syntax.PCUICCases]
B:167 [in MetaCoq.PCUIC.PCUICTyping]
b:167 [in MetaCoq.PCUIC.PCUICReduction]
B:1675 [in MetaCoq.Template.utils.All_Forall]
B:1675 [in MetaCoq.Translations.MiniHoTT]
B:1683 [in MetaCoq.Template.utils.All_Forall]
B:1683 [in MetaCoq.Translations.MiniHoTT_paths]
B:1684 [in MetaCoq.Translations.MiniHoTT]
B:1688 [in MetaCoq.Template.utils.All_Forall]
B:1692 [in MetaCoq.Translations.MiniHoTT_paths]
B:1693 [in MetaCoq.Translations.MiniHoTT]
b:17 [in MetaCoq.Template.BasicAst]
B:17 [in MetaCoq.PCUIC.Bidirectional.BDUnique]
b:17 [in MetaCoq.PCUIC.Syntax.PCUICInstDef]
B:170 [in MetaCoq.PCUIC.PCUICCumulProp]
B:1701 [in MetaCoq.Translations.MiniHoTT_paths]
B:1702 [in MetaCoq.Template.utils.All_Forall]
B:1703 [in MetaCoq.Translations.MiniHoTT]
B:1711 [in MetaCoq.Translations.MiniHoTT_paths]
B:1715 [in MetaCoq.Template.utils.All_Forall]
b:172 [in MetaCoq.SafeChecker.PCUICSafeConversion]
B:1723 [in MetaCoq.Template.utils.All_Forall]
B:1728 [in MetaCoq.Translations.MiniHoTT]
B:173 [in MetaCoq.Template.utils.MCList]
B:1735 [in MetaCoq.Template.utils.All_Forall]
B:1736 [in MetaCoq.Translations.MiniHoTT_paths]
B:1737 [in MetaCoq.Translations.MiniHoTT]
B:174 [in MetaCoq.Erasure.EArities]
B:1741 [in MetaCoq.Template.utils.All_Forall]
b:1745 [in MetaCoq.Template.utils.All_Forall]
B:1745 [in MetaCoq.Translations.MiniHoTT_paths]
B:1746 [in MetaCoq.Translations.MiniHoTT]
B:175 [in MetaCoq.Translations.MiniHoTT]
B:1751 [in MetaCoq.Template.utils.All_Forall]
B:1754 [in MetaCoq.Translations.MiniHoTT_paths]
B:1755 [in MetaCoq.Translations.MiniHoTT]
B:1759 [in MetaCoq.Template.utils.All_Forall]
B:176 [in MetaCoq.PCUIC.PCUICCumulProp]
B:1763 [in MetaCoq.Translations.MiniHoTT_paths]
B:1765 [in MetaCoq.Translations.MiniHoTT]
B:1767 [in MetaCoq.Template.utils.All_Forall]
b:177 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
B:1773 [in MetaCoq.Translations.MiniHoTT_paths]
B:1774 [in MetaCoq.Translations.MiniHoTT]
B:1775 [in MetaCoq.Template.utils.All_Forall]
B:1782 [in MetaCoq.Template.utils.All_Forall]
B:1782 [in MetaCoq.Translations.MiniHoTT_paths]
B:1788 [in MetaCoq.Template.utils.All_Forall]
B:179 [in MetaCoq.Erasure.EArities]
B:1793 [in MetaCoq.Translations.MiniHoTT]
B:1799 [in MetaCoq.Translations.MiniHoTT]
B:18 [in MetaCoq.Template.utils.ReflectEq]
B:18 [in MetaCoq.PCUIC.PCUICPrincipality]
B:18 [in MetaCoq.PCUIC.Syntax.PCUICReflect]
B:18 [in MetaCoq.Template.utils.MCProd]
B:1801 [in MetaCoq.Template.utils.All_Forall]
B:1801 [in MetaCoq.Translations.MiniHoTT_paths]
B:1804 [in MetaCoq.Translations.MiniHoTT]
B:1807 [in MetaCoq.Translations.MiniHoTT_paths]
B:1809 [in MetaCoq.Template.utils.All_Forall]
B:181 [in MetaCoq.Template.utils.MCList]
b:181 [in MetaCoq.PCUIC.PCUICEtaExpand]
b:181 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
B:1812 [in MetaCoq.Translations.MiniHoTT_paths]
B:183 [in MetaCoq.Template.utils.All_Forall]
b:183 [in MetaCoq.PCUIC.PCUICWcbvEval]
B:183 [in MetaCoq.PCUIC.PCUICNormal]
B:183 [in MetaCoq.Translations.MiniHoTT_paths]
B:1839 [in MetaCoq.Template.utils.All_Forall]
b:185 [in MetaCoq.PCUIC.PCUICWcbvEval]
B:185 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
b:186 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
B:187 [in MetaCoq.Template.utils.MCList]
b:187 [in MetaCoq.PCUIC.PCUICConversion]
B:1873 [in MetaCoq.Template.utils.All_Forall]
B:188 [in MetaCoq.Translations.times_bool_fun]
b:189 [in MetaCoq.PCUIC.PCUICWcbvEval]
B:19 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
B:19 [in MetaCoq.Template.utils.MCList]
b:19 [in MetaCoq.Template.WfAst]
b:19 [in MetaCoq.Template.utils.bytestring]
B:19 [in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
b:19 [in MetaCoq.SafeChecker.PCUICWfReduction]
B:190 [in MetaCoq.Template.utils.All_Forall]
b:190 [in MetaCoq.PCUIC.PCUICEtaExpand]
b:190 [in MetaCoq.PCUIC.PCUICNormal]
b:191 [in MetaCoq.PCUIC.PCUICInductiveInversion]
b:191 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
B:192 [in MetaCoq.Template.utils.MCList]
B:1935 [in MetaCoq.Template.utils.All_Forall]
B:194 [in MetaCoq.PCUIC.PCUICSafeLemmata]
B:194 [in MetaCoq.SafeChecker.PCUICSafeConversion]
B:1947 [in MetaCoq.Template.utils.All_Forall]
B:1955 [in MetaCoq.Template.utils.All_Forall]
B:196 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
B:1968 [in MetaCoq.Template.utils.All_Forall]
B:197 [in MetaCoq.Template.utils.All_Forall]
B:197 [in MetaCoq.Template.utils.MCList]
B:1978 [in MetaCoq.Template.utils.All_Forall]
B:1987 [in MetaCoq.Template.utils.All_Forall]
B:1996 [in MetaCoq.Template.utils.All_Forall]
B:2 [in MetaCoq.Translations.times_bool_fun]
B:2 [in MetaCoq.Template.utils.MCList]
B:2 [in MetaCoq.PCUIC.utils.PCUICUtils]
b:2 [in MetaCoq.Template.utils.bytestring]
B:2 [in MetaCoq.PCUIC.PCUICInductives]
B:2 [in MetaCoq.Translations.sigma]
B:2 [in MetaCoq.Template.utils.MCProd]
B:2 [in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
B:2 [in MetaCoq.Template.Transform]
b:2 [in MetaCoq.PCUIC.PCUICGuardCondition]
b:20 [in MetaCoq.Template.BasicAst]
B:20 [in MetaCoq.Translations.translation_utils]
B:20 [in MetaCoq.PCUIC.Syntax.PCUICViews]
b:20 [in MetaCoq.Translations.sigma]
b:20 [in MetaCoq.Template.utils.ReflectEq]
B:20 [in MetaCoq.SafeChecker.PCUICWfReduction]
b:20 [in MetaCoq.SafeChecker.PCUICSafeChecker]
b:20 [in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
b:20 [in MetaCoq.Translations.param_generous_packed]
B:2004 [in MetaCoq.Template.utils.All_Forall]
B:2009 [in MetaCoq.Template.utils.All_Forall]
B:201 [in MetaCoq.Translations.times_bool_fun]
b:201 [in MetaCoq.Erasure.EConstructorsAsBlocks]
b:201 [in MetaCoq.PCUIC.PCUICNormal]
B:2018 [in MetaCoq.Template.utils.All_Forall]
b:202 [in MetaCoq.PCUIC.PCUICAst]
B:2024 [in MetaCoq.Template.utils.All_Forall]
B:2030 [in MetaCoq.Template.utils.All_Forall]
B:2037 [in MetaCoq.Template.utils.All_Forall]
b:2044 [in MetaCoq.SafeChecker.PCUICSafeConversion]
B:2046 [in MetaCoq.Template.utils.All_Forall]
B:2052 [in MetaCoq.SafeChecker.PCUICSafeConversion]
B:206 [in MetaCoq.Translations.times_bool_fun]
B:206 [in MetaCoq.Template.utils.All_Forall]
b:206 [in MetaCoq.PCUIC.PCUICNormal]
B:2066 [in MetaCoq.Template.utils.All_Forall]
B:207 [in MetaCoq.Template.utils.MCList]
b:208 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
B:208 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
B:2087 [in MetaCoq.Template.utils.All_Forall]
B:209 [in MetaCoq.Translations.times_bool_fun]
B:2094 [in MetaCoq.Template.utils.All_Forall]
b:21 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
B:210 [in MetaCoq.PCUIC.PCUICProgress]
B:210 [in MetaCoq.Translations.times_bool_fun]
B:2102 [in MetaCoq.Template.utils.All_Forall]
B:2109 [in MetaCoq.Template.utils.All_Forall]
b:211 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
B:212 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
b:2128 [in MetaCoq.Template.utils.All_Forall]
b:2129 [in MetaCoq.Template.utils.All_Forall]
B:213 [in MetaCoq.Template.utils.All_Forall]
B:213 [in MetaCoq.Template.utils.MCList]
B:213 [in MetaCoq.PCUIC.PCUICCumulProp]
B:2132 [in MetaCoq.Template.utils.All_Forall]
B:2144 [in MetaCoq.Template.utils.All_Forall]
B:215 [in MetaCoq.PCUIC.PCUICNormal]
B:2156 [in MetaCoq.Template.utils.All_Forall]
b:216 [in MetaCoq.PCUIC.PCUICNormal]
b:216 [in MetaCoq.SafeChecker.PCUICSafeReduce]
B:216 [in MetaCoq.Template.TypingWf]
B:2162 [in MetaCoq.Translations.MiniHoTT]
B:2165 [in MetaCoq.Template.utils.All_Forall]
B:217 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
B:217 [in MetaCoq.SafeChecker.PCUICSafeReduce]
B:2170 [in MetaCoq.Translations.MiniHoTT]
B:2170 [in MetaCoq.Translations.MiniHoTT_paths]
B:2173 [in MetaCoq.Template.utils.All_Forall]
B:2176 [in MetaCoq.Translations.MiniHoTT]
B:2178 [in MetaCoq.Translations.MiniHoTT_paths]
B:218 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
B:2182 [in MetaCoq.Template.utils.All_Forall]
B:2184 [in MetaCoq.Translations.MiniHoTT]
B:2184 [in MetaCoq.Translations.MiniHoTT_paths]
B:219 [in MetaCoq.Template.utils.MCList]
B:2190 [in MetaCoq.Translations.MiniHoTT]
B:2192 [in MetaCoq.Translations.MiniHoTT_paths]
B:2198 [in MetaCoq.Translations.MiniHoTT]
B:2198 [in MetaCoq.Translations.MiniHoTT_paths]
b:22 [in MetaCoq.Template.WfAst]
B:22 [in MetaCoq.PCUIC.PCUICNormal]
b:22 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
b:22 [in MetaCoq.Erasure.EReflect]
B:2204 [in MetaCoq.Translations.MiniHoTT]
B:2206 [in MetaCoq.Translations.MiniHoTT_paths]
B:221 [in MetaCoq.PCUIC.PCUICSR]
B:2212 [in MetaCoq.Translations.MiniHoTT]
B:2212 [in MetaCoq.Translations.MiniHoTT_paths]
B:2220 [in MetaCoq.Translations.MiniHoTT_paths]
B:2223 [in MetaCoq.Template.utils.All_Forall]
B:2238 [in MetaCoq.Template.utils.All_Forall]
B:224 [in MetaCoq.Template.utils.All_Forall]
B:2241 [in MetaCoq.Translations.MiniHoTT]
B:2249 [in MetaCoq.Translations.MiniHoTT_paths]
b:225 [in MetaCoq.PCUIC.PCUICNormal]
b:225 [in MetaCoq.PCUIC.PCUICReduction]
B:2251 [in MetaCoq.Translations.MiniHoTT]
B:2259 [in MetaCoq.Translations.MiniHoTT_paths]
B:226 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
B:2261 [in MetaCoq.Translations.MiniHoTT]
B:2266 [in MetaCoq.Template.utils.All_Forall]
B:2269 [in MetaCoq.Translations.MiniHoTT_paths]
B:2271 [in MetaCoq.Translations.MiniHoTT]
B:2279 [in MetaCoq.Translations.MiniHoTT_paths]
b:228 [in MetaCoq.Template.TypingWf]
B:2281 [in MetaCoq.Translations.MiniHoTT]
B:2289 [in MetaCoq.Translations.MiniHoTT_paths]
b:23 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
b:23 [in MetaCoq.SafeChecker.PCUICWfReduction]
b:23 [in MetaCoq.PCUIC.Syntax.PCUICNamelessDef]
b:23 [in MetaCoq.PCUIC.PCUICGuardCondition]
b:231 [in MetaCoq.PCUIC.PCUICReduction]
B:234 [in MetaCoq.PCUIC.PCUICSR]
B:235 [in MetaCoq.Template.utils.All_Forall]
B:235 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
B:235 [in MetaCoq.SafeChecker.PCUICErrors]
B:2360 [in MetaCoq.SafeChecker.PCUICSafeConversion]
b:2366 [in MetaCoq.SafeChecker.PCUICSafeConversion]
b:237 [in MetaCoq.PCUIC.PCUICReduction]
B:2379 [in MetaCoq.Translations.MiniHoTT]
b:238 [in MetaCoq.Erasure.EWcbvEval]
B:2387 [in MetaCoq.Translations.MiniHoTT_paths]
b:239 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
B:2391 [in MetaCoq.Translations.MiniHoTT]
B:2399 [in MetaCoq.Translations.MiniHoTT_paths]
B:24 [in MetaCoq.Template.utils.All_Forall]
B:24 [in MetaCoq.SafeChecker.PCUICWfReduction]
B:24 [in MetaCoq.PCUIC.PCUICAst]
B:24 [in MetaCoq.Template.monad_utils]
B:2405 [in MetaCoq.Translations.MiniHoTT]
b:241 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
B:2413 [in MetaCoq.Translations.MiniHoTT]
B:2413 [in MetaCoq.Translations.MiniHoTT_paths]
B:242 [in MetaCoq.PCUIC.PCUICSubstitution]
B:2421 [in MetaCoq.Translations.MiniHoTT_paths]
B:2425 [in MetaCoq.Translations.MiniHoTT]
b:243 [in MetaCoq.PCUIC.PCUICProgress]
b:243 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
b:243 [in MetaCoq.SafeChecker.PCUICSafeConversion]
b:2431 [in MetaCoq.Translations.MiniHoTT]
B:2433 [in MetaCoq.Translations.MiniHoTT_paths]
b:2434 [in MetaCoq.Translations.MiniHoTT]
b:2435 [in MetaCoq.Translations.MiniHoTT]
B:2438 [in MetaCoq.Translations.MiniHoTT]
b:2439 [in MetaCoq.Translations.MiniHoTT_paths]
b:2442 [in MetaCoq.Translations.MiniHoTT_paths]
b:2443 [in MetaCoq.Translations.MiniHoTT_paths]
B:2446 [in MetaCoq.Translations.MiniHoTT_paths]
b:245 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
B:2452 [in MetaCoq.Translations.MiniHoTT]
B:246 [in MetaCoq.Template.utils.All_Forall]
B:2460 [in MetaCoq.Translations.MiniHoTT_paths]
B:2467 [in MetaCoq.Translations.MiniHoTT]
b:247 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
B:247 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
b:2470 [in MetaCoq.Translations.MiniHoTT]
b:2473 [in MetaCoq.Translations.MiniHoTT]
b:2475 [in MetaCoq.Translations.MiniHoTT]
B:2475 [in MetaCoq.Translations.MiniHoTT_paths]
B:2477 [in MetaCoq.Template.utils.All_Forall]
B:2478 [in MetaCoq.Translations.MiniHoTT]
b:2478 [in MetaCoq.Translations.MiniHoTT_paths]
b:2481 [in MetaCoq.Translations.MiniHoTT]
b:2481 [in MetaCoq.Translations.MiniHoTT_paths]
b:2483 [in MetaCoq.Translations.MiniHoTT_paths]
B:2486 [in MetaCoq.Translations.MiniHoTT_paths]
b:2487 [in MetaCoq.Translations.MiniHoTT]
b:2489 [in MetaCoq.Translations.MiniHoTT_paths]
b:249 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
b:249 [in MetaCoq.Template.Typing]
B:249 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
B:2490 [in MetaCoq.Translations.MiniHoTT]
B:2493 [in MetaCoq.Template.utils.All_Forall]
b:2495 [in MetaCoq.Translations.MiniHoTT]
b:2495 [in MetaCoq.Translations.MiniHoTT_paths]
B:2498 [in MetaCoq.Translations.MiniHoTT_paths]
B:25 [in MetaCoq.PCUIC.PCUICArities]
B:25 [in MetaCoq.PCUIC.PCUICNormal]
B:25 [in MetaCoq.Translations.times_bool_fun2]
b:25 [in MetaCoq.Erasure.EWcbvEval]
B:250 [in MetaCoq.PCUIC.PCUICElimination]
b:2503 [in MetaCoq.Translations.MiniHoTT_paths]
B:2505 [in MetaCoq.Template.utils.All_Forall]
B:2506 [in MetaCoq.Translations.MiniHoTT]
b:251 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
b:2510 [in MetaCoq.Translations.MiniHoTT]
B:2514 [in MetaCoq.Translations.MiniHoTT_paths]
b:2518 [in MetaCoq.Translations.MiniHoTT_paths]
B:2519 [in MetaCoq.Translations.MiniHoTT]
b:252 [in MetaCoq.PCUIC.PCUICProgress]
B:252 [in MetaCoq.Template.utils.MCList]
b:252 [in MetaCoq.PCUIC.PCUICConversion]
B:2523 [in MetaCoq.Template.utils.All_Forall]
b:2523 [in MetaCoq.Translations.MiniHoTT]
b:2525 [in MetaCoq.Translations.MiniHoTT]
B:2527 [in MetaCoq.Translations.MiniHoTT_paths]
b:2528 [in MetaCoq.Translations.MiniHoTT]
b:253 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
B:2531 [in MetaCoq.Translations.MiniHoTT]
b:2531 [in MetaCoq.Translations.MiniHoTT_paths]
b:2533 [in MetaCoq.Translations.MiniHoTT_paths]
b:2534 [in MetaCoq.Translations.MiniHoTT]
b:2536 [in MetaCoq.Translations.MiniHoTT_paths]
b:2537 [in MetaCoq.Translations.MiniHoTT]
B:2539 [in MetaCoq.Template.utils.All_Forall]
B:2539 [in MetaCoq.Translations.MiniHoTT_paths]
B:254 [in MetaCoq.Template.utils.All_Forall]
b:254 [in MetaCoq.Template.Typing]
b:254 [in MetaCoq.Template.Checker]
b:2542 [in MetaCoq.Translations.MiniHoTT_paths]
b:2545 [in MetaCoq.Translations.MiniHoTT_paths]
B:2546 [in MetaCoq.Translations.MiniHoTT]
B:2550 [in MetaCoq.Template.utils.All_Forall]
b:2550 [in MetaCoq.Translations.MiniHoTT]
b:2551 [in MetaCoq.Translations.MiniHoTT]
B:2553 [in MetaCoq.Translations.MiniHoTT]
B:2554 [in MetaCoq.Translations.MiniHoTT_paths]
b:2557 [in MetaCoq.Translations.MiniHoTT]
b:2558 [in MetaCoq.Translations.MiniHoTT_paths]
b:2559 [in MetaCoq.Translations.MiniHoTT_paths]
B:256 [in MetaCoq.PCUIC.PCUICElimination]
B:2560 [in MetaCoq.Translations.MiniHoTT]
B:2561 [in MetaCoq.Translations.MiniHoTT_paths]
B:2564 [in MetaCoq.Template.utils.All_Forall]
b:2565 [in MetaCoq.Translations.MiniHoTT_paths]
b:2566 [in MetaCoq.Translations.MiniHoTT]
B:2568 [in MetaCoq.Translations.MiniHoTT_paths]
b:2571 [in MetaCoq.Translations.MiniHoTT]
b:2574 [in MetaCoq.Translations.MiniHoTT_paths]
b:2576 [in MetaCoq.Translations.MiniHoTT]
b:2579 [in MetaCoq.Translations.MiniHoTT_paths]
B:258 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
B:2580 [in MetaCoq.Template.utils.All_Forall]
B:2581 [in MetaCoq.Translations.MiniHoTT]
b:2584 [in MetaCoq.Translations.MiniHoTT_paths]
b:2589 [in MetaCoq.Translations.MiniHoTT]
B:2589 [in MetaCoq.Translations.MiniHoTT_paths]
B:259 [in MetaCoq.Template.utils.MCList]
B:2591 [in MetaCoq.Template.utils.All_Forall]
b:2597 [in MetaCoq.Translations.MiniHoTT_paths]
B:26 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
B:26 [in MetaCoq.Template.utils.MCList]
B:26 [in MetaCoq.PCUIC.Syntax.PCUICReflect]
B:26 [in MetaCoq.Examples.demo]
B:26 [in MetaCoq.Template.utils.MCProd]
b:260 [in MetaCoq.PCUIC.PCUICProgress]
B:260 [in MetaCoq.SafeChecker.PCUICErrors]
B:2602 [in MetaCoq.Template.utils.All_Forall]
B:261 [in MetaCoq.Template.TypingWf]
B:2611 [in MetaCoq.Translations.MiniHoTT]
b:2614 [in MetaCoq.Translations.MiniHoTT]
b:2615 [in MetaCoq.Translations.MiniHoTT]
b:2618 [in MetaCoq.Translations.MiniHoTT]
B:2619 [in MetaCoq.Translations.MiniHoTT_paths]
B:262 [in MetaCoq.Template.utils.All_Forall]
B:2621 [in MetaCoq.Translations.MiniHoTT]
b:2622 [in MetaCoq.Translations.MiniHoTT_paths]
b:2623 [in MetaCoq.Translations.MiniHoTT_paths]
b:2626 [in MetaCoq.Translations.MiniHoTT_paths]
B:2628 [in MetaCoq.Translations.MiniHoTT]
B:2629 [in MetaCoq.Translations.MiniHoTT_paths]
b:2631 [in MetaCoq.Translations.MiniHoTT]
b:2632 [in MetaCoq.Translations.MiniHoTT]
B:2636 [in MetaCoq.Translations.MiniHoTT_paths]
b:2639 [in MetaCoq.Translations.MiniHoTT_paths]
B:264 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
B:264 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
b:2640 [in MetaCoq.Translations.MiniHoTT_paths]
b:2642 [in MetaCoq.Translations.MiniHoTT]
B:2644 [in MetaCoq.Translations.MiniHoTT]
b:2649 [in MetaCoq.Translations.MiniHoTT]
b:265 [in MetaCoq.Template.Checker]
B:265 [in MetaCoq.PCUIC.PCUICConversion]
b:2650 [in MetaCoq.Translations.MiniHoTT_paths]
B:2652 [in MetaCoq.Translations.MiniHoTT]
B:2652 [in MetaCoq.Translations.MiniHoTT_paths]
b:2656 [in MetaCoq.Translations.MiniHoTT]
b:2657 [in MetaCoq.Translations.MiniHoTT_paths]
B:2660 [in MetaCoq.Translations.MiniHoTT_paths]
b:2664 [in MetaCoq.Translations.MiniHoTT_paths]
B:267 [in MetaCoq.Template.utils.MCList]
B:268 [in MetaCoq.Template.common.uGraph]
b:27 [in MetaCoq.Erasure.EInlineProjections]
b:27 [in MetaCoq.SafeChecker.PCUICWfReduction]
B:271 [in MetaCoq.PCUIC.PCUICProgress]
b:271 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
B:272 [in MetaCoq.Template.utils.All_Forall]
B:272 [in MetaCoq.PCUIC.PCUICConversion]
B:274 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
b:274 [in MetaCoq.Template.EnvironmentTyping]
B:275 [in MetaCoq.Template.utils.MCList]
B:275 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
B:277 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
b:28 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
B:28 [in MetaCoq.Template.utils.MCReflect]
B:28 [in MetaCoq.PCUIC.PCUICProgress]
b:28 [in MetaCoq.Erasure.Extract]
b:28 [in MetaCoq.PCUIC.PCUICCumulProp]
B:28 [in MetaCoq.SafeChecker.PCUICWfReduction]
B:28 [in MetaCoq.Template.utils.MCOption]
B:28 [in MetaCoq.Translations.times_bool_fun2]
b:280 [in MetaCoq.Template.EtaExpand]
B:280 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
B:281 [in MetaCoq.PCUIC.PCUICAst]
b:281 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
B:282 [in MetaCoq.Template.utils.All_Forall]
b:283 [in MetaCoq.SafeChecker.PCUICErrors]
B:2838 [in MetaCoq.Translations.MiniHoTT]
B:284 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
b:2846 [in MetaCoq.Translations.MiniHoTT]
B:2846 [in MetaCoq.Translations.MiniHoTT_paths]
B:2848 [in MetaCoq.Translations.MiniHoTT]
B:285 [in MetaCoq.PCUIC.PCUICConversion]
b:2854 [in MetaCoq.Translations.MiniHoTT_paths]
B:2856 [in MetaCoq.Translations.MiniHoTT_paths]
B:286 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
B:286 [in MetaCoq.Template.utils.MCList]
B:2877 [in MetaCoq.Translations.MiniHoTT]
B:2885 [in MetaCoq.Translations.MiniHoTT_paths]
B:2888 [in MetaCoq.Translations.MiniHoTT]
B:2896 [in MetaCoq.Translations.MiniHoTT_paths]
B:2899 [in MetaCoq.Translations.MiniHoTT]
B:29 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
B:29 [in MetaCoq.PCUIC.Typing.PCUICInstTyp]
b:29 [in MetaCoq.Examples.tauto]
b:29 [in MetaCoq.Erasure.EOptimizePropDiscr]
b:29 [in MetaCoq.PCUIC.PCUICGuardCondition]
B:290 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
b:290 [in MetaCoq.SafeChecker.PCUICErrors]
B:2907 [in MetaCoq.Translations.MiniHoTT_paths]
B:291 [in MetaCoq.PCUIC.PCUICConversion]
B:2914 [in MetaCoq.Translations.MiniHoTT]
B:292 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
B:2922 [in MetaCoq.Translations.MiniHoTT]
B:2922 [in MetaCoq.Translations.MiniHoTT_paths]
B:2930 [in MetaCoq.Translations.MiniHoTT_paths]
B:2934 [in MetaCoq.Translations.MiniHoTT]
B:294 [in MetaCoq.Template.utils.MCList]
B:294 [in MetaCoq.PCUIC.PCUICSubstitution]
B:2942 [in MetaCoq.Translations.MiniHoTT_paths]
B:2949 [in MetaCoq.Translations.MiniHoTT]
B:2957 [in MetaCoq.Translations.MiniHoTT_paths]
B:2959 [in MetaCoq.Translations.MiniHoTT]
B:2967 [in MetaCoq.Translations.MiniHoTT_paths]
B:298 [in MetaCoq.Template.utils.MCList]
b:3 [in MetaCoq.Template.utils.ByteCompareSpec]
B:3003 [in MetaCoq.Translations.MiniHoTT]
b:304 [in MetaCoq.PCUIC.PCUICWcbvEval]
B:304 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
B:306 [in MetaCoq.Template.utils.MCList]
B:308 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
b:308 [in MetaCoq.Template.WcbvEval]
b:309 [in MetaCoq.Erasure.EArities]
b:31 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
b:31 [in MetaCoq.Template.utils.MCOption]
B:31 [in MetaCoq.Template.utils.MCProd]
b:310 [in MetaCoq.PCUIC.PCUICWcbvEval]
B:311 [in MetaCoq.PCUIC.PCUICElimination]
B:311 [in MetaCoq.PCUIC.PCUICSR]
B:312 [in MetaCoq.SafeChecker.PCUICSafeChecker]
B:313 [in MetaCoq.Template.utils.MCList]
b:313 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
b:314 [in MetaCoq.Template.EnvironmentTyping]
B:316 [in MetaCoq.PCUIC.PCUICElimination]
b:316 [in MetaCoq.Template.Typing]
B:318 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
b:319 [in MetaCoq.Erasure.EArities]
b:32 [in MetaCoq.PCUIC.PCUICFirstorder]
B:32 [in MetaCoq.Erasure.ErasureFunction]
B:32 [in MetaCoq.Examples.demo]
B:320 [in MetaCoq.Template.utils.MCList]
B:321 [in MetaCoq.PCUIC.PCUICElimination]
B:321 [in MetaCoq.PCUIC.PCUICSR]
b:322 [in MetaCoq.Template.Typing]
b:322 [in MetaCoq.Template.Environment]
b:323 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
b:324 [in MetaCoq.Template.common.uGraph]
B:326 [in MetaCoq.PCUIC.PCUICElimination]
b:327 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
B:328 [in MetaCoq.Template.utils.MCList]
b:328 [in MetaCoq.Template.Typing]
B:330 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
b:331 [in MetaCoq.Erasure.EEtaExpandedFix]
B:331 [in MetaCoq.Template.utils.All_Forall]
b:331 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
B:332 [in MetaCoq.PCUIC.PCUICAst]
b:333 [in MetaCoq.PCUIC.PCUICConversion]
B:334 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
B:334 [in MetaCoq.Template.utils.MCList]
B:334 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
b:334 [in MetaCoq.Template.common.uGraph]
b:335 [in MetaCoq.Template.Environment]
b:336 [in MetaCoq.Erasure.EEtaExpandedFix]
B:338 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
b:339 [in MetaCoq.Erasure.EEtaExpandedFix]
B:339 [in MetaCoq.Template.utils.All_Forall]
B:34 [in MetaCoq.Template.utils.All_Forall]
b:34 [in MetaCoq.PCUIC.Syntax.PCUICViews]
B:34 [in MetaCoq.PCUIC.PCUICParallelReduction]
b:34 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
B:34 [in MetaCoq.Template.utils.MCOption]
B:34 [in MetaCoq.Erasure.Prelim]
b:340 [in MetaCoq.PCUIC.PCUICConversion]
B:341 [in MetaCoq.Template.utils.MCList]
b:342 [in MetaCoq.Erasure.ERemoveParams]
b:342 [in MetaCoq.PCUIC.PCUICReduction]
b:343 [in MetaCoq.PCUIC.PCUICSR]
B:347 [in MetaCoq.Template.utils.All_Forall]
b:347 [in MetaCoq.PCUIC.PCUICSR]
b:347 [in MetaCoq.Erasure.ERemoveParams]
b:348 [in MetaCoq.Template.common.uGraph]
B:348 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
B:349 [in MetaCoq.Template.utils.MCList]
b:35 [in MetaCoq.Erasure.EOptimizePropDiscr]
b:353 [in MetaCoq.Erasure.ERemoveParams]
B:354 [in MetaCoq.Template.utils.All_Forall]
b:355 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
b:355 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
B:355 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
B:355 [in MetaCoq.Template.utils.MCList]
B:36 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
b:36 [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
b:36 [in MetaCoq.Template.LiftSubst]
b:36 [in MetaCoq.PCUIC.PCUICGuardCondition]
B:360 [in MetaCoq.PCUIC.PCUICProgress]
B:360 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
b:361 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
B:362 [in MetaCoq.Template.utils.MCList]
b:362 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
b:363 [in MetaCoq.PCUIC.PCUICAst]
b:365 [in MetaCoq.Template.common.uGraph]
b:366 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
b:366 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
B:367 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
B:368 [in MetaCoq.Template.utils.MCList]
B:37 [in MetaCoq.PCUIC.Typing.PCUICInstTyp]
b:37 [in MetaCoq.Translations.times_bool_fun]
B:37 [in MetaCoq.Template.utils.MCList]
b:37 [in MetaCoq.Erasure.ECSubst]
b:37 [in MetaCoq.Template.LiftSubst]
b:37 [in MetaCoq.Erasure.Prelim]
b:370 [in MetaCoq.PCUIC.PCUICAst]
b:371 [in MetaCoq.PCUIC.PCUICSpine]
B:373 [in MetaCoq.Template.utils.All_Forall]
B:373 [in MetaCoq.Template.utils.MCList]
B:373 [in MetaCoq.SafeChecker.PCUICSafeChecker]
b:374 [in MetaCoq.Erasure.EWcbvEval]
B:375 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
b:376 [in MetaCoq.PCUIC.PCUICAst]
B:377 [in MetaCoq.Template.utils.MCList]
B:379 [in MetaCoq.Template.EtaExpand]
b:38 [in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
B:38 [in MetaCoq.PCUIC.utils.PCUICUtils]
B:38 [in MetaCoq.PCUIC.PCUICConfluence]
B:38 [in MetaCoq.PCUIC.Syntax.PCUICReflect]
b:38 [in MetaCoq.PCUIC.Conversion.PCUICClosedConv]
b:38 [in MetaCoq.Erasure.EOptimizePropDiscr]
b:381 [in MetaCoq.PCUIC.PCUICAst]
B:383 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
B:383 [in MetaCoq.Template.utils.MCList]
B:383 [in MetaCoq.SafeChecker.PCUICSafeChecker]
B:385 [in MetaCoq.Template.utils.All_Forall]
b:386 [in MetaCoq.PCUIC.PCUICAst]
b:39 [in MetaCoq.Examples.demo]
B:39 [in MetaCoq.Template.utils.MCProd]
b:390 [in MetaCoq.PCUIC.PCUICWcbvEval]
B:390 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
B:390 [in MetaCoq.PCUIC.PCUICAst]
B:390 [in MetaCoq.Template.Checker]
B:392 [in MetaCoq.Template.utils.MCList]
B:394 [in MetaCoq.Template.utils.All_Forall]
b:394 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
B:395 [in MetaCoq.PCUIC.PCUICNormal]
B:396 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
B:397 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
b:397 [in MetaCoq.PCUIC.PCUICInductiveInversion]
B:397 [in MetaCoq.PCUIC.PCUICAst]
B:398 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
b:399 [in MetaCoq.PCUIC.PCUICReduction]
B:4 [in MetaCoq.Template.utils.MCSquash]
b:4 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
B:4 [in MetaCoq.PCUIC.PCUICParallelReduction]
B:4 [in MetaCoq.Template.utils.MCUtils]
B:4 [in MetaCoq.Template.Transform]
b:40 [in MetaCoq.Template.EtaExpand]
B:40 [in MetaCoq.PCUIC.PCUICInversion]
B:40 [in MetaCoq.PCUIC.PCUICCanonicity]
b:40 [in MetaCoq.Erasure.Prelim]
B:400 [in MetaCoq.PCUIC.PCUICNormal]
b:401 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
B:402 [in MetaCoq.Template.utils.All_Forall]
B:403 [in MetaCoq.Template.utils.MCList]
b:404 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
b:404 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
B:404 [in MetaCoq.PCUIC.PCUICAst]
b:405 [in MetaCoq.Template.common.uGraph]
B:405 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
b:405 [in MetaCoq.PCUIC.PCUICSR]
B:406 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
b:41 [in MetaCoq.Template.common.uGraph]
b:41 [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
b:41 [in MetaCoq.Erasure.ECSubst]
b:410 [in MetaCoq.PCUIC.PCUICInductiveInversion]
B:410 [in MetaCoq.PCUIC.PCUICConversion]
B:411 [in MetaCoq.Template.utils.All_Forall]
B:411 [in MetaCoq.PCUIC.PCUICAst]
b:411 [in MetaCoq.PCUIC.PCUICSR]
B:413 [in MetaCoq.PCUIC.PCUICNormal]
B:415 [in MetaCoq.Template.utils.MCList]
b:417 [in MetaCoq.PCUIC.PCUICSR]
b:418 [in MetaCoq.Template.EnvironmentTyping]
b:42 [in MetaCoq.PCUIC.PCUICEtaExpand]
B:42 [in MetaCoq.PCUIC.Typing.PCUICContextConversionTyp]
B:42 [in MetaCoq.Erasure.ErasureFunction]
B:420 [in MetaCoq.PCUIC.PCUICConversion]
B:421 [in MetaCoq.Template.utils.All_Forall]
B:423 [in MetaCoq.PCUIC.PCUICInductiveInversion]
B:423 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
B:425 [in MetaCoq.PCUIC.PCUICConversion]
B:426 [in MetaCoq.Translations.MiniHoTT]
B:428 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
b:43 [in MetaCoq.PCUIC.PCUICNormal]
B:43 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
B:43 [in MetaCoq.Template.Checker]
B:43 [in MetaCoq.Template.monad_utils]
B:430 [in MetaCoq.Translations.MiniHoTT]
B:434 [in MetaCoq.Translations.MiniHoTT_paths]
B:435 [in MetaCoq.Template.utils.All_Forall]
B:435 [in MetaCoq.Template.utils.MCList]
b:435 [in MetaCoq.PCUIC.PCUICAst]
B:435 [in MetaCoq.Translations.MiniHoTT]
B:438 [in MetaCoq.Translations.MiniHoTT_paths]
b:44 [in MetaCoq.Translations.times_bool_fun]
b:44 [in MetaCoq.PCUIC.Syntax.PCUICViews]
b:44 [in MetaCoq.Erasure.ESpineView]
B:44 [in MetaCoq.Examples.tauto]
B:44 [in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
B:441 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
B:441 [in MetaCoq.Template.utils.MCList]
b:442 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
B:443 [in MetaCoq.Translations.MiniHoTT]
B:443 [in MetaCoq.Translations.MiniHoTT_paths]
B:447 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
b:448 [in MetaCoq.SafeChecker.PCUICSafeChecker]
b:449 [in MetaCoq.PCUIC.PCUICInductives]
B:45 [in MetaCoq.PCUIC.utils.PCUICUtils]
B:45 [in MetaCoq.Template.utils.MCProd]
b:45 [in MetaCoq.PCUIC.PCUICGuardCondition]
b:451 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
B:451 [in MetaCoq.Translations.MiniHoTT_paths]
B:453 [in MetaCoq.Translations.MiniHoTT]
b:456 [in MetaCoq.PCUIC.PCUICAst]
b:457 [in MetaCoq.PCUIC.PCUICAst]
b:458 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
B:459 [in MetaCoq.Template.utils.All_Forall]
B:459 [in MetaCoq.PCUIC.PCUICAst]
B:46 [in MetaCoq.Template.utils.MCList]
b:46 [in MetaCoq.Template.Reflect]
B:46 [in MetaCoq.PCUIC.Syntax.PCUICReflect]
B:46 [in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
B:46 [in MetaCoq.Template.LiftSubst]
B:461 [in MetaCoq.Translations.MiniHoTT_paths]
b:462 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
B:463 [in MetaCoq.Translations.MiniHoTT]
B:465 [in MetaCoq.Template.utils.All_Forall]
b:465 [in MetaCoq.PCUIC.PCUICInductives]
b:465 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
B:465 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
b:468 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
B:468 [in MetaCoq.PCUIC.PCUICAst]
b:469 [in MetaCoq.PCUIC.PCUICInductives]
B:469 [in MetaCoq.Translations.MiniHoTT]
B:47 [in MetaCoq.Template.Ast]
B:47 [in MetaCoq.PCUIC.PCUICInversion]
b:471 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
B:471 [in MetaCoq.Translations.MiniHoTT_paths]
b:472 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
b:474 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
B:476 [in MetaCoq.PCUIC.PCUICAst]
b:477 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
B:477 [in MetaCoq.Translations.MiniHoTT_paths]
B:479 [in MetaCoq.Translations.MiniHoTT]
B:48 [in MetaCoq.PCUIC.PCUICNormal]
B:48 [in MetaCoq.PCUIC.PCUICSR]
b:482 [in MetaCoq.Template.EnvironmentTyping]
B:482 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
b:483 [in MetaCoq.PCUIC.PCUICTyping]
B:484 [in MetaCoq.PCUIC.PCUICAst]
b:484 [in MetaCoq.PCUIC.PCUICSpine]
B:487 [in MetaCoq.Translations.MiniHoTT]
B:487 [in MetaCoq.Translations.MiniHoTT_paths]
B:489 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
b:49 [in MetaCoq.PCUIC.PCUICNormal]
b:49 [in MetaCoq.Template.utils.MCProd]
b:491 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
b:492 [in MetaCoq.PCUIC.PCUICInductives]
b:492 [in MetaCoq.PCUIC.PCUICTyping]
B:495 [in MetaCoq.Translations.MiniHoTT_paths]
b:496 [in MetaCoq.Template.EnvironmentTyping]
B:496 [in MetaCoq.Translations.MiniHoTT]
B:497 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
b:498 [in MetaCoq.SafeChecker.PCUICSafeChecker]
b:5 [in MetaCoq.Template.utils.MCReflect]
B:5 [in MetaCoq.Template.TemplateMonad.Core]
b:5 [in MetaCoq.Template.utils.bytestring]
b:5 [in MetaCoq.Template.utils.ReflectEq]
B:5 [in MetaCoq.PCUIC.TemplateToPCUIC]
B:5 [in MetaCoq.Template.TemplateMonad.Extractable]
B:50 [in MetaCoq.Template.Normal]
B:50 [in MetaCoq.PCUIC.PCUICParallelReduction]
B:50 [in MetaCoq.Translations.MiniHoTT]
B:50 [in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
B:500 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
b:500 [in MetaCoq.PCUIC.PCUICTyping]
B:502 [in MetaCoq.Translations.MiniHoTT]
B:503 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
B:504 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
B:504 [in MetaCoq.Translations.MiniHoTT_paths]
B:51 [in MetaCoq.Template.utils.MCOption]
b:51 [in MetaCoq.Translations.MiniHoTT]
b:51 [in MetaCoq.Template.utils.MCProd]
B:51 [in MetaCoq.Translations.times_bool_fun2]
B:51 [in MetaCoq.Template.TypingWf]
B:510 [in MetaCoq.Translations.MiniHoTT_paths]
b:512 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
B:512 [in MetaCoq.PCUIC.PCUICTyping]
b:513 [in MetaCoq.Template.Universes]
B:514 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
B:516 [in MetaCoq.Template.utils.All_Forall]
b:518 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
b:519 [in MetaCoq.PCUIC.PCUICSubstitution]
B:52 [in MetaCoq.Template.BasicAst]
B:52 [in MetaCoq.Translations.times_bool_fun]
B:52 [in MetaCoq.PCUIC.utils.PCUICUtils]
b:52 [in MetaCoq.Erasure.EWellformed]
b:524 [in MetaCoq.SafeChecker.PCUICSafeChecker]
B:525 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
B:525 [in MetaCoq.Examples.tauto]
B:525 [in MetaCoq.Translations.MiniHoTT]
B:528 [in MetaCoq.Examples.tauto]
B:53 [in MetaCoq.Template.utils.MCRelations]
B:53 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
b:53 [in MetaCoq.Template.Typing]
B:53 [in MetaCoq.Template.Normal]
B:53 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
b:53 [in MetaCoq.Template.WcbvEval]
b:53 [in MetaCoq.PCUIC.PCUICGuardCondition]
b:530 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
b:531 [in MetaCoq.SafeChecker.PCUICSafeChecker]
B:533 [in MetaCoq.Translations.MiniHoTT_paths]
B:535 [in MetaCoq.PCUIC.PCUICAst]
B:538 [in MetaCoq.Translations.MiniHoTT]
b:54 [in MetaCoq.PCUIC.PCUICWcbvEval]
b:54 [in MetaCoq.Template.TermEquality]
B:54 [in MetaCoq.PCUIC.PCUICConfluence]
B:54 [in MetaCoq.Template.utils.MCProd]
B:54 [in MetaCoq.Translations.times_bool_fun2]
B:541 [in MetaCoq.Template.utils.MCList]
B:546 [in MetaCoq.PCUIC.PCUICAst]
B:546 [in MetaCoq.Translations.MiniHoTT_paths]
B:549 [in MetaCoq.Translations.MiniHoTT]
b:55 [in MetaCoq.Template.utils.bytestring]
B:55 [in MetaCoq.Erasure.ELiftSubst]
B:550 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
B:551 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
B:554 [in MetaCoq.SafeChecker.PCUICSafeRetyping]
B:557 [in MetaCoq.PCUIC.PCUICAst]
B:557 [in MetaCoq.Translations.MiniHoTT_paths]
B:558 [in MetaCoq.Template.utils.MCList]
B:57 [in MetaCoq.Template.BasicAst]
B:57 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
B:57 [in MetaCoq.PCUIC.utils.PCUICUtils]
b:57 [in MetaCoq.PCUIC.PCUICEquality]
B:57 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
b:57 [in MetaCoq.PCUIC.PCUICAst]
b:57 [in MetaCoq.PCUIC.Syntax.PCUICReflect]
B:57 [in MetaCoq.Translations.MiniHoTT]
b:57 [in MetaCoq.Erasure.EOptimizePropDiscr]
B:574 [in MetaCoq.PCUIC.PCUICEquality]
b:575 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
B:575 [in MetaCoq.PCUIC.PCUICSpine]
b:579 [in MetaCoq.PCUIC.PCUICEquality]
b:58 [in MetaCoq.Template.utils.MCRelations]
B:58 [in MetaCoq.Template.utils.MCOption]
B:58 [in MetaCoq.Examples.demo]
B:58 [in MetaCoq.Translations.MiniHoTT_paths]
B:58 [in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
B:58 [in MetaCoq.Template.AstUtils]
B:583 [in MetaCoq.Template.utils.wGraph]
B:584 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
B:589 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
b:59 [in MetaCoq.PCUIC.PCUICAst]
B:59 [in MetaCoq.PCUIC.Syntax.PCUICReflect]
b:59 [in MetaCoq.Translations.MiniHoTT]
b:59 [in MetaCoq.Translations.MiniHoTT_paths]
b:59 [in MetaCoq.PCUIC.PCUICReduction]
B:595 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
B:599 [in MetaCoq.Template.utils.All_Forall]
b:60 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
B:60 [in MetaCoq.PCUIC.PCUICInversion]
B:60 [in MetaCoq.Examples.demo]
B:60 [in MetaCoq.Template.utils.MCProd]
B:602 [in MetaCoq.PCUIC.PCUICTyping]
B:604 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
B:604 [in MetaCoq.Template.utils.MCList]
B:605 [in MetaCoq.Template.utils.All_Forall]
b:61 [in MetaCoq.Template.utils.MCRelations]
b:61 [in MetaCoq.Erasure.EPretty]
b:61 [in MetaCoq.PCUIC.PCUICSubstitution]
B:61 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
B:613 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
b:614 [in MetaCoq.Template.Typing]
B:616 [in MetaCoq.Template.utils.MCList]
b:619 [in MetaCoq.Template.Typing]
B:62 [in MetaCoq.Template.BasicAst]
b:62 [in MetaCoq.PCUIC.PCUICAst]
B:62 [in MetaCoq.PCUIC.PCUICConfluence]
B:62 [in MetaCoq.Examples.demo]
b:623 [in MetaCoq.Template.Typing]
B:628 [in MetaCoq.Translations.MiniHoTT]
B:63 [in MetaCoq.Template.utils.MCRelations]
b:63 [in MetaCoq.Erasure.EPretty]
b:63 [in MetaCoq.PCUIC.PCUICInversion]
b:63 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
B:633 [in MetaCoq.Translations.MiniHoTT]
B:636 [in MetaCoq.Translations.MiniHoTT_paths]
B:639 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
B:64 [in MetaCoq.PCUIC.PCUICInversion]
b:64 [in MetaCoq.PCUIC.Syntax.PCUICReflect]
b:64 [in MetaCoq.PCUIC.PCUICReduction]
B:641 [in MetaCoq.Translations.MiniHoTT_paths]
B:642 [in MetaCoq.Translations.MiniHoTT]
B:649 [in MetaCoq.Translations.MiniHoTT]
b:65 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
b:65 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
B:65 [in MetaCoq.Template.utils.MCOption]
B:65 [in MetaCoq.Translations.MiniHoTT_paths]
B:650 [in MetaCoq.Translations.MiniHoTT_paths]
B:651 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
B:653 [in MetaCoq.Translations.MiniHoTT]
B:657 [in MetaCoq.Translations.MiniHoTT_paths]
b:657 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
B:659 [in MetaCoq.Template.utils.MCList]
B:66 [in MetaCoq.Template.utils.MCList]
b:66 [in MetaCoq.PCUIC.utils.PCUICOnOne]
B:66 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
b:66 [in MetaCoq.PCUIC.PCUICAst]
B:66 [in MetaCoq.Template.utils.MCProd]
B:661 [in MetaCoq.Translations.MiniHoTT]
B:661 [in MetaCoq.Translations.MiniHoTT_paths]
b:663 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
B:667 [in MetaCoq.Translations.MiniHoTT]
B:669 [in MetaCoq.Translations.MiniHoTT_paths]
b:67 [in MetaCoq.Translations.MiniHoTT_paths]
b:670 [in MetaCoq.Template.utils.MCList]
b:671 [in MetaCoq.PCUIC.PCUICConversion]
b:674 [in MetaCoq.PCUIC.PCUICConversion]
B:675 [in MetaCoq.Translations.MiniHoTT_paths]
B:678 [in MetaCoq.Translations.MiniHoTT]
B:68 [in MetaCoq.PCUIC.PCUICSafeLemmata]
B:68 [in MetaCoq.Template.utils.MCOption]
b:68 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
b:680 [in MetaCoq.PCUIC.PCUICConversion]
b:684 [in MetaCoq.PCUIC.PCUICConversion]
B:686 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
B:686 [in MetaCoq.Template.Typing]
B:686 [in MetaCoq.Translations.MiniHoTT_paths]
B:687 [in MetaCoq.Translations.MiniHoTT]
B:69 [in MetaCoq.PCUIC.PCUICArities]
B:69 [in MetaCoq.Template.utils.MCProd]
b:69 [in MetaCoq.PCUIC.PCUICReduction]
b:691 [in MetaCoq.PCUIC.PCUICConversion]
B:693 [in MetaCoq.Template.Typing]
B:695 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
B:695 [in MetaCoq.PCUIC.PCUICConfluence]
B:695 [in MetaCoq.Translations.MiniHoTT_paths]
b:698 [in MetaCoq.PCUIC.PCUICConversion]
b:7 [in MetaCoq.Template.utils.MCReflect]
b:7 [in MetaCoq.Erasure.Extract]
b:7 [in MetaCoq.Template.utils.ReflectEq]
B:7 [in MetaCoq.Template.utils.MCProd]
B:7 [in MetaCoq.Translations.MiniHoTT_paths]
B:7 [in MetaCoq.Template.utils.MCPrelude]
b:7 [in MetaCoq.Template.AstUtils]
b:7 [in MetaCoq.PCUIC.PCUICReduction]
b:70 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
B:70 [in MetaCoq.PCUIC.PCUICFirstorder]
B:700 [in MetaCoq.Translations.MiniHoTT]
b:705 [in MetaCoq.PCUIC.PCUICConversion]
B:707 [in MetaCoq.Template.utils.MCList]
B:708 [in MetaCoq.Translations.MiniHoTT_paths]
B:71 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
b:71 [in MetaCoq.PCUIC.PCUICAst]
B:71 [in MetaCoq.Translations.times_bool_fun2]
B:717 [in MetaCoq.Template.utils.MCList]
b:718 [in MetaCoq.PCUIC.PCUICConversion]
b:72 [in MetaCoq.PCUIC.PCUICAst]
B:721 [in MetaCoq.Template.utils.MCList]
B:725 [in MetaCoq.PCUIC.PCUICEquality]
b:727 [in MetaCoq.PCUIC.PCUICConversion]
b:729 [in MetaCoq.Template.utils.wGraph]
B:73 [in MetaCoq.PCUIC.PCUICParallelReduction]
b:73 [in MetaCoq.PCUIC.PCUICAst]
B:73 [in MetaCoq.Template.monad_utils]
B:733 [in MetaCoq.Template.utils.MCList]
B:74 [in MetaCoq.SafeChecker.PCUICSafeReduce]
B:74 [in MetaCoq.PCUIC.PCUICConfluence]
B:745 [in MetaCoq.Template.utils.MCList]
B:75 [in MetaCoq.PCUIC.PCUICInversion]
B:75 [in MetaCoq.PCUIC.PCUICAst]
B:75 [in MetaCoq.Translations.times_bool_fun2]
B:764 [in MetaCoq.Template.utils.All_Forall]
B:765 [in MetaCoq.Template.utils.MCList]
B:77 [in MetaCoq.Template.BasicAst]
B:772 [in MetaCoq.Template.utils.All_Forall]
B:773 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
B:773 [in MetaCoq.Translations.MiniHoTT]
B:773 [in MetaCoq.PCUIC.PCUICReduction]
B:776 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
B:778 [in MetaCoq.Template.utils.MCList]
B:781 [in MetaCoq.Translations.MiniHoTT]
B:781 [in MetaCoq.Translations.MiniHoTT_paths]
B:782 [in MetaCoq.PCUIC.PCUICReduction]
b:785 [in MetaCoq.PCUIC.PCUICConversion]
b:786 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
b:787 [in MetaCoq.PCUIC.PCUICParallelReduction]
B:789 [in MetaCoq.Translations.MiniHoTT_paths]
B:79 [in MetaCoq.Template.utils.MCOption]
B:79 [in MetaCoq.Translations.times_bool_fun2]
B:790 [in MetaCoq.Translations.MiniHoTT]
b:793 [in MetaCoq.PCUIC.PCUICConversion]
B:794 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
B:798 [in MetaCoq.Translations.MiniHoTT_paths]
B:8 [in MetaCoq.Template.utils.MCRelations]
B:8 [in MetaCoq.Template.utils.MCList]
b:8 [in MetaCoq.Template.utils.bytestring]
B:8 [in MetaCoq.SafeChecker.PCUICWfReduction]
B:8 [in MetaCoq.Erasure.ErasureProperties]
b:8 [in MetaCoq.Erasure.ESpineView]
B:8 [in MetaCoq.Template.Pretty]
B:801 [in MetaCoq.Translations.MiniHoTT]
B:804 [in MetaCoq.PCUIC.PCUICSR]
b:808 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
B:809 [in MetaCoq.PCUIC.PCUICConversion]
B:809 [in MetaCoq.Translations.MiniHoTT_paths]
B:811 [in MetaCoq.Translations.MiniHoTT]
b:811 [in MetaCoq.PCUIC.PCUICTyping]
B:811 [in MetaCoq.PCUIC.PCUICSR]
B:814 [in MetaCoq.PCUIC.PCUICReduction]
B:817 [in MetaCoq.PCUIC.PCUICInductiveInversion]
B:817 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
B:819 [in MetaCoq.Translations.MiniHoTT_paths]
b:82 [in MetaCoq.Template.Universes]
B:82 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
b:820 [in MetaCoq.PCUIC.PCUICTyping]
B:822 [in MetaCoq.Translations.MiniHoTT]
b:828 [in MetaCoq.PCUIC.PCUICTyping]
b:83 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
B:83 [in MetaCoq.PCUIC.PCUICInversion]
b:83 [in MetaCoq.PCUIC.PCUICFirstorder]
B:830 [in MetaCoq.Translations.MiniHoTT_paths]
B:830 [in MetaCoq.PCUIC.PCUICReduction]
B:833 [in MetaCoq.Translations.MiniHoTT]
b:836 [in MetaCoq.Translations.MiniHoTT]
b:84 [in MetaCoq.PCUIC.PCUICAst]
B:840 [in MetaCoq.PCUIC.PCUICInductiveInversion]
B:840 [in MetaCoq.PCUIC.PCUICTyping]
B:841 [in MetaCoq.Translations.MiniHoTT_paths]
b:844 [in MetaCoq.Translations.MiniHoTT_paths]
B:85 [in MetaCoq.Template.BasicAst]
b:85 [in MetaCoq.Template.Typing]
b:85 [in MetaCoq.Erasure.Extract]
b:857 [in MetaCoq.PCUIC.PCUICSR]
B:86 [in MetaCoq.Template.utils.MCList]
b:86 [in MetaCoq.Template.Ast]
B:86 [in MetaCoq.Template.utils.ReflectEq]
B:86 [in MetaCoq.PCUIC.PCUICFirstorder]
b:86 [in MetaCoq.PCUIC.PCUICAst]
B:86 [in MetaCoq.Erasure.ELiftSubst]
B:86 [in MetaCoq.Translations.param_generous_packed]
B:865 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
B:868 [in MetaCoq.PCUIC.PCUICSR]
b:87 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
B:87 [in MetaCoq.Template.utils.MCOption]
B:871 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
B:873 [in MetaCoq.PCUIC.PCUICSR]
B:877 [in MetaCoq.Template.utils.MCList]
B:878 [in MetaCoq.PCUIC.PCUICSR]
b:88 [in MetaCoq.Template.Ast]
b:88 [in MetaCoq.PCUIC.PCUICAst]
B:88 [in MetaCoq.PCUIC.Syntax.PCUICDepth]
B:883 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
B:885 [in MetaCoq.Template.utils.All_Forall]
b:889 [in MetaCoq.Template.utils.All_Forall]
B:89 [in MetaCoq.PCUIC.PCUICArities]
b:89 [in MetaCoq.Template.Typing]
B:89 [in MetaCoq.PCUIC.Bidirectional.BDUnique]
B:890 [in MetaCoq.Template.utils.MCList]
B:891 [in MetaCoq.PCUIC.PCUICSR]
b:894 [in MetaCoq.Template.utils.All_Forall]
B:897 [in MetaCoq.Template.utils.MCList]
B:899 [in MetaCoq.Translations.MiniHoTT]
b:9 [in MetaCoq.Template.utils.MCReflect]
b:9 [in MetaCoq.Template.utils.ReflectEq]
b:9 [in MetaCoq.PCUIC.Syntax.PCUICNamelessDef]
b:9 [in MetaCoq.PCUIC.PCUICGuardCondition]
b:90 [in MetaCoq.PCUIC.PCUICProgress]
B:90 [in MetaCoq.Template.utils.All_Forall]
b:90 [in MetaCoq.Template.Ast]
B:90 [in MetaCoq.Translations.MiniHoTT]
B:900 [in MetaCoq.Template.utils.All_Forall]
b:904 [in MetaCoq.Translations.MiniHoTT]
B:907 [in MetaCoq.Translations.MiniHoTT_paths]
B:91 [in MetaCoq.Translations.param_binary]
B:91 [in MetaCoq.PCUIC.PCUICTyping]
b:91 [in MetaCoq.Template.Pretty]
B:910 [in MetaCoq.Template.utils.All_Forall]
B:912 [in MetaCoq.Translations.MiniHoTT]
b:912 [in MetaCoq.Translations.MiniHoTT_paths]
B:918 [in MetaCoq.Template.utils.MCList]
b:918 [in MetaCoq.Translations.MiniHoTT]
B:918 [in MetaCoq.PCUIC.PCUICReduction]
B:92 [in MetaCoq.Translations.times_bool_fun2]
B:92 [in MetaCoq.Translations.param_generous_packed]
b:92 [in MetaCoq.PCUIC.utils.PCUICPretty]
B:920 [in MetaCoq.Template.utils.All_Forall]
B:920 [in MetaCoq.Translations.MiniHoTT_paths]
B:923 [in MetaCoq.Template.utils.MCList]
B:924 [in MetaCoq.PCUIC.PCUICReduction]
B:925 [in MetaCoq.PCUIC.PCUICTyping]
b:926 [in MetaCoq.Translations.MiniHoTT_paths]
B:928 [in MetaCoq.Template.utils.All_Forall]
b:93 [in MetaCoq.PCUIC.PCUICElimination]
B:934 [in MetaCoq.Template.utils.All_Forall]
B:94 [in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
B:94 [in MetaCoq.Template.BasicAst]
b:94 [in MetaCoq.Template.Ast]
B:94 [in MetaCoq.Template.utils.ReflectEq]
B:940 [in MetaCoq.Template.utils.All_Forall]
B:941 [in MetaCoq.Template.Typing]
B:95 [in MetaCoq.Translations.param_binary]
B:95 [in MetaCoq.PCUIC.PCUICArities]
b:95 [in MetaCoq.Template.Ast]
B:95 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
B:950 [in MetaCoq.Template.utils.All_Forall]
B:958 [in MetaCoq.Template.utils.All_Forall]
B:959 [in MetaCoq.Translations.MiniHoTT]
B:96 [in MetaCoq.PCUIC.Bidirectional.BDTyping]
B:96 [in MetaCoq.Template.utils.All_Forall]
b:96 [in MetaCoq.PCUIC.PCUICNormal]
B:96 [in MetaCoq.Template.utils.ReflectEq]
B:966 [in MetaCoq.Translations.MiniHoTT]
B:967 [in MetaCoq.Translations.MiniHoTT_paths]
B:969 [in MetaCoq.Template.utils.All_Forall]
B:97 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
B:97 [in MetaCoq.SafeChecker.PCUICSafeReduce]
B:97 [in MetaCoq.Translations.times_bool_fun2]
B:974 [in MetaCoq.Translations.MiniHoTT]
B:974 [in MetaCoq.Translations.MiniHoTT_paths]
B:978 [in MetaCoq.Template.utils.All_Forall]
B:98 [in MetaCoq.PCUIC.PCUICAst]
B:98 [in MetaCoq.PCUIC.PCUICTyping]
B:98 [in MetaCoq.Translations.MiniHoTT_paths]
B:98 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
B:982 [in MetaCoq.Translations.MiniHoTT_paths]
B:984 [in MetaCoq.Translations.MiniHoTT]
b:986 [in MetaCoq.PCUIC.PCUICConversion]
b:99 [in MetaCoq.PCUIC.PCUICProgress]
B:99 [in MetaCoq.PCUIC.utils.PCUICUtils]
B:990 [in MetaCoq.Template.utils.All_Forall]
b:990 [in MetaCoq.Template.Typing]
B:992 [in MetaCoq.Translations.MiniHoTT_paths]
B:994 [in MetaCoq.Translations.MiniHoTT]
b:998 [in MetaCoq.Template.utils.All_Forall]
b:999 [in MetaCoq.Template.Typing]
| 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) |