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)

G (binder)

gamma:511 [in MetaCoq.Examples.tauto]
Gamma:513 [in MetaCoq.Examples.tauto]
gcstrs:170 [in MetaCoq.Template.common.uGraph]
gcs:503 [in MetaCoq.Template.common.uGraph]
gcs:511 [in MetaCoq.Template.common.uGraph]
gcs:626 [in MetaCoq.Template.common.uGraph]
gcs:644 [in MetaCoq.Template.common.uGraph]
gcs:646 [in MetaCoq.Template.common.uGraph]
gcs:651 [in MetaCoq.Template.common.uGraph]
gcs:653 [in MetaCoq.Template.common.uGraph]
gctx':714 [in MetaCoq.Template.common.uGraph]
gctx1:675 [in MetaCoq.Template.common.uGraph]
gctx2:676 [in MetaCoq.Template.common.uGraph]
gctx:167 [in MetaCoq.Template.common.uGraph]
gctx:717 [in MetaCoq.Template.common.uGraph]
gc1:662 [in MetaCoq.Template.common.uGraph]
gc1:86 [in MetaCoq.Template.common.uGraph]
gc2:663 [in MetaCoq.Template.common.uGraph]
gc2:87 [in MetaCoq.Template.common.uGraph]
gc:111 [in MetaCoq.Template.common.uGraph]
gc:113 [in MetaCoq.Template.common.uGraph]
gc:160 [in MetaCoq.Template.common.uGraph]
gc:174 [in MetaCoq.Template.common.uGraph]
gc:190 [in MetaCoq.Template.common.uGraph]
gc:213 [in MetaCoq.Template.common.uGraph]
gc:216 [in MetaCoq.Template.common.uGraph]
gc:219 [in MetaCoq.Template.common.uGraph]
gc:438 [in MetaCoq.Template.common.uGraph]
gc:441 [in MetaCoq.Template.common.uGraph]
gc:501 [in MetaCoq.Template.common.uGraph]
gc:508 [in MetaCoq.Template.common.uGraph]
gc:514 [in MetaCoq.Template.common.uGraph]
gc:516 [in MetaCoq.Template.common.uGraph]
gc:518 [in MetaCoq.Template.common.uGraph]
gc:521 [in MetaCoq.Template.common.uGraph]
gc:624 [in MetaCoq.Template.common.uGraph]
gc:642 [in MetaCoq.Template.common.uGraph]
gc:664 [in MetaCoq.Template.common.uGraph]
gc:69 [in MetaCoq.Template.common.uGraph]
genv:33 [in MetaCoq.Template.EnvMap]
genv:35 [in MetaCoq.Template.EnvMap]
gen_compare_global_instance':365 [in MetaCoq.SafeChecker.PCUICEqualityDec]
gen_compare_global_instance:364 [in MetaCoq.SafeChecker.PCUICEqualityDec]
gen_compare_global_instance:348 [in MetaCoq.SafeChecker.PCUICEqualityDec]
gen_compare_global_instance:334 [in MetaCoq.SafeChecker.PCUICEqualityDec]
gen_compare_global_instance:318 [in MetaCoq.SafeChecker.PCUICEqualityDec]
gen_compare_global_instance':265 [in MetaCoq.SafeChecker.PCUICEqualityDec]
gen_compare_global_instance:264 [in MetaCoq.SafeChecker.PCUICEqualityDec]
gen_compare_global_instance:225 [in MetaCoq.SafeChecker.PCUICEqualityDec]
gen_compare_global_instance:207 [in MetaCoq.SafeChecker.PCUICEqualityDec]
gen_compare_global_instance:151 [in MetaCoq.SafeChecker.PCUICEqualityDec]
gen_compare_global_instance:124 [in MetaCoq.SafeChecker.PCUICEqualityDec]
gen_compare_global_instance:38 [in MetaCoq.SafeChecker.PCUICEqualityDec]
global_levels:80 [in MetaCoq.PCUIC.PCUICWeakeningEnv]
global_levels:469 [in MetaCoq.Template.EnvironmentTyping]
global_levels:81 [in MetaCoq.SafeChecker.PCUICSafeChecker]
Gl:793 [in MetaCoq.Template.utils.wGraph]
Gl:799 [in MetaCoq.Template.utils.wGraph]
Gl:805 [in MetaCoq.Template.utils.wGraph]
Gl:808 [in MetaCoq.Template.utils.wGraph]
Gl:813 [in MetaCoq.Template.utils.wGraph]
Gl:990 [in MetaCoq.Template.utils.wGraph]
goal:1 [in MetaCoq.Examples.constructor_tac]
gph:679 [in MetaCoq.Template.common.uGraph]
gph:711 [in MetaCoq.Template.common.uGraph]
gph:716 [in MetaCoq.Template.common.uGraph]
gref:227 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
gref:376 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
gref:654 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
gr':113 [in MetaCoq.Translations.translation_utils]
gr':122 [in MetaCoq.Translations.translation_utils]
gr':131 [in MetaCoq.Translations.translation_utils]
gr':148 [in MetaCoq.Translations.translation_utils]
gr':80 [in MetaCoq.Translations.translation_utils]
gr':93 [in MetaCoq.Template.Kernames]
gr':96 [in MetaCoq.Translations.translation_utils]
gr:103 [in MetaCoq.Translations.translation_utils]
gr:12 [in MetaCoq.Translations.translation_utils]
gr:153 [in MetaCoq.Template.TermEquality]
gr:178 [in MetaCoq.Template.TermEquality]
gr:192 [in MetaCoq.SafeChecker.PCUICEqualityDec]
gr:204 [in MetaCoq.Template.TermEquality]
gr:213 [in MetaCoq.Template.TermEquality]
gr:220 [in MetaCoq.PCUIC.PCUICEquality]
gr:24 [in MetaCoq.PCUIC.PCUICEquality]
gr:250 [in MetaCoq.PCUIC.PCUICEquality]
gr:26 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
gr:27 [in MetaCoq.Template.TermEquality]
gr:271 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
gr:272 [in MetaCoq.PCUIC.PCUICEquality]
gr:279 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
gr:286 [in MetaCoq.SafeChecker.PCUICEqualityDec]
gr:287 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
gr:302 [in MetaCoq.SafeChecker.PCUICEqualityDec]
gr:31 [in MetaCoq.Translations.translation_utils]
gr:31 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
gr:315 [in MetaCoq.PCUIC.PCUICEquality]
gr:32 [in MetaCoq.SafeChecker.PCUICEqualityDec]
gr:321 [in MetaCoq.PCUIC.PCUICEquality]
gr:331 [in MetaCoq.PCUIC.PCUICEquality]
gr:34 [in MetaCoq.PCUIC.PCUICEquality]
gr:340 [in MetaCoq.PCUIC.PCUICEquality]
gr:347 [in MetaCoq.PCUIC.PCUICEquality]
gr:350 [in MetaCoq.PCUIC.PCUICEquality]
gr:358 [in MetaCoq.PCUIC.PCUICEquality]
gr:37 [in MetaCoq.Template.TermEquality]
gr:39 [in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
gr:48 [in MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv]
gr:48 [in MetaCoq.Examples.demo]
gr:49 [in MetaCoq.Translations.translation_utils]
gr:54 [in MetaCoq.Translations.translation_utils]
gr:678 [in MetaCoq.SafeChecker.PCUICSafeConversion]
gr:689 [in MetaCoq.PCUIC.PCUICEquality]
gr:7 [in MetaCoq.Translations.translation_utils]
gr:70 [in MetaCoq.Examples.demo]
gr:71 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
gr:86 [in MetaCoq.Template.Kernames]
gr:92 [in MetaCoq.Template.Kernames]
guarded:1106 [in MetaCoq.SafeChecker.PCUICTypeChecker]
guarded:1110 [in MetaCoq.SafeChecker.PCUICTypeChecker]
guarded:67 [in MetaCoq.Erasure.EWcbvEval]
guarded:73 [in MetaCoq.Erasure.EWcbvEvalInd]
guarded:76 [in MetaCoq.Erasure.EWcbvEval]
guarded:83 [in MetaCoq.Erasure.EWcbvEvalInd]
guard:1 [in MetaCoq.Erasure.Erasure]
guard:103 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
guard:109 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
guard:130 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
guard:132 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
guard:147 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
guard:153 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
guard:16 [in MetaCoq.Erasure.ETransform]
guard:170 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
guard:177 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
guard:18 [in MetaCoq.SafeChecker.SafeTemplateChecker]
guard:181 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
guard:185 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
guard:189 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
guard:19 [in MetaCoq.Erasure.ETransform]
guard:200 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
guard:203 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
guard:206 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
guard:214 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
guard:216 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
guard:218 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
guard:220 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
guard:24 [in MetaCoq.SafeChecker.PCUICConsistency]
guard:24 [in MetaCoq.Erasure.ETransform]
guard:3 [in MetaCoq.Erasure.Erasure]
guard:32 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
guard:4 [in MetaCoq.SafeChecker.SafeTemplateChecker]
guard:4 [in MetaCoq.Erasure.ETransform]
guard:4 [in MetaCoq.Erasure.Erasure]
guard:53 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
guard:6 [in MetaCoq.SafeChecker.SafeTemplateChecker]
guard:6 [in MetaCoq.Erasure.Erasure]
guard:69 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
guard:75 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
guard:9 [in MetaCoq.SafeChecker.SafeTemplateChecker]
g'':60 [in MetaCoq.Template.Transform]
g':100 [in MetaCoq.Template.BasicAst]
g':1009 [in MetaCoq.Translations.MiniHoTT]
g':1017 [in MetaCoq.Translations.MiniHoTT_paths]
g':103 [in MetaCoq.Erasure.ETransform]
g':113 [in MetaCoq.Template.BasicAst]
g':113 [in MetaCoq.Erasure.ETransform]
g':121 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
g':127 [in MetaCoq.Template.BasicAst]
g':134 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
g':167 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
g':174 [in MetaCoq.Template.Ast]
g':18 [in MetaCoq.Template.EnvMap]
g':20 [in MetaCoq.Template.EnvMap]
g':2485 [in MetaCoq.Translations.MiniHoTT]
g':2493 [in MetaCoq.Translations.MiniHoTT_paths]
G':250 [in MetaCoq.Template.common.uGraph]
g':252 [in MetaCoq.Template.common.uGraph]
g':256 [in MetaCoq.Template.common.uGraph]
g':268 [in MetaCoq.PCUIC.PCUICAst]
g':287 [in MetaCoq.PCUIC.PCUICAst]
g':30 [in MetaCoq.Erasure.ETransform]
g':340 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
g':38 [in MetaCoq.Template.Ast]
g':45 [in MetaCoq.Erasure.ETransform]
g':503 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
g':53 [in MetaCoq.Template.Ast]
g':57 [in MetaCoq.Template.Transform]
g':58 [in MetaCoq.Erasure.ETransform]
g':672 [in MetaCoq.Translations.MiniHoTT]
g':680 [in MetaCoq.Translations.MiniHoTT_paths]
g':682 [in MetaCoq.Translations.MiniHoTT]
g':69 [in MetaCoq.Erasure.ETransform]
g':690 [in MetaCoq.Translations.MiniHoTT_paths]
g':693 [in MetaCoq.Translations.MiniHoTT]
G':701 [in MetaCoq.Template.common.uGraph]
g':701 [in MetaCoq.Translations.MiniHoTT_paths]
g':704 [in MetaCoq.Translations.MiniHoTT]
G':709 [in MetaCoq.Template.common.uGraph]
g':712 [in MetaCoq.Translations.MiniHoTT_paths]
g':79 [in MetaCoq.Erasure.ETransform]
g':82 [in MetaCoq.Template.BasicAst]
g':820 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
G':89 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
g':898 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
g':90 [in MetaCoq.Template.BasicAst]
g':91 [in MetaCoq.Erasure.ETransform]
g0:24 [in MetaCoq.Template.EnvMap]
g0:2497 [in MetaCoq.Translations.MiniHoTT]
g0:2505 [in MetaCoq.Translations.MiniHoTT_paths]
g0:2588 [in MetaCoq.Translations.MiniHoTT]
g0:2596 [in MetaCoq.Translations.MiniHoTT_paths]
G1:1048 [in MetaCoq.Template.utils.wGraph]
G1:1054 [in MetaCoq.Template.utils.wGraph]
G1:1058 [in MetaCoq.Template.utils.wGraph]
G1:1060 [in MetaCoq.Template.utils.wGraph]
G1:1069 [in MetaCoq.Template.utils.wGraph]
G1:1094 [in MetaCoq.Template.utils.wGraph]
G1:1122 [in MetaCoq.Template.utils.wGraph]
G1:1128 [in MetaCoq.Template.utils.wGraph]
G1:1132 [in MetaCoq.Template.utils.wGraph]
G1:1139 [in MetaCoq.Template.utils.wGraph]
G1:1144 [in MetaCoq.Template.utils.wGraph]
G1:1148 [in MetaCoq.Template.utils.wGraph]
G1:1150 [in MetaCoq.Template.utils.wGraph]
G1:1182 [in MetaCoq.Template.utils.wGraph]
g1:2499 [in MetaCoq.Translations.MiniHoTT]
g1:2507 [in MetaCoq.Translations.MiniHoTT_paths]
g1:2590 [in MetaCoq.Translations.MiniHoTT]
g1:2598 [in MetaCoq.Translations.MiniHoTT_paths]
G1:814 [in MetaCoq.Template.utils.wGraph]
G1:817 [in MetaCoq.Template.utils.wGraph]
G1:871 [in MetaCoq.Template.utils.wGraph]
G1:943 [in MetaCoq.Template.utils.wGraph]
G1:987 [in MetaCoq.Template.utils.wGraph]
G2:1049 [in MetaCoq.Template.utils.wGraph]
G2:1055 [in MetaCoq.Template.utils.wGraph]
G2:1059 [in MetaCoq.Template.utils.wGraph]
G2:1061 [in MetaCoq.Template.utils.wGraph]
G2:1095 [in MetaCoq.Template.utils.wGraph]
G2:1123 [in MetaCoq.Template.utils.wGraph]
G2:1129 [in MetaCoq.Template.utils.wGraph]
G2:1133 [in MetaCoq.Template.utils.wGraph]
G2:1140 [in MetaCoq.Template.utils.wGraph]
G2:1145 [in MetaCoq.Template.utils.wGraph]
G2:1149 [in MetaCoq.Template.utils.wGraph]
G2:1151 [in MetaCoq.Template.utils.wGraph]
G2:1183 [in MetaCoq.Template.utils.wGraph]
G2:818 [in MetaCoq.Template.utils.wGraph]
G2:872 [in MetaCoq.Template.utils.wGraph]
G2:944 [in MetaCoq.Template.utils.wGraph]
G2:988 [in MetaCoq.Template.utils.wGraph]
g:1 [in MetaCoq.Template.utils.MCPrelude]
G:10 [in MetaCoq.Translations.param_cheap_packed]
g:100 [in MetaCoq.Translations.MiniHoTT]
g:1008 [in MetaCoq.Translations.MiniHoTT]
g:1016 [in MetaCoq.Translations.MiniHoTT_paths]
g:102 [in MetaCoq.Erasure.ETransform]
g:104 [in MetaCoq.Translations.param_generous_packed]
g:1053 [in MetaCoq.Translations.MiniHoTT]
g:106 [in MetaCoq.Translations.MiniHoTT]
g:1061 [in MetaCoq.Translations.MiniHoTT_paths]
g:107 [in MetaCoq.Template.Ast]
g:1076 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
g:108 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
g:108 [in MetaCoq.Translations.MiniHoTT_paths]
g:1082 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
g:109 [in MetaCoq.Translations.MiniHoTT]
g:11 [in MetaCoq.PCUIC.PCUICSpine]
g:112 [in MetaCoq.Template.BasicAst]
g:112 [in MetaCoq.Erasure.ETransform]
g:113 [in MetaCoq.Translations.MiniHoTT]
g:114 [in MetaCoq.Translations.MiniHoTT_paths]
g:115 [in MetaCoq.Template.utils.MCOption]
g:115 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
G:1160 [in MetaCoq.Template.utils.wGraph]
g:117 [in MetaCoq.Translations.MiniHoTT_paths]
g:1170 [in MetaCoq.Translations.MiniHoTT]
g:1175 [in MetaCoq.Template.utils.All_Forall]
g:1178 [in MetaCoq.Translations.MiniHoTT_paths]
g:118 [in MetaCoq.Translations.MiniHoTT]
g:1181 [in MetaCoq.Translations.MiniHoTT]
g:1187 [in MetaCoq.Template.utils.All_Forall]
g:1189 [in MetaCoq.Translations.MiniHoTT_paths]
g:12 [in MetaCoq.Template.EnvMap]
g:121 [in MetaCoq.Template.utils.All_Forall]
g:121 [in MetaCoq.Template.utils.MCList]
g:121 [in MetaCoq.Translations.MiniHoTT_paths]
g:122 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
g:122 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
g:126 [in MetaCoq.Template.BasicAst]
g:126 [in MetaCoq.Translations.MiniHoTT_paths]
g:128 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
g:128 [in MetaCoq.PCUIC.PCUICCumulProp]
g:13 [in MetaCoq.Template.TemplateCheckWf]
g:130 [in MetaCoq.Template.utils.All_Forall]
g:1308 [in MetaCoq.Template.utils.All_Forall]
g:134 [in MetaCoq.Template.Ast]
g:135 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
g:135 [in MetaCoq.PCUIC.PCUICCumulProp]
g:136 [in MetaCoq.PCUIC.Syntax.PCUICLiftSubst]
g:1365 [in MetaCoq.Template.utils.All_Forall]
g:137 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
g:138 [in MetaCoq.Erasure.ErasureProperties]
g:139 [in MetaCoq.PCUIC.PCUICCumulProp]
g:139 [in MetaCoq.PCUIC.PCUICContexts]
g:1428 [in MetaCoq.Translations.MiniHoTT]
g:1434 [in MetaCoq.Template.utils.All_Forall]
g:1436 [in MetaCoq.Translations.MiniHoTT_paths]
g:1437 [in MetaCoq.Translations.MiniHoTT]
g:1441 [in MetaCoq.Translations.MiniHoTT]
g:1445 [in MetaCoq.Erasure.ErasureFunction]
g:1445 [in MetaCoq.Translations.MiniHoTT_paths]
g:1448 [in MetaCoq.Translations.MiniHoTT]
g:1449 [in MetaCoq.Translations.MiniHoTT_paths]
g:145 [in MetaCoq.Template.Ast]
g:1451 [in MetaCoq.Translations.MiniHoTT]
g:1455 [in MetaCoq.Translations.MiniHoTT]
g:1456 [in MetaCoq.Translations.MiniHoTT_paths]
g:1459 [in MetaCoq.Translations.MiniHoTT_paths]
g:146 [in MetaCoq.Template.utils.MCList]
g:1463 [in MetaCoq.Translations.MiniHoTT_paths]
g:147 [in MetaCoq.PCUIC.PCUICFirstorder]
g:1478 [in MetaCoq.Translations.MiniHoTT]
g:148 [in MetaCoq.Template.LiftSubst]
g:1486 [in MetaCoq.Translations.MiniHoTT]
g:1486 [in MetaCoq.Translations.MiniHoTT_paths]
g:149 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
g:1492 [in MetaCoq.Translations.MiniHoTT]
g:1494 [in MetaCoq.Translations.MiniHoTT_paths]
g:15 [in MetaCoq.Template.TemplateCheckWf]
g:15 [in MetaCoq.Template.utils.MCProd]
G:15 [in MetaCoq.SafeChecker.PCUICSafeChecker]
g:1500 [in MetaCoq.Translations.MiniHoTT]
g:1500 [in MetaCoq.Translations.MiniHoTT_paths]
g:1508 [in MetaCoq.Translations.MiniHoTT_paths]
g:1509 [in MetaCoq.Translations.MiniHoTT]
g:1517 [in MetaCoq.Translations.MiniHoTT_paths]
g:1521 [in MetaCoq.Translations.MiniHoTT]
g:1529 [in MetaCoq.Translations.MiniHoTT_paths]
g:153 [in MetaCoq.Template.Ast]
g:1536 [in MetaCoq.Translations.MiniHoTT]
g:154 [in MetaCoq.Template.utils.MCList]
g:154 [in MetaCoq.PCUIC.PCUICParallelReduction]
g:154 [in MetaCoq.Translations.MiniHoTT]
g:1544 [in MetaCoq.Translations.MiniHoTT_paths]
g:157 [in MetaCoq.Template.BasicAst]
g:157 [in MetaCoq.Translations.times_bool_fun]
G:16 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
g:16 [in MetaCoq.Template.TemplateCheckWf]
G:16 [in MetaCoq.Translations.param_cheap_packed]
g:16 [in MetaCoq.Template.EnvMap]
g:16 [in MetaCoq.Translations.times_bool_fun2]
g:160 [in MetaCoq.PCUIC.PCUICCumulativity]
g:1608 [in MetaCoq.Translations.MiniHoTT]
g:1609 [in MetaCoq.Translations.MiniHoTT]
g:1612 [in MetaCoq.Template.utils.All_Forall]
g:1614 [in MetaCoq.Translations.MiniHoTT]
g:1616 [in MetaCoq.Translations.MiniHoTT_paths]
g:1617 [in MetaCoq.Translations.MiniHoTT_paths]
g:162 [in MetaCoq.Template.Ast]
g:162 [in MetaCoq.Translations.MiniHoTT_paths]
g:1621 [in MetaCoq.Translations.MiniHoTT]
g:1622 [in MetaCoq.Translations.MiniHoTT_paths]
g:1627 [in MetaCoq.Translations.MiniHoTT]
g:1629 [in MetaCoq.Translations.MiniHoTT_paths]
g:163 [in MetaCoq.Template.BasicAst]
g:163 [in MetaCoq.PCUIC.PCUICParallelReduction]
g:1634 [in MetaCoq.Translations.MiniHoTT]
g:1635 [in MetaCoq.Translations.MiniHoTT]
g:1635 [in MetaCoq.Translations.MiniHoTT_paths]
g:1640 [in MetaCoq.Translations.MiniHoTT]
g:1642 [in MetaCoq.Translations.MiniHoTT_paths]
g:1643 [in MetaCoq.Translations.MiniHoTT_paths]
g:1647 [in MetaCoq.Translations.MiniHoTT]
g:1648 [in MetaCoq.Translations.MiniHoTT_paths]
g:165 [in MetaCoq.Translations.MiniHoTT]
g:1653 [in MetaCoq.Translations.MiniHoTT]
g:1655 [in MetaCoq.Translations.MiniHoTT_paths]
g:166 [in MetaCoq.Template.utils.All_Forall]
g:166 [in MetaCoq.Template.utils.MCList]
g:166 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
g:1661 [in MetaCoq.Translations.MiniHoTT_paths]
g:168 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
g:169 [in MetaCoq.PCUIC.PCUICEtaExpand]
g:1690 [in MetaCoq.Translations.MiniHoTT]
g:1693 [in MetaCoq.Template.utils.All_Forall]
g:1698 [in MetaCoq.Translations.MiniHoTT_paths]
g:17 [in MetaCoq.Template.EnvMap]
g:1706 [in MetaCoq.Translations.MiniHoTT]
g:1714 [in MetaCoq.Translations.MiniHoTT_paths]
g:172 [in MetaCoq.Translations.MiniHoTT]
g:1728 [in MetaCoq.Template.utils.All_Forall]
g:173 [in MetaCoq.Template.Ast]
G:173 [in MetaCoq.SafeChecker.PCUICErrors]
g:173 [in MetaCoq.Translations.MiniHoTT_paths]
g:1738 [in MetaCoq.Translations.MiniHoTT]
g:1746 [in MetaCoq.Translations.MiniHoTT_paths]
g:1748 [in MetaCoq.Translations.MiniHoTT]
g:175 [in MetaCoq.Template.utils.MCList]
g:1756 [in MetaCoq.Translations.MiniHoTT_paths]
g:1758 [in MetaCoq.Translations.MiniHoTT]
g:1766 [in MetaCoq.Translations.MiniHoTT_paths]
g:1767 [in MetaCoq.Translations.MiniHoTT]
g:1775 [in MetaCoq.Translations.MiniHoTT_paths]
g:1776 [in MetaCoq.Translations.MiniHoTT]
g:1784 [in MetaCoq.Translations.MiniHoTT_paths]
g:180 [in MetaCoq.Translations.MiniHoTT]
g:180 [in MetaCoq.Translations.MiniHoTT_paths]
G:181 [in MetaCoq.SafeChecker.PCUICErrors]
g:183 [in MetaCoq.Template.utils.MCList]
g:1878 [in MetaCoq.Template.utils.All_Forall]
G:188 [in MetaCoq.Template.utils.wGraph]
g:188 [in MetaCoq.Translations.MiniHoTT_paths]
G:189 [in MetaCoq.Template.utils.wGraph]
g:189 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
g:19 [in MetaCoq.Template.EnvMap]
G:190 [in MetaCoq.Template.utils.wGraph]
g:191 [in MetaCoq.Translations.times_bool_fun]
g:192 [in MetaCoq.Template.common.uGraph]
G:192 [in MetaCoq.Template.utils.wGraph]
G:193 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
g:193 [in MetaCoq.Template.common.uGraph]
g:1940 [in MetaCoq.Template.utils.All_Forall]
g:1962 [in MetaCoq.Template.utils.All_Forall]
G:199 [in MetaCoq.SafeChecker.PCUICErrors]
g:2 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
g:201 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
g:203 [in MetaCoq.Template.common.uGraph]
G:204 [in MetaCoq.Template.Checker]
g:2071 [in MetaCoq.Template.utils.All_Forall]
g:21 [in MetaCoq.PCUIC.utils.PCUICOnOne]
g:212 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
g:2137 [in MetaCoq.Template.utils.All_Forall]
g:2148 [in MetaCoq.Template.utils.All_Forall]
g:218 [in MetaCoq.Template.BasicAst]
g:218 [in MetaCoq.Template.utils.All_Forall]
g:22 [in MetaCoq.Template.utils.MCProd]
g:221 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
g:2252 [in MetaCoq.Translations.MiniHoTT]
g:2260 [in MetaCoq.Translations.MiniHoTT_paths]
g:2263 [in MetaCoq.Translations.MiniHoTT]
g:2271 [in MetaCoq.Translations.MiniHoTT_paths]
g:2273 [in MetaCoq.Translations.MiniHoTT]
g:2281 [in MetaCoq.Translations.MiniHoTT_paths]
g:2283 [in MetaCoq.Translations.MiniHoTT]
g:229 [in MetaCoq.Template.utils.All_Forall]
g:2291 [in MetaCoq.Translations.MiniHoTT_paths]
g:23 [in MetaCoq.Template.EnvMap]
g:230 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
g:2316 [in MetaCoq.Translations.MiniHoTT]
g:2322 [in MetaCoq.Translations.MiniHoTT]
g:2324 [in MetaCoq.Translations.MiniHoTT_paths]
g:2330 [in MetaCoq.Translations.MiniHoTT_paths]
g:2333 [in MetaCoq.Translations.MiniHoTT]
g:2338 [in MetaCoq.Translations.MiniHoTT]
g:2341 [in MetaCoq.Translations.MiniHoTT_paths]
g:2343 [in MetaCoq.Translations.MiniHoTT]
g:2346 [in MetaCoq.Translations.MiniHoTT_paths]
g:2348 [in MetaCoq.Translations.MiniHoTT]
g:2351 [in MetaCoq.Translations.MiniHoTT_paths]
g:2356 [in MetaCoq.Translations.MiniHoTT_paths]
g:2357 [in MetaCoq.Translations.MiniHoTT]
g:2365 [in MetaCoq.Translations.MiniHoTT_paths]
g:238 [in MetaCoq.Erasure.Extract]
G:24 [in MetaCoq.Translations.param_cheap_packed]
g:240 [in MetaCoq.Template.utils.All_Forall]
g:240 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
g:2408 [in MetaCoq.Translations.MiniHoTT]
g:2416 [in MetaCoq.Translations.MiniHoTT_paths]
g:2419 [in MetaCoq.Translations.MiniHoTT]
g:2427 [in MetaCoq.Translations.MiniHoTT_paths]
g:244 [in MetaCoq.PCUIC.PCUICSubstitution]
g:2447 [in MetaCoq.Translations.MiniHoTT]
g:2455 [in MetaCoq.Translations.MiniHoTT_paths]
g:2460 [in MetaCoq.Translations.MiniHoTT]
g:2468 [in MetaCoq.Translations.MiniHoTT_paths]
g:2474 [in MetaCoq.Translations.MiniHoTT]
g:248 [in MetaCoq.SafeChecker.PCUICSafeConversion]
g:2482 [in MetaCoq.Translations.MiniHoTT_paths]
g:2484 [in MetaCoq.Translations.MiniHoTT]
g:2487 [in MetaCoq.Template.utils.All_Forall]
G:249 [in MetaCoq.Template.common.uGraph]
g:2492 [in MetaCoq.Translations.MiniHoTT_paths]
g:251 [in MetaCoq.Template.common.uGraph]
g:2511 [in MetaCoq.Translations.MiniHoTT]
g:2519 [in MetaCoq.Translations.MiniHoTT_paths]
g:2524 [in MetaCoq.Translations.MiniHoTT]
g:2532 [in MetaCoq.Translations.MiniHoTT_paths]
g:2535 [in MetaCoq.Translations.MiniHoTT]
g:2542 [in MetaCoq.Translations.MiniHoTT]
g:2543 [in MetaCoq.Translations.MiniHoTT_paths]
g:255 [in MetaCoq.Template.common.uGraph]
g:2550 [in MetaCoq.Translations.MiniHoTT_paths]
g:2564 [in MetaCoq.Translations.MiniHoTT]
g:2572 [in MetaCoq.Translations.MiniHoTT_paths]
g:26 [in MetaCoq.PCUIC.Syntax.PCUICClosed]
G:262 [in MetaCoq.Template.common.uGraph]
g:2625 [in MetaCoq.Translations.MiniHoTT]
g:2626 [in MetaCoq.Translations.MiniHoTT]
g:263 [in MetaCoq.Template.utils.MCList]
g:2633 [in MetaCoq.Translations.MiniHoTT_paths]
g:2634 [in MetaCoq.Translations.MiniHoTT_paths]
g:266 [in MetaCoq.SafeChecker.PCUICErrors]
g:266 [in MetaCoq.PCUIC.PCUICAst]
g:268 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
g:2685 [in MetaCoq.Translations.MiniHoTT]
g:269 [in MetaCoq.Template.EtaExpand]
g:2693 [in MetaCoq.Translations.MiniHoTT_paths]
g:271 [in MetaCoq.Template.utils.MCList]
g:278 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
G:284 [in MetaCoq.Template.Checker]
g:286 [in MetaCoq.PCUIC.PCUICAst]
g:288 [in MetaCoq.Template.utils.MCList]
g:29 [in MetaCoq.Erasure.ETransform]
g:29 [in MetaCoq.Template.EnvMap]
g:2918 [in MetaCoq.Translations.MiniHoTT]
g:2926 [in MetaCoq.Translations.MiniHoTT]
g:2926 [in MetaCoq.Translations.MiniHoTT_paths]
g:2934 [in MetaCoq.Translations.MiniHoTT_paths]
g:2939 [in MetaCoq.Translations.MiniHoTT]
G:294 [in MetaCoq.Template.Checker]
g:2947 [in MetaCoq.Translations.MiniHoTT_paths]
g:295 [in MetaCoq.PCUIC.PCUICAst]
g:2954 [in MetaCoq.Translations.MiniHoTT]
g:2962 [in MetaCoq.Translations.MiniHoTT_paths]
g:2963 [in MetaCoq.Translations.MiniHoTT]
g:2968 [in MetaCoq.Translations.MiniHoTT]
g:297 [in MetaCoq.PCUIC.PCUICSubstitution]
g:2971 [in MetaCoq.Translations.MiniHoTT_paths]
g:2976 [in MetaCoq.Translations.MiniHoTT_paths]
g:300 [in MetaCoq.Template.utils.MCList]
g:308 [in MetaCoq.Template.utils.MCList]
g:308 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
g:31 [in MetaCoq.Template.EnvMap]
G:318 [in MetaCoq.Template.Checker]
g:32 [in MetaCoq.Template.LiftSubst]
g:324 [in MetaCoq.Template.BasicAst]
g:328 [in MetaCoq.Template.BasicAst]
g:331 [in MetaCoq.Template.BasicAst]
g:336 [in MetaCoq.Template.BasicAst]
g:338 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
g:339 [in MetaCoq.Template.BasicAst]
g:342 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
g:343 [in MetaCoq.Template.BasicAst]
g:347 [in MetaCoq.Template.BasicAst]
g:348 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
g:35 [in MetaCoq.PCUIC.utils.PCUICOnOne]
g:35 [in MetaCoq.Template.utils.MCProd]
g:351 [in MetaCoq.Template.BasicAst]
g:352 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
g:354 [in MetaCoq.Template.BasicAst]
G:355 [in MetaCoq.Template.common.uGraph]
g:357 [in MetaCoq.Template.BasicAst]
g:36 [in MetaCoq.Template.Ast]
g:361 [in MetaCoq.Template.BasicAst]
g:362 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
g:362 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
g:366 [in MetaCoq.Template.BasicAst]
g:37 [in MetaCoq.Template.EnvMap]
g:370 [in MetaCoq.Template.BasicAst]
g:38 [in MetaCoq.Template.EnvMap]
g:383 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
G:389 [in MetaCoq.SafeChecker.PCUICEqualityDec]
g:392 [in MetaCoq.Template.BasicAst]
g:394 [in MetaCoq.PCUIC.PCUICAst]
g:40 [in MetaCoq.PCUIC.PCUICParallelReduction]
g:40 [in MetaCoq.Template.EnvMap]
g:400 [in MetaCoq.PCUIC.PCUICAst]
G:400 [in MetaCoq.Template.Checker]
g:400 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
g:401 [in MetaCoq.Template.BasicAst]
G:404 [in MetaCoq.Template.Checker]
g:406 [in MetaCoq.PCUIC.PCUICAst]
G:408 [in MetaCoq.Template.Checker]
g:410 [in MetaCoq.Template.BasicAst]
g:410 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
G:411 [in MetaCoq.Template.Checker]
g:413 [in MetaCoq.PCUIC.PCUICAst]
g:413 [in MetaCoq.Template.Checker]
g:42 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
g:42 [in MetaCoq.Template.EnvMap]
g:42 [in MetaCoq.Template.utils.MCProd]
G:422 [in MetaCoq.Template.Checker]
G:425 [in MetaCoq.Template.Checker]
g:426 [in MetaCoq.Template.Checker]
G:433 [in MetaCoq.Template.Checker]
g:44 [in MetaCoq.Erasure.ETransform]
g:449 [in MetaCoq.PCUIC.PCUICAst]
g:454 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
g:463 [in MetaCoq.PCUIC.PCUICAst]
G:47 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
g:47 [in MetaCoq.Template.EnvMap]
g:47 [in MetaCoq.PCUIC.utils.PCUICPretty]
G:470 [in MetaCoq.Template.common.uGraph]
G:473 [in MetaCoq.Template.common.uGraph]
g:473 [in MetaCoq.PCUIC.PCUICAst]
g:481 [in MetaCoq.PCUIC.PCUICAst]
g:482 [in MetaCoq.Translations.MiniHoTT]
g:488 [in MetaCoq.PCUIC.PCUICAst]
g:49 [in MetaCoq.Template.BasicAst]
g:49 [in MetaCoq.Template.utils.MCList]
g:490 [in MetaCoq.Translations.MiniHoTT]
g:490 [in MetaCoq.Translations.MiniHoTT_paths]
g:498 [in MetaCoq.Translations.MiniHoTT_paths]
g:5 [in MetaCoq.Template.EnvMap]
g:5 [in MetaCoq.PCUIC.PCUICProgram]
g:50 [in MetaCoq.Template.EnvMap]
g:50 [in MetaCoq.Template.monad_utils]
g:504 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
g:504 [in MetaCoq.Translations.MiniHoTT]
g:51 [in MetaCoq.PCUIC.Conversion.PCUICRenameConv]
g:512 [in MetaCoq.Translations.MiniHoTT_paths]
g:52 [in MetaCoq.Template.Ast]
g:52 [in MetaCoq.PCUIC.PCUICParallelReduction]
g:527 [in MetaCoq.Translations.MiniHoTT]
g:53 [in MetaCoq.Translations.MiniHoTT]
g:535 [in MetaCoq.Translations.MiniHoTT_paths]
G:536 [in MetaCoq.Template.common.uGraph]
g:537 [in MetaCoq.Template.EtaExpand]
g:54 [in MetaCoq.Template.EnvMap]
g:54 [in MetaCoq.Template.utils.MCOption]
g:540 [in MetaCoq.Translations.MiniHoTT]
g:541 [in MetaCoq.Template.EtaExpand]
g:541 [in MetaCoq.PCUIC.PCUICAst]
g:545 [in MetaCoq.Template.EtaExpand]
g:545 [in MetaCoq.Template.common.uGraph]
g:547 [in MetaCoq.Template.common.uGraph]
g:548 [in MetaCoq.Translations.MiniHoTT_paths]
g:550 [in MetaCoq.Template.common.uGraph]
g:551 [in MetaCoq.PCUIC.PCUICAst]
g:551 [in MetaCoq.Translations.MiniHoTT]
g:555 [in MetaCoq.Template.common.uGraph]
g:559 [in MetaCoq.Translations.MiniHoTT_paths]
g:56 [in MetaCoq.Template.Pretty]
g:56 [in MetaCoq.Template.Transform]
g:563 [in MetaCoq.PCUIC.PCUICAst]
g:57 [in MetaCoq.Erasure.ETransform]
g:571 [in MetaCoq.Translations.MiniHoTT]
g:579 [in MetaCoq.Translations.MiniHoTT_paths]
g:59 [in MetaCoq.Template.BasicAst]
g:59 [in MetaCoq.Erasure.ELiftSubst]
g:6 [in MetaCoq.PCUIC.PCUICParallelReduction]
g:6 [in MetaCoq.PCUIC.PCUICProgram]
G:60 [in MetaCoq.Translations.param_cheap_packed]
g:60 [in MetaCoq.Template.utils.MCOption]
g:60 [in MetaCoq.Translations.MiniHoTT]
g:600 [in MetaCoq.Translations.MiniHoTT]
G:608 [in MetaCoq.Template.utils.wGraph]
g:608 [in MetaCoq.Translations.MiniHoTT_paths]
g:609 [in MetaCoq.Translations.MiniHoTT]
g:61 [in MetaCoq.Translations.MiniHoTT_paths]
g:615 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
G:616 [in MetaCoq.Template.common.uGraph]
G:617 [in MetaCoq.Template.common.uGraph]
g:617 [in MetaCoq.Translations.MiniHoTT_paths]
g:624 [in MetaCoq.PCUIC.PCUICParallelReduction]
g:63 [in MetaCoq.Erasure.EEnvMap]
g:631 [in MetaCoq.PCUIC.PCUICParallelReduction]
g:64 [in MetaCoq.Template.BasicAst]
g:64 [in MetaCoq.PCUIC.PCUICSigmaCalculus]
g:64 [in MetaCoq.Erasure.ELiftSubst]
g:640 [in MetaCoq.PCUIC.PCUICParallelReduction]
g:644 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
g:645 [in MetaCoq.Translations.MiniHoTT]
g:65 [in MetaCoq.PCUIC.PCUICParallelReduction]
g:653 [in MetaCoq.Translations.MiniHoTT_paths]
G:654 [in MetaCoq.Template.utils.wGraph]
g:655 [in MetaCoq.Template.utils.MCList]
g:661 [in MetaCoq.Template.EnvironmentTyping]
g:662 [in MetaCoq.Template.EnvironmentTyping]
g:663 [in MetaCoq.Translations.MiniHoTT]
G:669 [in MetaCoq.Template.common.uGraph]
g:67 [in MetaCoq.Template.EnvMap]
g:671 [in MetaCoq.Translations.MiniHoTT]
g:671 [in MetaCoq.Translations.MiniHoTT_paths]
g:673 [in MetaCoq.Template.EnvironmentTyping]
g:679 [in MetaCoq.Translations.MiniHoTT_paths]
g:68 [in MetaCoq.Erasure.ETransform]
g:68 [in MetaCoq.Translations.MiniHoTT_paths]
g:681 [in MetaCoq.Translations.MiniHoTT]
G:682 [in MetaCoq.Template.common.uGraph]
g:682 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
G:685 [in MetaCoq.Template.common.uGraph]
g:686 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
g:689 [in MetaCoq.Translations.MiniHoTT_paths]
G:690 [in MetaCoq.Template.common.uGraph]
g:692 [in MetaCoq.Translations.MiniHoTT]
G:695 [in MetaCoq.Template.common.uGraph]
G:699 [in MetaCoq.Template.common.uGraph]
g:70 [in MetaCoq.PCUIC.PCUICAst]
g:700 [in MetaCoq.Translations.MiniHoTT_paths]
g:703 [in MetaCoq.Translations.MiniHoTT]
G:707 [in MetaCoq.Template.common.uGraph]
g:711 [in MetaCoq.Translations.MiniHoTT_paths]
g:725 [in MetaCoq.Template.utils.MCList]
g:73 [in MetaCoq.Translations.times_bool_fun2]
g:738 [in MetaCoq.Template.utils.MCList]
g:748 [in MetaCoq.Template.utils.MCList]
g:77 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
g:775 [in MetaCoq.Translations.MiniHoTT]
g:775 [in MetaCoq.PCUIC.PCUICReduction]
g:778 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
g:78 [in MetaCoq.PCUIC.PCUICSubstitution]
g:78 [in MetaCoq.Erasure.ETransform]
g:783 [in MetaCoq.Translations.MiniHoTT_paths]
g:784 [in MetaCoq.PCUIC.PCUICReduction]
G:788 [in MetaCoq.Template.utils.wGraph]
G:791 [in MetaCoq.Template.utils.wGraph]
G:797 [in MetaCoq.Template.utils.wGraph]
G:8 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
g:8 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
G:803 [in MetaCoq.Template.utils.wGraph]
G:806 [in MetaCoq.Template.utils.wGraph]
g:81 [in MetaCoq.Template.BasicAst]
g:81 [in MetaCoq.PCUIC.PCUICParallelReduction]
G:811 [in MetaCoq.Template.utils.wGraph]
g:82 [in MetaCoq.PCUIC.PCUICAst]
G:82 [in MetaCoq.Translations.param_cheap_packed]
g:82 [in MetaCoq.Template.utils.MCOption]
g:82 [in MetaCoq.Translations.times_bool_fun2]
G:820 [in MetaCoq.Template.utils.wGraph]
g:821 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
G:825 [in MetaCoq.Template.utils.wGraph]
g:832 [in MetaCoq.PCUIC.PCUICInductiveInversion]
G:832 [in MetaCoq.Template.utils.wGraph]
G:836 [in MetaCoq.Template.utils.wGraph]
g:85 [in MetaCoq.Translations.times_bool_fun2]
G:856 [in MetaCoq.Template.utils.wGraph]
g:86 [in MetaCoq.Erasure.EPretty]
g:86 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
g:86 [in MetaCoq.PCUIC.utils.PCUICOnOne]
g:86 [in MetaCoq.PCUIC.PCUICEquality]
G:865 [in MetaCoq.Template.utils.wGraph]
g:875 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
g:876 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
g:879 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
G:88 [in MetaCoq.SafeChecker.PCUICWfEnvImpl]
G:88 [in MetaCoq.Translations.param_cheap_packed]
g:886 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
g:89 [in MetaCoq.Template.BasicAst]
G:89 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
g:89 [in MetaCoq.Translations.param_generous_packed]
g:897 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
g:90 [in MetaCoq.Erasure.ETransform]
g:93 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
g:932 [in MetaCoq.PCUIC.PCUICConversion]
G:938 [in MetaCoq.Template.utils.wGraph]
g:94 [in MetaCoq.Translations.param_generous_packed]
g:950 [in MetaCoq.PCUIC.PCUICConversion]
g:960 [in MetaCoq.PCUIC.PCUICConversion]
g:965 [in MetaCoq.Template.utils.All_Forall]
g:98 [in MetaCoq.Template.utils.All_Forall]
g:99 [in MetaCoq.Template.BasicAst]
g:99 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]



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)