| 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) |
Y (binder)
ys':2198 [in MetaCoq.Template.utils.All_Forall]ys':2205 [in MetaCoq.Template.utils.All_Forall]
ys':2221 [in MetaCoq.Template.utils.All_Forall]
ys:2197 [in MetaCoq.Template.utils.All_Forall]
ys:2204 [in MetaCoq.Template.utils.All_Forall]
ys:2213 [in MetaCoq.Template.utils.All_Forall]
ys:2220 [in MetaCoq.Template.utils.All_Forall]
ys:60 [in MetaCoq.Template.utils.bytestring]
ys:65 [in MetaCoq.Template.utils.bytestring]
ys:837 [in MetaCoq.Template.utils.MCList]
YY:764 [in MetaCoq.Template.utils.wGraph]
YY:765 [in MetaCoq.Template.utils.wGraph]
yzw:2908 [in MetaCoq.Translations.MiniHoTT]
yzw:2916 [in MetaCoq.Translations.MiniHoTT_paths]
yz:2884 [in MetaCoq.Translations.MiniHoTT]
yz:2892 [in MetaCoq.Translations.MiniHoTT_paths]
yz:2894 [in MetaCoq.Translations.MiniHoTT]
yz:2902 [in MetaCoq.Translations.MiniHoTT_paths]
y_0:657 [in MetaCoq.Template.utils.wGraph]
y_0:611 [in MetaCoq.Template.utils.wGraph]
y':1050 [in MetaCoq.Translations.MiniHoTT]
y':1058 [in MetaCoq.Translations.MiniHoTT_paths]
y':11 [in MetaCoq.PCUIC.utils.PCUICUtils]
y':1248 [in MetaCoq.PCUIC.PCUICConfluence]
y':1261 [in MetaCoq.PCUIC.PCUICConfluence]
y':135 [in MetaCoq.PCUIC.utils.PCUICUtils]
y':1397 [in MetaCoq.Translations.MiniHoTT]
y':14 [in MetaCoq.PCUIC.utils.PCUICUtils]
y':1404 [in MetaCoq.Translations.MiniHoTT]
y':1405 [in MetaCoq.Translations.MiniHoTT_paths]
y':1412 [in MetaCoq.Translations.MiniHoTT_paths]
y':165 [in MetaCoq.Template.utils.wGraph]
y':173 [in MetaCoq.Template.utils.wGraph]
y':1849 [in MetaCoq.Translations.MiniHoTT]
y':1857 [in MetaCoq.Translations.MiniHoTT_paths]
y':1859 [in MetaCoq.Translations.MiniHoTT]
y':1867 [in MetaCoq.Translations.MiniHoTT_paths]
y':24 [in MetaCoq.PCUIC.Syntax.PCUICReflect]
y':2695 [in MetaCoq.Translations.MiniHoTT]
y':2703 [in MetaCoq.Translations.MiniHoTT_paths]
y':29 [in MetaCoq.PCUIC.utils.PCUICUtils]
y':33 [in MetaCoq.PCUIC.utils.PCUICUtils]
y':34 [in MetaCoq.PCUIC.Syntax.PCUICReflect]
y':44 [in MetaCoq.PCUIC.Syntax.PCUICReflect]
y':52 [in MetaCoq.PCUIC.Syntax.PCUICReflect]
y':58 [in MetaCoq.Template.utils.MCProd]
y':63 [in MetaCoq.PCUIC.Syntax.PCUICReflect]
y':64 [in MetaCoq.Template.utils.MCProd]
y':807 [in MetaCoq.Translations.MiniHoTT]
y':815 [in MetaCoq.Translations.MiniHoTT_paths]
y':819 [in MetaCoq.Translations.MiniHoTT]
y':827 [in MetaCoq.Translations.MiniHoTT_paths]
y':830 [in MetaCoq.Translations.MiniHoTT]
y':838 [in MetaCoq.Translations.MiniHoTT_paths]
y':842 [in MetaCoq.Translations.MiniHoTT]
y':850 [in MetaCoq.Translations.MiniHoTT_paths]
y':93 [in MetaCoq.PCUIC.utils.PCUICUtils]
y0:125 [in MetaCoq.PCUIC.PCUICConfluence]
y0:136 [in MetaCoq.PCUIC.PCUICConfluence]
y0:138 [in MetaCoq.PCUIC.PCUICConfluence]
y0:165 [in MetaCoq.PCUIC.PCUICInductiveInversion]
y1:1025 [in MetaCoq.Translations.MiniHoTT]
y1:1033 [in MetaCoq.Translations.MiniHoTT_paths]
y1:1716 [in MetaCoq.Translations.MiniHoTT]
y1:1724 [in MetaCoq.Translations.MiniHoTT_paths]
y1:1739 [in MetaCoq.Translations.MiniHoTT]
y1:1747 [in MetaCoq.Translations.MiniHoTT_paths]
y1:2227 [in MetaCoq.Translations.MiniHoTT]
y1:2235 [in MetaCoq.Translations.MiniHoTT_paths]
y1:2254 [in MetaCoq.Translations.MiniHoTT]
y1:2262 [in MetaCoq.Translations.MiniHoTT_paths]
y1:2398 [in MetaCoq.Translations.MiniHoTT]
y1:2406 [in MetaCoq.Translations.MiniHoTT_paths]
y1:2444 [in MetaCoq.Translations.MiniHoTT]
y1:2448 [in MetaCoq.Translations.MiniHoTT]
y1:2452 [in MetaCoq.Translations.MiniHoTT_paths]
y1:2456 [in MetaCoq.Translations.MiniHoTT_paths]
y1:2457 [in MetaCoq.Translations.MiniHoTT]
y1:2461 [in MetaCoq.Translations.MiniHoTT]
y1:2465 [in MetaCoq.Translations.MiniHoTT_paths]
y1:2469 [in MetaCoq.Translations.MiniHoTT_paths]
y1:2834 [in MetaCoq.Translations.MiniHoTT]
y1:2842 [in MetaCoq.Translations.MiniHoTT_paths]
y1:483 [in MetaCoq.Template.utils.wGraph]
y1:932 [in MetaCoq.Translations.MiniHoTT]
y1:940 [in MetaCoq.Translations.MiniHoTT_paths]
y2:1026 [in MetaCoq.Translations.MiniHoTT]
y2:1034 [in MetaCoq.Translations.MiniHoTT_paths]
y2:1717 [in MetaCoq.Translations.MiniHoTT]
y2:1725 [in MetaCoq.Translations.MiniHoTT_paths]
y2:1740 [in MetaCoq.Translations.MiniHoTT]
y2:1748 [in MetaCoq.Translations.MiniHoTT_paths]
y2:2228 [in MetaCoq.Translations.MiniHoTT]
y2:2236 [in MetaCoq.Translations.MiniHoTT_paths]
y2:2255 [in MetaCoq.Translations.MiniHoTT]
y2:2263 [in MetaCoq.Translations.MiniHoTT_paths]
y2:2399 [in MetaCoq.Translations.MiniHoTT]
y2:2407 [in MetaCoq.Translations.MiniHoTT_paths]
y2:2446 [in MetaCoq.Translations.MiniHoTT]
y2:2454 [in MetaCoq.Translations.MiniHoTT_paths]
y2:2459 [in MetaCoq.Translations.MiniHoTT]
y2:2467 [in MetaCoq.Translations.MiniHoTT_paths]
y2:2835 [in MetaCoq.Translations.MiniHoTT]
y2:2843 [in MetaCoq.Translations.MiniHoTT_paths]
y2:484 [in MetaCoq.Template.utils.wGraph]
y2:933 [in MetaCoq.Translations.MiniHoTT]
y2:941 [in MetaCoq.Translations.MiniHoTT_paths]
y:10 [in MetaCoq.PCUIC.utils.PCUICUtils]
y:10 [in MetaCoq.Template.common.uGraph]
y:10 [in MetaCoq.Translations.MiniHoTT_paths]
y:10 [in MetaCoq.SafeChecker.PCUICSafeChecker]
y:10 [in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
y:100 [in MetaCoq.Template.utils.bytestring]
y:100 [in MetaCoq.PCUIC.PCUICConvCumInversion]
y:100 [in MetaCoq.PCUIC.Syntax.PCUICReflect]
y:100 [in MetaCoq.Translations.times_bool_fun2]
y:1001 [in MetaCoq.Template.utils.All_Forall]
y:1003 [in MetaCoq.PCUIC.PCUICConfluence]
y:1003 [in MetaCoq.PCUIC.PCUICConversion]
y:1005 [in MetaCoq.Template.utils.wGraph]
y:1008 [in MetaCoq.Template.utils.wGraph]
y:101 [in MetaCoq.Translations.MiniHoTT_paths]
y:1010 [in MetaCoq.PCUIC.PCUICConfluence]
y:1011 [in MetaCoq.Template.utils.wGraph]
y:1012 [in MetaCoq.PCUIC.PCUICConfluence]
y:1014 [in MetaCoq.Template.utils.wGraph]
y:1015 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
y:1016 [in MetaCoq.Translations.MiniHoTT]
y:1018 [in MetaCoq.Template.utils.wGraph]
y:102 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
y:102 [in MetaCoq.PCUIC.PCUICSR]
y:1023 [in MetaCoq.Template.utils.wGraph]
y:1024 [in MetaCoq.Translations.MiniHoTT_paths]
y:1027 [in MetaCoq.Template.utils.wGraph]
y:1028 [in MetaCoq.Template.utils.All_Forall]
y:103 [in MetaCoq.Template.utils.bytestring]
y:103 [in MetaCoq.Template.Reflect]
y:103 [in MetaCoq.Translations.MiniHoTT_paths]
y:103 [in MetaCoq.SafeChecker.PCUICEqualityDec]
y:1034 [in MetaCoq.Translations.MiniHoTT]
y:1035 [in MetaCoq.Template.utils.wGraph]
y:1039 [in MetaCoq.Translations.MiniHoTT]
y:104 [in MetaCoq.SafeChecker.PCUICSafeConversion]
y:104 [in MetaCoq.PCUIC.PCUICConfluence]
y:1041 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
y:1042 [in MetaCoq.Template.utils.wGraph]
y:1042 [in MetaCoq.Translations.MiniHoTT_paths]
y:1043 [in MetaCoq.Template.utils.All_Forall]
y:1044 [in MetaCoq.Template.utils.wGraph]
y:1045 [in MetaCoq.PCUIC.PCUICConversion]
y:1047 [in MetaCoq.Template.utils.wGraph]
y:1047 [in MetaCoq.Translations.MiniHoTT_paths]
y:105 [in MetaCoq.Template.utils.bytestring]
y:1053 [in MetaCoq.PCUIC.PCUICConfluence]
y:1054 [in MetaCoq.Template.utils.All_Forall]
y:1055 [in MetaCoq.Translations.MiniHoTT]
y:1057 [in MetaCoq.Template.utils.wGraph]
y:106 [in MetaCoq.PCUIC.PCUICParallelReduction]
y:106 [in MetaCoq.PCUIC.PCUICFirstorder]
y:106 [in MetaCoq.Template.utils.wGraph]
y:1060 [in MetaCoq.PCUIC.PCUICConfluence]
y:1060 [in MetaCoq.Translations.MiniHoTT]
y:1061 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
y:1063 [in MetaCoq.PCUIC.PCUICConfluence]
y:1063 [in MetaCoq.Translations.MiniHoTT_paths]
y:1066 [in MetaCoq.Template.utils.All_Forall]
y:1068 [in MetaCoq.Template.utils.wGraph]
y:1068 [in MetaCoq.PCUIC.PCUICConfluence]
y:1068 [in MetaCoq.Translations.MiniHoTT]
y:1068 [in MetaCoq.Translations.MiniHoTT_paths]
y:107 [in MetaCoq.Template.Reflect]
y:1074 [in MetaCoq.Translations.MiniHoTT]
y:1076 [in MetaCoq.Translations.MiniHoTT_paths]
y:1078 [in MetaCoq.Translations.MiniHoTT]
y:1079 [in MetaCoq.PCUIC.PCUICConfluence]
y:108 [in MetaCoq.PCUIC.utils.PCUICUtils]
y:108 [in MetaCoq.Template.utils.bytestring]
y:1081 [in MetaCoq.PCUIC.PCUICConfluence]
y:1082 [in MetaCoq.Translations.MiniHoTT_paths]
y:1084 [in MetaCoq.PCUIC.PCUICConfluence]
y:1084 [in MetaCoq.Translations.MiniHoTT]
y:1086 [in MetaCoq.Translations.MiniHoTT_paths]
y:1088 [in MetaCoq.PCUIC.PCUICConfluence]
y:109 [in MetaCoq.Translations.param_binary]
y:109 [in MetaCoq.Template.monad_utils]
y:109 [in MetaCoq.PCUIC.PCUICSR]
y:1090 [in MetaCoq.Translations.MiniHoTT]
y:1092 [in MetaCoq.Translations.MiniHoTT_paths]
y:1096 [in MetaCoq.Template.utils.All_Forall]
y:1098 [in MetaCoq.Translations.MiniHoTT]
y:1098 [in MetaCoq.Translations.MiniHoTT_paths]
y:11 [in MetaCoq.Template.utils.ByteCompareSpec]
y:11 [in MetaCoq.Template.utils.MCEquality]
y:11 [in MetaCoq.PCUIC.PCUICConvCumInversion]
y:11 [in MetaCoq.PCUIC.Syntax.PCUICReflect]
y:11 [in MetaCoq.Translations.times_bool_fun2]
y:110 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
y:110 [in MetaCoq.SafeChecker.PCUICSafeReduce]
y:1100 [in MetaCoq.Template.utils.wGraph]
y:1105 [in MetaCoq.Template.utils.All_Forall]
y:1106 [in MetaCoq.Translations.MiniHoTT]
y:1106 [in MetaCoq.Translations.MiniHoTT_paths]
y:1108 [in MetaCoq.Template.utils.wGraph]
y:111 [in MetaCoq.PCUIC.utils.PCUICUtils]
y:111 [in MetaCoq.Template.utils.bytestring]
y:111 [in MetaCoq.Template.Reflect]
y:1112 [in MetaCoq.Template.utils.wGraph]
y:1114 [in MetaCoq.Translations.MiniHoTT]
y:1114 [in MetaCoq.Translations.MiniHoTT_paths]
y:1117 [in MetaCoq.PCUIC.PCUICConfluence]
y:1118 [in MetaCoq.Template.utils.wGraph]
y:1119 [in MetaCoq.PCUIC.PCUICConfluence]
y:1121 [in MetaCoq.Template.utils.wGraph]
y:1122 [in MetaCoq.Translations.MiniHoTT]
y:1122 [in MetaCoq.Translations.MiniHoTT_paths]
y:1125 [in MetaCoq.Template.utils.All_Forall]
y:1127 [in MetaCoq.Template.utils.wGraph]
y:1128 [in MetaCoq.Translations.MiniHoTT]
y:113 [in MetaCoq.Template.utils.bytestring]
y:113 [in MetaCoq.PCUIC.PCUICConfluence]
y:1130 [in MetaCoq.Translations.MiniHoTT_paths]
y:1131 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
y:1134 [in MetaCoq.Template.utils.All_Forall]
y:1134 [in MetaCoq.PCUIC.PCUICConfluence]
y:1134 [in MetaCoq.Translations.MiniHoTT]
y:1136 [in MetaCoq.PCUIC.PCUICConfluence]
y:1136 [in MetaCoq.Translations.MiniHoTT_paths]
y:1138 [in MetaCoq.Template.utils.wGraph]
y:1138 [in MetaCoq.PCUIC.PCUICConfluence]
y:114 [in MetaCoq.PCUIC.Syntax.PCUICReflect]
y:1140 [in MetaCoq.Translations.MiniHoTT]
y:1142 [in MetaCoq.Translations.MiniHoTT_paths]
y:1143 [in MetaCoq.Template.utils.All_Forall]
y:1145 [in MetaCoq.PCUIC.PCUICConfluence]
y:1145 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
y:1147 [in MetaCoq.Template.utils.wGraph]
y:1147 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
y:1148 [in MetaCoq.Translations.MiniHoTT_paths]
y:115 [in MetaCoq.Template.utils.bytestring]
y:1152 [in MetaCoq.Template.utils.All_Forall]
y:1152 [in MetaCoq.Translations.MiniHoTT]
y:1156 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
y:1158 [in MetaCoq.Translations.MiniHoTT]
y:1158 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
y:116 [in MetaCoq.Template.utils.wGraph]
y:116 [in MetaCoq.Erasure.ErasureFunction]
y:1160 [in MetaCoq.Translations.MiniHoTT_paths]
y:1161 [in MetaCoq.Template.utils.All_Forall]
y:1164 [in MetaCoq.Translations.MiniHoTT]
y:1166 [in MetaCoq.Translations.MiniHoTT_paths]
y:1167 [in MetaCoq.PCUIC.PCUICReduction]
y:1169 [in MetaCoq.PCUIC.PCUICConfluence]
y:117 [in MetaCoq.PCUIC.utils.PCUICUtils]
Y:117 [in MetaCoq.Template.monad_utils]
y:1170 [in MetaCoq.Template.utils.All_Forall]
y:1172 [in MetaCoq.Template.utils.wGraph]
y:1172 [in MetaCoq.PCUIC.PCUICConfluence]
y:1172 [in MetaCoq.Translations.MiniHoTT_paths]
y:1175 [in MetaCoq.Translations.MiniHoTT]
y:118 [in MetaCoq.Template.utils.bytestring]
y:1183 [in MetaCoq.Translations.MiniHoTT_paths]
y:1186 [in MetaCoq.Translations.MiniHoTT]
Y:119 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
y:1194 [in MetaCoq.Translations.MiniHoTT_paths]
y:1196 [in MetaCoq.Translations.MiniHoTT]
y:12 [in MetaCoq.Template.utils.MCRelations]
y:12 [in MetaCoq.Translations.MiniHoTT]
y:120 [in MetaCoq.PCUIC.utils.PCUICUtils]
y:120 [in MetaCoq.Template.utils.bytestring]
y:1204 [in MetaCoq.Translations.MiniHoTT_paths]
y:1206 [in MetaCoq.Translations.MiniHoTT]
y:121 [in MetaCoq.Translations.MiniHoTT]
y:1211 [in MetaCoq.PCUIC.PCUICConfluence]
y:1213 [in MetaCoq.PCUIC.PCUICConfluence]
y:1214 [in MetaCoq.Translations.MiniHoTT]
y:1214 [in MetaCoq.Translations.MiniHoTT_paths]
y:1216 [in MetaCoq.PCUIC.PCUICConfluence]
y:122 [in MetaCoq.Template.utils.bytestring]
y:122 [in MetaCoq.Template.utils.wGraph]
y:1221 [in MetaCoq.PCUIC.PCUICConfluence]
y:1221 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
y:1222 [in MetaCoq.Translations.MiniHoTT]
y:1222 [in MetaCoq.Translations.MiniHoTT_paths]
y:1224 [in MetaCoq.PCUIC.PCUICConfluence]
y:1227 [in MetaCoq.PCUIC.PCUICConfluence]
y:123 [in MetaCoq.PCUIC.utils.PCUICUtils]
y:123 [in MetaCoq.Template.monad_utils]
y:1230 [in MetaCoq.Translations.MiniHoTT]
y:1230 [in MetaCoq.Translations.MiniHoTT_paths]
y:1233 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
y:1238 [in MetaCoq.Translations.MiniHoTT]
y:1238 [in MetaCoq.Translations.MiniHoTT_paths]
y:124 [in MetaCoq.PCUIC.PCUICConfluence]
y:1246 [in MetaCoq.PCUIC.PCUICConfluence]
y:1246 [in MetaCoq.Translations.MiniHoTT_paths]
y:1249 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
y:125 [in MetaCoq.Template.utils.All_Forall]
Y:125 [in MetaCoq.Template.monad_utils]
y:1252 [in MetaCoq.Translations.MiniHoTT]
y:1259 [in MetaCoq.PCUIC.PCUICConfluence]
y:1259 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
y:126 [in MetaCoq.Template.TermEquality]
y:126 [in MetaCoq.Template.utils.bytestring]
y:126 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
y:1260 [in MetaCoq.Translations.MiniHoTT_paths]
y:1264 [in MetaCoq.Translations.MiniHoTT]
y:1271 [in MetaCoq.SafeChecker.PCUICSafeReduce]
y:1272 [in MetaCoq.Translations.MiniHoTT]
y:1272 [in MetaCoq.Translations.MiniHoTT_paths]
y:1276 [in MetaCoq.Template.utils.All_Forall]
y:1277 [in MetaCoq.SafeChecker.PCUICSafeReduce]
y:128 [in MetaCoq.Translations.MiniHoTT]
y:1280 [in MetaCoq.SafeChecker.PCUICSafeReduce]
y:1280 [in MetaCoq.Translations.MiniHoTT_paths]
y:1284 [in MetaCoq.Translations.MiniHoTT]
y:1287 [in MetaCoq.SafeChecker.PCUICSafeReduce]
y:129 [in MetaCoq.Translations.MiniHoTT_paths]
y:1291 [in MetaCoq.SafeChecker.PCUICSafeReduce]
y:1292 [in MetaCoq.Translations.MiniHoTT]
y:1292 [in MetaCoq.Translations.MiniHoTT_paths]
y:1295 [in MetaCoq.PCUIC.PCUICConfluence]
y:1298 [in MetaCoq.SafeChecker.PCUICSafeReduce]
y:13 [in MetaCoq.Template.utils.ByteCompareSpec]
y:13 [in MetaCoq.PCUIC.utils.PCUICUtils]
y:13 [in MetaCoq.Template.utils.bytestring]
y:13 [in MetaCoq.PCUIC.Syntax.PCUICReflect]
y:130 [in MetaCoq.PCUIC.utils.PCUICUtils]
y:130 [in MetaCoq.Translations.MiniHoTT]
y:1300 [in MetaCoq.Translations.MiniHoTT_paths]
y:1302 [in MetaCoq.Translations.MiniHoTT]
y:1310 [in MetaCoq.Translations.MiniHoTT_paths]
y:1313 [in MetaCoq.Translations.MiniHoTT]
y:1315 [in MetaCoq.SafeChecker.PCUICSafeReduce]
y:1321 [in MetaCoq.Translations.MiniHoTT_paths]
y:1323 [in MetaCoq.Translations.MiniHoTT]
y:133 [in MetaCoq.PCUIC.PCUICConfluence]
y:1331 [in MetaCoq.Translations.MiniHoTT_paths]
y:1332 [in MetaCoq.Translations.MiniHoTT]
y:134 [in MetaCoq.PCUIC.utils.PCUICUtils]
y:134 [in MetaCoq.Template.TermEquality]
y:134 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
y:134 [in MetaCoq.Erasure.Prelim]
y:1340 [in MetaCoq.Translations.MiniHoTT_paths]
y:135 [in MetaCoq.Erasure.EInduction]
y:1359 [in MetaCoq.Translations.MiniHoTT]
y:136 [in MetaCoq.Translations.MiniHoTT_paths]
y:1361 [in MetaCoq.Template.utils.All_Forall]
y:1363 [in MetaCoq.Translations.MiniHoTT]
y:1367 [in MetaCoq.Translations.MiniHoTT_paths]
y:1367 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
y:137 [in MetaCoq.PCUIC.PCUICSafeLemmata]
y:137 [in MetaCoq.PCUIC.utils.PCUICUtils]
y:1371 [in MetaCoq.Translations.MiniHoTT]
y:1371 [in MetaCoq.Translations.MiniHoTT_paths]
y:1375 [in MetaCoq.Translations.MiniHoTT]
y:1379 [in MetaCoq.SafeChecker.PCUICSafeReduce]
y:1379 [in MetaCoq.Translations.MiniHoTT_paths]
y:138 [in MetaCoq.Translations.MiniHoTT_paths]
y:1380 [in MetaCoq.Translations.MiniHoTT]
y:1383 [in MetaCoq.Translations.MiniHoTT]
y:1383 [in MetaCoq.Translations.MiniHoTT_paths]
y:1388 [in MetaCoq.Translations.MiniHoTT]
y:1388 [in MetaCoq.Translations.MiniHoTT_paths]
y:139 [in MetaCoq.Template.TermEquality]
y:1391 [in MetaCoq.Translations.MiniHoTT_paths]
y:1393 [in MetaCoq.Translations.MiniHoTT]
y:1394 [in MetaCoq.Template.utils.All_Forall]
y:1396 [in MetaCoq.Translations.MiniHoTT_paths]
y:14 [in MetaCoq.Template.utils.MCCompare]
y:14 [in MetaCoq.Template.common.uGraph]
y:14 [in MetaCoq.Translations.MiniHoTT]
y:1400 [in MetaCoq.Translations.MiniHoTT]
y:1401 [in MetaCoq.Translations.MiniHoTT_paths]
y:1407 [in MetaCoq.Translations.MiniHoTT]
y:1408 [in MetaCoq.Translations.MiniHoTT_paths]
y:1410 [in MetaCoq.Template.utils.All_Forall]
y:1411 [in MetaCoq.Translations.MiniHoTT]
y:1415 [in MetaCoq.Translations.MiniHoTT_paths]
y:1418 [in MetaCoq.Translations.MiniHoTT]
y:1419 [in MetaCoq.Translations.MiniHoTT_paths]
y:142 [in MetaCoq.PCUIC.PCUICNormal]
y:142 [in MetaCoq.SafeChecker.PCUICSafeChecker]
y:1420 [in MetaCoq.Translations.MiniHoTT]
y:1426 [in MetaCoq.Translations.MiniHoTT_paths]
y:1428 [in MetaCoq.Translations.MiniHoTT_paths]
y:1438 [in MetaCoq.Template.utils.All_Forall]
y:144 [in MetaCoq.PCUIC.PCUICSafeLemmata]
y:144 [in MetaCoq.Template.utils.MCProd]
y:1449 [in MetaCoq.SafeChecker.PCUICSafeReduce]
y:145 [in MetaCoq.Template.Universes]
y:1452 [in MetaCoq.SafeChecker.PCUICSafeReduce]
y:1457 [in MetaCoq.Template.utils.All_Forall]
y:146 [in MetaCoq.PCUIC.PCUICAlpha]
y:1469 [in MetaCoq.Translations.MiniHoTT]
y:1470 [in MetaCoq.Translations.MiniHoTT]
y:1471 [in MetaCoq.Translations.MiniHoTT]
y:1477 [in MetaCoq.Translations.MiniHoTT_paths]
y:1478 [in MetaCoq.Translations.MiniHoTT_paths]
y:1479 [in MetaCoq.Translations.MiniHoTT_paths]
y:1488 [in MetaCoq.Template.utils.All_Forall]
y:15 [in MetaCoq.Template.utils.ByteCompareSpec]
y:1503 [in MetaCoq.Template.utils.All_Forall]
y:151 [in MetaCoq.PCUIC.PCUICConfluence]
y:153 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
y:1530 [in MetaCoq.Template.utils.All_Forall]
y:1531 [in MetaCoq.Translations.MiniHoTT]
y:1537 [in MetaCoq.Template.utils.All_Forall]
y:1539 [in MetaCoq.Translations.MiniHoTT_paths]
y:154 [in MetaCoq.PCUIC.PCUICConfluence]
y:1545 [in MetaCoq.Template.utils.All_Forall]
y:155 [in MetaCoq.PCUIC.PCUICCumulativity]
y:1558 [in MetaCoq.Translations.MiniHoTT]
y:1565 [in MetaCoq.Translations.MiniHoTT]
y:1566 [in MetaCoq.Translations.MiniHoTT_paths]
y:1567 [in MetaCoq.Template.utils.All_Forall]
y:157 [in MetaCoq.PCUIC.PCUICConfluence]
y:1572 [in MetaCoq.Translations.MiniHoTT]
y:1573 [in MetaCoq.Translations.MiniHoTT_paths]
y:1579 [in MetaCoq.Translations.MiniHoTT]
y:158 [in MetaCoq.PCUIC.PCUICElimination]
y:1580 [in MetaCoq.Translations.MiniHoTT_paths]
y:1582 [in MetaCoq.Template.utils.All_Forall]
y:1587 [in MetaCoq.Translations.MiniHoTT_paths]
y:159 [in MetaCoq.PCUIC.PCUICConfluence]
y:159 [in MetaCoq.Translations.MiniHoTT]
Y:160 [in MetaCoq.Template.monad_utils]
y:1605 [in MetaCoq.Template.utils.All_Forall]
y:161 [in MetaCoq.Template.utils.wGraph]
y:161 [in MetaCoq.PCUIC.PCUICConfluence]
y:1610 [in MetaCoq.Translations.MiniHoTT]
y:1616 [in MetaCoq.Template.utils.All_Forall]
y:1618 [in MetaCoq.Translations.MiniHoTT_paths]
y:1625 [in MetaCoq.Template.utils.All_Forall]
y:163 [in MetaCoq.SafeChecker.PCUICSafeReduce]
y:163 [in MetaCoq.PCUIC.PCUICConfluence]
y:1633 [in MetaCoq.Template.utils.All_Forall]
y:1636 [in MetaCoq.Translations.MiniHoTT]
y:1641 [in MetaCoq.Template.utils.All_Forall]
y:1644 [in MetaCoq.Translations.MiniHoTT_paths]
y:1649 [in MetaCoq.Template.utils.All_Forall]
y:167 [in MetaCoq.Translations.MiniHoTT_paths]
y:1679 [in MetaCoq.Translations.MiniHoTT]
y:1687 [in MetaCoq.Translations.MiniHoTT_paths]
y:1689 [in MetaCoq.Translations.MiniHoTT]
y:169 [in MetaCoq.Template.utils.wGraph]
y:1691 [in MetaCoq.Translations.MiniHoTT]
y:1697 [in MetaCoq.Template.utils.All_Forall]
y:1697 [in MetaCoq.Translations.MiniHoTT_paths]
y:1699 [in MetaCoq.Translations.MiniHoTT_paths]
y:17 [in MetaCoq.Template.utils.MCCompare]
y:17 [in MetaCoq.Template.common.uGraph]
y:170 [in MetaCoq.PCUIC.PCUICEquality]
y:170 [in MetaCoq.PCUIC.PCUICConfluence]
y:1700 [in MetaCoq.Translations.MiniHoTT]
y:1701 [in MetaCoq.Translations.MiniHoTT]
y:1708 [in MetaCoq.Template.utils.All_Forall]
y:1708 [in MetaCoq.Translations.MiniHoTT_paths]
y:1709 [in MetaCoq.Translations.MiniHoTT_paths]
y:1710 [in MetaCoq.Translations.MiniHoTT]
y:1718 [in MetaCoq.Translations.MiniHoTT_paths]
y:1720 [in MetaCoq.Translations.MiniHoTT]
y:1728 [in MetaCoq.Translations.MiniHoTT_paths]
y:1732 [in MetaCoq.Template.utils.All_Forall]
y:1732 [in MetaCoq.Translations.MiniHoTT]
y:174 [in MetaCoq.Translations.times_bool_fun]
y:1740 [in MetaCoq.Translations.MiniHoTT_paths]
y:1744 [in MetaCoq.Translations.MiniHoTT]
y:175 [in MetaCoq.PCUIC.PCUICConfluence]
Y:175 [in MetaCoq.Template.monad_utils]
y:175 [in MetaCoq.PCUIC.PCUICSR]
y:1752 [in MetaCoq.Translations.MiniHoTT_paths]
y:1757 [in MetaCoq.Template.utils.All_Forall]
y:177 [in MetaCoq.SafeChecker.PCUICSafeReduce]
y:178 [in MetaCoq.PCUIC.PCUICEquality]
y:178 [in MetaCoq.Template.utils.wGraph]
y:178 [in MetaCoq.Translations.MiniHoTT]
y:1780 [in MetaCoq.Template.utils.All_Forall]
y:1784 [in MetaCoq.Translations.MiniHoTT]
y:1792 [in MetaCoq.Translations.MiniHoTT_paths]
y:1794 [in MetaCoq.Template.utils.All_Forall]
y:1797 [in MetaCoq.Translations.MiniHoTT]
y:18 [in MetaCoq.Template.utils.MCReflect]
y:18 [in MetaCoq.Template.utils.MCRelations]
y:18 [in MetaCoq.Template.utils.ByteCompareSpec]
y:18 [in MetaCoq.PCUIC.PCUICSR]
y:180 [in MetaCoq.Translations.times_bool_fun]
y:180 [in MetaCoq.Template.utils.wGraph]
y:180 [in MetaCoq.PCUIC.PCUICConfluence]
y:1802 [in MetaCoq.Translations.MiniHoTT]
y:1805 [in MetaCoq.Translations.MiniHoTT_paths]
y:1808 [in MetaCoq.Translations.MiniHoTT]
y:1810 [in MetaCoq.Translations.MiniHoTT_paths]
y:1811 [in MetaCoq.Translations.MiniHoTT]
y:1814 [in MetaCoq.Translations.MiniHoTT]
y:1816 [in MetaCoq.Translations.MiniHoTT_paths]
y:1817 [in MetaCoq.Translations.MiniHoTT]
y:1819 [in MetaCoq.Translations.MiniHoTT_paths]
y:182 [in MetaCoq.Template.utils.wGraph]
y:182 [in MetaCoq.Translations.MiniHoTT]
y:1822 [in MetaCoq.Translations.MiniHoTT]
y:1822 [in MetaCoq.Translations.MiniHoTT_paths]
y:1825 [in MetaCoq.Translations.MiniHoTT_paths]
y:1826 [in MetaCoq.Translations.MiniHoTT]
y:183 [in MetaCoq.Translations.times_bool_fun]
y:183 [in MetaCoq.PCUIC.PCUICEquality]
y:1830 [in MetaCoq.Translations.MiniHoTT_paths]
y:1834 [in MetaCoq.Translations.MiniHoTT_paths]
y:1835 [in MetaCoq.Template.utils.All_Forall]
y:184 [in MetaCoq.Template.utils.wGraph]
y:1840 [in MetaCoq.Translations.MiniHoTT]
y:1847 [in MetaCoq.Template.utils.All_Forall]
y:1848 [in MetaCoq.Translations.MiniHoTT]
y:1848 [in MetaCoq.Translations.MiniHoTT_paths]
y:185 [in MetaCoq.Template.Checker]
y:185 [in MetaCoq.PCUIC.PCUICConfluence]
y:1856 [in MetaCoq.Translations.MiniHoTT_paths]
y:1858 [in MetaCoq.Translations.MiniHoTT]
y:186 [in MetaCoq.Translations.times_bool_fun]
y:186 [in MetaCoq.Template.common.uGraph]
y:186 [in MetaCoq.Template.utils.wGraph]
y:186 [in MetaCoq.Translations.MiniHoTT_paths]
y:1864 [in MetaCoq.Template.utils.All_Forall]
y:1865 [in MetaCoq.Translations.MiniHoTT]
y:1866 [in MetaCoq.Translations.MiniHoTT_paths]
y:187 [in MetaCoq.Template.Checker]
y:187 [in MetaCoq.Translations.MiniHoTT]
y:1871 [in MetaCoq.Template.utils.All_Forall]
y:1872 [in MetaCoq.Translations.MiniHoTT]
y:1873 [in MetaCoq.Translations.MiniHoTT_paths]
y:1879 [in MetaCoq.Translations.MiniHoTT]
y:188 [in MetaCoq.Template.utils.All_Forall]
y:188 [in MetaCoq.Template.common.uGraph]
y:188 [in MetaCoq.PCUIC.PCUICConfluence]
y:1880 [in MetaCoq.Translations.MiniHoTT_paths]
y:1886 [in MetaCoq.Translations.MiniHoTT]
y:1887 [in MetaCoq.Translations.MiniHoTT_paths]
y:1893 [in MetaCoq.Translations.MiniHoTT]
y:1894 [in MetaCoq.Translations.MiniHoTT_paths]
y:19 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
y:19 [in MetaCoq.Template.common.uGraph]
y:19 [in MetaCoq.Translations.times_bool_fun2]
y:190 [in MetaCoq.Translations.MiniHoTT_paths]
y:1901 [in MetaCoq.Translations.MiniHoTT]
y:1901 [in MetaCoq.Translations.MiniHoTT_paths]
y:1909 [in MetaCoq.Translations.MiniHoTT]
y:1909 [in MetaCoq.Translations.MiniHoTT_paths]
y:191 [in MetaCoq.Translations.MiniHoTT]
y:1916 [in MetaCoq.Translations.MiniHoTT]
y:1917 [in MetaCoq.Translations.MiniHoTT_paths]
Y:192 [in MetaCoq.Template.monad_utils]
y:1923 [in MetaCoq.Translations.MiniHoTT]
y:1924 [in MetaCoq.Translations.MiniHoTT_paths]
y:193 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
y:193 [in MetaCoq.PCUIC.PCUICConfluence]
y:1930 [in MetaCoq.Translations.MiniHoTT]
y:1931 [in MetaCoq.Translations.MiniHoTT_paths]
y:1937 [in MetaCoq.Translations.MiniHoTT]
y:1938 [in MetaCoq.Translations.MiniHoTT_paths]
y:1944 [in MetaCoq.Translations.MiniHoTT]
y:1945 [in MetaCoq.Template.utils.All_Forall]
y:1945 [in MetaCoq.Translations.MiniHoTT_paths]
y:195 [in MetaCoq.Template.utils.All_Forall]
y:195 [in MetaCoq.Examples.tauto]
y:195 [in MetaCoq.Translations.MiniHoTT]
y:195 [in MetaCoq.Translations.MiniHoTT_paths]
y:1951 [in MetaCoq.Translations.MiniHoTT]
y:1952 [in MetaCoq.Translations.MiniHoTT_paths]
y:1958 [in MetaCoq.Translations.MiniHoTT]
y:1959 [in MetaCoq.Translations.MiniHoTT_paths]
y:196 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
y:196 [in MetaCoq.Template.utils.wGraph]
y:1965 [in MetaCoq.Translations.MiniHoTT]
y:1966 [in MetaCoq.Template.utils.All_Forall]
y:1966 [in MetaCoq.Translations.MiniHoTT_paths]
y:197 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
y:1972 [in MetaCoq.Template.utils.All_Forall]
y:1972 [in MetaCoq.Translations.MiniHoTT]
y:1973 [in MetaCoq.Translations.MiniHoTT_paths]
y:1979 [in MetaCoq.Translations.MiniHoTT]
y:198 [in MetaCoq.Template.Checker]
y:198 [in MetaCoq.PCUIC.PCUICConfluence]
y:1980 [in MetaCoq.Translations.MiniHoTT_paths]
y:1985 [in MetaCoq.Template.utils.All_Forall]
y:1986 [in MetaCoq.Translations.MiniHoTT]
y:1987 [in MetaCoq.Translations.MiniHoTT_paths]
y:199 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
y:199 [in MetaCoq.Translations.MiniHoTT_paths]
y:1992 [in MetaCoq.Template.utils.All_Forall]
y:1993 [in MetaCoq.Translations.MiniHoTT]
y:1994 [in MetaCoq.Translations.MiniHoTT_paths]
y:2 [in MetaCoq.Template.utils.ByteCompare]
Y:2 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
y:2 [in MetaCoq.Template.WfAst]
Y:2 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
y:2 [in MetaCoq.Template.Reflect]
y:2 [in MetaCoq.Erasure.EReflect]
y:20 [in MetaCoq.Template.utils.MCCompare]
y:20 [in MetaCoq.Template.utils.MCRelations]
y:20 [in MetaCoq.Template.utils.All_Forall]
y:20 [in MetaCoq.Translations.MiniHoTT_paths]
y:20 [in MetaCoq.Erasure.EReflect]
y:200 [in MetaCoq.PCUIC.utils.PCUICAstUtils]
y:200 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
y:200 [in MetaCoq.Template.Checker]
y:2000 [in MetaCoq.Translations.MiniHoTT]
y:2001 [in MetaCoq.Translations.MiniHoTT_paths]
y:2007 [in MetaCoq.Translations.MiniHoTT]
y:2008 [in MetaCoq.Translations.MiniHoTT_paths]
y:201 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
y:201 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
y:2014 [in MetaCoq.Translations.MiniHoTT]
y:2015 [in MetaCoq.Translations.MiniHoTT_paths]
y:2016 [in MetaCoq.Template.utils.All_Forall]
y:202 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
y:202 [in MetaCoq.Template.utils.wGraph]
y:2021 [in MetaCoq.Translations.MiniHoTT]
y:2022 [in MetaCoq.Translations.MiniHoTT_paths]
y:2028 [in MetaCoq.Translations.MiniHoTT]
y:2029 [in MetaCoq.Translations.MiniHoTT_paths]
y:203 [in MetaCoq.Translations.MiniHoTT]
y:203 [in MetaCoq.Translations.MiniHoTT_paths]
y:203 [in MetaCoq.PCUIC.PCUICSR]
y:2035 [in MetaCoq.Translations.MiniHoTT]
y:2036 [in MetaCoq.Translations.MiniHoTT_paths]
y:2040 [in MetaCoq.Translations.MiniHoTT]
y:2043 [in MetaCoq.Translations.MiniHoTT_paths]
y:2045 [in MetaCoq.Translations.MiniHoTT]
y:2048 [in MetaCoq.Translations.MiniHoTT_paths]
Y:205 [in MetaCoq.SafeChecker.PCUICWfEnv]
y:205 [in MetaCoq.Template.utils.wGraph]
y:205 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
y:2050 [in MetaCoq.Translations.MiniHoTT]
y:2051 [in MetaCoq.Template.utils.All_Forall]
y:2053 [in MetaCoq.Translations.MiniHoTT_paths]
y:2055 [in MetaCoq.Translations.MiniHoTT]
y:2058 [in MetaCoq.Translations.MiniHoTT_paths]
y:2060 [in MetaCoq.Translations.MiniHoTT]
y:2063 [in MetaCoq.Translations.MiniHoTT_paths]
y:2065 [in MetaCoq.Translations.MiniHoTT]
y:2068 [in MetaCoq.Translations.MiniHoTT_paths]
y:2070 [in MetaCoq.Translations.MiniHoTT]
y:2073 [in MetaCoq.Translations.MiniHoTT_paths]
y:2075 [in MetaCoq.Template.utils.All_Forall]
y:2076 [in MetaCoq.Translations.MiniHoTT]
y:2078 [in MetaCoq.Translations.MiniHoTT_paths]
y:208 [in MetaCoq.PCUIC.PCUICSR]
y:2084 [in MetaCoq.Translations.MiniHoTT]
y:2084 [in MetaCoq.Translations.MiniHoTT_paths]
y:2085 [in MetaCoq.Template.utils.All_Forall]
y:209 [in MetaCoq.PCUIC.PCUICConfluence]
Y:209 [in MetaCoq.Template.monad_utils]
y:2092 [in MetaCoq.Template.utils.All_Forall]
y:2092 [in MetaCoq.Translations.MiniHoTT]
y:2092 [in MetaCoq.Translations.MiniHoTT_paths]
y:2099 [in MetaCoq.Translations.MiniHoTT]
y:21 [in MetaCoq.PCUIC.PCUICRedTypeIrrelevance]
y:21 [in MetaCoq.Template.utils.ByteCompareSpec]
y:21 [in MetaCoq.Template.common.uGraph]
y:21 [in MetaCoq.Translations.MiniHoTT]
y:210 [in MetaCoq.Template.utils.wGraph]
y:2100 [in MetaCoq.Template.utils.All_Forall]
y:2100 [in MetaCoq.Translations.MiniHoTT_paths]
y:2106 [in MetaCoq.Translations.MiniHoTT]
y:2107 [in MetaCoq.Translations.MiniHoTT_paths]
y:211 [in MetaCoq.Translations.MiniHoTT]
y:211 [in MetaCoq.Translations.MiniHoTT_paths]
y:2114 [in MetaCoq.Translations.MiniHoTT]
y:2114 [in MetaCoq.Translations.MiniHoTT_paths]
Y:212 [in MetaCoq.SafeChecker.PCUICWfEnv]
y:212 [in MetaCoq.PCUIC.PCUICConfluence]
y:2122 [in MetaCoq.Translations.MiniHoTT]
y:2122 [in MetaCoq.Translations.MiniHoTT_paths]
Y:2124 [in MetaCoq.Template.utils.All_Forall]
y:2129 [in MetaCoq.Translations.MiniHoTT]
y:2130 [in MetaCoq.Translations.MiniHoTT_paths]
y:2136 [in MetaCoq.Translations.MiniHoTT]
y:2137 [in MetaCoq.Translations.MiniHoTT_paths]
y:214 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
y:2143 [in MetaCoq.Template.utils.All_Forall]
y:2143 [in MetaCoq.Translations.MiniHoTT]
y:2144 [in MetaCoq.Translations.MiniHoTT_paths]
y:215 [in MetaCoq.Template.utils.wGraph]
y:215 [in MetaCoq.Translations.MiniHoTT]
y:2150 [in MetaCoq.Translations.MiniHoTT]
y:2151 [in MetaCoq.Translations.MiniHoTT_paths]
y:2154 [in MetaCoq.Template.utils.All_Forall]
y:2157 [in MetaCoq.Translations.MiniHoTT]
y:2158 [in MetaCoq.Translations.MiniHoTT_paths]
y:216 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
y:2163 [in MetaCoq.Template.utils.All_Forall]
y:2165 [in MetaCoq.Translations.MiniHoTT_paths]
y:2166 [in MetaCoq.Translations.MiniHoTT]
y:217 [in MetaCoq.PCUIC.PCUICSR]
y:2171 [in MetaCoq.Template.utils.All_Forall]
y:2174 [in MetaCoq.Translations.MiniHoTT]
y:2174 [in MetaCoq.Translations.MiniHoTT_paths]
y:2180 [in MetaCoq.Translations.MiniHoTT]
y:2182 [in MetaCoq.Translations.MiniHoTT_paths]
y:2188 [in MetaCoq.Translations.MiniHoTT]
y:2188 [in MetaCoq.Translations.MiniHoTT_paths]
y:219 [in MetaCoq.Translations.MiniHoTT]
y:219 [in MetaCoq.Translations.MiniHoTT_paths]
y:219 [in MetaCoq.PCUIC.PCUICSR]
Y:2191 [in MetaCoq.Template.utils.All_Forall]
y:2194 [in MetaCoq.Translations.MiniHoTT]
y:2196 [in MetaCoq.Translations.MiniHoTT_paths]
y:22 [in MetaCoq.Template.utils.MCRelations]
y:22 [in MetaCoq.PCUIC.Syntax.PCUICViews]
y:22 [in MetaCoq.PCUIC.PCUICAlpha]
y:22 [in MetaCoq.Template.utils.ReflectEq]
y:22 [in MetaCoq.Translations.MiniHoTT_paths]
y:22 [in MetaCoq.Translations.times_bool_fun2]
y:220 [in MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance]
Y:2200 [in MetaCoq.Template.utils.All_Forall]
y:2202 [in MetaCoq.Translations.MiniHoTT]
y:2202 [in MetaCoq.Translations.MiniHoTT_paths]
y:2208 [in MetaCoq.Translations.MiniHoTT]
Y:2209 [in MetaCoq.Template.utils.All_Forall]
y:2210 [in MetaCoq.Translations.MiniHoTT_paths]
Y:2215 [in MetaCoq.Template.utils.All_Forall]
y:2216 [in MetaCoq.Translations.MiniHoTT]
y:2216 [in MetaCoq.Translations.MiniHoTT_paths]
y:222 [in MetaCoq.Template.utils.All_Forall]
y:222 [in MetaCoq.PCUIC.PCUICContexts]
y:2220 [in MetaCoq.Translations.MiniHoTT]
y:2224 [in MetaCoq.Translations.MiniHoTT_paths]
y:2228 [in MetaCoq.Translations.MiniHoTT_paths]
y:223 [in MetaCoq.Template.utils.wGraph]
y:223 [in MetaCoq.PCUIC.PCUICConfluence]
y:223 [in MetaCoq.Translations.MiniHoTT_paths]
y:2232 [in MetaCoq.Translations.MiniHoTT]
y:2235 [in MetaCoq.Template.utils.All_Forall]
y:224 [in MetaCoq.PCUIC.PCUICContexts]
y:2240 [in MetaCoq.Translations.MiniHoTT_paths]
y:2245 [in MetaCoq.Translations.MiniHoTT]
y:2249 [in MetaCoq.Template.utils.All_Forall]
y:225 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
y:225 [in MetaCoq.Translations.MiniHoTT]
y:2253 [in MetaCoq.Translations.MiniHoTT_paths]
y:2259 [in MetaCoq.Translations.MiniHoTT]
y:226 [in MetaCoq.Template.TypingWf]
y:2267 [in MetaCoq.Translations.MiniHoTT_paths]
y:227 [in MetaCoq.Translations.MiniHoTT_paths]
y:228 [in MetaCoq.PCUIC.PCUICConfluence]
y:229 [in MetaCoq.PCUIC.PCUICSR]
y:2292 [in MetaCoq.Translations.MiniHoTT]
y:23 [in MetaCoq.Template.utils.MCReflect]
y:23 [in MetaCoq.PCUIC.Syntax.PCUICReflect]
y:23 [in MetaCoq.Translations.times_bool_fun2]
y:2300 [in MetaCoq.Translations.MiniHoTT_paths]
y:231 [in MetaCoq.Translations.MiniHoTT]
y:231 [in MetaCoq.PCUIC.PCUICSR]
y:233 [in MetaCoq.Template.utils.All_Forall]
y:233 [in MetaCoq.PCUIC.PCUICConfluence]
y:233 [in MetaCoq.Translations.MiniHoTT_paths]
y:235 [in MetaCoq.Template.utils.wGraph]
y:237 [in MetaCoq.Translations.MiniHoTT]
y:2372 [in MetaCoq.Template.utils.All_Forall]
y:2373 [in MetaCoq.Translations.MiniHoTT]
y:2376 [in MetaCoq.Translations.MiniHoTT]
y:2377 [in MetaCoq.Template.utils.All_Forall]
y:2377 [in MetaCoq.Translations.MiniHoTT]
y:238 [in MetaCoq.PCUIC.PCUICConfluence]
y:2381 [in MetaCoq.Translations.MiniHoTT_paths]
y:2384 [in MetaCoq.Translations.MiniHoTT]
y:2384 [in MetaCoq.Translations.MiniHoTT_paths]
y:2385 [in MetaCoq.Translations.MiniHoTT_paths]
y:2387 [in MetaCoq.Translations.MiniHoTT]
y:2388 [in MetaCoq.Translations.MiniHoTT]
y:239 [in MetaCoq.Translations.MiniHoTT_paths]
y:2392 [in MetaCoq.Translations.MiniHoTT_paths]
y:2395 [in MetaCoq.Translations.MiniHoTT_paths]
y:2396 [in MetaCoq.Translations.MiniHoTT]
y:2396 [in MetaCoq.Translations.MiniHoTT_paths]
y:24 [in MetaCoq.PCUIC.PCUICRedTypeIrrelevance]
y:24 [in MetaCoq.PCUIC.PCUICParallelReduction]
y:24 [in MetaCoq.Template.common.uGraph]
y:24 [in MetaCoq.Template.utils.ReflectEq]
y:24 [in MetaCoq.Template.utils.MCOption]
y:240 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
y:2402 [in MetaCoq.Translations.MiniHoTT]
y:2404 [in MetaCoq.Translations.MiniHoTT_paths]
y:2410 [in MetaCoq.Translations.MiniHoTT_paths]
y:2417 [in MetaCoq.Translations.MiniHoTT]
y:242 [in MetaCoq.PCUIC.PCUICTyping]
y:2425 [in MetaCoq.Translations.MiniHoTT_paths]
y:2427 [in MetaCoq.Template.utils.All_Forall]
y:2428 [in MetaCoq.Translations.MiniHoTT]
y:243 [in MetaCoq.PCUIC.PCUICConfluence]
y:243 [in MetaCoq.Translations.MiniHoTT]
y:2434 [in MetaCoq.Template.utils.All_Forall]
y:2436 [in MetaCoq.Translations.MiniHoTT_paths]
y:244 [in MetaCoq.Template.utils.All_Forall]
y:244 [in MetaCoq.PCUIC.PCUICSR]
y:2443 [in MetaCoq.Template.utils.All_Forall]
y:245 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
y:245 [in MetaCoq.Translations.MiniHoTT_paths]
y:2450 [in MetaCoq.Translations.MiniHoTT]
y:2452 [in MetaCoq.Template.utils.All_Forall]
y:2458 [in MetaCoq.Translations.MiniHoTT_paths]
y:246 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
y:246 [in MetaCoq.Template.utils.wGraph]
y:246 [in MetaCoq.PCUIC.PCUICConfluence]
y:2461 [in MetaCoq.Template.utils.All_Forall]
y:2464 [in MetaCoq.Translations.MiniHoTT]
y:247 [in MetaCoq.PCUIC.PCUICSR]
y:2472 [in MetaCoq.Translations.MiniHoTT_paths]
y:249 [in MetaCoq.Translations.MiniHoTT]
y:2490 [in MetaCoq.Template.utils.All_Forall]
y:25 [in MetaCoq.PCUIC.PCUICSR]
y:2500 [in MetaCoq.Template.utils.All_Forall]
y:2503 [in MetaCoq.Template.utils.All_Forall]
y:251 [in MetaCoq.PCUIC.PCUICConfluence]
y:251 [in MetaCoq.Translations.MiniHoTT_paths]
y:2510 [in MetaCoq.Template.utils.All_Forall]
y:2513 [in MetaCoq.Template.utils.All_Forall]
y:2514 [in MetaCoq.Translations.MiniHoTT]
y:2516 [in MetaCoq.Translations.MiniHoTT]
y:252 [in MetaCoq.Template.utils.All_Forall]
y:252 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
y:252 [in MetaCoq.Template.Checker]
y:2522 [in MetaCoq.Translations.MiniHoTT_paths]
y:2524 [in MetaCoq.Translations.MiniHoTT_paths]
y:2531 [in MetaCoq.Template.utils.All_Forall]
y:2533 [in MetaCoq.Template.utils.All_Forall]
y:2535 [in MetaCoq.Template.utils.All_Forall]
y:2537 [in MetaCoq.Template.utils.All_Forall]
y:254 [in MetaCoq.Template.common.uGraph]
y:2544 [in MetaCoq.Template.utils.All_Forall]
y:2547 [in MetaCoq.Template.utils.All_Forall]
y:255 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
y:255 [in MetaCoq.Template.utils.wGraph]
y:255 [in MetaCoq.Translations.MiniHoTT]
y:2555 [in MetaCoq.Template.utils.All_Forall]
y:2558 [in MetaCoq.Template.utils.All_Forall]
y:256 [in MetaCoq.PCUIC.PCUICConfluence]
y:257 [in MetaCoq.Translations.MiniHoTT_paths]
y:2576 [in MetaCoq.Template.utils.All_Forall]
y:258 [in MetaCoq.Template.common.uGraph]
y:2588 [in MetaCoq.Template.utils.All_Forall]
y:259 [in MetaCoq.PCUIC.PCUICEquality]
y:259 [in MetaCoq.Template.utils.wGraph]
y:2599 [in MetaCoq.Template.utils.All_Forall]
y:26 [in MetaCoq.Template.Kernames]
y:26 [in MetaCoq.PCUIC.PCUICConfluence]
y:26 [in MetaCoq.Erasure.EReflect]
y:260 [in MetaCoq.Template.utils.All_Forall]
y:261 [in MetaCoq.Translations.MiniHoTT]
y:262 [in MetaCoq.PCUIC.PCUICNormal]
y:263 [in MetaCoq.Translations.MiniHoTT_paths]
y:265 [in MetaCoq.Erasure.EEtaExpandedFix]
y:265 [in MetaCoq.Template.utils.wGraph]
y:267 [in MetaCoq.PCUIC.PCUICConfluence]
y:267 [in MetaCoq.Translations.MiniHoTT]
y:268 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
y:268 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
y:2680 [in MetaCoq.Translations.MiniHoTT]
y:2688 [in MetaCoq.Translations.MiniHoTT_paths]
y:269 [in MetaCoq.Translations.MiniHoTT_paths]
y:269 [in MetaCoq.Template.TypingWf]
y:2694 [in MetaCoq.Translations.MiniHoTT]
y:27 [in MetaCoq.Template.utils.MCCompare]
y:270 [in MetaCoq.Template.utils.All_Forall]
y:270 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
y:270 [in MetaCoq.PCUIC.PCUICConfluence]
y:2702 [in MetaCoq.Translations.MiniHoTT_paths]
y:271 [in MetaCoq.Template.utils.wGraph]
y:271 [in MetaCoq.Translations.MiniHoTT]
y:272 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
y:272 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
y:272 [in MetaCoq.PCUIC.PCUICNormal]
y:274 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
y:274 [in MetaCoq.Template.utils.wGraph]
y:275 [in MetaCoq.Translations.MiniHoTT_paths]
y:276 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
y:278 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
y:278 [in MetaCoq.PCUIC.PCUICNormal]
Y:278 [in MetaCoq.SafeChecker.PCUICErrors]
y:278 [in MetaCoq.Translations.MiniHoTT]
y:279 [in MetaCoq.Template.utils.wGraph]
y:279 [in MetaCoq.Translations.MiniHoTT_paths]
y:28 [in MetaCoq.PCUIC.utils.PCUICUtils]
y:28 [in MetaCoq.Template.Kernames]
y:28 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
y:280 [in MetaCoq.Template.utils.All_Forall]
y:280 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
y:280 [in MetaCoq.PCUIC.PCUICEquality]
y:281 [in MetaCoq.PCUIC.PCUICConfluence]
y:282 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
y:282 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
y:282 [in MetaCoq.Template.utils.wGraph]
y:284 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
y:284 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
y:284 [in MetaCoq.PCUIC.PCUICNormal]
y:2843 [in MetaCoq.Translations.MiniHoTT]
Y:285 [in MetaCoq.SafeChecker.PCUICErrors]
y:285 [in MetaCoq.Translations.MiniHoTT]
y:2851 [in MetaCoq.Translations.MiniHoTT_paths]
y:2854 [in MetaCoq.Translations.MiniHoTT]
y:286 [in MetaCoq.Translations.MiniHoTT_paths]
y:2862 [in MetaCoq.Translations.MiniHoTT_paths]
y:287 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
y:288 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
y:2883 [in MetaCoq.Translations.MiniHoTT]
y:2886 [in MetaCoq.Translations.MiniHoTT]
y:2891 [in MetaCoq.Translations.MiniHoTT_paths]
y:2893 [in MetaCoq.Translations.MiniHoTT]
y:2894 [in MetaCoq.Translations.MiniHoTT_paths]
y:2896 [in MetaCoq.Translations.MiniHoTT]
y:29 [in MetaCoq.Template.utils.MCCompare]
y:29 [in MetaCoq.Template.utils.MCRelations]
y:29 [in MetaCoq.Template.utils.ReflectEq]
y:29 [in MetaCoq.Translations.MiniHoTT_paths]
y:290 [in MetaCoq.Template.utils.All_Forall]
y:290 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
y:2901 [in MetaCoq.Translations.MiniHoTT_paths]
y:2904 [in MetaCoq.Translations.MiniHoTT_paths]
y:2906 [in MetaCoq.Translations.MiniHoTT]
y:291 [in MetaCoq.Template.utils.wGraph]
y:2910 [in MetaCoq.Translations.MiniHoTT]
y:2914 [in MetaCoq.Translations.MiniHoTT_paths]
y:2918 [in MetaCoq.Translations.MiniHoTT_paths]
y:292 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
y:292 [in MetaCoq.PCUIC.PCUICCumulProp]
Y:292 [in MetaCoq.SafeChecker.PCUICErrors]
y:292 [in MetaCoq.Translations.MiniHoTT]
y:293 [in MetaCoq.Translations.MiniHoTT_paths]
y:294 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
y:2942 [in MetaCoq.Translations.MiniHoTT]
y:2944 [in MetaCoq.Translations.MiniHoTT]
y:2950 [in MetaCoq.Translations.MiniHoTT_paths]
y:2952 [in MetaCoq.Translations.MiniHoTT_paths]
y:296 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
y:296 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
Y:297 [in MetaCoq.SafeChecker.PCUICErrors]
y:297 [in MetaCoq.Template.utils.wGraph]
y:298 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
y:299 [in MetaCoq.Translations.MiniHoTT]
Y:3 [in MetaCoq.Examples.typing_correctness]
y:3 [in MetaCoq.PCUIC.PCUICAst]
y:3 [in MetaCoq.Examples.tauto]
Y:3 [in MetaCoq.Examples.metacoq_tour_prelude]
y:30 [in MetaCoq.Template.utils.All_Forall]
y:30 [in MetaCoq.Template.Kernames]
y:30 [in MetaCoq.PCUIC.PCUICAlpha]
y:300 [in MetaCoq.PCUIC.PCUICSubstitution]
y:300 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
y:300 [in MetaCoq.Translations.MiniHoTT_paths]
y:302 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
y:304 [in MetaCoq.Template.Universes]
y:304 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
y:304 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
Y:304 [in MetaCoq.SafeChecker.PCUICErrors]
y:306 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
y:306 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
y:306 [in MetaCoq.Translations.MiniHoTT]
y:307 [in MetaCoq.Translations.MiniHoTT_paths]
y:31 [in MetaCoq.Template.utils.MCReflect]
y:31 [in MetaCoq.Template.utils.MCCompare]
y:31 [in MetaCoq.Template.Universes]
y:31 [in MetaCoq.PCUIC.utils.PCUICPrimitive]
y:311 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
y:312 [in MetaCoq.PCUIC.PCUICConfluence]
y:313 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
y:313 [in MetaCoq.Translations.MiniHoTT]
y:314 [in MetaCoq.Translations.MiniHoTT_paths]
y:315 [in MetaCoq.Template.utils.wGraph]
y:315 [in MetaCoq.PCUIC.Conversion.PCUICNamelessConv]
y:319 [in MetaCoq.PCUIC.PCUICSR]
y:32 [in MetaCoq.PCUIC.utils.PCUICUtils]
y:32 [in MetaCoq.PCUIC.PCUICParallelReduction]
y:320 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
y:320 [in MetaCoq.Translations.MiniHoTT]
y:320 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
y:321 [in MetaCoq.Translations.MiniHoTT_paths]
y:322 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
y:323 [in MetaCoq.Template.TypingWf]
y:324 [in MetaCoq.Template.utils.wGraph]
y:326 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
y:327 [in MetaCoq.Translations.MiniHoTT]
y:327 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
y:328 [in MetaCoq.Template.utils.wGraph]
y:328 [in MetaCoq.Translations.MiniHoTT_paths]
y:33 [in MetaCoq.Template.Kernames]
y:33 [in MetaCoq.PCUIC.Syntax.PCUICReflect]
y:33 [in MetaCoq.Translations.MiniHoTT]
y:33 [in MetaCoq.Translations.times_bool_fun2]
y:33 [in MetaCoq.PCUIC.utils.PCUICPrimitive]
y:330 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
y:330 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
y:330 [in MetaCoq.PCUIC.PCUICConfluence]
y:332 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
y:332 [in MetaCoq.Translations.MiniHoTT]
y:333 [in MetaCoq.PCUIC.PCUICParallelReduction]
y:334 [in MetaCoq.Template.utils.wGraph]
y:335 [in MetaCoq.Translations.MiniHoTT_paths]
y:335 [in MetaCoq.PCUIC.PCUICReduction]
y:337 [in MetaCoq.Template.utils.All_Forall]
y:337 [in MetaCoq.Translations.MiniHoTT]
y:34 [in MetaCoq.Template.utils.ReflectEq]
y:34 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
y:34 [in MetaCoq.PCUIC.PCUICPrincipality]
y:34 [in MetaCoq.PCUIC.PCUICConfluence]
y:34 [in MetaCoq.PCUIC.PCUICSR]
y:340 [in MetaCoq.Translations.MiniHoTT_paths]
y:342 [in MetaCoq.Translations.MiniHoTT]
y:344 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
y:344 [in MetaCoq.PCUIC.PCUICConfluence]
y:345 [in MetaCoq.Template.utils.All_Forall]
y:345 [in MetaCoq.Translations.MiniHoTT_paths]
y:346 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
y:347 [in MetaCoq.Translations.MiniHoTT]
y:349 [in MetaCoq.Template.utils.wGraph]
y:35 [in MetaCoq.Template.utils.MCRelations]
y:35 [in MetaCoq.Template.common.uGraph]
y:35 [in MetaCoq.PCUIC.PCUICSN]
y:35 [in MetaCoq.PCUIC.utils.PCUICPrimitive]
y:35 [in MetaCoq.SafeChecker.PCUICEqualityDec]
y:350 [in MetaCoq.Translations.MiniHoTT_paths]
y:352 [in MetaCoq.Template.utils.All_Forall]
y:352 [in MetaCoq.Translations.MiniHoTT]
y:355 [in MetaCoq.Translations.MiniHoTT_paths]
y:356 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
y:356 [in MetaCoq.Template.utils.wGraph]
y:357 [in MetaCoq.Translations.MiniHoTT]
y:358 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
y:36 [in MetaCoq.PCUIC.PCUICConfluence]
y:360 [in MetaCoq.Template.Universes]
y:360 [in MetaCoq.Template.utils.All_Forall]
y:360 [in MetaCoq.Template.common.uGraph]
y:360 [in MetaCoq.Translations.MiniHoTT_paths]
y:362 [in MetaCoq.Template.common.uGraph]
y:362 [in MetaCoq.Template.utils.wGraph]
y:362 [in MetaCoq.Translations.MiniHoTT]
y:363 [in MetaCoq.PCUIC.PCUICConfluence]
y:364 [in MetaCoq.Template.Universes]
y:364 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
y:365 [in MetaCoq.Template.utils.All_Forall]
y:365 [in MetaCoq.Translations.MiniHoTT_paths]
y:366 [in MetaCoq.Template.Universes]
y:366 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
y:366 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
y:367 [in MetaCoq.PCUIC.PCUICEquality]
y:367 [in MetaCoq.Template.utils.wGraph]
y:368 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
y:368 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
y:368 [in MetaCoq.PCUIC.PCUICConfluence]
y:368 [in MetaCoq.Translations.MiniHoTT]
y:37 [in MetaCoq.Template.utils.MCCompare]
y:37 [in MetaCoq.Template.common.uGraph]
y:37 [in MetaCoq.Template.Kernames]
y:37 [in MetaCoq.Translations.times_bool_fun2]
y:370 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
y:370 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
y:370 [in MetaCoq.Translations.MiniHoTT_paths]
y:371 [in MetaCoq.PCUIC.PCUICCumulProp]
y:372 [in MetaCoq.PCUIC.PCUICReduction]
y:373 [in MetaCoq.Template.utils.wGraph]
y:375 [in MetaCoq.PCUIC.PCUICConfluence]
y:375 [in MetaCoq.Translations.MiniHoTT]
y:375 [in MetaCoq.PCUIC.PCUICReduction]
y:376 [in MetaCoq.Translations.MiniHoTT_paths]
y:377 [in MetaCoq.Template.utils.wGraph]
y:377 [in MetaCoq.SafeChecker.PCUICSafeChecker]
y:378 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
y:378 [in MetaCoq.Erasure.ERemoveParams]
y:38 [in MetaCoq.Template.utils.ReflectEq]
y:38 [in MetaCoq.PCUIC.PCUICPrincipality]
y:380 [in MetaCoq.Template.utils.All_Forall]
y:380 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
y:380 [in MetaCoq.PCUIC.PCUICConfluence]
y:381 [in MetaCoq.Template.utils.wGraph]
y:382 [in MetaCoq.Translations.MiniHoTT]
y:382 [in MetaCoq.Erasure.ERemoveParams]
y:383 [in MetaCoq.Template.utils.All_Forall]
y:383 [in MetaCoq.PCUIC.PCUICConfluence]
y:383 [in MetaCoq.Translations.MiniHoTT_paths]
y:385 [in MetaCoq.Template.Typing]
y:385 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
y:385 [in MetaCoq.PCUIC.PCUICConfluence]
y:387 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
y:388 [in MetaCoq.PCUIC.PCUICConfluence]
y:389 [in MetaCoq.Translations.MiniHoTT]
y:39 [in MetaCoq.Translations.MiniHoTT]
y:390 [in MetaCoq.PCUIC.PCUICConfluence]
y:390 [in MetaCoq.Translations.MiniHoTT_paths]
y:391 [in MetaCoq.Template.utils.All_Forall]
y:391 [in MetaCoq.SafeChecker.PCUICSafeChecker]
y:393 [in MetaCoq.Template.utils.All_Forall]
y:393 [in MetaCoq.PCUIC.PCUICConfluence]
y:394 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
y:396 [in MetaCoq.Template.Universes]
y:396 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
y:396 [in MetaCoq.Translations.MiniHoTT]
y:397 [in MetaCoq.Translations.MiniHoTT_paths]
y:398 [in MetaCoq.Template.Universes]
y:398 [in MetaCoq.Template.utils.MCList]
y:4 [in MetaCoq.Template.utils.ByteCompare]
y:4 [in MetaCoq.Template.utils.MCEquality]
y:4 [in MetaCoq.SafeChecker.PCUICSafeChecker]
y:4 [in MetaCoq.Erasure.EReflect]
y:40 [in MetaCoq.Template.utils.All_Forall]
y:40 [in MetaCoq.PCUIC.PCUICSafeLemmata]
y:40 [in MetaCoq.Template.Kernames]
y:400 [in MetaCoq.Template.Universes]
y:401 [in MetaCoq.Template.utils.All_Forall]
y:401 [in MetaCoq.Template.Typing]
y:402 [in MetaCoq.Template.utils.wGraph]
y:404 [in MetaCoq.Translations.MiniHoTT]
y:404 [in MetaCoq.Translations.MiniHoTT_paths]
y:404 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
y:406 [in MetaCoq.PCUIC.PCUICConfluence]
y:409 [in MetaCoq.Template.utils.All_Forall]
y:409 [in MetaCoq.PCUIC.PCUICConfluence]
y:41 [in MetaCoq.Template.Universes]
y:41 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
y:41 [in MetaCoq.Template.utils.MCOption]
y:41 [in MetaCoq.Translations.MiniHoTT_paths]
y:411 [in MetaCoq.PCUIC.PCUICConfluence]
y:412 [in MetaCoq.Translations.MiniHoTT]
y:412 [in MetaCoq.Translations.MiniHoTT_paths]
y:414 [in MetaCoq.PCUIC.PCUICConfluence]
y:414 [in MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
y:419 [in MetaCoq.Template.utils.All_Forall]
y:42 [in MetaCoq.PCUIC.PCUICPrincipality]
y:42 [in MetaCoq.Examples.add_constructor]
y:420 [in MetaCoq.Template.utils.wGraph]
y:420 [in MetaCoq.Translations.MiniHoTT]
y:420 [in MetaCoq.Translations.MiniHoTT_paths]
y:422 [in MetaCoq.PCUIC.PCUICNormal]
y:427 [in MetaCoq.PCUIC.PCUICConfluence]
y:428 [in MetaCoq.Translations.MiniHoTT_paths]
y:429 [in MetaCoq.Template.utils.All_Forall]
y:43 [in MetaCoq.PCUIC.utils.PCUICUtils]
y:43 [in MetaCoq.PCUIC.PCUICConfluence]
y:43 [in MetaCoq.PCUIC.Syntax.PCUICReflect]
y:43 [in MetaCoq.Translations.times_bool_fun2]
y:430 [in MetaCoq.Template.EnvironmentTyping]
y:430 [in MetaCoq.PCUIC.PCUICConfluence]
y:432 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
y:432 [in MetaCoq.PCUIC.PCUICConfluence]
y:433 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
y:435 [in MetaCoq.PCUIC.PCUICConfluence]
y:436 [in MetaCoq.Template.utils.wGraph]
y:437 [in MetaCoq.PCUIC.PCUICConfluence]
y:438 [in MetaCoq.Translations.MiniHoTT]
y:44 [in MetaCoq.PCUIC.PCUICParallelReduction]
y:44 [in MetaCoq.Template.common.uGraph]
y:44 [in MetaCoq.Template.Reflect]
y:440 [in MetaCoq.PCUIC.PCUICConfluence]
y:4413 [in MetaCoq.SafeChecker.PCUICSafeConversion]
y:442 [in MetaCoq.PCUIC.PCUICConfluence]
y:443 [in MetaCoq.Template.Universes]
y:445 [in MetaCoq.Template.Universes]
y:445 [in MetaCoq.Template.utils.wGraph]
y:446 [in MetaCoq.Template.EtaExpand]
y:446 [in MetaCoq.Translations.MiniHoTT_paths]
y:447 [in MetaCoq.Template.Universes]
y:447 [in MetaCoq.PCUIC.PCUICConfluence]
y:447 [in MetaCoq.Translations.MiniHoTT]
y:449 [in MetaCoq.Template.Universes]
y:449 [in MetaCoq.PCUIC.PCUICEquality]
y:45 [in MetaCoq.Template.Universes]
y:45 [in MetaCoq.Template.utils.ReflectEq]
y:452 [in MetaCoq.Template.Universes]
y:452 [in MetaCoq.Template.utils.wGraph]
y:452 [in MetaCoq.PCUIC.PCUICConfluence]
y:454 [in MetaCoq.Template.Universes]
y:454 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
y:454 [in MetaCoq.PCUIC.PCUICEquality]
y:455 [in MetaCoq.Template.utils.wGraph]
y:455 [in MetaCoq.PCUIC.PCUICConfluence]
y:455 [in MetaCoq.Translations.MiniHoTT_paths]
y:455 [in MetaCoq.Erasure.EWcbvEval]
y:456 [in MetaCoq.Template.EtaExpand]
y:456 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
y:456 [in MetaCoq.Translations.MiniHoTT]
y:457 [in MetaCoq.PCUIC.PCUICConfluence]
y:458 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
y:46 [in MetaCoq.Template.Kernames]
y:46 [in MetaCoq.PCUIC.PCUICPrincipality]
y:460 [in MetaCoq.PCUIC.PCUICConfluence]
y:461 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
y:462 [in MetaCoq.PCUIC.PCUICConfluence]
y:463 [in MetaCoq.Template.utils.wGraph]
y:464 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
y:464 [in MetaCoq.Translations.MiniHoTT_paths]
y:465 [in MetaCoq.PCUIC.PCUICConfluence]
y:466 [in MetaCoq.Template.EtaExpand]
y:466 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
y:466 [in MetaCoq.Translations.MiniHoTT]
y:47 [in MetaCoq.Template.Universes]
y:47 [in MetaCoq.PCUIC.PCUICValidity]
y:47 [in MetaCoq.Translations.MiniHoTT_paths]
y:47 [in MetaCoq.PCUIC.PCUICCanonicity]
y:47 [in MetaCoq.Translations.times_bool_fun2]
y:471 [in MetaCoq.PCUIC.PCUICEquality]
y:472 [in MetaCoq.Template.utils.wGraph]
y:472 [in MetaCoq.Translations.MiniHoTT]
y:474 [in MetaCoq.Translations.MiniHoTT_paths]
y:475 [in MetaCoq.Template.utils.wGraph]
y:476 [in MetaCoq.Translations.MiniHoTT]
y:477 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
y:478 [in MetaCoq.PCUIC.PCUICConfluence]
y:48 [in MetaCoq.Template.common.uGraph]
y:48 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
y:48 [in MetaCoq.PCUIC.PCUICCasesContexts]
y:48 [in MetaCoq.SafeChecker.PCUICEqualityDec]
y:480 [in MetaCoq.Translations.MiniHoTT_paths]
y:481 [in MetaCoq.PCUIC.PCUICConfluence]
y:483 [in MetaCoq.PCUIC.PCUICConfluence]
y:483 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
y:484 [in MetaCoq.Translations.MiniHoTT]
y:484 [in MetaCoq.Translations.MiniHoTT_paths]
y:486 [in MetaCoq.PCUIC.PCUICConfluence]
y:49 [in MetaCoq.Template.Kernames]
y:49 [in MetaCoq.Template.utils.ReflectEq]
y:49 [in MetaCoq.Template.TypingWf]
y:492 [in MetaCoq.Translations.MiniHoTT]
y:492 [in MetaCoq.Translations.MiniHoTT_paths]
y:496 [in MetaCoq.Template.utils.wGraph]
y:498 [in MetaCoq.Translations.MiniHoTT]
y:499 [in MetaCoq.Template.utils.wGraph]
y:499 [in MetaCoq.PCUIC.PCUICConfluence]
y:5 [in MetaCoq.Template.utils.ByteCompareSpec]
y:5 [in MetaCoq.Examples.metacoq_tour]
y:5 [in MetaCoq.Erasure.EWcbvEvalInd]
y:5 [in MetaCoq.PCUIC.PCUICCasesContexts]
y:5 [in MetaCoq.Template.utils.MCPrelude]
y:50 [in MetaCoq.PCUIC.utils.PCUICUtils]
y:50 [in MetaCoq.SafeChecker.PCUICSafeReduce]
y:50 [in MetaCoq.PCUIC.PCUICPrincipality]
y:50 [in MetaCoq.SafeChecker.PCUICEqualityDec]
y:500 [in MetaCoq.PCUIC.PCUICNormal]
y:500 [in MetaCoq.Translations.MiniHoTT_paths]
y:502 [in MetaCoq.PCUIC.PCUICConfluence]
y:503 [in MetaCoq.Template.utils.wGraph]
y:504 [in MetaCoq.PCUIC.PCUICConfluence]
y:506 [in MetaCoq.Translations.MiniHoTT_paths]
y:507 [in MetaCoq.PCUIC.PCUICConfluence]
y:508 [in MetaCoq.Translations.MiniHoTT]
y:509 [in MetaCoq.PCUIC.PCUICConfluence]
y:51 [in MetaCoq.Template.common.uGraph]
y:51 [in MetaCoq.PCUIC.PCUICAlpha]
y:51 [in MetaCoq.PCUIC.Syntax.PCUICReflect]
y:510 [in MetaCoq.Template.utils.wGraph]
y:511 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
y:512 [in MetaCoq.PCUIC.PCUICConfluence]
y:514 [in MetaCoq.PCUIC.PCUICConfluence]
y:515 [in MetaCoq.Translations.MiniHoTT]
y:516 [in MetaCoq.Translations.MiniHoTT_paths]
y:518 [in MetaCoq.Template.utils.wGraph]
y:518 [in MetaCoq.PCUIC.PCUICConfluence]
y:52 [in MetaCoq.Template.Kernames]
y:52 [in MetaCoq.PCUIC.PCUICConfluence]
y:52 [in MetaCoq.SafeChecker.PCUICEqualityDec]
y:522 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
y:522 [in MetaCoq.Translations.MiniHoTT]
y:523 [in MetaCoq.Translations.MiniHoTT_paths]
y:53 [in MetaCoq.Template.utils.MCList]
y:53 [in MetaCoq.PCUIC.utils.PCUICOnOne]
y:53 [in MetaCoq.Template.utils.ReflectEq]
y:530 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
y:530 [in MetaCoq.Translations.MiniHoTT_paths]
y:531 [in MetaCoq.Translations.MiniHoTT]
y:533 [in MetaCoq.Template.utils.wGraph]
y:537 [in MetaCoq.Template.utils.wGraph]
y:539 [in MetaCoq.Translations.MiniHoTT_paths]
y:54 [in MetaCoq.PCUIC.PCUICValidity]
y:54 [in MetaCoq.Template.common.uGraph]
y:54 [in MetaCoq.Template.Kernames]
y:541 [in MetaCoq.Template.utils.wGraph]
y:544 [in MetaCoq.Translations.MiniHoTT]
y:546 [in MetaCoq.Template.utils.MCList]
y:549 [in MetaCoq.Template.Universes]
y:55 [in MetaCoq.Template.utils.MCCompare]
y:55 [in MetaCoq.PCUIC.PCUICAlpha]
y:55 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
y:55 [in MetaCoq.PCUIC.PCUICPrincipality]
y:552 [in MetaCoq.Translations.MiniHoTT_paths]
Y:555 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
y:555 [in MetaCoq.Translations.MiniHoTT]
y:556 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
y:557 [in MetaCoq.Template.utils.wGraph]
y:56 [in MetaCoq.PCUIC.Syntax.PCUICReflect]
y:5607 [in MetaCoq.SafeChecker.PCUICSafeConversion]
y:561 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
y:561 [in MetaCoq.Template.utils.wGraph]
y:563 [in MetaCoq.Translations.MiniHoTT_paths]
y:5639 [in MetaCoq.SafeChecker.PCUICSafeConversion]
y:564 [in MetaCoq.Translations.MiniHoTT]
y:5646 [in MetaCoq.SafeChecker.PCUICSafeConversion]
y:565 [in MetaCoq.Template.utils.wGraph]
y:57 [in MetaCoq.Template.utils.MCCompare]
y:57 [in MetaCoq.Template.utils.MCRelations]
y:57 [in MetaCoq.Template.common.uGraph]
y:57 [in MetaCoq.Template.utils.MCProd]
y:572 [in MetaCoq.Translations.MiniHoTT_paths]
y:573 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
y:575 [in MetaCoq.Translations.MiniHoTT]
y:58 [in MetaCoq.Template.Kernames]
y:58 [in MetaCoq.Template.Reflect]
y:581 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
y:583 [in MetaCoq.Template.utils.All_Forall]
y:583 [in MetaCoq.Translations.MiniHoTT_paths]
y:586 [in MetaCoq.Translations.MiniHoTT]
y:587 [in MetaCoq.PCUIC.PCUICConversion]
y:588 [in MetaCoq.PCUIC.PCUICAst]
y:588 [in MetaCoq.PCUIC.PCUICConfluence]
y:589 [in MetaCoq.PCUIC.PCUICConversion]
y:59 [in MetaCoq.PCUIC.PCUICConfluence]
y:593 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
y:594 [in MetaCoq.Translations.MiniHoTT_paths]
y:595 [in MetaCoq.PCUIC.PCUICConversion]
y:595 [in MetaCoq.Translations.MiniHoTT]
y:598 [in MetaCoq.Template.utils.wGraph]
y:6 [in MetaCoq.Template.utils.MCRelations]
y:6 [in MetaCoq.Template.utils.MCArith]
y:6 [in MetaCoq.Template.common.uGraph]
y:6 [in MetaCoq.SafeChecker.PCUICSafeChecker]
y:6 [in MetaCoq.Erasure.EReflect]
y:60 [in MetaCoq.Template.utils.MCCompare]
y:60 [in MetaCoq.Template.utils.MCRelations]
y:60 [in MetaCoq.PCUIC.PCUICParallelReduction]
y:60 [in MetaCoq.Template.common.uGraph]
y:60 [in MetaCoq.SafeChecker.PCUICSafeReduce]
y:60 [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
y:600 [in MetaCoq.PCUIC.PCUICConfluence]
y:601 [in MetaCoq.SafeChecker.PCUICSafeChecker]
y:603 [in MetaCoq.Translations.MiniHoTT_paths]
y:604 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
y:604 [in MetaCoq.Translations.MiniHoTT]
y:607 [in MetaCoq.Template.utils.wGraph]
y:61 [in MetaCoq.Translations.times_bool_fun2]
y:612 [in MetaCoq.PCUIC.PCUICConfluence]
y:612 [in MetaCoq.Translations.MiniHoTT_paths]
y:613 [in MetaCoq.Translations.MiniHoTT]
y:615 [in MetaCoq.Template.utils.All_Forall]
y:619 [in MetaCoq.PCUIC.PCUICConversion]
y:62 [in MetaCoq.Template.utils.MCCompare]
y:62 [in MetaCoq.PCUIC.PCUICValidity]
y:62 [in MetaCoq.Template.common.uGraph]
y:62 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
y:62 [in MetaCoq.PCUIC.Syntax.PCUICReflect]
y:620 [in MetaCoq.Template.common.uGraph]
y:621 [in MetaCoq.Translations.MiniHoTT_paths]
y:622 [in MetaCoq.Template.utils.All_Forall]
y:628 [in MetaCoq.PCUIC.PCUICParallelReduction]
y:628 [in MetaCoq.PCUIC.PCUICEquality]
y:63 [in MetaCoq.PCUIC.TemplateToPCUIC]
y:63 [in MetaCoq.Template.utils.MCProd]
y:63 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
y:633 [in MetaCoq.Template.utils.All_Forall]
y:638 [in MetaCoq.Template.utils.wGraph]
y:64 [in MetaCoq.Template.utils.MCCompare]
y:64 [in MetaCoq.PCUIC.PCUICValidity]
y:64 [in MetaCoq.PCUIC.PCUICCasesContexts]
y:649 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
y:65 [in MetaCoq.Template.common.uGraph]
y:65 [in MetaCoq.PCUIC.TemplateToPCUICWcbvEval]
y:652 [in MetaCoq.Template.utils.wGraph]
y:652 [in MetaCoq.PCUIC.PCUICConversion]
y:653 [in MetaCoq.Template.utils.All_Forall]
y:656 [in MetaCoq.SafeChecker.PCUICSafeConversion]
y:658 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
y:66 [in MetaCoq.PCUIC.utils.PCUICUtils]
y:66 [in MetaCoq.PCUIC.PCUICCasesContexts]
y:664 [in MetaCoq.PCUIC.PCUICReduction]
y:665 [in MetaCoq.Template.utils.All_Forall]
y:668 [in MetaCoq.PCUIC.PCUICReduction]
y:67 [in MetaCoq.Template.common.uGraph]
y:67 [in MetaCoq.Template.Reflect]
y:67 [in MetaCoq.Translations.MiniHoTT]
y:672 [in MetaCoq.PCUIC.PCUICReduction]
y:673 [in MetaCoq.Template.utils.All_Forall]
y:676 [in MetaCoq.Template.Universes]
y:678 [in MetaCoq.PCUIC.PCUICReduction]
y:679 [in MetaCoq.PCUIC.PCUICConversion]
y:68 [in MetaCoq.Template.utils.MCRelations]
y:682 [in MetaCoq.Template.utils.All_Forall]
y:683 [in MetaCoq.Template.utils.MCList]
y:685 [in MetaCoq.PCUIC.PCUICReduction]
y:688 [in MetaCoq.Template.utils.wGraph]
y:69 [in MetaCoq.PCUIC.utils.PCUICUtils]
y:69 [in MetaCoq.PCUIC.PCUICConfluence]
y:693 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
y:693 [in MetaCoq.PCUIC.PCUICReduction]
y:697 [in MetaCoq.PCUIC.PCUICEquality]
y:7 [in MetaCoq.Template.utils.ByteCompareSpec]
y:7 [in MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
y:7 [in MetaCoq.PCUIC.PCUICCasesContexts]
y:70 [in MetaCoq.Template.utils.MCCompare]
y:70 [in MetaCoq.Template.utils.MCRelations]
y:70 [in MetaCoq.PCUIC.PCUICValidity]
y:70 [in MetaCoq.PCUIC.Syntax.PCUICReflect]
y:70 [in MetaCoq.Translations.MiniHoTT]
y:701 [in MetaCoq.PCUIC.PCUICSpine]
y:703 [in MetaCoq.Template.utils.All_Forall]
y:704 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
y:704 [in MetaCoq.Template.utils.wGraph]
y:706 [in MetaCoq.PCUIC.PCUICEquality]
y:71 [in MetaCoq.Template.utils.bytestring]
y:71 [in MetaCoq.PCUIC.PCUICParallelReduction]
y:71 [in MetaCoq.Template.Reflect]
y:71 [in MetaCoq.PCUIC.PCUICCasesContexts]
y:712 [in MetaCoq.Template.utils.All_Forall]
y:714 [in MetaCoq.Template.utils.All_Forall]
y:714 [in MetaCoq.Template.utils.wGraph]
y:716 [in MetaCoq.Translations.MiniHoTT]
y:717 [in MetaCoq.Template.utils.wGraph]
y:719 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
y:72 [in MetaCoq.Template.utils.MCCompare]
y:72 [in MetaCoq.Template.common.uGraph]
y:721 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
y:723 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
y:724 [in MetaCoq.Template.utils.All_Forall]
y:724 [in MetaCoq.Translations.MiniHoTT]
y:724 [in MetaCoq.Translations.MiniHoTT_paths]
y:725 [in MetaCoq.Template.utils.wGraph]
y:729 [in MetaCoq.PCUIC.PCUICReduction]
y:73 [in MetaCoq.PCUIC.PCUICConfluence]
y:73 [in MetaCoq.PCUIC.PCUICCasesContexts]
y:73 [in MetaCoq.PCUIC.Syntax.PCUICInduction]
y:730 [in MetaCoq.Template.utils.MCList]
y:731 [in MetaCoq.Template.utils.wGraph]
y:731 [in MetaCoq.Translations.MiniHoTT]
y:732 [in MetaCoq.Translations.MiniHoTT_paths]
y:732 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
y:734 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
y:736 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
y:737 [in MetaCoq.Template.utils.wGraph]
y:738 [in MetaCoq.Translations.MiniHoTT]
y:739 [in MetaCoq.Translations.MiniHoTT_paths]
Y:74 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
y:74 [in MetaCoq.PCUIC.Syntax.PCUICReflect]
y:743 [in MetaCoq.Template.utils.MCList]
y:743 [in MetaCoq.Template.Typing]
y:743 [in MetaCoq.Template.utils.wGraph]
y:745 [in MetaCoq.Template.utils.All_Forall]
y:746 [in MetaCoq.Template.Typing]
y:746 [in MetaCoq.Translations.MiniHoTT_paths]
y:749 [in MetaCoq.Translations.MiniHoTT]
y:75 [in MetaCoq.PCUIC.utils.PCUICUtils]
y:75 [in MetaCoq.Template.common.uGraph]
y:75 [in MetaCoq.Template.Reflect]
y:75 [in MetaCoq.Translations.MiniHoTT]
y:75 [in MetaCoq.Translations.MiniHoTT_paths]
y:751 [in MetaCoq.Template.utils.wGraph]
y:753 [in MetaCoq.Template.utils.MCList]
y:755 [in MetaCoq.Template.utils.wGraph]
y:755 [in MetaCoq.Translations.MiniHoTT]
y:757 [in MetaCoq.Translations.MiniHoTT_paths]
y:76 [in MetaCoq.Template.utils.bytestring]
y:761 [in MetaCoq.Translations.MiniHoTT]
y:763 [in MetaCoq.Translations.MiniHoTT_paths]
y:769 [in MetaCoq.Translations.MiniHoTT]
y:769 [in MetaCoq.Translations.MiniHoTT_paths]
y:77 [in MetaCoq.Template.common.uGraph]
Y:771 [in MetaCoq.SafeChecker.PCUICSafeChecker]
y:772 [in MetaCoq.Template.utils.wGraph]
y:775 [in MetaCoq.Template.utils.wGraph]
y:776 [in MetaCoq.PCUIC.PCUICConfluence]
y:777 [in MetaCoq.Translations.MiniHoTT_paths]
y:778 [in MetaCoq.Translations.MiniHoTT]
y:78 [in MetaCoq.PCUIC.utils.PCUICUtils]
y:78 [in MetaCoq.Template.utils.bytestring]
y:78 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
y:78 [in MetaCoq.Translations.MiniHoTT]
y:78 [in MetaCoq.Translations.MiniHoTT_paths]
y:780 [in MetaCoq.PCUIC.PCUICConfluence]
y:782 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
y:786 [in MetaCoq.Template.utils.All_Forall]
y:786 [in MetaCoq.Translations.MiniHoTT_paths]
y:787 [in MetaCoq.Template.utils.wGraph]
y:787 [in MetaCoq.Translations.MiniHoTT]
y:79 [in MetaCoq.Erasure.EInduction]
y:79 [in MetaCoq.Template.Reflect]
y:795 [in MetaCoq.Template.utils.All_Forall]
y:795 [in MetaCoq.Template.utils.wGraph]
y:795 [in MetaCoq.Translations.MiniHoTT_paths]
y:796 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
y:797 [in MetaCoq.Translations.MiniHoTT]
y:8 [in MetaCoq.PCUIC.PCUICSR]
y:8 [in MetaCoq.Erasure.EReflect]
y:80 [in MetaCoq.Template.common.uGraph]
y:80 [in MetaCoq.PCUIC.PCUICEquality]
y:80 [in MetaCoq.Template.utils.ReflectEq]
y:80 [in MetaCoq.PCUIC.PCUICConfluence]
y:800 [in MetaCoq.PCUIC.PCUICInductiveInversion]
y:801 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
y:801 [in MetaCoq.Template.utils.wGraph]
y:805 [in MetaCoq.Translations.MiniHoTT_paths]
y:806 [in MetaCoq.Translations.MiniHoTT]
y:807 [in MetaCoq.PCUIC.PCUICConfluence]
y:808 [in MetaCoq.Template.utils.All_Forall]
y:81 [in MetaCoq.PCUIC.PCUICToTemplateCorrectness]
y:81 [in MetaCoq.PCUIC.utils.PCUICUtils]
y:81 [in MetaCoq.Template.utils.bytestring]
y:810 [in MetaCoq.Template.utils.wGraph]
y:814 [in MetaCoq.Translations.MiniHoTT_paths]
y:818 [in MetaCoq.Translations.MiniHoTT]
y:82 [in MetaCoq.PCUIC.PCUICEquality]
y:82 [in MetaCoq.PCUIC.Syntax.PCUICReflect]
y:822 [in MetaCoq.Template.utils.wGraph]
y:824 [in MetaCoq.PCUIC.PCUICInductiveInversion]
y:826 [in MetaCoq.Translations.MiniHoTT_paths]
y:827 [in MetaCoq.Template.utils.wGraph]
y:829 [in MetaCoq.Translations.MiniHoTT]
y:83 [in MetaCoq.Template.Reflect]
y:83 [in MetaCoq.PCUIC.PCUICConfluence]
y:83 [in MetaCoq.Translations.MiniHoTT_paths]
y:832 [in MetaCoq.Template.utils.All_Forall]
y:835 [in MetaCoq.PCUIC.PCUICReduction]
y:836 [in MetaCoq.Template.utils.MCList]
y:837 [in MetaCoq.Translations.MiniHoTT_paths]
y:84 [in MetaCoq.Template.utils.bytestring]
y:84 [in MetaCoq.Erasure.EConstructorsAsBlocks]
y:84 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
y:84 [in MetaCoq.PCUIC.Syntax.PCUICReflect]
y:84 [in MetaCoq.Translations.MiniHoTT]
y:84 [in MetaCoq.Erasure.ERemoveParams]
y:841 [in MetaCoq.Translations.MiniHoTT]
y:845 [in MetaCoq.PCUIC.PCUICInductiveInversion]
y:846 [in MetaCoq.Template.utils.All_Forall]
y:847 [in MetaCoq.Translations.MiniHoTT]
y:849 [in MetaCoq.Translations.MiniHoTT_paths]
y:85 [in MetaCoq.Template.Universes]
y:85 [in MetaCoq.Template.utils.MCOption]
y:855 [in MetaCoq.Translations.MiniHoTT_paths]
y:856 [in MetaCoq.Template.utils.All_Forall]
y:856 [in MetaCoq.Translations.MiniHoTT]
y:86 [in MetaCoq.Template.utils.bytestring]
y:86 [in MetaCoq.PCUIC.PCUICConfluence]
y:86 [in MetaCoq.Translations.MiniHoTT_paths]
y:861 [in MetaCoq.Template.utils.wGraph]
y:864 [in MetaCoq.Translations.MiniHoTT]
y:864 [in MetaCoq.Translations.MiniHoTT_paths]
y:867 [in MetaCoq.Template.utils.All_Forall]
y:869 [in MetaCoq.Template.utils.wGraph]
y:87 [in MetaCoq.Erasure.EEtaExpanded]
Y:871 [in MetaCoq.SafeChecker.PCUICSafeChecker]
y:872 [in MetaCoq.Translations.MiniHoTT_paths]
y:874 [in MetaCoq.Template.utils.wGraph]
y:874 [in MetaCoq.Translations.MiniHoTT]
y:877 [in MetaCoq.Template.utils.wGraph]
y:88 [in MetaCoq.PCUIC.utils.PCUICUtils]
y:88 [in MetaCoq.PCUIC.PCUICParallelReduction]
y:88 [in MetaCoq.Template.utils.wGraph]
y:88 [in MetaCoq.Template.Reflect]
y:881 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
y:882 [in MetaCoq.Translations.MiniHoTT]
y:882 [in MetaCoq.Translations.MiniHoTT_paths]
y:887 [in MetaCoq.Template.utils.wGraph]
y:89 [in MetaCoq.Template.Universes]
y:89 [in MetaCoq.Template.Kernames]
y:890 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
y:890 [in MetaCoq.Translations.MiniHoTT_paths]
y:891 [in MetaCoq.Template.utils.wGraph]
y:893 [in MetaCoq.Translations.MiniHoTT]
y:894 [in MetaCoq.Template.utils.wGraph]
y:898 [in MetaCoq.Template.utils.wGraph]
y:9 [in MetaCoq.Template.utils.ByteCompareSpec]
y:9 [in MetaCoq.Translations.sigma]
y:9 [in MetaCoq.PCUIC.Syntax.PCUICReflect]
y:9 [in MetaCoq.Translations.times_bool_fun2]
y:90 [in MetaCoq.Erasure.EInduction]
y:90 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
y:90 [in MetaCoq.PCUIC.PCUICEquality]
y:90 [in MetaCoq.Template.utils.ReflectEq]
y:90 [in MetaCoq.PCUIC.PCUICWellScopedCumulativity]
y:90 [in MetaCoq.SafeChecker.PCUICSafeReduce]
y:901 [in MetaCoq.Translations.MiniHoTT_paths]
y:902 [in MetaCoq.Template.utils.wGraph]
y:908 [in MetaCoq.Template.utils.All_Forall]
y:909 [in MetaCoq.PCUIC.PCUICParallelReduction]
y:909 [in MetaCoq.Translations.MiniHoTT]
y:91 [in MetaCoq.Template.utils.MCOption]
y:916 [in MetaCoq.Template.utils.wGraph]
y:917 [in MetaCoq.Translations.MiniHoTT_paths]
y:918 [in MetaCoq.Template.utils.All_Forall]
y:92 [in MetaCoq.PCUIC.utils.PCUICUtils]
y:92 [in MetaCoq.PCUIC.PCUICEquality]
y:92 [in MetaCoq.Translations.MiniHoTT_paths]
y:920 [in MetaCoq.PCUIC.PCUICInductiveInversion]
y:921 [in MetaCoq.Template.utils.wGraph]
y:924 [in MetaCoq.Template.utils.wGraph]
y:924 [in MetaCoq.Translations.MiniHoTT]
Y:928 [in MetaCoq.Translations.MiniHoTT]
y:929 [in MetaCoq.Template.utils.wGraph]
y:93 [in MetaCoq.Template.Universes]
y:93 [in MetaCoq.Template.utils.wGraph]
y:93 [in MetaCoq.Template.Reflect]
y:93 [in MetaCoq.Translations.MiniHoTT]
y:932 [in MetaCoq.Translations.MiniHoTT_paths]
y:933 [in MetaCoq.Template.utils.wGraph]
y:935 [in MetaCoq.PCUIC.PCUICInductiveInversion]
Y:936 [in MetaCoq.Translations.MiniHoTT_paths]
y:937 [in MetaCoq.Template.utils.wGraph]
y:938 [in MetaCoq.PCUIC.PCUICConfluence]
y:939 [in MetaCoq.PCUIC.PCUICConfluence]
y:94 [in MetaCoq.Template.common.uGraph]
y:94 [in MetaCoq.PCUIC.PCUICConfluence]
y:94 [in MetaCoq.PCUIC.Syntax.PCUICReflect]
y:94 [in MetaCoq.Translations.times_bool_fun2]
y:940 [in MetaCoq.PCUIC.PCUICConfluence]
y:941 [in MetaCoq.Template.utils.wGraph]
y:946 [in MetaCoq.PCUIC.PCUICConfluence]
y:946 [in MetaCoq.PCUIC.PCUICConversion]
y:947 [in MetaCoq.Template.utils.wGraph]
y:947 [in MetaCoq.PCUIC.PCUICConfluence]
y:947 [in MetaCoq.Translations.MiniHoTT]
y:948 [in MetaCoq.PCUIC.PCUICConfluence]
y:948 [in MetaCoq.PCUIC.PCUICReduction]
y:95 [in MetaCoq.PCUIC.utils.PCUICUtils]
y:95 [in MetaCoq.Translations.MiniHoTT]
y:950 [in MetaCoq.PCUIC.PCUICReduction]
y:955 [in MetaCoq.PCUIC.PCUICConversion]
y:955 [in MetaCoq.Translations.MiniHoTT_paths]
y:956 [in MetaCoq.Translations.MiniHoTT]
y:96 [in MetaCoq.Template.utils.bytestring]
y:96 [in MetaCoq.PCUIC.Syntax.PCUICReflect]
y:96 [in MetaCoq.PCUIC.PCUICSR]
y:963 [in MetaCoq.Translations.MiniHoTT]
y:964 [in MetaCoq.Translations.MiniHoTT_paths]
y:97 [in MetaCoq.PCUIC.PCUICCumulativitySpec]
y:971 [in MetaCoq.Translations.MiniHoTT_paths]
y:972 [in MetaCoq.Translations.MiniHoTT]
y:976 [in MetaCoq.Template.utils.All_Forall]
y:976 [in MetaCoq.Translations.MiniHoTT]
y:98 [in MetaCoq.Template.utils.bytestring]
y:98 [in MetaCoq.PCUIC.PCUICParallelReduction]
y:98 [in MetaCoq.SafeChecker.PCUICSafeConversion]
y:98 [in MetaCoq.Template.Reflect]
y:98 [in MetaCoq.PCUIC.Syntax.PCUICReflect]
y:98 [in MetaCoq.Translations.param_generous_packed]
y:980 [in MetaCoq.PCUIC.PCUICConfluence]
y:980 [in MetaCoq.Translations.MiniHoTT_paths]
y:981 [in MetaCoq.Template.utils.wGraph]
y:981 [in MetaCoq.PCUIC.PCUICConfluence]
y:982 [in MetaCoq.PCUIC.PCUICConfluence]
y:984 [in MetaCoq.Translations.MiniHoTT_paths]
y:985 [in MetaCoq.Template.utils.wGraph]
y:986 [in MetaCoq.Template.utils.All_Forall]
Y:99 [in MetaCoq.Template.monad_utils]
y:991 [in MetaCoq.Translations.MiniHoTT]
y:995 [in MetaCoq.Template.utils.wGraph]
y:995 [in MetaCoq.PCUIC.PCUICConfluence]
y:997 [in MetaCoq.Template.utils.wGraph]
y:997 [in MetaCoq.PCUIC.PCUICConfluence]
y:999 [in MetaCoq.PCUIC.PCUICConfluence]
y:999 [in MetaCoq.Translations.MiniHoTT_paths]
| 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) |