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 (binder)

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