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