| 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) |
H
HAcc:136 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]Happ_2:242 [binder, in MetaCoq.PCUIC.PCUICNormal]
Happ_1:238 [binder, in MetaCoq.PCUIC.PCUICNormal]
Happ:102 [binder, in MetaCoq.Erasure.Extract]
Happ:80 [binder, in MetaCoq.Erasure.EDeps]
Hargs:1009 [binder, in MetaCoq.Erasure.ErasureFunction]
Hargs:362 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
hasco:87 [binder, in MetaCoq.Erasure.EWellformed]
HasLen [record, in MetaCoq.PCUIC.PCUICAst]
HasLen [inductive, in MetaCoq.PCUIC.PCUICAst]
hastbox:108 [binder, in MetaCoq.Erasure.ETransform]
hastbox:175 [binder, in MetaCoq.Erasure.EInlineProjections]
hastbox:188 [binder, in MetaCoq.Erasure.EOptimizePropDiscr]
hastbox:86 [binder, in MetaCoq.Erasure.ETransform]
hastbox:98 [binder, in MetaCoq.Erasure.ETransform]
hastrel:107 [binder, in MetaCoq.Erasure.ETransform]
hastrel:176 [binder, in MetaCoq.Erasure.EInlineProjections]
hastrel:189 [binder, in MetaCoq.Erasure.EOptimizePropDiscr]
hastrel:85 [binder, in MetaCoq.Erasure.ETransform]
hastrel:97 [binder, in MetaCoq.Erasure.ETransform]
hast:110 [binder, in MetaCoq.Erasure.EWellformed]
hast:85 [binder, in MetaCoq.Erasure.EWellformed]
has_nparams [definition, in MetaCoq.Template.Typing]
has_atom [definition, in MetaCoq.Erasure.EWcbvEvalEtaInd]
has_cstr_params [projection, in MetaCoq.Erasure.EWellformed]
has_axioms [projection, in MetaCoq.Erasure.EWellformed]
has_tCoFix [projection, in MetaCoq.Erasure.EWellformed]
has_tFix [projection, in MetaCoq.Erasure.EWellformed]
has_tProj [projection, in MetaCoq.Erasure.EWellformed]
has_tCase [projection, in MetaCoq.Erasure.EWellformed]
has_tConstruct [projection, in MetaCoq.Erasure.EWellformed]
has_tConst [projection, in MetaCoq.Erasure.EWellformed]
has_tApp [projection, in MetaCoq.Erasure.EWellformed]
has_tLetIn [projection, in MetaCoq.Erasure.EWellformed]
has_tLambda [projection, in MetaCoq.Erasure.EWellformed]
has_tEvar [projection, in MetaCoq.Erasure.EWellformed]
has_tVar [projection, in MetaCoq.Erasure.EWellformed]
has_tRel [projection, in MetaCoq.Erasure.EWellformed]
has_tBox [projection, in MetaCoq.Erasure.EWellformed]
has_nparams [definition, in MetaCoq.PCUIC.PCUICTyping]
has_app:354 [binder, in MetaCoq.Erasure.EWcbvEval]
has_blocks:350 [binder, in MetaCoq.Erasure.EWcbvEval]
has_pars:348 [binder, in MetaCoq.Erasure.EWcbvEval]
has_ax:347 [binder, in MetaCoq.Erasure.EWcbvEval]
ha:1790 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
hA:209 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
ha:2532 [binder, in MetaCoq.Template.utils.All_Forall]
HA:55 [binder, in MetaCoq.PCUIC.PCUICProgress]
ha:61 [binder, in MetaCoq.Erasure.EGenericMapEnv]
HA:63 [binder, in MetaCoq.Template.utils.ReflectEq]
Hbeta_nobeta:227 [binder, in MetaCoq.PCUIC.PCUICNormal]
Hbox:150 [binder, in MetaCoq.Erasure.Extract]
Hbox:63 [binder, in MetaCoq.Erasure.EDeps]
hb':1058 [binder, in MetaCoq.PCUIC.PCUICConfluence]
hb':1066 [binder, in MetaCoq.PCUIC.PCUICConfluence]
hb':1071 [binder, in MetaCoq.PCUIC.PCUICConfluence]
hb:1057 [binder, in MetaCoq.PCUIC.PCUICConfluence]
hb:1065 [binder, in MetaCoq.PCUIC.PCUICConfluence]
hb:1070 [binder, in MetaCoq.PCUIC.PCUICConfluence]
Hcase_noiota:318 [binder, in MetaCoq.PCUIC.PCUICNormal]
Hcase_branch:312 [binder, in MetaCoq.PCUIC.PCUICNormal]
Hcase_discr:303 [binder, in MetaCoq.PCUIC.PCUICNormal]
Hcase_motive:297 [binder, in MetaCoq.PCUIC.PCUICNormal]
Hcase_params:291 [binder, in MetaCoq.PCUIC.PCUICNormal]
Hcase:105 [binder, in MetaCoq.Erasure.EDeps]
Hcase:123 [binder, in MetaCoq.Erasure.Extract]
hcb:1252 [binder, in MetaCoq.Erasure.ErasureFunction]
Hcb:668 [binder, in MetaCoq.Erasure.ErasureFunction]
Hcl:28 [binder, in MetaCoq.Template.UnivSubst]
Hcl:38 [binder, in MetaCoq.PCUIC.Syntax.PCUICUnivSubst]
Hcl:745 [binder, in MetaCoq.Template.Universes]
Hcofix:126 [binder, in MetaCoq.Erasure.EDeps]
Hcofix:147 [binder, in MetaCoq.Erasure.Extract]
Hconstruct:111 [binder, in MetaCoq.Erasure.Extract]
Hconstruct:95 [binder, in MetaCoq.Erasure.EDeps]
Hconst_nodelta:222 [binder, in MetaCoq.PCUIC.PCUICNormal]
Hconst:106 [binder, in MetaCoq.Erasure.Extract]
Hconst:86 [binder, in MetaCoq.Erasure.EDeps]
hcon:55 [binder, in MetaCoq.Erasure.EDeps]
Hcs:367 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
Hcs:810 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
HC:265 [binder, in MetaCoq.Template.common.uGraph]
Hc:278 [binder, in MetaCoq.Template.EnvironmentTyping]
HC:476 [binder, in MetaCoq.Template.common.uGraph]
Hdecl:122 [binder, in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
Hdecl:136 [binder, in MetaCoq.PCUIC.PCUICElimination]
Hdecl:137 [binder, in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
Hdecl:167 [binder, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
Hdecl:172 [binder, in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
Hdecl:184 [binder, in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
Hdecl:292 [binder, in MetaCoq.PCUIC.PCUICInductives]
Hdecl:316 [binder, in MetaCoq.PCUIC.PCUICInductives]
Hdecl:327 [binder, in MetaCoq.PCUIC.PCUICInductives]
Hdecl:350 [binder, in MetaCoq.PCUIC.PCUICInductives]
Hdecl:739 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
Hdecl:81 [binder, in MetaCoq.PCUIC.PCUICInductives]
Hdecl:93 [binder, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
Hdecl:97 [binder, in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
hdiscr:5242 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
hdrel:552 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
hd':111 [binder, in MetaCoq.PCUIC.PCUICConvCumInversion]
hd':25 [binder, in MetaCoq.PCUIC.PCUICAlpha]
hd':370 [binder, in MetaCoq.PCUIC.PCUICNormal]
hd':431 [binder, in MetaCoq.PCUIC.PCUICNormal]
hd':439 [binder, in MetaCoq.PCUIC.PCUICNormal]
hd':444 [binder, in MetaCoq.PCUIC.PCUICNormal]
hd':452 [binder, in MetaCoq.PCUIC.PCUICNormal]
hd':457 [binder, in MetaCoq.PCUIC.PCUICConversion]
hd':49 [binder, in MetaCoq.Template.utils.MCCompare]
hd':572 [binder, in MetaCoq.Template.utils.All_Forall]
hd':731 [binder, in MetaCoq.Template.utils.All_Forall]
hd':892 [binder, in MetaCoq.Template.utils.All_Forall]
hd:109 [binder, in MetaCoq.PCUIC.PCUICConvCumInversion]
hd:117 [binder, in MetaCoq.Erasure.EEtaExpanded]
hd:12 [binder, in MetaCoq.Template.utils.All_Forall]
hd:122 [binder, in MetaCoq.PCUIC.PCUICSpine]
hd:123 [binder, in MetaCoq.Erasure.EEtaExpanded]
hd:137 [binder, in MetaCoq.Template.AstUtils]
hd:1396 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
hd:1399 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
hd:1428 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
hd:1437 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
hd:16 [binder, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
hd:16 [binder, in MetaCoq.Examples.add_constructor]
hd:170 [binder, in MetaCoq.Erasure.ERemoveParams]
hd:174 [binder, in MetaCoq.Erasure.ERemoveParams]
hd:187 [binder, in MetaCoq.PCUIC.PCUICCanonicity]
hd:197 [binder, in MetaCoq.Erasure.Extract]
hd:20 [binder, in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
hd:21 [binder, in MetaCoq.PCUIC.PCUICArities]
hd:23 [binder, in MetaCoq.PCUIC.PCUICAlpha]
hd:230 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
hd:24 [binder, in MetaCoq.PCUIC.PCUICProgress]
hd:25 [binder, in MetaCoq.PCUIC.PCUICTyping]
hd:3 [binder, in MetaCoq.Erasure.EDeps]
hd:33 [binder, in MetaCoq.PCUIC.PCUICTyping]
hd:342 [binder, in MetaCoq.Template.TypingWf]
hd:369 [binder, in MetaCoq.PCUIC.PCUICNormal]
hd:370 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
hd:415 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
hd:423 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
hd:429 [binder, in MetaCoq.PCUIC.PCUICProgress]
hd:430 [binder, in MetaCoq.PCUIC.PCUICNormal]
hd:436 [binder, in MetaCoq.PCUIC.PCUICNormal]
hd:437 [binder, in MetaCoq.PCUIC.PCUICProgress]
hd:446 [binder, in MetaCoq.PCUIC.PCUICNormal]
hd:45 [binder, in MetaCoq.Template.utils.MCCompare]
hd:450 [binder, in MetaCoq.PCUIC.PCUICNormal]
hd:455 [binder, in MetaCoq.PCUIC.PCUICConversion]
hd:460 [binder, in MetaCoq.Template.utils.MCList]
hd:47 [binder, in MetaCoq.Template.utils.MCCompare]
hd:51 [binder, in MetaCoq.Template.utils.MCCompare]
hd:516 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
hd:546 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
hd:571 [binder, in MetaCoq.Template.utils.All_Forall]
hd:574 [binder, in MetaCoq.Template.utils.All_Forall]
hd:586 [binder, in MetaCoq.Template.Typing]
hd:593 [binder, in MetaCoq.Template.Typing]
hd:64 [binder, in MetaCoq.PCUIC.PCUICFirstorder]
hd:689 [binder, in MetaCoq.Template.Typing]
hd:7 [binder, in MetaCoq.Erasure.EDeps]
hd:73 [binder, in MetaCoq.Erasure.EAstUtils]
hd:730 [binder, in MetaCoq.Template.utils.All_Forall]
hd:734 [binder, in MetaCoq.Template.utils.All_Forall]
hd:78 [binder, in MetaCoq.Erasure.EDeps]
hd:8 [binder, in MetaCoq.PCUIC.PCUICGeneration]
hd:84 [binder, in MetaCoq.PCUIC.PCUICConvCumInversion]
hd:891 [binder, in MetaCoq.Template.utils.All_Forall]
hd:896 [binder, in MetaCoq.Template.utils.All_Forall]
hd:937 [binder, in MetaCoq.Template.Typing]
head [definition, in MetaCoq.PCUIC.utils.PCUICAstUtils]
head [definition, in MetaCoq.Erasure.EAstUtils]
HeadMismatch [constructor, in MetaCoq.SafeChecker.PCUICErrors]
headrel:494 [binder, in MetaCoq.Template.EnvironmentTyping]
head_tapp [lemma, in MetaCoq.PCUIC.utils.PCUICAstUtils]
head_nApp [lemma, in MetaCoq.PCUIC.utils.PCUICAstUtils]
head_arguments [lemma, in MetaCoq.PCUIC.utils.PCUICAstUtils]
head_mkApps [lemma, in MetaCoq.PCUIC.PCUICWcbvEval]
head_subst [lemma, in MetaCoq.PCUIC.PCUICInductives]
head_mkApps [lemma, in MetaCoq.PCUIC.PCUICCanonicity]
head_nApp_eq [lemma, in MetaCoq.Erasure.EAstUtils]
head_nApp [lemma, in MetaCoq.Erasure.EAstUtils]
head_tApp [lemma, in MetaCoq.Erasure.EAstUtils]
head_mkApps [lemma, in MetaCoq.Erasure.EAstUtils]
head:22 [binder, in MetaCoq.PCUIC.PCUICInductives]
head:235 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
head:412 [binder, in MetaCoq.Template.EtaExpand]
heq:1041 [binder, in MetaCoq.Erasure.ErasureFunction]
heq:1249 [binder, in MetaCoq.Erasure.ErasureFunction]
heq:1262 [binder, in MetaCoq.Erasure.ErasureFunction]
heq:1270 [binder, in MetaCoq.Erasure.ErasureFunction]
Heq:134 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
Heq:156 [binder, in MetaCoq.Template.EtaExpand]
heq:639 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
heq:807 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
heq:840 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
Heval:368 [binder, in MetaCoq.Erasure.EWcbvEval]
Heval:387 [binder, in MetaCoq.Erasure.EWcbvEval]
Hevar:212 [binder, in MetaCoq.PCUIC.PCUICNormal]
Hevar:70 [binder, in MetaCoq.Erasure.EDeps]
Hevar:82 [binder, in MetaCoq.Erasure.Extract]
hext:1189 [binder, in MetaCoq.Template.utils.wGraph]
He':380 [binder, in MetaCoq.Erasure.EWcbvEval]
He1:400 [binder, in MetaCoq.Template.common.uGraph]
He1:488 [binder, in MetaCoq.Template.common.uGraph]
he:297 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
he:319 [binder, in MetaCoq.PCUIC.PCUICConfluence]
He:379 [binder, in MetaCoq.Erasure.EWcbvEval]
He:486 [binder, in MetaCoq.Template.utils.wGraph]
heΣ [definition, in MetaCoq.SafeChecker.PCUICSafeRetyping]
heΣ [definition, in MetaCoq.Erasure.ErasureFunction]
heΣ [definition, in MetaCoq.SafeChecker.PCUICSafeReduce]
heΣ [definition, in MetaCoq.SafeChecker.PCUICSafeConversion]
heΣ [definition, in MetaCoq.SafeChecker.PCUICSafeChecker]
heΣ [definition, in MetaCoq.SafeChecker.PCUICTypeChecker]
Hfix_red_body_nofix:285 [binder, in MetaCoq.PCUIC.PCUICNormal]
Hfix_red_type_nofix:279 [binder, in MetaCoq.PCUIC.PCUICNormal]
Hfix_red_def_body:273 [binder, in MetaCoq.PCUIC.PCUICNormal]
Hfix_red_def_type:263 [binder, in MetaCoq.PCUIC.PCUICNormal]
Hfix_red_arg:253 [binder, in MetaCoq.PCUIC.PCUICNormal]
Hfix_nofix:234 [binder, in MetaCoq.PCUIC.PCUICNormal]
Hfix:121 [binder, in MetaCoq.Erasure.EDeps]
Hfix:138 [binder, in MetaCoq.Erasure.Extract]
Hfresh:976 [binder, in MetaCoq.Erasure.ErasureFunction]
Hf:53 [binder, in MetaCoq.PCUIC.PCUICProgress]
hf:54 [binder, in MetaCoq.Erasure.ESpineView]
Hf:580 [binder, in MetaCoq.Template.utils.wGraph]
Hf:69 [binder, in MetaCoq.Erasure.EInduction]
Hf:73 [binder, in MetaCoq.Erasure.EInduction]
Hf:99 [binder, in MetaCoq.Translations.times_bool_fun2]
Hglobal:94 [binder, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
HGl:1155 [binder, in MetaCoq.Template.utils.wGraph]
HGl:998 [binder, in MetaCoq.Template.utils.wGraph]
HG:194 [binder, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
HG:266 [binder, in MetaCoq.Template.common.uGraph]
HG:390 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
HG:477 [binder, in MetaCoq.Template.common.uGraph]
HG:48 [binder, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
HG:480 [binder, in MetaCoq.Template.utils.wGraph]
HG:512 [binder, in MetaCoq.Template.utils.wGraph]
HG:523 [binder, in MetaCoq.Template.utils.wGraph]
HG:527 [binder, in MetaCoq.Template.utils.wGraph]
HG:542 [binder, in MetaCoq.Template.utils.wGraph]
HG:548 [binder, in MetaCoq.Template.utils.wGraph]
HG:551 [binder, in MetaCoq.Template.utils.wGraph]
HG:555 [binder, in MetaCoq.Template.utils.wGraph]
HG:559 [binder, in MetaCoq.Template.utils.wGraph]
HG:567 [binder, in MetaCoq.Template.utils.wGraph]
HG:570 [binder, in MetaCoq.Template.utils.wGraph]
HG:593 [binder, in MetaCoq.Template.utils.wGraph]
HG:599 [binder, in MetaCoq.Template.utils.wGraph]
HG:602 [binder, in MetaCoq.Template.utils.wGraph]
HG:605 [binder, in MetaCoq.Template.utils.wGraph]
HG:610 [binder, in MetaCoq.Template.utils.wGraph]
Hg:64 [binder, in MetaCoq.Erasure.EEnvMap]
HG:656 [binder, in MetaCoq.Template.utils.wGraph]
HHl':330 [binder, in MetaCoq.Template.common.uGraph]
HHl:329 [binder, in MetaCoq.Template.common.uGraph]
HH:175 [binder, in MetaCoq.Template.common.uGraph]
hin:162 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
hin:168 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
hin:342 [binder, in MetaCoq.Template.utils.wGraph]
hin:344 [binder, in MetaCoq.Template.utils.wGraph]
Hi:223 [binder, in MetaCoq.Template.common.uGraph]
HI:516 [binder, in MetaCoq.Template.utils.wGraph]
HI:609 [binder, in MetaCoq.Template.utils.wGraph]
HI:655 [binder, in MetaCoq.Template.utils.wGraph]
Hk:1168 [binder, in MetaCoq.Template.utils.wGraph]
Hk:384 [binder, in MetaCoq.Template.utils.wGraph]
Hlam_nobeta_2:208 [binder, in MetaCoq.PCUIC.PCUICNormal]
Hlam_nobeta_1:203 [binder, in MetaCoq.PCUIC.PCUICNormal]
Hlam:73 [binder, in MetaCoq.Erasure.EDeps]
Hlam:88 [binder, in MetaCoq.Erasure.Extract]
Hletin_nozeta_1:218 [binder, in MetaCoq.PCUIC.PCUICNormal]
Hletin:77 [binder, in MetaCoq.Erasure.EDeps]
Hletin:96 [binder, in MetaCoq.Erasure.Extract]
Hle:14 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
Hle:14 [binder, in MetaCoq.PCUIC.PCUICEtaExpand]
hle:298 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
hle:320 [binder, in MetaCoq.PCUIC.PCUICConfluence]
hle:65 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
hle:72 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
Hlookup [definition, in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
Hlookup [definition, in MetaCoq.Erasure.ErasureFunction]
Hl':299 [binder, in MetaCoq.Template.common.uGraph]
Hl':304 [binder, in MetaCoq.Template.common.uGraph]
Hl':315 [binder, in MetaCoq.Template.common.uGraph]
Hl:1164 [binder, in MetaCoq.Template.utils.wGraph]
hl:168 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
Hl:215 [binder, in MetaCoq.Erasure.ErasureFunction]
hl:227 [binder, in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
Hl:239 [binder, in MetaCoq.Template.common.uGraph]
Hl:2514 [binder, in MetaCoq.Template.utils.All_Forall]
Hl:2548 [binder, in MetaCoq.Template.utils.All_Forall]
Hl:298 [binder, in MetaCoq.Template.common.uGraph]
Hl:303 [binder, in MetaCoq.Template.common.uGraph]
hl:308 [binder, in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
Hl:314 [binder, in MetaCoq.Template.common.uGraph]
hl:39 [binder, in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
Hl:470 [binder, in MetaCoq.Template.utils.wGraph]
Hl:70 [binder, in MetaCoq.Erasure.EInduction]
Hl:74 [binder, in MetaCoq.Erasure.EInduction]
hnf [definition, in MetaCoq.SafeChecker.PCUICSafeReduce]
hnf [constructor, in MetaCoq.Template.TemplateMonad.Common]
hnf [abbreviation, in MetaCoq.SafeChecker.PCUICTypeChecker]
hnf_subterm_rel [definition, in MetaCoq.SafeChecker.PCUICWfReduction]
hnf_complete [lemma, in MetaCoq.SafeChecker.PCUICSafeReduce]
hnf_sound [lemma, in MetaCoq.SafeChecker.PCUICSafeReduce]
hnf_stack [definition, in MetaCoq.Template.Checker]
hnth:190 [binder, in MetaCoq.Template.monad_utils]
hnth:637 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
hnth:805 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
hnth:839 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
hnth:869 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
hnth:897 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
hnth:979 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
Hoib:1011 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
hole [definition, in MetaCoq.Template.Ast]
hole_branch_context [definition, in MetaCoq.PCUIC.PCUICReduction]
hole_list_context [definition, in MetaCoq.PCUIC.PCUICReduction]
hole_context [definition, in MetaCoq.PCUIC.PCUICReduction]
hpctx:732 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
hpp:53 [binder, in MetaCoq.Template.Transform]
HPQ:138 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
hprefix':1493 [binder, in MetaCoq.Erasure.ErasureFunction]
hprefix':1501 [binder, in MetaCoq.Erasure.ErasureFunction]
hprefix:1492 [binder, in MetaCoq.Erasure.ErasureFunction]
hprefix:1500 [binder, in MetaCoq.Erasure.ErasureFunction]
Hproj_discr_noiota:338 [binder, in MetaCoq.PCUIC.PCUICNormal]
Hproj_noiota:334 [binder, in MetaCoq.PCUIC.PCUICNormal]
Hproj_cofix_noiota:329 [binder, in MetaCoq.PCUIC.PCUICNormal]
Hproj:116 [binder, in MetaCoq.Erasure.EDeps]
Hproj:129 [binder, in MetaCoq.Erasure.Extract]
Hproj:322 [binder, in MetaCoq.PCUIC.PCUICNormal]
hp':136 [binder, in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
hp':173 [binder, in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
Hp0:289 [binder, in MetaCoq.Template.utils.wGraph]
HP:105 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
HP:119 [binder, in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
hp:1266 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
hp:1295 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
HP:134 [binder, in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
hp:135 [binder, in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
hp:1476 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
hp:172 [binder, in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
hp:22 [binder, in MetaCoq.PCUIC.PCUICTransform]
hp:2352 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
hp:27 [binder, in MetaCoq.Erasure.ETransform]
Hp:284 [binder, in MetaCoq.Template.utils.wGraph]
Hp:515 [binder, in MetaCoq.PCUIC.PCUICTyping]
hp:55 [binder, in MetaCoq.Template.Transform]
HP:82 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
HP:94 [binder, in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
HQ:100 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
HQ:125 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
Hq:575 [binder, in MetaCoq.Template.utils.wGraph]
Hq:576 [binder, in MetaCoq.Template.utils.wGraph]
HQ:77 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
Hrefl:811 [binder, in MetaCoq.PCUIC.PCUICConfluence]
Hrel:198 [binder, in MetaCoq.PCUIC.PCUICNormal]
Hrel:65 [binder, in MetaCoq.Erasure.EDeps]
Hrel:73 [binder, in MetaCoq.Erasure.Extract]
Hre:185 [binder, in MetaCoq.Template.TermEquality]
Hre:196 [binder, in MetaCoq.Template.TermEquality]
hRe:294 [binder, in MetaCoq.PCUIC.PCUICEquality]
hRe:311 [binder, in MetaCoq.PCUIC.PCUICEquality]
hRe:320 [binder, in MetaCoq.PCUIC.PCUICEquality]
hRe:326 [binder, in MetaCoq.PCUIC.PCUICEquality]
Hrle:199 [binder, in MetaCoq.Template.TermEquality]
hr':87 [binder, in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
hr':93 [binder, in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
hr:1320 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
hR:1392 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
hR:1457 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
hR:1461 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
hR:1465 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
hR:1469 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
hR:308 [binder, in MetaCoq.PCUIC.PCUICEquality]
hR:314 [binder, in MetaCoq.PCUIC.PCUICEquality]
HR:32 [binder, in MetaCoq.Template.utils.ReflectEq]
hr:85 [binder, in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
hr:91 [binder, in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
Hs:271 [binder, in MetaCoq.Template.EnvironmentTyping]
Hs:280 [binder, in MetaCoq.Template.EnvironmentTyping]
Hs:302 [binder, in MetaCoq.Template.utils.wGraph]
Hs:308 [binder, in MetaCoq.Template.utils.wGraph]
Hs:312 [binder, in MetaCoq.Template.utils.wGraph]
Hs:320 [binder, in MetaCoq.Template.utils.wGraph]
Hs:329 [binder, in MetaCoq.Template.utils.wGraph]
Hs:356 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
Hs:394 [binder, in MetaCoq.Template.utils.wGraph]
Hs:399 [binder, in MetaCoq.Template.utils.wGraph]
Hs:411 [binder, in MetaCoq.Template.utils.wGraph]
Hs:414 [binder, in MetaCoq.Template.utils.wGraph]
Hs:424 [binder, in MetaCoq.Template.utils.wGraph]
Hs:580 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
Hty:1142 [binder, in MetaCoq.Template.Typing]
Hty:1146 [binder, in MetaCoq.Template.Typing]
Hty:1150 [binder, in MetaCoq.Template.Typing]
Hty:1154 [binder, in MetaCoq.Template.Typing]
Hty:1158 [binder, in MetaCoq.Template.Typing]
Hty:1167 [binder, in MetaCoq.Template.Typing]
Hty:1176 [binder, in MetaCoq.Template.Typing]
Hty:1180 [binder, in MetaCoq.Template.Typing]
Hty:1193 [binder, in MetaCoq.Template.Typing]
Hty:1202 [binder, in MetaCoq.Template.Typing]
Hty:1212 [binder, in MetaCoq.Template.Typing]
Hty:1219 [binder, in MetaCoq.Template.Typing]
Hty:1225 [binder, in MetaCoq.Template.Typing]
Hty:1234 [binder, in MetaCoq.Template.Typing]
Hty:1244 [binder, in MetaCoq.Template.Typing]
Hty:1251 [binder, in MetaCoq.Template.Typing]
Hty:639 [binder, in MetaCoq.PCUIC.PCUICTyping]
Hty:643 [binder, in MetaCoq.PCUIC.PCUICTyping]
Hty:651 [binder, in MetaCoq.PCUIC.PCUICTyping]
Hty:655 [binder, in MetaCoq.PCUIC.PCUICTyping]
Hty:669 [binder, in MetaCoq.PCUIC.PCUICTyping]
Hty:673 [binder, in MetaCoq.PCUIC.PCUICTyping]
Hty:697 [binder, in MetaCoq.PCUIC.PCUICTyping]
Hty:703 [binder, in MetaCoq.PCUIC.PCUICTyping]
Hty:708 [binder, in MetaCoq.PCUIC.PCUICTyping]
Hty:717 [binder, in MetaCoq.PCUIC.PCUICTyping]
hty:725 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
Hty:727 [binder, in MetaCoq.PCUIC.PCUICTyping]
Hty:733 [binder, in MetaCoq.PCUIC.PCUICTyping]
Hty:739 [binder, in MetaCoq.PCUIC.PCUICTyping]
Hty:745 [binder, in MetaCoq.PCUIC.PCUICTyping]
Hty:750 [binder, in MetaCoq.PCUIC.PCUICTyping]
Hty:759 [binder, in MetaCoq.PCUIC.PCUICTyping]
Hty:769 [binder, in MetaCoq.PCUIC.PCUICTyping]
Hty:776 [binder, in MetaCoq.PCUIC.PCUICTyping]
ht':1016 [binder, in MetaCoq.PCUIC.PCUICConfluence]
ht':1166 [binder, in MetaCoq.PCUIC.PCUICConfluence]
Ht':124 [binder, in MetaCoq.PCUIC.PCUICProgress]
Ht':519 [binder, in MetaCoq.PCUIC.PCUICTyping]
Ht':629 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
ht':68 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
ht':75 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
Ht:1008 [binder, in MetaCoq.Erasure.ErasureFunction]
ht:1015 [binder, in MetaCoq.PCUIC.PCUICConfluence]
HT:112 [binder, in MetaCoq.Erasure.ErasureFunction]
ht:1163 [binder, in MetaCoq.PCUIC.PCUICConfluence]
Ht:121 [binder, in MetaCoq.PCUIC.PCUICProgress]
Ht:211 [binder, in MetaCoq.Erasure.ErasureFunction]
Ht:221 [binder, in MetaCoq.Erasure.ErasureFunction]
Ht:226 [binder, in MetaCoq.Erasure.ErasureFunction]
Ht:231 [binder, in MetaCoq.Erasure.ErasureFunction]
Ht:274 [binder, in MetaCoq.PCUIC.PCUICProgress]
HT:51 [binder, in MetaCoq.PCUIC.PCUICProgress]
Ht:516 [binder, in MetaCoq.PCUIC.PCUICTyping]
Ht:52 [binder, in MetaCoq.Template.Reflect]
HT:53 [binder, in MetaCoq.Erasure.ErasureFunction]
ht:67 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
ht:74 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
ht:88 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
Huctx:166 [binder, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
Huctx:237 [binder, in MetaCoq.Template.common.uGraph]
Huctx:248 [binder, in MetaCoq.Template.common.uGraph]
Huctx:264 [binder, in MetaCoq.Template.common.uGraph]
Huctx:475 [binder, in MetaCoq.Template.common.uGraph]
Huctx:88 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
Hunivs:1023 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
hu':1167 [binder, in MetaCoq.PCUIC.PCUICConfluence]
hu':79 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
hu':83 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
Hu1:419 [binder, in MetaCoq.Template.common.uGraph]
Hu1:428 [binder, in MetaCoq.Template.common.uGraph]
Hu1:434 [binder, in MetaCoq.Template.common.uGraph]
Hu1:467 [binder, in MetaCoq.Template.common.uGraph]
Hu2:420 [binder, in MetaCoq.Template.common.uGraph]
Hu2:429 [binder, in MetaCoq.Template.common.uGraph]
Hu2:435 [binder, in MetaCoq.Template.common.uGraph]
Hu2:468 [binder, in MetaCoq.Template.common.uGraph]
hu:1165 [binder, in MetaCoq.PCUIC.PCUICConfluence]
Hu:333 [binder, in MetaCoq.PCUIC.PCUICSR]
Hu:370 [binder, in MetaCoq.Template.utils.wGraph]
Hu:401 [binder, in MetaCoq.Template.common.uGraph]
Hu:489 [binder, in MetaCoq.Template.common.uGraph]
hu:78 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
hu:82 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
hu:91 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
Hvar:67 [binder, in MetaCoq.Erasure.EDeps]
Hvar:76 [binder, in MetaCoq.Erasure.Extract]
Hwf:358 [binder, in MetaCoq.PCUIC.PCUICTyping]
hwf:50 [binder, in MetaCoq.Erasure.ETransform]
Hwf:645 [binder, in MetaCoq.PCUIC.PCUICTyping]
Hwf:647 [binder, in MetaCoq.PCUIC.PCUICTyping]
Hxs:616 [binder, in MetaCoq.Template.utils.wGraph]
Hxs:661 [binder, in MetaCoq.Template.utils.wGraph]
hxy:1176 [binder, in MetaCoq.Template.utils.wGraph]
hx:1173 [binder, in MetaCoq.Template.utils.wGraph]
hx:1263 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
hx:1292 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
hx:1376 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
hx:1473 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
Hx:148 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
hx:1521 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
hx:1780 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
Hx:190 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
hx:1949 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
Hx:208 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
hx:2158 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
Hx:229 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
hx:2351 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
hx:2380 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
hx:2395 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
hx:2566 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
hx:260 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
Hx:383 [binder, in MetaCoq.Template.utils.wGraph]
Hx:391 [binder, in MetaCoq.Template.utils.wGraph]
hx:4427 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
hx:4574 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
hx:5243 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
Hx:529 [binder, in MetaCoq.Template.utils.wGraph]
hx:5662 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
hx:5673 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
hx:5684 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
Hx:572 [binder, in MetaCoq.Template.utils.wGraph]
Hx:58 [binder, in MetaCoq.PCUIC.PCUICProgress]
Hx:584 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
Hx:588 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
Hx:607 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
Hx:616 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
Hx:621 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
Hx:625 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
Hx:628 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
Hx:648 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
hx:718 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
HX:795 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
hyp [projection, in MetaCoq.Erasure.EInduction]
Hyp [record, in MetaCoq.Erasure.EInduction]
hyp [constructor, in MetaCoq.Erasure.EInduction]
Hyp [inductive, in MetaCoq.Erasure.EInduction]
HypH [constructor, in MetaCoq.Template.utils.LibHypsNaming]
HypH_ [constructor, in MetaCoq.Template.utils.LibHypsNaming]
HypNone [constructor, in MetaCoq.Template.utils.LibHypsNaming]
HypPrefixes [inductive, in MetaCoq.Template.utils.LibHypsNaming]
hyps [projection, in MetaCoq.Examples.tauto]
hyps_size_app [lemma, in MetaCoq.Examples.tauto]
hyps_size [definition, in MetaCoq.Examples.tauto]
hy:1174 [binder, in MetaCoq.Template.utils.wGraph]
Hy:1282 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
Hy:1293 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
hy:1380 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
Hy:487 [binder, in MetaCoq.Template.utils.wGraph]
Hy:5641 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
Hy:5648 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
Hy:61 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
h':1046 [binder, in MetaCoq.Translations.MiniHoTT]
h':1054 [binder, in MetaCoq.Translations.MiniHoTT_paths]
H':124 [binder, in MetaCoq.Template.utils.wGraph]
h':1262 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
h':1291 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
h':1472 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
h':1520 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
H':165 [binder, in MetaCoq.SafeChecker.PCUICWfEnv]
h':1779 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
h':1948 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
h':2090 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
h':2109 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
h':2130 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
h':2350 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
h':270 [binder, in MetaCoq.PCUIC.PCUICAst]
h':289 [binder, in MetaCoq.PCUIC.PCUICAst]
H':31 [binder, in MetaCoq.PCUIC.PCUICProgress]
h':362 [binder, in MetaCoq.PCUIC.PCUICAst]
h':367 [binder, in MetaCoq.PCUIC.PCUICAst]
h':408 [binder, in MetaCoq.PCUIC.PCUICAst]
h':415 [binder, in MetaCoq.PCUIC.PCUICAst]
h':433 [binder, in MetaCoq.PCUIC.PCUICAst]
h':452 [binder, in MetaCoq.PCUIC.PCUICAst]
h':465 [binder, in MetaCoq.PCUIC.PCUICAst]
h':543 [binder, in MetaCoq.PCUIC.PCUICAst]
h':553 [binder, in MetaCoq.PCUIC.PCUICAst]
h':565 [binder, in MetaCoq.PCUIC.PCUICAst]
h':639 [binder, in MetaCoq.Translations.MiniHoTT]
h':647 [binder, in MetaCoq.Translations.MiniHoTT_paths]
H':65 [binder, in MetaCoq.Template.Reflect]
h':658 [binder, in MetaCoq.Translations.MiniHoTT]
h':666 [binder, in MetaCoq.Translations.MiniHoTT_paths]
H':68 [binder, in MetaCoq.Translations.times_bool_fun2]
h':686 [binder, in MetaCoq.Erasure.ErasureFunction]
H':69 [binder, in MetaCoq.Translations.times_bool_fun2]
H0:100 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
H0:1104 [binder, in MetaCoq.Template.utils.wGraph]
H0:1114 [binder, in MetaCoq.Template.utils.wGraph]
H0:1135 [binder, in MetaCoq.Template.utils.wGraph]
H0:1142 [binder, in MetaCoq.Template.utils.wGraph]
H0:1153 [binder, in MetaCoq.Template.utils.wGraph]
H0:1185 [binder, in MetaCoq.Template.utils.wGraph]
H0:1429 [binder, in MetaCoq.Translations.MiniHoTT]
H0:1437 [binder, in MetaCoq.Translations.MiniHoTT_paths]
H0:1444 [binder, in MetaCoq.Translations.MiniHoTT]
H0:1452 [binder, in MetaCoq.Translations.MiniHoTT_paths]
H0:1480 [binder, in MetaCoq.Translations.MiniHoTT]
H0:1488 [binder, in MetaCoq.Translations.MiniHoTT]
H0:1488 [binder, in MetaCoq.Translations.MiniHoTT_paths]
H0:1495 [binder, in MetaCoq.Translations.MiniHoTT]
H0:1496 [binder, in MetaCoq.Translations.MiniHoTT_paths]
H0:1503 [binder, in MetaCoq.Translations.MiniHoTT]
H0:1503 [binder, in MetaCoq.Translations.MiniHoTT_paths]
H0:1511 [binder, in MetaCoq.Translations.MiniHoTT_paths]
H0:1514 [binder, in MetaCoq.Translations.MiniHoTT]
H0:1522 [binder, in MetaCoq.Translations.MiniHoTT_paths]
H0:1526 [binder, in MetaCoq.Translations.MiniHoTT]
H0:1534 [binder, in MetaCoq.Translations.MiniHoTT_paths]
H0:1585 [binder, in MetaCoq.Translations.MiniHoTT]
H0:1593 [binder, in MetaCoq.Translations.MiniHoTT]
H0:1593 [binder, in MetaCoq.Translations.MiniHoTT_paths]
H0:1601 [binder, in MetaCoq.Translations.MiniHoTT]
H0:1601 [binder, in MetaCoq.Translations.MiniHoTT_paths]
H0:1607 [binder, in MetaCoq.Translations.MiniHoTT]
H0:1609 [binder, in MetaCoq.Translations.MiniHoTT_paths]
H0:1615 [binder, in MetaCoq.Translations.MiniHoTT_paths]
H0:1620 [binder, in MetaCoq.Translations.MiniHoTT]
H0:1628 [binder, in MetaCoq.Translations.MiniHoTT_paths]
H0:1633 [binder, in MetaCoq.Translations.MiniHoTT]
H0:1641 [binder, in MetaCoq.Translations.MiniHoTT_paths]
H0:1646 [binder, in MetaCoq.Translations.MiniHoTT]
H0:1654 [binder, in MetaCoq.Translations.MiniHoTT_paths]
H0:179 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
H0:193 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
H0:2329 [binder, in MetaCoq.Translations.MiniHoTT]
H0:2337 [binder, in MetaCoq.Translations.MiniHoTT_paths]
H0:2509 [binder, in MetaCoq.Translations.MiniHoTT]
H0:2517 [binder, in MetaCoq.Translations.MiniHoTT_paths]
H0:252 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
H0:2522 [binder, in MetaCoq.Translations.MiniHoTT]
H0:2530 [binder, in MetaCoq.Translations.MiniHoTT_paths]
H0:2598 [binder, in MetaCoq.Translations.MiniHoTT]
H0:2603 [binder, in MetaCoq.Translations.MiniHoTT]
H0:2606 [binder, in MetaCoq.Translations.MiniHoTT_paths]
H0:2611 [binder, in MetaCoq.Translations.MiniHoTT_paths]
H0:2940 [binder, in MetaCoq.Translations.MiniHoTT]
H0:2948 [binder, in MetaCoq.Translations.MiniHoTT_paths]
H0:2956 [binder, in MetaCoq.Translations.MiniHoTT]
H0:2964 [binder, in MetaCoq.Translations.MiniHoTT_paths]
H0:435 [binder, in MetaCoq.Template.Checker]
H0:528 [binder, in MetaCoq.PCUIC.PCUICConfluence]
H0:703 [binder, in MetaCoq.Template.common.uGraph]
H0:999 [binder, in MetaCoq.Template.utils.wGraph]
h1':240 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
h1':4410 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
H1:1000 [binder, in MetaCoq.Template.utils.wGraph]
H1:1000 [binder, in MetaCoq.Erasure.ErasureFunction]
H1:1016 [binder, in MetaCoq.Erasure.ErasureFunction]
H1:107 [binder, in MetaCoq.Template.utils.wGraph]
H1:1105 [binder, in MetaCoq.Template.utils.wGraph]
H1:1115 [binder, in MetaCoq.Template.utils.wGraph]
H1:1136 [binder, in MetaCoq.Template.utils.wGraph]
H1:1143 [binder, in MetaCoq.Template.utils.wGraph]
H1:117 [binder, in MetaCoq.Template.utils.wGraph]
H1:12 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
h1:1269 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
h1:1298 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
H1:1515 [binder, in MetaCoq.Translations.MiniHoTT]
H1:1523 [binder, in MetaCoq.Translations.MiniHoTT_paths]
h1:1526 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
H1:1527 [binder, in MetaCoq.Translations.MiniHoTT]
H1:1535 [binder, in MetaCoq.Translations.MiniHoTT_paths]
h1:1785 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
H1:18 [binder, in MetaCoq.Translations.times_bool_fun2]
H1:180 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
H1:194 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
h1:2151 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
H1:23 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
h1:2373 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
h1:2388 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
H1:2512 [binder, in MetaCoq.Translations.MiniHoTT]
H1:2520 [binder, in MetaCoq.Translations.MiniHoTT_paths]
H1:2526 [binder, in MetaCoq.Translations.MiniHoTT]
H1:253 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
H1:2534 [binder, in MetaCoq.Translations.MiniHoTT_paths]
h1:256 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
h1:2562 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
H1:291 [binder, in MetaCoq.Template.Universes]
H1:31 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
H1:39 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
h1:4420 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
h1:4570 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
H1:52 [binder, in MetaCoq.PCUIC.PCUICInversion]
h1:5236 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
H1:529 [binder, in MetaCoq.PCUIC.PCUICConfluence]
h1:5486 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
h1:5612 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
h1:5658 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
h1:5669 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
h1:5680 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
h1:5691 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
h1:5701 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
h1:5709 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
H1:6 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
H1:704 [binder, in MetaCoq.Template.common.uGraph]
h1:712 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
H1:85 [binder, in MetaCoq.PCUIC.PCUICInversion]
h1:88 [binder, in MetaCoq.Examples.tauto]
h1:90 [binder, in MetaCoq.Examples.tauto]
h2':241 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
h2':4411 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
h2':5629 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
H2:1001 [binder, in MetaCoq.Erasure.ErasureFunction]
H2:1007 [binder, in MetaCoq.Erasure.ErasureFunction]
H2:108 [binder, in MetaCoq.Template.utils.wGraph]
H2:109 [binder, in MetaCoq.SafeChecker.PCUICWfReduction]
H2:1106 [binder, in MetaCoq.Template.utils.wGraph]
H2:1116 [binder, in MetaCoq.Template.utils.wGraph]
H2:118 [binder, in MetaCoq.Template.utils.wGraph]
H2:14 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
H2:181 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
H2:195 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
h2:2157 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
h2:234 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
h2:2379 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
h2:2394 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
H2:25 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
h2:2565 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
h2:259 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
H2:292 [binder, in MetaCoq.Template.Universes]
H2:33 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
H2:35 [binder, in MetaCoq.Erasure.ErasureFunction]
H2:41 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
H2:429 [binder, in MetaCoq.Template.EtaExpand]
h2:4404 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
h2:4425 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
h2:4573 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
h2:5239 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
H2:53 [binder, in MetaCoq.PCUIC.PCUICInversion]
H2:530 [binder, in MetaCoq.PCUIC.PCUICConfluence]
h2:5489 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
h2:5615 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
h2:5661 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
h2:5672 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
h2:5683 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
h2:5695 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
h2:5703 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
h2:5711 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
h2:716 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
H2:8 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
H2:86 [binder, in MetaCoq.PCUIC.PCUICInversion]
h2:89 [binder, in MetaCoq.Examples.tauto]
H2:91 [binder, in MetaCoq.SafeChecker.PCUICWfReduction]
H2:994 [binder, in MetaCoq.Erasure.ErasureFunction]
H3:182 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
H3:196 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
H3:531 [binder, in MetaCoq.PCUIC.PCUICConfluence]
H3:87 [binder, in MetaCoq.PCUIC.PCUICInversion]
H4:183 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
H4:532 [binder, in MetaCoq.PCUIC.PCUICConfluence]
H5:184 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
H:1 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
H:1 [binder, in MetaCoq.PCUIC.PCUICCumulativity]
H:1 [binder, in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
H:1 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
H:100 [binder, in MetaCoq.Erasure.ERemoveParams]
H:1009 [binder, in MetaCoq.PCUIC.PCUICTyping]
H:101 [binder, in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
h:1011 [binder, in MetaCoq.Template.utils.All_Forall]
h:1011 [binder, in MetaCoq.Translations.MiniHoTT]
H:1011 [binder, in MetaCoq.PCUIC.PCUICTyping]
h:1012 [binder, in MetaCoq.Translations.MiniHoTT]
H:1012 [binder, in MetaCoq.PCUIC.PCUICTyping]
h:1015 [binder, in MetaCoq.Template.utils.All_Forall]
h:1019 [binder, in MetaCoq.Translations.MiniHoTT_paths]
H:102 [binder, in MetaCoq.Erasure.EConstructorsAsBlocks]
h:1020 [binder, in MetaCoq.Translations.MiniHoTT_paths]
H:103 [binder, in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
h:1045 [binder, in MetaCoq.Translations.MiniHoTT]
H:105 [binder, in MetaCoq.SafeChecker.PCUICWfReduction]
H:105 [binder, in MetaCoq.PCUIC.Bidirectional.BDUnique]
H:105 [binder, in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
h:1053 [binder, in MetaCoq.Translations.MiniHoTT_paths]
H:106 [binder, in MetaCoq.PCUIC.PCUICCumulativity]
H:106 [binder, in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
h:1063 [binder, in MetaCoq.Translations.MiniHoTT]
h:107 [binder, in MetaCoq.Translations.MiniHoTT]
h:1071 [binder, in MetaCoq.Translations.MiniHoTT_paths]
H:109 [binder, in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
h:1095 [binder, in MetaCoq.Translations.MiniHoTT]
H:1096 [binder, in MetaCoq.Template.utils.wGraph]
h:11 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
H:11 [binder, in MetaCoq.Translations.MiniHoTT_paths]
h:1102 [binder, in MetaCoq.Translations.MiniHoTT]
h:1103 [binder, in MetaCoq.Translations.MiniHoTT_paths]
h:1109 [binder, in MetaCoq.Template.utils.wGraph]
H:111 [binder, in MetaCoq.PCUIC.PCUICWeakeningEnv]
H:111 [binder, in MetaCoq.Template.utils.wGraph]
h:1110 [binder, in MetaCoq.Translations.MiniHoTT_paths]
h:1111 [binder, in MetaCoq.Translations.MiniHoTT]
H:1114 [binder, in MetaCoq.PCUIC.PCUICConfluence]
h:1119 [binder, in MetaCoq.Template.utils.wGraph]
h:1119 [binder, in MetaCoq.Translations.MiniHoTT]
h:1119 [binder, in MetaCoq.Translations.MiniHoTT_paths]
H:112 [binder, in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
h:1125 [binder, in MetaCoq.Translations.MiniHoTT]
h:1127 [binder, in MetaCoq.Translations.MiniHoTT_paths]
H:113 [binder, in MetaCoq.PCUIC.PCUICCumulativity]
h:1133 [binder, in MetaCoq.Translations.MiniHoTT_paths]
H:1134 [binder, in MetaCoq.Template.utils.wGraph]
h:114 [binder, in MetaCoq.Translations.MiniHoTT]
H:1141 [binder, in MetaCoq.Template.utils.wGraph]
h:1143 [binder, in MetaCoq.Translations.MiniHoTT]
h:1146 [binder, in MetaCoq.Translations.MiniHoTT]
h:1149 [binder, in MetaCoq.Translations.MiniHoTT]
H:115 [binder, in MetaCoq.PCUIC.Syntax.PCUICViews]
h:115 [binder, in MetaCoq.Translations.MiniHoTT_paths]
H:115 [binder, in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
H:115 [binder, in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
h:1151 [binder, in MetaCoq.Translations.MiniHoTT_paths]
H:1152 [binder, in MetaCoq.Template.utils.wGraph]
h:1154 [binder, in MetaCoq.Translations.MiniHoTT_paths]
h:1155 [binder, in MetaCoq.Translations.MiniHoTT]
h:1157 [binder, in MetaCoq.Translations.MiniHoTT_paths]
h:1161 [binder, in MetaCoq.Translations.MiniHoTT]
h:1163 [binder, in MetaCoq.Translations.MiniHoTT_paths]
h:1169 [binder, in MetaCoq.Translations.MiniHoTT_paths]
H:117 [binder, in MetaCoq.PCUIC.PCUICWeakeningEnv]
H:117 [binder, in MetaCoq.PCUIC.Bidirectional.BDUnique]
h:1171 [binder, in MetaCoq.Translations.MiniHoTT]
h:1179 [binder, in MetaCoq.Translations.MiniHoTT_paths]
H:118 [binder, in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
H:118 [binder, in MetaCoq.PCUIC.PCUICCumulativity]
h:1182 [binder, in MetaCoq.Translations.MiniHoTT]
H:1184 [binder, in MetaCoq.Template.utils.wGraph]
h:119 [binder, in MetaCoq.Translations.MiniHoTT]
H:119 [binder, in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
h:1190 [binder, in MetaCoq.Translations.MiniHoTT_paths]
H:1190 [binder, in MetaCoq.PCUIC.PCUICReduction]
H:12 [binder, in MetaCoq.PCUIC.PCUICWeakeningEnv]
H:12 [binder, in MetaCoq.Template.utils.wGraph]
H:121 [binder, in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
h:122 [binder, in MetaCoq.Translations.MiniHoTT_paths]
h:123 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
H:123 [binder, in MetaCoq.Template.utils.wGraph]
H:124 [binder, in MetaCoq.PCUIC.PCUICWeakeningEnv]
H:124 [binder, in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
H:125 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
h:1256 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
H:1259 [binder, in MetaCoq.Template.Typing]
H:126 [binder, in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
H:127 [binder, in MetaCoq.PCUIC.PCUICProgress]
h:127 [binder, in MetaCoq.Translations.MiniHoTT_paths]
H:127 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
H:1276 [binder, in MetaCoq.Template.Typing]
H:128 [binder, in MetaCoq.Translations.param_binary]
H:1283 [binder, in MetaCoq.Template.Typing]
h:1285 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
H:129 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
H:129 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
H:129 [binder, in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
H:1291 [binder, in MetaCoq.Template.Typing]
H:13 [binder, in MetaCoq.Template.TypingWf]
H:130 [binder, in MetaCoq.PCUIC.Bidirectional.BDUnique]
h:1305 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
H:1308 [binder, in MetaCoq.Template.Typing]
H:1319 [binder, in MetaCoq.Template.Typing]
H:132 [binder, in MetaCoq.Template.utils.wGraph]
H:132 [binder, in MetaCoq.Template.monad_utils]
H:1321 [binder, in MetaCoq.Template.Typing]
H:1322 [binder, in MetaCoq.Template.Typing]
H:1323 [binder, in MetaCoq.Template.Typing]
h:1326 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
h:1332 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
h:1338 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
H:134 [binder, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
H:1341 [binder, in MetaCoq.Template.Typing]
h:1342 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
h:1346 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
H:135 [binder, in MetaCoq.Template.utils.wGraph]
h:1351 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
h:1355 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
H:1357 [binder, in MetaCoq.Translations.MiniHoTT]
h:1359 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
H:1361 [binder, in MetaCoq.Translations.MiniHoTT]
h:1363 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
H:1365 [binder, in MetaCoq.Translations.MiniHoTT_paths]
h:1367 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
H:1369 [binder, in MetaCoq.Translations.MiniHoTT]
H:1369 [binder, in MetaCoq.Translations.MiniHoTT_paths]
H:137 [binder, in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
H:1377 [binder, in MetaCoq.Translations.MiniHoTT_paths]
H:138 [binder, in MetaCoq.Template.utils.wGraph]
h:1384 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
h:1388 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
H:14 [binder, in MetaCoq.Template.utils.MCUtils]
H:14 [binder, in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
H:141 [binder, in MetaCoq.SafeChecker.PCUICSafeChecker]
H:141 [binder, in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
H:1416 [binder, in MetaCoq.Translations.MiniHoTT]
H:142 [binder, in MetaCoq.Template.utils.wGraph]
H:142 [binder, in MetaCoq.PCUIC.Bidirectional.BDUnique]
H:1424 [binder, in MetaCoq.Translations.MiniHoTT_paths]
H:1426 [binder, in MetaCoq.Translations.MiniHoTT]
H:1434 [binder, in MetaCoq.Translations.MiniHoTT_paths]
H:144 [binder, in MetaCoq.PCUIC.Typing.PCUICClosedTyp]
H:1443 [binder, in MetaCoq.Translations.MiniHoTT]
h:1445 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
H:145 [binder, in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
H:1451 [binder, in MetaCoq.Translations.MiniHoTT_paths]
H:1456 [binder, in MetaCoq.Translations.MiniHoTT]
H:146 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
H:146 [binder, in MetaCoq.Template.TermEquality]
H:146 [binder, in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
H:146 [binder, in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
H:1464 [binder, in MetaCoq.Translations.MiniHoTT_paths]
h:1466 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
H:147 [binder, in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
h:1474 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
H:1479 [binder, in MetaCoq.Translations.MiniHoTT]
H:148 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
h:1481 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
h:1486 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
H:1487 [binder, in MetaCoq.Translations.MiniHoTT]
H:1487 [binder, in MetaCoq.Translations.MiniHoTT_paths]
h:1493 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
H:1494 [binder, in MetaCoq.Translations.MiniHoTT]
H:1495 [binder, in MetaCoq.Translations.MiniHoTT_paths]
H:1502 [binder, in MetaCoq.Translations.MiniHoTT]
H:1502 [binder, in MetaCoq.Translations.MiniHoTT_paths]
H:1508 [binder, in MetaCoq.Erasure.ErasureFunction]
H:151 [binder, in MetaCoq.PCUIC.PCUICCumulativitySpec]
H:151 [binder, in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
h:1510 [binder, in MetaCoq.Translations.MiniHoTT]
H:1510 [binder, in MetaCoq.Translations.MiniHoTT_paths]
H:1513 [binder, in MetaCoq.Translations.MiniHoTT]
h:1516 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
h:1518 [binder, in MetaCoq.Translations.MiniHoTT_paths]
H:152 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
H:1521 [binder, in MetaCoq.Translations.MiniHoTT_paths]
h:1522 [binder, in MetaCoq.Translations.MiniHoTT]
H:1525 [binder, in MetaCoq.Translations.MiniHoTT]
H:153 [binder, in MetaCoq.Translations.times_bool_fun]
H:153 [binder, in MetaCoq.PCUIC.Bidirectional.BDUnique]
h:1530 [binder, in MetaCoq.Translations.MiniHoTT_paths]
H:1533 [binder, in MetaCoq.Translations.MiniHoTT_paths]
H:154 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
h:155 [binder, in MetaCoq.Translations.MiniHoTT]
H:155 [binder, in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
h:1552 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
H:1556 [binder, in MetaCoq.Translations.MiniHoTT]
H:156 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
H:1563 [binder, in MetaCoq.Translations.MiniHoTT]
H:1564 [binder, in MetaCoq.Translations.MiniHoTT_paths]
H:1570 [binder, in MetaCoq.Translations.MiniHoTT]
H:1571 [binder, in MetaCoq.Translations.MiniHoTT_paths]
H:1577 [binder, in MetaCoq.Translations.MiniHoTT]
H:1578 [binder, in MetaCoq.Translations.MiniHoTT_paths]
H:158 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
H:158 [binder, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
H:158 [binder, in MetaCoq.SafeChecker.PCUICWfEnv]
H:1584 [binder, in MetaCoq.Translations.MiniHoTT]
H:1585 [binder, in MetaCoq.Translations.MiniHoTT_paths]
H:1589 [binder, in MetaCoq.Translations.MiniHoTT]
H:159 [binder, in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
H:1592 [binder, in MetaCoq.Translations.MiniHoTT]
H:1592 [binder, in MetaCoq.Translations.MiniHoTT_paths]
H:1597 [binder, in MetaCoq.Translations.MiniHoTT_paths]
H:1600 [binder, in MetaCoq.Translations.MiniHoTT]
H:1600 [binder, in MetaCoq.Translations.MiniHoTT_paths]
H:1602 [binder, in MetaCoq.Translations.MiniHoTT]
H:1608 [binder, in MetaCoq.Translations.MiniHoTT_paths]
H:1610 [binder, in MetaCoq.Translations.MiniHoTT_paths]
h:1611 [binder, in MetaCoq.Translations.MiniHoTT]
h:1613 [binder, in MetaCoq.Translations.MiniHoTT]
H:1615 [binder, in MetaCoq.Translations.MiniHoTT]
h:1618 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
h:1619 [binder, in MetaCoq.Translations.MiniHoTT_paths]
H:162 [binder, in MetaCoq.Template.common.uGraph]
h:1621 [binder, in MetaCoq.Translations.MiniHoTT_paths]
H:1622 [binder, in MetaCoq.Translations.MiniHoTT]
H:1623 [binder, in MetaCoq.Translations.MiniHoTT_paths]
H:1628 [binder, in MetaCoq.Translations.MiniHoTT]
h:163 [binder, in MetaCoq.Translations.MiniHoTT_paths]
H:1630 [binder, in MetaCoq.Translations.MiniHoTT_paths]
H:1636 [binder, in MetaCoq.Translations.MiniHoTT_paths]
h:1637 [binder, in MetaCoq.Translations.MiniHoTT]
h:1639 [binder, in MetaCoq.Translations.MiniHoTT]
H:164 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
H:164 [binder, in MetaCoq.SafeChecker.PCUICWfEnv]
H:1641 [binder, in MetaCoq.Translations.MiniHoTT]
h:1645 [binder, in MetaCoq.Translations.MiniHoTT_paths]
h:1647 [binder, in MetaCoq.Translations.MiniHoTT_paths]
H:1648 [binder, in MetaCoq.Translations.MiniHoTT]
H:1649 [binder, in MetaCoq.Translations.MiniHoTT_paths]
H:165 [binder, in MetaCoq.Template.TermEquality]
H:165 [binder, in MetaCoq.Template.common.uGraph]
H:165 [binder, in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
H:1656 [binder, in MetaCoq.Translations.MiniHoTT_paths]
h:1658 [binder, in MetaCoq.Translations.MiniHoTT]
H:166 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
h:1666 [binder, in MetaCoq.Translations.MiniHoTT_paths]
h:1667 [binder, in MetaCoq.Translations.MiniHoTT]
H:167 [binder, in MetaCoq.Translations.MiniHoTT]
h:1673 [binder, in MetaCoq.Translations.MiniHoTT]
h:1675 [binder, in MetaCoq.Translations.MiniHoTT_paths]
H:1677 [binder, in MetaCoq.Translations.MiniHoTT]
H:168 [binder, in MetaCoq.Template.common.uGraph]
h:1681 [binder, in MetaCoq.Translations.MiniHoTT_paths]
H:1685 [binder, in MetaCoq.Translations.MiniHoTT_paths]
H:1686 [binder, in MetaCoq.Translations.MiniHoTT]
H:169 [binder, in MetaCoq.Template.TermEquality]
H:1694 [binder, in MetaCoq.Translations.MiniHoTT_paths]
H:1695 [binder, in MetaCoq.Translations.MiniHoTT]
H:17 [binder, in MetaCoq.PCUIC.PCUICProgress]
H:17 [binder, in MetaCoq.PCUIC.PCUICWeakeningEnv]
H:170 [binder, in MetaCoq.Erasure.EInduction]
H:1703 [binder, in MetaCoq.Translations.MiniHoTT_paths]
H:171 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
H:1710 [binder, in MetaCoq.Template.utils.All_Forall]
H:173 [binder, in MetaCoq.Translations.MiniHoTT]
H:174 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
H:174 [binder, in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
H:175 [binder, in MetaCoq.Template.Checker]
H:175 [binder, in MetaCoq.Translations.MiniHoTT_paths]
H:175 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
H:176 [binder, in MetaCoq.Erasure.EInduction]
H:176 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
H:176 [binder, in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
h:1775 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
H:178 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
H:179 [binder, in MetaCoq.Erasure.EInduction]
H:1795 [binder, in MetaCoq.Translations.MiniHoTT]
H:1803 [binder, in MetaCoq.Translations.MiniHoTT_paths]
H:1806 [binder, in MetaCoq.Translations.MiniHoTT]
H:181 [binder, in MetaCoq.Erasure.EInduction]
H:181 [binder, in MetaCoq.Translations.MiniHoTT_paths]
H:1814 [binder, in MetaCoq.Translations.MiniHoTT_paths]
H:182 [binder, in MetaCoq.Template.common.uGraph]
h:183 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
H:184 [binder, in MetaCoq.Erasure.EInduction]
H:184 [binder, in MetaCoq.PCUIC.PCUICEquality]
h:185 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
H:186 [binder, in MetaCoq.Erasure.EInduction]
H:187 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
H:188 [binder, in MetaCoq.Template.Checker]
h:1898 [binder, in MetaCoq.Translations.MiniHoTT]
H:190 [binder, in MetaCoq.PCUIC.Syntax.PCUICDepth]
h:1906 [binder, in MetaCoq.Translations.MiniHoTT]
h:1906 [binder, in MetaCoq.Translations.MiniHoTT_paths]
H:191 [binder, in MetaCoq.PCUIC.PCUICEquality]
h:1914 [binder, in MetaCoq.Translations.MiniHoTT_paths]
H:192 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
H:193 [binder, in MetaCoq.PCUIC.PCUICInductives]
h:1944 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
H:197 [binder, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
H:197 [binder, in MetaCoq.PCUIC.PCUICEquality]
H:197 [binder, in MetaCoq.Erasure.EWcbvEvalInd]
H:197 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
H:1973 [binder, in MetaCoq.Template.utils.All_Forall]
H:198 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
H:198 [binder, in MetaCoq.SafeChecker.PCUICWfEnv]
H:199 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
H:199 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
H:2 [binder, in MetaCoq.PCUIC.Syntax.PCUICUnivSubst]
H:2 [binder, in MetaCoq.Template.ReflectAst]
H:200 [binder, in MetaCoq.Erasure.EWcbvEvalInd]
H:201 [binder, in MetaCoq.Template.Checker]
H:205 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
H:205 [binder, in MetaCoq.PCUIC.PCUICEquality]
H:205 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
h:2063 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
h:2089 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
h:2097 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
h:2108 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
H:211 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
H:211 [binder, in MetaCoq.PCUIC.PCUICEquality]
h:2129 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
H:214 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
H:2164 [binder, in MetaCoq.Translations.MiniHoTT]
H:2172 [binder, in MetaCoq.Translations.MiniHoTT]
H:2172 [binder, in MetaCoq.Translations.MiniHoTT_paths]
H:2178 [binder, in MetaCoq.Translations.MiniHoTT]
H:2180 [binder, in MetaCoq.Translations.MiniHoTT_paths]
H:2186 [binder, in MetaCoq.Translations.MiniHoTT]
H:2186 [binder, in MetaCoq.Translations.MiniHoTT_paths]
H:219 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
H:2192 [binder, in MetaCoq.Translations.MiniHoTT]
H:2194 [binder, in MetaCoq.Translations.MiniHoTT_paths]
h:22 [binder, in MetaCoq.Examples.tauto]
H:22 [binder, in MetaCoq.Template.Reflect]
H:22 [binder, in MetaCoq.PCUIC.PCUICGuardCondition]
H:22 [binder, in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
H:2200 [binder, in MetaCoq.Translations.MiniHoTT]
H:2200 [binder, in MetaCoq.Translations.MiniHoTT_paths]
H:2206 [binder, in MetaCoq.Translations.MiniHoTT]
H:2208 [binder, in MetaCoq.Translations.MiniHoTT_paths]
H:2214 [binder, in MetaCoq.Translations.MiniHoTT]
H:2214 [binder, in MetaCoq.Translations.MiniHoTT_paths]
H:2222 [binder, in MetaCoq.Translations.MiniHoTT_paths]
H:223 [binder, in MetaCoq.Template.TermEquality]
H:226 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
H:227 [binder, in MetaCoq.PCUIC.Bidirectional.BDTyping]
H:228 [binder, in MetaCoq.Template.TermEquality]
H:2297 [binder, in MetaCoq.Translations.MiniHoTT]
h:23 [binder, in MetaCoq.Examples.tauto]
H:23 [binder, in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
H:2304 [binder, in MetaCoq.Translations.MiniHoTT]
H:2305 [binder, in MetaCoq.Translations.MiniHoTT_paths]
H:2311 [binder, in MetaCoq.Translations.MiniHoTT]
H:2312 [binder, in MetaCoq.Translations.MiniHoTT_paths]
h:2317 [binder, in MetaCoq.Translations.MiniHoTT]
H:2319 [binder, in MetaCoq.Translations.MiniHoTT_paths]
h:2325 [binder, in MetaCoq.Translations.MiniHoTT_paths]
H:234 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
h:2346 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
h:2349 [binder, in MetaCoq.Translations.MiniHoTT]
H:235 [binder, in MetaCoq.Template.TermEquality]
h:2357 [binder, in MetaCoq.Translations.MiniHoTT_paths]
h:2362 [binder, in MetaCoq.Translations.MiniHoTT]
h:2364 [binder, in MetaCoq.Translations.MiniHoTT]
H:237 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
h:2370 [binder, in MetaCoq.Translations.MiniHoTT_paths]
h:2372 [binder, in MetaCoq.Translations.MiniHoTT_paths]
H:238 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
H:240 [binder, in MetaCoq.Template.TermEquality]
h:241 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
H:244 [binder, in MetaCoq.Template.common.uGraph]
h:245 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
H:246 [binder, in MetaCoq.Template.common.uGraph]
H:248 [binder, in MetaCoq.PCUIC.PCUICAst]
h:2486 [binder, in MetaCoq.Translations.MiniHoTT]
h:2488 [binder, in MetaCoq.Template.utils.All_Forall]
H:249 [binder, in MetaCoq.Template.TermEquality]
h:249 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
H:249 [binder, in MetaCoq.PCUIC.Syntax.PCUICInduction]
H:249 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
h:2494 [binder, in MetaCoq.Translations.MiniHoTT_paths]
H:25 [binder, in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
H:251 [binder, in MetaCoq.PCUIC.PCUICContextConversion]
H:2559 [binder, in MetaCoq.Template.utils.All_Forall]
H:256 [binder, in MetaCoq.Template.TermEquality]
h:2567 [binder, in MetaCoq.Translations.MiniHoTT]
h:2572 [binder, in MetaCoq.Translations.MiniHoTT]
h:2575 [binder, in MetaCoq.Translations.MiniHoTT_paths]
H:258 [binder, in MetaCoq.PCUIC.PCUICTyping]
h:2580 [binder, in MetaCoq.Translations.MiniHoTT_paths]
h:2592 [binder, in MetaCoq.Translations.MiniHoTT]
H:26 [binder, in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
h:2600 [binder, in MetaCoq.Translations.MiniHoTT_paths]
H:262 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
H:263 [binder, in MetaCoq.PCUIC.Syntax.PCUICDepth]
H:266 [binder, in MetaCoq.Erasure.EWcbvEvalEtaInd]
H:266 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
H:267 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
h:2681 [binder, in MetaCoq.Translations.MiniHoTT]
h:2689 [binder, in MetaCoq.Translations.MiniHoTT_paths]
H:269 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
h:269 [binder, in MetaCoq.PCUIC.PCUICAst]
H:269 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
H:271 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
H:273 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
H:274 [binder, in MetaCoq.Template.BasicAst]
H:276 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
H:277 [binder, in MetaCoq.PCUIC.PCUICProgress]
H:278 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
h:28 [binder, in MetaCoq.Examples.tauto]
H:28 [binder, in MetaCoq.Template.Reflect]
H:280 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
H:280 [binder, in MetaCoq.Template.Checker]
H:280 [binder, in MetaCoq.PCUIC.PCUICTyping]
H:282 [binder, in MetaCoq.Erasure.EEtaExpandedFix]
H:285 [binder, in MetaCoq.Template.EnvironmentTyping]
h:288 [binder, in MetaCoq.PCUIC.PCUICAst]
H:288 [binder, in MetaCoq.Template.Checker]
H:29 [binder, in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
H:29 [binder, in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
H:290 [binder, in MetaCoq.Template.Checker]
H:290 [binder, in MetaCoq.PCUIC.PCUICTyping]
H:292 [binder, in MetaCoq.Template.Checker]
H:292 [binder, in MetaCoq.PCUIC.PCUICTyping]
H:2937 [binder, in MetaCoq.Translations.MiniHoTT]
H:294 [binder, in MetaCoq.Template.BasicAst]
H:294 [binder, in MetaCoq.PCUIC.PCUICTyping]
H:2945 [binder, in MetaCoq.Translations.MiniHoTT_paths]
H:2952 [binder, in MetaCoq.Translations.MiniHoTT]
H:2960 [binder, in MetaCoq.Translations.MiniHoTT_paths]
H:2972 [binder, in MetaCoq.Translations.MiniHoTT]
H:2978 [binder, in MetaCoq.Translations.MiniHoTT]
H:298 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
H:298 [binder, in MetaCoq.Template.EnvironmentTyping]
H:2980 [binder, in MetaCoq.Translations.MiniHoTT_paths]
H:2981 [binder, in MetaCoq.Translations.MiniHoTT]
H:2986 [binder, in MetaCoq.Translations.MiniHoTT_paths]
H:2989 [binder, in MetaCoq.Translations.MiniHoTT_paths]
H:299 [binder, in MetaCoq.PCUIC.PCUICTyping]
h:3 [binder, in MetaCoq.Template.ReflectAst]
H:3 [binder, in MetaCoq.Template.TypingWf]
H:303 [binder, in MetaCoq.PCUIC.PCUICTyping]
H:306 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
H:308 [binder, in MetaCoq.PCUIC.PCUICTyping]
H:31 [binder, in MetaCoq.Erasure.ErasureFunction]
H:313 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
H:32 [binder, in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
H:32 [binder, in MetaCoq.PCUIC.PCUICProgress]
h:321 [binder, in MetaCoq.PCUIC.PCUICAst]
H:323 [binder, in MetaCoq.PCUIC.PCUICTyping]
H:324 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
H:331 [binder, in MetaCoq.PCUIC.PCUICTyping]
H:334 [binder, in MetaCoq.PCUIC.PCUICTyping]
H:336 [binder, in MetaCoq.PCUIC.utils.PCUICAstUtils]
H:341 [binder, in MetaCoq.PCUIC.PCUICWcbvEval]
H:341 [binder, in MetaCoq.PCUIC.PCUICTyping]
H:343 [binder, in MetaCoq.PCUIC.PCUICTyping]
h:348 [binder, in MetaCoq.SafeChecker.PCUICSafeReduce]
H:35 [binder, in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
H:353 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
H:354 [binder, in MetaCoq.PCUIC.PCUICTyping]
H:359 [binder, in MetaCoq.PCUIC.PCUICTyping]
H:36 [binder, in MetaCoq.Template.utils.ReflectEq]
H:361 [binder, in MetaCoq.PCUIC.PCUICSubstitution]
h:361 [binder, in MetaCoq.PCUIC.PCUICAst]
h:364 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
h:366 [binder, in MetaCoq.PCUIC.PCUICAst]
H:37 [binder, in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
H:372 [binder, in MetaCoq.Erasure.EWcbvEval]
H:38 [binder, in MetaCoq.Examples.tauto]
H:38 [binder, in MetaCoq.PCUIC.Bidirectional.BDUnique]
H:388 [binder, in MetaCoq.Template.utils.wGraph]
H:39 [binder, in MetaCoq.PCUIC.PCUICTyping]
H:394 [binder, in MetaCoq.Erasure.EWcbvEval]
H:397 [binder, in MetaCoq.Erasure.EWcbvEval]
H:398 [binder, in MetaCoq.Erasure.EWcbvEval]
H:4 [binder, in MetaCoq.Template.utils.wGraph]
h:406 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
H:407 [binder, in MetaCoq.PCUIC.PCUICEquality]
h:407 [binder, in MetaCoq.PCUIC.PCUICAst]
H:409 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
h:414 [binder, in MetaCoq.PCUIC.PCUICAst]
H:415 [binder, in MetaCoq.PCUIC.PCUICEquality]
H:42 [binder, in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
H:423 [binder, in MetaCoq.PCUIC.PCUICEquality]
h:424 [binder, in MetaCoq.PCUIC.PCUICAst]
h:432 [binder, in MetaCoq.PCUIC.PCUICAst]
H:434 [binder, in MetaCoq.Template.Checker]
H:44 [binder, in MetaCoq.PCUIC.PCUICGuardCondition]
H:440 [binder, in MetaCoq.PCUIC.PCUICTyping]
H:450 [binder, in MetaCoq.Template.Typing]
h:451 [binder, in MetaCoq.PCUIC.PCUICAst]
H:455 [binder, in MetaCoq.Template.Typing]
H:460 [binder, in MetaCoq.Template.Typing]
h:464 [binder, in MetaCoq.PCUIC.PCUICAst]
h:4671 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
h:47 [binder, in MetaCoq.Examples.tauto]
H:47 [binder, in MetaCoq.PCUIC.Bidirectional.BDUnique]
H:474 [binder, in MetaCoq.Template.Typing]
H:478 [binder, in MetaCoq.Template.Typing]
H:482 [binder, in MetaCoq.Template.Typing]
h:4867 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
h:4876 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
h:488 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
h:4883 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
H:489 [binder, in MetaCoq.Template.Typing]
H:49 [binder, in MetaCoq.PCUIC.PCUICInversion]
H:49 [binder, in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
H:49 [binder, in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
H:494 [binder, in MetaCoq.Template.Typing]
h:497 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
H:50 [binder, in MetaCoq.PCUIC.PCUICProgress]
h:505 [binder, in MetaCoq.Examples.tauto]
h:506 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
h:507 [binder, in MetaCoq.Examples.tauto]
h:5092 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
h:5099 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
H:51 [binder, in MetaCoq.Template.utils.ReflectEq]
h:5104 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
h:515 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
h:5199 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
h:5207 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
h:5215 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
h:5221 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
h:5229 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
H:523 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
h:524 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
H:527 [binder, in MetaCoq.PCUIC.PCUICConfluence]
H:53 [binder, in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
h:53 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
H:539 [binder, in MetaCoq.Template.utils.wGraph]
h:54 [binder, in MetaCoq.Examples.tauto]
h:542 [binder, in MetaCoq.PCUIC.PCUICAst]
H:55 [binder, in MetaCoq.PCUIC.Bidirectional.BDUnique]
H:55 [binder, in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
H:55 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
h:552 [binder, in MetaCoq.PCUIC.PCUICAst]
H:553 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
H:553 [binder, in MetaCoq.Template.utils.wGraph]
H:554 [binder, in MetaCoq.Template.utils.wGraph]
H:56 [binder, in MetaCoq.Template.LiftSubst]
h:564 [binder, in MetaCoq.PCUIC.PCUICAst]
H:567 [binder, in MetaCoq.PCUIC.Syntax.PCUICPosition]
h:58 [binder, in MetaCoq.Examples.tauto]
H:58 [binder, in MetaCoq.PCUIC.Typing.PCUICWeakeningTyp]
H:584 [binder, in MetaCoq.Template.utils.wGraph]
H:598 [binder, in MetaCoq.Template.Typing]
H:6 [binder, in MetaCoq.PCUIC.PCUICCumulativity]
H:60 [binder, in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
H:601 [binder, in MetaCoq.Template.Universes]
H:608 [binder, in MetaCoq.Template.Universes]
H:61 [binder, in MetaCoq.PCUIC.PCUICTyping]
h:61 [binder, in MetaCoq.Template.monad_utils]
H:61 [binder, in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
H:62 [binder, in MetaCoq.Template.utils.MCOption]
H:63 [binder, in MetaCoq.PCUIC.Bidirectional.BDUnique]
H:63 [binder, in MetaCoq.PCUIC.PCUICGuardCondition]
h:638 [binder, in MetaCoq.Translations.MiniHoTT]
h:64 [binder, in MetaCoq.Examples.tauto]
H:64 [binder, in MetaCoq.Template.Reflect]
H:64 [binder, in MetaCoq.Template.LiftSubst]
H:64 [binder, in MetaCoq.PCUIC.PCUICGuardCondition]
h:640 [binder, in MetaCoq.Template.utils.All_Forall]
h:643 [binder, in MetaCoq.Template.utils.All_Forall]
H:645 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
h:646 [binder, in MetaCoq.Translations.MiniHoTT]
h:646 [binder, in MetaCoq.Translations.MiniHoTT_paths]
H:65 [binder, in MetaCoq.PCUIC.PCUICCumulProp]
H:65 [binder, in MetaCoq.PCUIC.PCUICGuardCondition]
h:654 [binder, in MetaCoq.Translations.MiniHoTT_paths]
h:657 [binder, in MetaCoq.Translations.MiniHoTT]
H:659 [binder, in MetaCoq.Template.common.uGraph]
H:66 [binder, in MetaCoq.Template.utils.wGraph]
H:66 [binder, in MetaCoq.PCUIC.PCUICGuardCondition]
H:66 [binder, in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
h:664 [binder, in MetaCoq.Translations.MiniHoTT]
h:665 [binder, in MetaCoq.Translations.MiniHoTT_paths]
H:67 [binder, in MetaCoq.PCUIC.PCUICGuardCondition]
H:672 [binder, in MetaCoq.Template.common.uGraph]
h:672 [binder, in MetaCoq.Translations.MiniHoTT_paths]
h:676 [binder, in MetaCoq.Translations.MiniHoTT]
H:68 [binder, in MetaCoq.PCUIC.PCUICGuardCondition]
H:68 [binder, in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
H:680 [binder, in MetaCoq.Template.common.uGraph]
h:684 [binder, in MetaCoq.Translations.MiniHoTT_paths]
h:685 [binder, in MetaCoq.Erasure.ErasureFunction]
h:685 [binder, in MetaCoq.Translations.MiniHoTT]
H:688 [binder, in MetaCoq.Template.common.uGraph]
H:693 [binder, in MetaCoq.Template.common.uGraph]
h:693 [binder, in MetaCoq.Translations.MiniHoTT_paths]
h:697 [binder, in MetaCoq.Translations.MiniHoTT]
H:7 [binder, in MetaCoq.PCUIC.PCUICWeakeningEnv]
H:7 [binder, in MetaCoq.Template.utils.MCUtils]
H:70 [binder, in MetaCoq.PCUIC.PCUICWeakeningEnv]
H:70 [binder, in MetaCoq.Template.utils.wGraph]
H:701 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
H:702 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
H:702 [binder, in MetaCoq.Template.common.uGraph]
H:705 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
h:705 [binder, in MetaCoq.Translations.MiniHoTT_paths]
h:707 [binder, in MetaCoq.Translations.MiniHoTT]
H:709 [binder, in MetaCoq.Template.Typing]
H:71 [binder, in MetaCoq.PCUIC.Bidirectional.BDUnique]
H:71 [binder, in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
H:710 [binder, in MetaCoq.Template.EnvironmentTyping]
H:712 [binder, in MetaCoq.Template.EnvironmentTyping]
h:715 [binder, in MetaCoq.Translations.MiniHoTT_paths]
H:716 [binder, in MetaCoq.Template.EnvironmentTyping]
H:718 [binder, in MetaCoq.Template.EnvironmentTyping]
H:722 [binder, in MetaCoq.Template.EnvironmentTyping]
H:728 [binder, in MetaCoq.Template.EnvironmentTyping]
H:73 [binder, in MetaCoq.Template.utils.MCRelations]
H:730 [binder, in MetaCoq.Template.EnvironmentTyping]
H:736 [binder, in MetaCoq.Template.Typing]
H:74 [binder, in MetaCoq.Template.utils.wGraph]
H:75 [binder, in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
H:76 [binder, in MetaCoq.Template.utils.MCRelations]
H:76 [binder, in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
H:764 [binder, in MetaCoq.Template.Typing]
H:769 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
H:77 [binder, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
H:77 [binder, in MetaCoq.Template.utils.ReflectEq]
h:77 [binder, in MetaCoq.PCUIC.PCUICAst]
H:774 [binder, in MetaCoq.Template.Typing]
H:776 [binder, in MetaCoq.Template.utils.MCList]
H:776 [binder, in MetaCoq.Template.Typing]
h:776 [binder, in MetaCoq.Translations.MiniHoTT]
H:777 [binder, in MetaCoq.Template.Typing]
h:779 [binder, in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
h:78 [binder, in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
H:78 [binder, in MetaCoq.Template.utils.wGraph]
H:782 [binder, in MetaCoq.Template.Typing]
H:784 [binder, in MetaCoq.Template.Typing]
h:784 [binder, in MetaCoq.Translations.MiniHoTT_paths]
H:787 [binder, in MetaCoq.Template.Typing]
H:788 [binder, in MetaCoq.Template.utils.MCList]
H:79 [binder, in MetaCoq.Template.utils.MCRelations]
H:79 [binder, in MetaCoq.PCUIC.Bidirectional.BDUnique]
H:8 [binder, in MetaCoq.Template.utils.wGraph]
H:80 [binder, in MetaCoq.PCUIC.PCUICInversion]
H:804 [binder, in MetaCoq.Template.Typing]
H:81 [binder, in MetaCoq.PCUIC.PCUICTyping]
H:81 [binder, in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
H:81 [binder, in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
H:813 [binder, in MetaCoq.Template.Typing]
h:816 [binder, in MetaCoq.Template.utils.All_Forall]
h:82 [binder, in MetaCoq.PCUIC.PCUICParallelReduction]
h:820 [binder, in MetaCoq.Template.utils.All_Forall]
H:820 [binder, in MetaCoq.Template.Typing]
H:825 [binder, in MetaCoq.Template.Typing]
H:829 [binder, in MetaCoq.Template.Typing]
H:83 [binder, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
H:83 [binder, in MetaCoq.Template.utils.ReflectEq]
H:842 [binder, in MetaCoq.Template.utils.MCList]
h:85 [binder, in MetaCoq.Examples.tauto]
H:852 [binder, in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
H:86 [binder, in MetaCoq.Erasure.EConstructorsAsBlocks]
H:86 [binder, in MetaCoq.Erasure.ERemoveParams]
H:86 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
H:860 [binder, in MetaCoq.Template.utils.MCList]
H:87 [binder, in MetaCoq.SafeChecker.PCUICWfReduction]
H:87 [binder, in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
H:88 [binder, in MetaCoq.Erasure.EConstructorsAsBlocks]
H:88 [binder, in MetaCoq.Template.common.uGraph]
H:88 [binder, in MetaCoq.Erasure.ERemoveParams]
H:88 [binder, in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
H:89 [binder, in MetaCoq.PCUIC.PCUICCumulativity]
H:89 [binder, in MetaCoq.Template.EnvironmentTyping]
H:89 [binder, in MetaCoq.Erasure.EEtaExpanded]
H:90 [binder, in MetaCoq.Erasure.ERemoveParams]
H:904 [binder, in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
H:91 [binder, in MetaCoq.Erasure.EInduction]
H:91 [binder, in MetaCoq.Erasure.EConstructorsAsBlocks]
H:91 [binder, in MetaCoq.Erasure.EEtaExpanded]
H:91 [binder, in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
H:915 [binder, in MetaCoq.Template.Typing]
H:92 [binder, in MetaCoq.Erasure.ERemoveParams]
H:927 [binder, in MetaCoq.Template.Typing]
H:93 [binder, in MetaCoq.PCUIC.Bidirectional.BDUnique]
H:93 [binder, in MetaCoq.Erasure.EEtaExpanded]
H:93 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
H:939 [binder, in MetaCoq.Template.utils.wGraph]
H:94 [binder, in MetaCoq.Erasure.EConstructorsAsBlocks]
H:94 [binder, in MetaCoq.Erasure.ERemoveParams]
H:94 [binder, in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
H:95 [binder, in MetaCoq.Erasure.EEtaExpanded]
H:95 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
H:96 [binder, in MetaCoq.Erasure.EConstructorsAsBlocks]
H:96 [binder, in MetaCoq.Template.EnvironmentTyping]
H:97 [binder, in MetaCoq.Erasure.EEtaExpanded]
H:97 [binder, in MetaCoq.Erasure.ERemoveParams]
H:97 [binder, in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
H:99 [binder, in MetaCoq.Erasure.EConstructorsAsBlocks]
H:99 [binder, in MetaCoq.Erasure.EEtaExpanded]
H:99 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
H:991 [binder, in MetaCoq.Template.utils.wGraph]
HΓ:109 [binder, in MetaCoq.Erasure.ErasureFunction]
HΓ:1125 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
HΓ:168 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
HΓ:177 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
HΓ:192 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
HΓ:204 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
HΓ:233 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
HΓ:234 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
hΓ:4 [binder, in MetaCoq.PCUIC.Typing.PCUICNamelessTyp]
HΓ:50 [binder, in MetaCoq.Erasure.ErasureFunction]
HΓ:704 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
HΓ:779 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
HΓ:833 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
HΓ:85 [binder, in MetaCoq.PCUIC.PCUICArities]
HΓ:91 [binder, in MetaCoq.PCUIC.PCUICArities]
HΔ:462 [binder, in MetaCoq.SafeChecker.PCUICTypeChecker]
hΣ [definition, in MetaCoq.SafeChecker.PCUICSafeRetyping]
HΣ [definition, in MetaCoq.Erasure.ErasureFunction]
hΣ [definition, in MetaCoq.SafeChecker.PCUICSafeReduce]
hΣ [definition, in MetaCoq.SafeChecker.PCUICSafeConversion]
hΣ [definition, in MetaCoq.SafeChecker.PCUICSafeChecker]
hΣ [definition, in MetaCoq.SafeChecker.PCUICTypeChecker]
HΣ' [definition, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
hΣ' [definition, in MetaCoq.SafeChecker.PCUICEqualityDec]
HΣ':886 [binder, in MetaCoq.PCUIC.PCUICSR]
HΣ:11 [binder, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
HΣ:121 [binder, in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
hΣ:13 [binder, in MetaCoq.PCUIC.PCUICSN]
HΣ:136 [binder, in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
HΣ:15 [binder, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
hΣ:173 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
hΣ:180 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
hΣ:183 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
hΣ:188 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
HΣ:191 [binder, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
hΣ:193 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
hΣ:197 [binder, in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
hΣ:218 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
hΣ:231 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
hΣ:241 [binder, in MetaCoq.PCUIC.PCUICInductiveInversion]
hΣ:293 [binder, in MetaCoq.PCUIC.PCUICTyping]
HΣ:295 [binder, in MetaCoq.PCUIC.PCUICSafeLemmata]
HΣ:3 [binder, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
hΣ:387 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
HΣ:410 [binder, in MetaCoq.Erasure.ERemoveParams]
HΣ:46 [binder, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
HΣ:53 [binder, in MetaCoq.Erasure.EInlineProjections]
HΣ:7 [binder, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
hΣ:70 [binder, in MetaCoq.PCUIC.PCUICSafeLemmata]
HΣ:70 [binder, in MetaCoq.SafeChecker.PCUICWfReduction]
HΣ:86 [binder, in MetaCoq.Erasure.EOptimizePropDiscr]
HΣ:96 [binder, in MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp]
hπ1:4421 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
hπ2:4426 [binder, in MetaCoq.SafeChecker.PCUICSafeConversion]
Hφ:192 [binder, in MetaCoq.SafeChecker.PCUICWfEnvImpl]
Hφ:388 [binder, in MetaCoq.SafeChecker.PCUICEqualityDec]
| 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) |