| 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) |
Q (binder)
qi:3 [in MetaCoq.Examples.constructor_tac]Qpres:132 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
Qs:187 [in MetaCoq.Template.EnvironmentTyping]
qt:243 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
qt:246 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
qt:251 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
qt:254 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
qt:44 [in MetaCoq.Examples.demo]
qt:8 [in MetaCoq.Examples.metacoq_tour]
q'':1191 [in MetaCoq.Translations.MiniHoTT]
q'':1199 [in MetaCoq.Translations.MiniHoTT_paths]
q'':1245 [in MetaCoq.Translations.MiniHoTT]
q'':1253 [in MetaCoq.Translations.MiniHoTT_paths]
q'':24 [in MetaCoq.Template.utils.MCCompare]
q':1044 [in MetaCoq.Translations.MiniHoTT]
q':1052 [in MetaCoq.Translations.MiniHoTT_paths]
q':1169 [in MetaCoq.Translations.MiniHoTT]
q':1177 [in MetaCoq.Translations.MiniHoTT_paths]
q':1180 [in MetaCoq.Translations.MiniHoTT]
q':1188 [in MetaCoq.Translations.MiniHoTT_paths]
q':1190 [in MetaCoq.Translations.MiniHoTT]
q':1198 [in MetaCoq.Translations.MiniHoTT_paths]
q':1210 [in MetaCoq.Translations.MiniHoTT]
q':1218 [in MetaCoq.Translations.MiniHoTT]
q':1218 [in MetaCoq.Translations.MiniHoTT_paths]
q':1226 [in MetaCoq.Translations.MiniHoTT_paths]
q':1244 [in MetaCoq.Translations.MiniHoTT]
q':1252 [in MetaCoq.Translations.MiniHoTT_paths]
q':1257 [in MetaCoq.Translations.MiniHoTT]
q':1265 [in MetaCoq.Translations.MiniHoTT_paths]
q':1307 [in MetaCoq.Translations.MiniHoTT]
q':1315 [in MetaCoq.Translations.MiniHoTT_paths]
q':211 [in MetaCoq.Template.utils.All_Forall]
q':23 [in MetaCoq.Template.utils.MCCompare]
Q':2527 [in MetaCoq.Template.utils.All_Forall]
Q':262 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
Q':873 [in MetaCoq.PCUIC.PCUICParallelReduction]
q1:128 [in MetaCoq.SafeChecker.PCUICSafeConversion]
q1:146 [in MetaCoq.SafeChecker.PCUICSafeConversion]
q1:160 [in MetaCoq.SafeChecker.PCUICSafeConversion]
q1:2793 [in MetaCoq.Translations.MiniHoTT]
q1:2801 [in MetaCoq.Translations.MiniHoTT_paths]
q1:2805 [in MetaCoq.Translations.MiniHoTT]
q1:2813 [in MetaCoq.Translations.MiniHoTT_paths]
q1:328 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
q2:129 [in MetaCoq.SafeChecker.PCUICSafeConversion]
q2:147 [in MetaCoq.SafeChecker.PCUICSafeConversion]
q2:161 [in MetaCoq.SafeChecker.PCUICSafeConversion]
q2:2795 [in MetaCoq.Translations.MiniHoTT]
q2:2803 [in MetaCoq.Translations.MiniHoTT_paths]
q2:2807 [in MetaCoq.Translations.MiniHoTT]
q2:2815 [in MetaCoq.Translations.MiniHoTT_paths]
q2:329 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
Q:100 [in MetaCoq.PCUIC.PCUICParallelReduction]
q:100 [in MetaCoq.Translations.param_generous_packed]
q:1002 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
Q:1009 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
Q:101 [in MetaCoq.PCUIC.PCUICElimination]
Q:1023 [in MetaCoq.PCUIC.PCUICTyping]
q:1027 [in MetaCoq.Translations.MiniHoTT]
Q:103 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
Q:1030 [in MetaCoq.PCUIC.PCUICTyping]
q:1035 [in MetaCoq.Translations.MiniHoTT_paths]
q:104 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
q:1043 [in MetaCoq.Translations.MiniHoTT]
q:1051 [in MetaCoq.Translations.MiniHoTT_paths]
Q:106 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
Q:1060 [in MetaCoq.Template.utils.All_Forall]
q:1062 [in MetaCoq.Translations.MiniHoTT]
q:1070 [in MetaCoq.Translations.MiniHoTT_paths]
Q:108 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
q:108 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
Q:108 [in MetaCoq.PCUIC.PCUICConfluence]
q:1080 [in MetaCoq.Translations.MiniHoTT]
q:1086 [in MetaCoq.Translations.MiniHoTT]
q:1088 [in MetaCoq.Translations.MiniHoTT_paths]
Q:1090 [in MetaCoq.Template.utils.All_Forall]
q:1093 [in MetaCoq.Translations.MiniHoTT]
q:1094 [in MetaCoq.Translations.MiniHoTT_paths]
q:11 [in MetaCoq.Template.utils.MCPred]
Q:110 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
q:110 [in MetaCoq.PCUIC.utils.PCUICOnOne]
q:1101 [in MetaCoq.Translations.MiniHoTT]
q:1101 [in MetaCoq.Translations.MiniHoTT_paths]
q:1109 [in MetaCoq.Translations.MiniHoTT]
q:1109 [in MetaCoq.Translations.MiniHoTT_paths]
q:1117 [in MetaCoq.Translations.MiniHoTT]
q:1117 [in MetaCoq.Translations.MiniHoTT_paths]
q:1118 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
q:112 [in MetaCoq.PCUIC.Syntax.PCUICViews]
q:1124 [in MetaCoq.Translations.MiniHoTT]
q:1125 [in MetaCoq.Translations.MiniHoTT_paths]
q:1131 [in MetaCoq.Translations.MiniHoTT]
q:1132 [in MetaCoq.Translations.MiniHoTT_paths]
q:1137 [in MetaCoq.Translations.MiniHoTT]
q:1139 [in MetaCoq.Translations.MiniHoTT_paths]
q:114 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
q:1142 [in MetaCoq.Translations.MiniHoTT]
q:1145 [in MetaCoq.Translations.MiniHoTT_paths]
q:1150 [in MetaCoq.Translations.MiniHoTT_paths]
q:1154 [in MetaCoq.Translations.MiniHoTT]
Q:116 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
q:1160 [in MetaCoq.Translations.MiniHoTT]
q:1162 [in MetaCoq.Translations.MiniHoTT_paths]
Q:1165 [in MetaCoq.PCUIC.PCUICReduction]
q:1168 [in MetaCoq.Translations.MiniHoTT]
q:1168 [in MetaCoq.Translations.MiniHoTT_paths]
q:117 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
q:1176 [in MetaCoq.Translations.MiniHoTT_paths]
q:1179 [in MetaCoq.Translations.MiniHoTT]
q:1187 [in MetaCoq.Translations.MiniHoTT_paths]
q:1189 [in MetaCoq.Translations.MiniHoTT]
q:119 [in MetaCoq.PCUIC.utils.PCUICOnOne]
q:1197 [in MetaCoq.Translations.MiniHoTT_paths]
Q:12 [in MetaCoq.PCUIC.Bidirectional.BDFromPCUIC]
Q:120 [in MetaCoq.SafeChecker.PCUICSafeReduce]
q:1201 [in MetaCoq.Translations.MiniHoTT]
Q:1209 [in MetaCoq.Template.utils.All_Forall]
q:1209 [in MetaCoq.Translations.MiniHoTT]
q:1209 [in MetaCoq.Translations.MiniHoTT_paths]
q:1217 [in MetaCoq.Translations.MiniHoTT]
q:1217 [in MetaCoq.Translations.MiniHoTT_paths]
q:122 [in MetaCoq.SafeChecker.PCUICSafeReduce]
q:1225 [in MetaCoq.Translations.MiniHoTT_paths]
q:1227 [in MetaCoq.Translations.MiniHoTT]
q:1235 [in MetaCoq.Translations.MiniHoTT]
q:1235 [in MetaCoq.Translations.MiniHoTT_paths]
Q:124 [in MetaCoq.Template.EnvironmentTyping]
q:1243 [in MetaCoq.Translations.MiniHoTT]
q:1243 [in MetaCoq.Translations.MiniHoTT_paths]
q:1251 [in MetaCoq.Translations.MiniHoTT_paths]
q:1256 [in MetaCoq.Translations.MiniHoTT]
Q:126 [in MetaCoq.PCUIC.utils.PCUICOnOne]
q:1264 [in MetaCoq.Translations.MiniHoTT_paths]
q:1267 [in MetaCoq.Translations.MiniHoTT]
q:1275 [in MetaCoq.Translations.MiniHoTT]
q:1275 [in MetaCoq.Translations.MiniHoTT_paths]
q:1279 [in MetaCoq.Translations.MiniHoTT]
q:1283 [in MetaCoq.Translations.MiniHoTT_paths]
q:1286 [in MetaCoq.Translations.MiniHoTT]
q:1287 [in MetaCoq.Translations.MiniHoTT_paths]
Q:129 [in MetaCoq.PCUIC.PCUICConfluence]
q:1294 [in MetaCoq.Translations.MiniHoTT_paths]
q:13 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
Q:130 [in MetaCoq.Template.EnvironmentTyping]
q:1306 [in MetaCoq.Translations.MiniHoTT]
Q:131 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
q:1314 [in MetaCoq.Translations.MiniHoTT_paths]
q:1315 [in MetaCoq.Translations.MiniHoTT]
q:1323 [in MetaCoq.Translations.MiniHoTT_paths]
q:1325 [in MetaCoq.Translations.MiniHoTT]
q:1333 [in MetaCoq.Translations.MiniHoTT_paths]
Q:1336 [in MetaCoq.PCUIC.PCUICParallelReductionConfluence]
q:1341 [in MetaCoq.Translations.MiniHoTT]
q:1349 [in MetaCoq.Template.utils.All_Forall]
q:1349 [in MetaCoq.Translations.MiniHoTT]
q:1349 [in MetaCoq.Translations.MiniHoTT_paths]
q:1355 [in MetaCoq.Translations.MiniHoTT]
q:1357 [in MetaCoq.Translations.MiniHoTT_paths]
q:1363 [in MetaCoq.Translations.MiniHoTT_paths]
q:1365 [in MetaCoq.Translations.MiniHoTT]
q:1373 [in MetaCoq.Translations.MiniHoTT_paths]
Q:1382 [in MetaCoq.Template.utils.All_Forall]
q:1396 [in MetaCoq.Translations.MiniHoTT]
q:1403 [in MetaCoq.Translations.MiniHoTT]
q:1404 [in MetaCoq.Translations.MiniHoTT_paths]
q:1411 [in MetaCoq.Translations.MiniHoTT_paths]
Q:142 [in MetaCoq.Template.utils.MCProd]
q:143 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
Q:1453 [in MetaCoq.Template.utils.All_Forall]
q:146 [in MetaCoq.Template.utils.All_Forall]
Q:15 [in MetaCoq.PCUIC.Syntax.PCUICReflect]
Q:150 [in MetaCoq.Template.utils.All_Forall]
Q:1526 [in MetaCoq.Template.utils.All_Forall]
Q:1533 [in MetaCoq.Template.utils.All_Forall]
Q:1541 [in MetaCoq.Template.utils.All_Forall]
Q:155 [in MetaCoq.PCUIC.PCUICAlpha]
q:155 [in MetaCoq.SafeChecker.PCUICEqualityDec]
Q:1563 [in MetaCoq.Template.utils.All_Forall]
Q:1578 [in MetaCoq.Template.utils.All_Forall]
Q:16 [in MetaCoq.PCUIC.PCUICRedTypeIrrelevance]
Q:16 [in MetaCoq.Template.TypingWf]
Q:165 [in MetaCoq.PCUIC.PCUICAlpha]
Q:165 [in MetaCoq.Template.monad_utils]
q:1681 [in MetaCoq.Translations.MiniHoTT]
q:1682 [in MetaCoq.Translations.MiniHoTT]
q:1689 [in MetaCoq.Translations.MiniHoTT_paths]
q:1690 [in MetaCoq.Translations.MiniHoTT_paths]
Q:1705 [in MetaCoq.Template.utils.All_Forall]
Q:171 [in MetaCoq.Template.utils.All_Forall]
q:1712 [in MetaCoq.Translations.MiniHoTT]
q:1719 [in MetaCoq.Translations.MiniHoTT]
q:1720 [in MetaCoq.Translations.MiniHoTT_paths]
q:1725 [in MetaCoq.Translations.MiniHoTT]
q:1727 [in MetaCoq.Translations.MiniHoTT_paths]
q:1733 [in MetaCoq.Translations.MiniHoTT_paths]
q:1734 [in MetaCoq.Translations.MiniHoTT]
q:1742 [in MetaCoq.Translations.MiniHoTT_paths]
q:1743 [in MetaCoq.Translations.MiniHoTT]
q:175 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
q:1751 [in MetaCoq.Translations.MiniHoTT_paths]
q:1752 [in MetaCoq.Translations.MiniHoTT]
Q:1753 [in MetaCoq.Template.utils.All_Forall]
q:176 [in MetaCoq.Translations.times_bool_fun]
q:1760 [in MetaCoq.Translations.MiniHoTT_paths]
q:1762 [in MetaCoq.Translations.MiniHoTT]
q:1770 [in MetaCoq.Translations.MiniHoTT_paths]
q:1771 [in MetaCoq.Translations.MiniHoTT]
q:1779 [in MetaCoq.Translations.MiniHoTT_paths]
q:1780 [in MetaCoq.Translations.MiniHoTT]
q:1786 [in MetaCoq.Translations.MiniHoTT]
q:1788 [in MetaCoq.Translations.MiniHoTT_paths]
q:1789 [in MetaCoq.Translations.MiniHoTT]
Q:1790 [in MetaCoq.Template.utils.All_Forall]
q:1791 [in MetaCoq.Translations.MiniHoTT]
q:1794 [in MetaCoq.Translations.MiniHoTT_paths]
Q:1797 [in MetaCoq.Template.utils.All_Forall]
q:1797 [in MetaCoq.Translations.MiniHoTT_paths]
q:1799 [in MetaCoq.Translations.MiniHoTT_paths]
Q:18 [in MetaCoq.PCUIC.PCUICParallelReduction]
q:180 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
Q:1822 [in MetaCoq.Template.utils.All_Forall]
Q:1827 [in MetaCoq.Template.utils.All_Forall]
q:1830 [in MetaCoq.Translations.MiniHoTT]
q:1831 [in MetaCoq.Translations.MiniHoTT]
q:1832 [in MetaCoq.Translations.MiniHoTT]
q:1833 [in MetaCoq.Translations.MiniHoTT]
q:1834 [in MetaCoq.Translations.MiniHoTT]
q:1835 [in MetaCoq.Translations.MiniHoTT]
q:1836 [in MetaCoq.Translations.MiniHoTT]
q:1837 [in MetaCoq.Translations.MiniHoTT]
q:1838 [in MetaCoq.Translations.MiniHoTT]
q:1838 [in MetaCoq.Translations.MiniHoTT_paths]
q:1839 [in MetaCoq.Translations.MiniHoTT_paths]
q:184 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
q:1840 [in MetaCoq.Translations.MiniHoTT_paths]
Q:1841 [in MetaCoq.Template.utils.All_Forall]
q:1841 [in MetaCoq.Translations.MiniHoTT_paths]
q:1842 [in MetaCoq.Translations.MiniHoTT_paths]
q:1843 [in MetaCoq.Translations.MiniHoTT_paths]
q:1844 [in MetaCoq.Translations.MiniHoTT]
q:1844 [in MetaCoq.Translations.MiniHoTT_paths]
q:1845 [in MetaCoq.Translations.MiniHoTT_paths]
q:1846 [in MetaCoq.Translations.MiniHoTT_paths]
q:1851 [in MetaCoq.Translations.MiniHoTT]
q:1852 [in MetaCoq.Translations.MiniHoTT_paths]
q:1859 [in MetaCoq.Translations.MiniHoTT_paths]
Q:186 [in MetaCoq.Template.EnvironmentTyping]
Q:1860 [in MetaCoq.Template.utils.All_Forall]
q:1861 [in MetaCoq.Translations.MiniHoTT]
Q:1867 [in MetaCoq.Template.utils.All_Forall]
q:1868 [in MetaCoq.Translations.MiniHoTT]
q:1869 [in MetaCoq.Translations.MiniHoTT_paths]
q:1875 [in MetaCoq.Translations.MiniHoTT]
q:1876 [in MetaCoq.Translations.MiniHoTT_paths]
q:188 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
q:1882 [in MetaCoq.Translations.MiniHoTT]
q:1883 [in MetaCoq.Translations.MiniHoTT_paths]
q:1889 [in MetaCoq.Template.utils.All_Forall]
q:1889 [in MetaCoq.Translations.MiniHoTT]
q:1890 [in MetaCoq.Translations.MiniHoTT_paths]
q:1896 [in MetaCoq.Translations.MiniHoTT]
q:1897 [in MetaCoq.Translations.MiniHoTT_paths]
q:1904 [in MetaCoq.Translations.MiniHoTT]
q:1904 [in MetaCoq.Translations.MiniHoTT_paths]
q:1906 [in MetaCoq.Template.utils.All_Forall]
q:1911 [in MetaCoq.Template.utils.All_Forall]
q:1912 [in MetaCoq.Translations.MiniHoTT]
q:1912 [in MetaCoq.Translations.MiniHoTT_paths]
q:1919 [in MetaCoq.Translations.MiniHoTT]
q:1920 [in MetaCoq.Translations.MiniHoTT_paths]
Q:1921 [in MetaCoq.Template.utils.All_Forall]
Q:1926 [in MetaCoq.Template.utils.All_Forall]
q:1926 [in MetaCoq.Translations.MiniHoTT]
q:1927 [in MetaCoq.Translations.MiniHoTT_paths]
Q:1931 [in MetaCoq.Template.utils.All_Forall]
q:1933 [in MetaCoq.Translations.MiniHoTT]
q:1934 [in MetaCoq.Translations.MiniHoTT_paths]
q:1940 [in MetaCoq.Translations.MiniHoTT]
q:1941 [in MetaCoq.Translations.MiniHoTT_paths]
q:1947 [in MetaCoq.Translations.MiniHoTT]
q:1948 [in MetaCoq.Translations.MiniHoTT_paths]
q:1954 [in MetaCoq.Translations.MiniHoTT]
q:1955 [in MetaCoq.Translations.MiniHoTT_paths]
q:196 [in MetaCoq.SafeChecker.PCUICSafeConversion]
q:196 [in MetaCoq.Examples.tauto]
q:1961 [in MetaCoq.Translations.MiniHoTT]
q:1962 [in MetaCoq.Translations.MiniHoTT_paths]
q:1968 [in MetaCoq.Translations.MiniHoTT]
q:1969 [in MetaCoq.Translations.MiniHoTT_paths]
q:197 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
q:197 [in MetaCoq.PCUIC.PCUICInductiveInversion]
q:1975 [in MetaCoq.Translations.MiniHoTT]
q:1976 [in MetaCoq.Translations.MiniHoTT_paths]
q:1982 [in MetaCoq.Translations.MiniHoTT]
q:1983 [in MetaCoq.Translations.MiniHoTT_paths]
q:1989 [in MetaCoq.Translations.MiniHoTT]
q:199 [in MetaCoq.Translations.MiniHoTT]
q:1990 [in MetaCoq.Translations.MiniHoTT_paths]
q:1996 [in MetaCoq.Translations.MiniHoTT]
q:1997 [in MetaCoq.Translations.MiniHoTT_paths]
Q:2 [in MetaCoq.Template.utils.MCRelations]
Q:2 [in MetaCoq.Template.utils.ByteCompareSpec]
Q:2 [in MetaCoq.Template.utils.MCArith]
q:2003 [in MetaCoq.Translations.MiniHoTT]
q:2004 [in MetaCoq.Translations.MiniHoTT_paths]
Q:201 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
Q:201 [in MetaCoq.Template.monad_utils]
q:2010 [in MetaCoq.Translations.MiniHoTT]
Q:2011 [in MetaCoq.Template.utils.All_Forall]
q:2011 [in MetaCoq.Translations.MiniHoTT_paths]
q:2017 [in MetaCoq.Translations.MiniHoTT]
q:2018 [in MetaCoq.Translations.MiniHoTT_paths]
q:2024 [in MetaCoq.Translations.MiniHoTT]
q:2025 [in MetaCoq.Translations.MiniHoTT_paths]
q:2031 [in MetaCoq.Translations.MiniHoTT]
q:2032 [in MetaCoq.Translations.MiniHoTT_paths]
q:2037 [in MetaCoq.Translations.MiniHoTT]
q:2039 [in MetaCoq.Translations.MiniHoTT_paths]
q:204 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
q:204 [in MetaCoq.SafeChecker.PCUICEqualityDec]
q:2042 [in MetaCoq.Translations.MiniHoTT]
q:2045 [in MetaCoq.Translations.MiniHoTT_paths]
q:2047 [in MetaCoq.Translations.MiniHoTT]
q:2050 [in MetaCoq.Translations.MiniHoTT_paths]
q:2052 [in MetaCoq.Translations.MiniHoTT]
q:2055 [in MetaCoq.Translations.MiniHoTT_paths]
q:2057 [in MetaCoq.Translations.MiniHoTT]
q:2060 [in MetaCoq.Translations.MiniHoTT_paths]
q:2062 [in MetaCoq.Translations.MiniHoTT]
q:2065 [in MetaCoq.Translations.MiniHoTT_paths]
q:2067 [in MetaCoq.Translations.MiniHoTT]
q:207 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
q:207 [in MetaCoq.Translations.MiniHoTT]
q:207 [in MetaCoq.Translations.MiniHoTT_paths]
q:2070 [in MetaCoq.Translations.MiniHoTT_paths]
q:2072 [in MetaCoq.Translations.MiniHoTT]
q:2075 [in MetaCoq.Translations.MiniHoTT_paths]
q:208 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
q:208 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
q:2080 [in MetaCoq.Translations.MiniHoTT]
q:2080 [in MetaCoq.Translations.MiniHoTT_paths]
q:2088 [in MetaCoq.Translations.MiniHoTT]
q:2088 [in MetaCoq.Translations.MiniHoTT_paths]
q:2096 [in MetaCoq.Translations.MiniHoTT_paths]
q:21 [in MetaCoq.Template.utils.MCUtils]
Q:21 [in MetaCoq.PCUIC.PCUICConfluence]
q:210 [in MetaCoq.Template.utils.All_Forall]
q:2110 [in MetaCoq.Translations.MiniHoTT]
q:2118 [in MetaCoq.Translations.MiniHoTT]
q:2118 [in MetaCoq.Translations.MiniHoTT_paths]
q:2126 [in MetaCoq.Translations.MiniHoTT_paths]
q:213 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
q:215 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
q:215 [in MetaCoq.Translations.MiniHoTT_paths]
q:2167 [in MetaCoq.Translations.MiniHoTT]
q:2168 [in MetaCoq.Translations.MiniHoTT]
q:2175 [in MetaCoq.Translations.MiniHoTT_paths]
q:2176 [in MetaCoq.Translations.MiniHoTT_paths]
Q:218 [in MetaCoq.Template.EnvironmentTyping]
q:2181 [in MetaCoq.Translations.MiniHoTT]
q:2182 [in MetaCoq.Translations.MiniHoTT]
q:2189 [in MetaCoq.Translations.MiniHoTT_paths]
Q:219 [in MetaCoq.Template.TypingWf]
q:2190 [in MetaCoq.Translations.MiniHoTT_paths]
q:2195 [in MetaCoq.Translations.MiniHoTT]
q:2196 [in MetaCoq.Translations.MiniHoTT]
q:22 [in MetaCoq.Template.utils.MCCompare]
Q:220 [in MetaCoq.Template.EnvironmentTyping]
q:220 [in MetaCoq.Template.utils.wGraph]
q:2203 [in MetaCoq.Translations.MiniHoTT_paths]
q:2204 [in MetaCoq.Translations.MiniHoTT_paths]
q:2209 [in MetaCoq.Translations.MiniHoTT]
q:221 [in MetaCoq.Template.utils.wGraph]
q:2210 [in MetaCoq.Translations.MiniHoTT]
q:2217 [in MetaCoq.Translations.MiniHoTT_paths]
q:2218 [in MetaCoq.Translations.MiniHoTT_paths]
q:222 [in MetaCoq.Translations.MiniHoTT]
q:2222 [in MetaCoq.Translations.MiniHoTT]
Q:2227 [in MetaCoq.Template.utils.All_Forall]
q:2230 [in MetaCoq.Translations.MiniHoTT]
q:2230 [in MetaCoq.Translations.MiniHoTT_paths]
q:2237 [in MetaCoq.Translations.MiniHoTT]
q:2238 [in MetaCoq.Translations.MiniHoTT_paths]
Q:2241 [in MetaCoq.Template.utils.All_Forall]
q:2245 [in MetaCoq.Translations.MiniHoTT_paths]
q:2247 [in MetaCoq.Translations.MiniHoTT]
q:2255 [in MetaCoq.Translations.MiniHoTT_paths]
q:2257 [in MetaCoq.Translations.MiniHoTT]
q:2265 [in MetaCoq.Translations.MiniHoTT_paths]
q:2267 [in MetaCoq.Translations.MiniHoTT]
q:227 [in MetaCoq.SafeChecker.PCUICEqualityDec]
q:2275 [in MetaCoq.Translations.MiniHoTT_paths]
q:2277 [in MetaCoq.Translations.MiniHoTT]
q:228 [in MetaCoq.Translations.MiniHoTT]
Q:2284 [in MetaCoq.Template.utils.All_Forall]
q:2285 [in MetaCoq.Translations.MiniHoTT_paths]
q:2287 [in MetaCoq.Translations.MiniHoTT]
q:2294 [in MetaCoq.Translations.MiniHoTT]
q:2295 [in MetaCoq.Translations.MiniHoTT_paths]
Q:2298 [in MetaCoq.Template.utils.All_Forall]
q:230 [in MetaCoq.Translations.MiniHoTT_paths]
q:2302 [in MetaCoq.Translations.MiniHoTT_paths]
Q:2307 [in MetaCoq.Template.utils.All_Forall]
Q:231 [in MetaCoq.Template.EnvironmentTyping]
Q:2316 [in MetaCoq.Template.utils.All_Forall]
Q:2337 [in MetaCoq.Template.utils.All_Forall]
q:234 [in MetaCoq.Translations.MiniHoTT]
q:2351 [in MetaCoq.Translations.MiniHoTT]
q:2359 [in MetaCoq.Translations.MiniHoTT_paths]
q:236 [in MetaCoq.Translations.MiniHoTT_paths]
Q:2362 [in MetaCoq.Template.utils.All_Forall]
Q:2397 [in MetaCoq.Template.utils.All_Forall]
q:240 [in MetaCoq.Translations.MiniHoTT]
q:2400 [in MetaCoq.Translations.MiniHoTT]
q:2408 [in MetaCoq.Translations.MiniHoTT_paths]
Q:242 [in MetaCoq.Template.EnvironmentTyping]
q:242 [in MetaCoq.Translations.MiniHoTT_paths]
Q:2421 [in MetaCoq.Template.utils.All_Forall]
Q:2428 [in MetaCoq.Template.utils.All_Forall]
Q:2437 [in MetaCoq.Template.utils.All_Forall]
Q:2446 [in MetaCoq.Template.utils.All_Forall]
Q:2455 [in MetaCoq.Template.utils.All_Forall]
q:246 [in MetaCoq.Translations.MiniHoTT]
Q:2464 [in MetaCoq.Template.utils.All_Forall]
Q:2468 [in MetaCoq.Translations.MiniHoTT]
q:247 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
Q:2476 [in MetaCoq.Translations.MiniHoTT_paths]
Q:2479 [in MetaCoq.Translations.MiniHoTT]
Q:248 [in MetaCoq.Template.utils.All_Forall]
q:248 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
q:248 [in MetaCoq.Translations.MiniHoTT_paths]
Q:2487 [in MetaCoq.Translations.MiniHoTT_paths]
Q:2491 [in MetaCoq.Translations.MiniHoTT]
Q:2495 [in MetaCoq.Template.utils.All_Forall]
Q:2499 [in MetaCoq.Translations.MiniHoTT_paths]
Q:2507 [in MetaCoq.Template.utils.All_Forall]
Q:2507 [in MetaCoq.Translations.MiniHoTT]
Q:2515 [in MetaCoq.Translations.MiniHoTT_paths]
q:252 [in MetaCoq.Translations.MiniHoTT]
Q:2520 [in MetaCoq.Translations.MiniHoTT]
Q:2525 [in MetaCoq.Template.utils.All_Forall]
Q:2528 [in MetaCoq.Translations.MiniHoTT_paths]
Q:2532 [in MetaCoq.Translations.MiniHoTT]
q:254 [in MetaCoq.Translations.MiniHoTT_paths]
Q:2540 [in MetaCoq.Translations.MiniHoTT]
Q:2540 [in MetaCoq.Translations.MiniHoTT_paths]
Q:2541 [in MetaCoq.Template.utils.All_Forall]
Q:2548 [in MetaCoq.Translations.MiniHoTT_paths]
Q:2552 [in MetaCoq.Template.utils.All_Forall]
Q:2554 [in MetaCoq.Translations.MiniHoTT]
Q:256 [in MetaCoq.Template.utils.All_Forall]
Q:2561 [in MetaCoq.Translations.MiniHoTT]
Q:2562 [in MetaCoq.Translations.MiniHoTT_paths]
Q:2568 [in MetaCoq.Template.utils.All_Forall]
Q:2569 [in MetaCoq.Translations.MiniHoTT_paths]
q:258 [in MetaCoq.Translations.MiniHoTT]
Q:2582 [in MetaCoq.Translations.MiniHoTT]
Q:2590 [in MetaCoq.Translations.MiniHoTT_paths]
Q:2594 [in MetaCoq.Template.utils.All_Forall]
Q:26 [in MetaCoq.PCUIC.PCUICParallelReduction]
q:260 [in MetaCoq.Translations.MiniHoTT_paths]
Q:261 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
q:261 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
q:263 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
Q:263 [in MetaCoq.Template.TypingWf]
Q:2636 [in MetaCoq.Translations.MiniHoTT]
Q:264 [in MetaCoq.Template.utils.All_Forall]
q:264 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
q:264 [in MetaCoq.Translations.MiniHoTT]
Q:2644 [in MetaCoq.Translations.MiniHoTT_paths]
q:265 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
q:266 [in MetaCoq.Translations.MiniHoTT_paths]
q:2669 [in MetaCoq.Translations.MiniHoTT]
q:2677 [in MetaCoq.Translations.MiniHoTT_paths]
Q:2678 [in MetaCoq.Translations.MiniHoTT]
Q:2686 [in MetaCoq.Translations.MiniHoTT_paths]
q:2697 [in MetaCoq.Translations.MiniHoTT]
q:2705 [in MetaCoq.Translations.MiniHoTT_paths]
q:272 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
q:272 [in MetaCoq.Translations.MiniHoTT_paths]
Q:2733 [in MetaCoq.Translations.MiniHoTT]
Q:274 [in MetaCoq.Template.utils.All_Forall]
q:274 [in MetaCoq.Translations.MiniHoTT]
q:2740 [in MetaCoq.Translations.MiniHoTT]
Q:2741 [in MetaCoq.Translations.MiniHoTT_paths]
q:2746 [in MetaCoq.Translations.MiniHoTT]
q:2748 [in MetaCoq.Translations.MiniHoTT_paths]
q:2752 [in MetaCoq.Translations.MiniHoTT]
q:2754 [in MetaCoq.Translations.MiniHoTT_paths]
q:2760 [in MetaCoq.Translations.MiniHoTT_paths]
q:2764 [in MetaCoq.Translations.MiniHoTT]
Q:2765 [in MetaCoq.Translations.MiniHoTT]
q:2772 [in MetaCoq.Translations.MiniHoTT_paths]
Q:2773 [in MetaCoq.Translations.MiniHoTT_paths]
q:279 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
q:280 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
q:281 [in MetaCoq.Translations.MiniHoTT]
q:2815 [in MetaCoq.Translations.MiniHoTT]
q:282 [in MetaCoq.Translations.MiniHoTT_paths]
q:2823 [in MetaCoq.Translations.MiniHoTT_paths]
q:2825 [in MetaCoq.Translations.MiniHoTT]
q:2833 [in MetaCoq.Translations.MiniHoTT_paths]
q:2836 [in MetaCoq.Translations.MiniHoTT]
Q:284 [in MetaCoq.Template.utils.All_Forall]
q:2844 [in MetaCoq.Translations.MiniHoTT_paths]
q:2863 [in MetaCoq.Translations.MiniHoTT]
q:2871 [in MetaCoq.Translations.MiniHoTT_paths]
q:2872 [in MetaCoq.Translations.MiniHoTT]
q:288 [in MetaCoq.Translations.MiniHoTT]
q:2880 [in MetaCoq.Translations.MiniHoTT_paths]
q:289 [in MetaCoq.Translations.MiniHoTT_paths]
Q:29 [in MetaCoq.PCUIC.PCUICConfluence]
q:291 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
Q:2915 [in MetaCoq.Translations.MiniHoTT]
Q:2923 [in MetaCoq.Translations.MiniHoTT]
Q:2923 [in MetaCoq.Translations.MiniHoTT_paths]
q:2930 [in MetaCoq.Translations.MiniHoTT]
Q:2931 [in MetaCoq.Translations.MiniHoTT_paths]
Q:2935 [in MetaCoq.Translations.MiniHoTT]
q:2938 [in MetaCoq.Translations.MiniHoTT_paths]
Q:294 [in MetaCoq.PCUIC.PCUICParallelReduction]
q:294 [in MetaCoq.Template.utils.wGraph]
Q:2943 [in MetaCoq.Translations.MiniHoTT_paths]
q:295 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
q:295 [in MetaCoq.Translations.MiniHoTT]
Q:2950 [in MetaCoq.Translations.MiniHoTT]
Q:2958 [in MetaCoq.Translations.MiniHoTT_paths]
q:296 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
q:296 [in MetaCoq.Translations.MiniHoTT_paths]
Q:2960 [in MetaCoq.Translations.MiniHoTT]
Q:2966 [in MetaCoq.Translations.MiniHoTT]
Q:2968 [in MetaCoq.Translations.MiniHoTT_paths]
Q:2974 [in MetaCoq.Translations.MiniHoTT_paths]
q:2987 [in MetaCoq.Translations.MiniHoTT]
q:2988 [in MetaCoq.Translations.MiniHoTT]
Q:2992 [in MetaCoq.Translations.MiniHoTT]
q:2995 [in MetaCoq.Translations.MiniHoTT_paths]
q:2996 [in MetaCoq.Translations.MiniHoTT_paths]
q:3 [in MetaCoq.Template.utils.MCPred]
q:30 [in MetaCoq.Template.TemplateMonad.Core]
Q:30 [in MetaCoq.PCUIC.utils.PCUICOnOne]
Q:3000 [in MetaCoq.Translations.MiniHoTT_paths]
q:302 [in MetaCoq.Translations.MiniHoTT]
q:303 [in MetaCoq.Translations.MiniHoTT_paths]
Q:305 [in MetaCoq.PCUIC.PCUICParallelReduction]
q:309 [in MetaCoq.Translations.MiniHoTT]
q:310 [in MetaCoq.Translations.MiniHoTT_paths]
q:311 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
q:312 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
Q:313 [in MetaCoq.PCUIC.PCUICSR]
Q:316 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
q:316 [in MetaCoq.Translations.MiniHoTT]
q:317 [in MetaCoq.Translations.MiniHoTT_paths]
Q:319 [in MetaCoq.Template.EnvironmentTyping]
q:321 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
q:323 [in MetaCoq.Translations.MiniHoTT]
q:324 [in MetaCoq.Translations.MiniHoTT_paths]
q:326 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
Q:327 [in MetaCoq.Template.utils.All_Forall]
q:329 [in MetaCoq.Translations.MiniHoTT]
q:33 [in MetaCoq.Examples.demo]
q:331 [in MetaCoq.Translations.MiniHoTT_paths]
q:332 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
Q:333 [in MetaCoq.Template.utils.All_Forall]
q:334 [in MetaCoq.Translations.MiniHoTT]
q:335 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
q:337 [in MetaCoq.Translations.MiniHoTT_paths]
q:339 [in MetaCoq.Translations.MiniHoTT]
Q:34 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
q:34 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
Q:340 [in MetaCoq.Template.Environment]
Q:341 [in MetaCoq.Template.utils.All_Forall]
Q:341 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
q:342 [in MetaCoq.Translations.MiniHoTT_paths]
q:343 [in MetaCoq.Template.utils.wGraph]
q:344 [in MetaCoq.Translations.MiniHoTT]
q:345 [in MetaCoq.Template.utils.wGraph]
Q:346 [in MetaCoq.Template.Environment]
q:346 [in MetaCoq.SafeChecker.PCUICEqualityDec]
Q:347 [in MetaCoq.PCUIC.Conversion.PCUICInstConv]
q:347 [in MetaCoq.Translations.MiniHoTT_paths]
q:349 [in MetaCoq.Translations.MiniHoTT]
q:352 [in MetaCoq.Translations.MiniHoTT_paths]
q:353 [in MetaCoq.Template.utils.wGraph]
q:354 [in MetaCoq.Translations.MiniHoTT]
Q:356 [in MetaCoq.Template.utils.All_Forall]
q:357 [in MetaCoq.Translations.MiniHoTT_paths]
q:359 [in MetaCoq.Translations.MiniHoTT]
Q:36 [in MetaCoq.PCUIC.PCUICParallelReduction]
q:361 [in MetaCoq.PCUIC.PCUICWcbvEval]
q:362 [in MetaCoq.Translations.MiniHoTT_paths]
q:364 [in MetaCoq.Translations.MiniHoTT]
q:367 [in MetaCoq.Translations.MiniHoTT_paths]
q:372 [in MetaCoq.Translations.MiniHoTT_paths]
q:38 [in MetaCoq.Examples.demo]
Q:383 [in MetaCoq.Template.BasicAst]
Q:4 [in MetaCoq.PCUIC.Bidirectional.BDToPCUIC]
Q:40 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
q:400 [in MetaCoq.Translations.MiniHoTT]
q:403 [in MetaCoq.Template.utils.wGraph]
q:408 [in MetaCoq.Translations.MiniHoTT]
q:408 [in MetaCoq.Translations.MiniHoTT_paths]
q:41 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
Q:413 [in MetaCoq.Template.utils.All_Forall]
Q:416 [in MetaCoq.PCUIC.PCUICNormal]
q:416 [in MetaCoq.Translations.MiniHoTT]
q:416 [in MetaCoq.Translations.MiniHoTT_paths]
q:421 [in MetaCoq.Template.utils.wGraph]
Q:423 [in MetaCoq.Template.utils.All_Forall]
q:424 [in MetaCoq.Translations.MiniHoTT]
q:424 [in MetaCoq.Translations.MiniHoTT_paths]
q:432 [in MetaCoq.Translations.MiniHoTT_paths]
q:441 [in MetaCoq.Translations.MiniHoTT]
Q:448 [in MetaCoq.Template.utils.All_Forall]
q:449 [in MetaCoq.Translations.MiniHoTT_paths]
Q:45 [in MetaCoq.Template.TypingWf]
q:451 [in MetaCoq.Translations.MiniHoTT]
Q:453 [in MetaCoq.Template.utils.All_Forall]
q:459 [in MetaCoq.Translations.MiniHoTT_paths]
q:46 [in MetaCoq.Translations.translation_utils]
q:460 [in MetaCoq.Translations.MiniHoTT]
q:468 [in MetaCoq.Translations.MiniHoTT_paths]
Q:47 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
Q:47 [in MetaCoq.PCUIC.utils.PCUICOnOne]
Q:47 [in MetaCoq.PCUIC.PCUICConfluence]
Q:481 [in MetaCoq.Template.utils.All_Forall]
Q:484 [in MetaCoq.Examples.tauto]
Q:486 [in MetaCoq.Examples.tauto]
Q:488 [in MetaCoq.Template.utils.All_Forall]
Q:488 [in MetaCoq.Examples.tauto]
q:5 [in MetaCoq.Template.utils.MCCompare]
q:508 [in MetaCoq.PCUIC.PCUICAst]
q:509 [in MetaCoq.Translations.MiniHoTT]
q:516 [in MetaCoq.Translations.MiniHoTT]
q:517 [in MetaCoq.PCUIC.PCUICAst]
q:517 [in MetaCoq.Translations.MiniHoTT_paths]
q:523 [in MetaCoq.Translations.MiniHoTT]
q:524 [in MetaCoq.PCUIC.PCUICAst]
q:524 [in MetaCoq.Translations.MiniHoTT_paths]
q:53 [in MetaCoq.Template.utils.All_Forall]
q:531 [in MetaCoq.Translations.MiniHoTT_paths]
q:532 [in MetaCoq.Translations.MiniHoTT]
q:540 [in MetaCoq.Translations.MiniHoTT_paths]
q:545 [in MetaCoq.Translations.MiniHoTT]
Q:553 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
q:553 [in MetaCoq.Translations.MiniHoTT_paths]
q:556 [in MetaCoq.Translations.MiniHoTT]
Q:56 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
Q:562 [in MetaCoq.Template.utils.All_Forall]
q:564 [in MetaCoq.Translations.MiniHoTT_paths]
q:565 [in MetaCoq.Translations.MiniHoTT]
Q:568 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
q:572 [in MetaCoq.PCUIC.PCUICAst]
q:573 [in MetaCoq.Translations.MiniHoTT_paths]
Q:576 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
q:576 [in MetaCoq.Translations.MiniHoTT]
Q:579 [in MetaCoq.Template.utils.All_Forall]
q:584 [in MetaCoq.Translations.MiniHoTT_paths]
q:587 [in MetaCoq.Translations.MiniHoTT]
q:590 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
q:595 [in MetaCoq.Translations.MiniHoTT_paths]
q:596 [in MetaCoq.Translations.MiniHoTT]
Q:6 [in MetaCoq.Template.TypingWf]
q:60 [in MetaCoq.Template.utils.All_Forall]
q:604 [in MetaCoq.Translations.MiniHoTT_paths]
q:605 [in MetaCoq.Translations.MiniHoTT]
q:61 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
q:61 [in MetaCoq.Template.utils.wGraph]
Q:61 [in MetaCoq.PCUIC.PCUICConvCumInversion]
q:613 [in MetaCoq.Translations.MiniHoTT_paths]
q:614 [in MetaCoq.Translations.MiniHoTT]
Q:618 [in MetaCoq.Template.utils.All_Forall]
q:619 [in MetaCoq.Template.utils.wGraph]
q:620 [in MetaCoq.Translations.MiniHoTT]
q:622 [in MetaCoq.Translations.MiniHoTT_paths]
q:625 [in MetaCoq.Template.utils.wGraph]
q:625 [in MetaCoq.Translations.MiniHoTT]
q:628 [in MetaCoq.Template.utils.wGraph]
q:628 [in MetaCoq.Translations.MiniHoTT_paths]
Q:63 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
Q:63 [in MetaCoq.PCUIC.PCUICConvCumInversion]
Q:63 [in MetaCoq.PCUIC.Typing.PCUICRenameTyp]
q:632 [in MetaCoq.Template.utils.wGraph]
q:633 [in MetaCoq.Translations.MiniHoTT_paths]
q:636 [in MetaCoq.Template.utils.wGraph]
q:65 [in MetaCoq.PCUIC.Syntax.PCUICOnFreeVars]
Q:65 [in MetaCoq.Template.TypingWf]
Q:660 [in MetaCoq.PCUIC.PCUICParallelReduction]
q:665 [in MetaCoq.Template.utils.wGraph]
q:671 [in MetaCoq.Template.utils.wGraph]
q:674 [in MetaCoq.Template.utils.wGraph]
Q:676 [in MetaCoq.Template.EnvironmentTyping]
Q:678 [in MetaCoq.Template.utils.All_Forall]
Q:68 [in MetaCoq.PCUIC.PCUICContextReduction]
q:680 [in MetaCoq.Template.utils.wGraph]
q:684 [in MetaCoq.Template.utils.wGraph]
Q:685 [in MetaCoq.Template.EnvironmentTyping]
q:69 [in MetaCoq.Examples.demo]
Q:696 [in MetaCoq.Template.EnvironmentTyping]
Q:699 [in MetaCoq.Template.utils.All_Forall]
q:7 [in MetaCoq.Template.utils.MCCompare]
Q:7 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
Q:71 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
q:719 [in MetaCoq.Translations.MiniHoTT]
Q:72 [in MetaCoq.PCUIC.PCUICAlpha]
Q:72 [in MetaCoq.SafeChecker.PCUICSafeReduce]
q:727 [in MetaCoq.Translations.MiniHoTT_paths]
Q:734 [in MetaCoq.Template.EnvironmentTyping]
Q:739 [in MetaCoq.Template.utils.All_Forall]
q:742 [in MetaCoq.Translations.MiniHoTT]
Q:749 [in MetaCoq.SafeChecker.PCUICSafeChecker]
Q:75 [in MetaCoq.PCUIC.PCUICParallelReduction]
q:750 [in MetaCoq.Translations.MiniHoTT_paths]
Q:78 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
Q:789 [in MetaCoq.Template.utils.All_Forall]
Q:80 [in MetaCoq.PCUIC.utils.PCUICOnOne]
q:80 [in MetaCoq.SafeChecker.PCUICSafeConversion]
Q:800 [in MetaCoq.PCUIC.PCUICReduction]
Q:805 [in MetaCoq.PCUIC.PCUICReduction]
q:809 [in MetaCoq.Translations.MiniHoTT]
q:817 [in MetaCoq.Translations.MiniHoTT_paths]
q:820 [in MetaCoq.Translations.MiniHoTT]
q:824 [in MetaCoq.Template.utils.wGraph]
q:828 [in MetaCoq.Translations.MiniHoTT_paths]
Q:83 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
q:831 [in MetaCoq.Template.utils.wGraph]
q:831 [in MetaCoq.Translations.MiniHoTT]
q:839 [in MetaCoq.Translations.MiniHoTT_paths]
q:84 [in MetaCoq.Template.utils.All_Forall]
Q:84 [in MetaCoq.PCUIC.TemplateToPCUICExpanded]
q:843 [in MetaCoq.Translations.MiniHoTT]
Q:846 [in MetaCoq.PCUIC.PCUICParallelReduction]
q:849 [in MetaCoq.Translations.MiniHoTT]
q:851 [in MetaCoq.Translations.MiniHoTT_paths]
Q:854 [in MetaCoq.Translations.MiniHoTT]
Q:857 [in MetaCoq.PCUIC.PCUICParallelReduction]
q:857 [in MetaCoq.Translations.MiniHoTT_paths]
q:858 [in MetaCoq.Translations.MiniHoTT]
q:86 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
Q:861 [in MetaCoq.Template.utils.All_Forall]
Q:862 [in MetaCoq.Translations.MiniHoTT_paths]
q:863 [in MetaCoq.Template.utils.wGraph]
q:866 [in MetaCoq.Translations.MiniHoTT_paths]
q:87 [in MetaCoq.Translations.MiniHoTT]
Q:872 [in MetaCoq.PCUIC.PCUICParallelReduction]
Q:872 [in MetaCoq.Translations.MiniHoTT]
q:876 [in MetaCoq.Translations.MiniHoTT]
Q:880 [in MetaCoq.Translations.MiniHoTT_paths]
Q:882 [in MetaCoq.PCUIC.TemplateToPCUICCorrectness]
Q:884 [in MetaCoq.PCUIC.PCUICParallelReduction]
q:884 [in MetaCoq.Translations.MiniHoTT]
q:884 [in MetaCoq.Translations.MiniHoTT_paths]
Q:89 [in MetaCoq.PCUIC.PCUICConfluence]
Q:891 [in MetaCoq.Translations.MiniHoTT]
q:892 [in MetaCoq.Translations.MiniHoTT_paths]
Q:896 [in MetaCoq.PCUIC.PCUICParallelReduction]
Q:899 [in MetaCoq.Translations.MiniHoTT_paths]
Q:9 [in MetaCoq.PCUIC.Bidirectional.BDStrengthening]
q:9 [in MetaCoq.Template.utils.MCPred]
Q:90 [in MetaCoq.PCUIC.PCUICSubstitution]
Q:90 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
Q:902 [in MetaCoq.Template.utils.All_Forall]
Q:912 [in MetaCoq.Template.utils.All_Forall]
Q:915 [in MetaCoq.PCUIC.PCUICParallelReduction]
Q:92 [in MetaCoq.PCUIC.PCUICParallelReduction]
Q:927 [in MetaCoq.PCUIC.PCUICParallelReduction]
q:934 [in MetaCoq.Translations.MiniHoTT]
Q:941 [in MetaCoq.PCUIC.PCUICConversion]
q:942 [in MetaCoq.Translations.MiniHoTT_paths]
Q:948 [in MetaCoq.PCUIC.PCUICParallelReduction]
Q:95 [in MetaCoq.SafeChecker.PCUICSafeReduce]
q:95 [in MetaCoq.Translations.MiniHoTT_paths]
q:950 [in MetaCoq.Translations.MiniHoTT]
q:958 [in MetaCoq.Translations.MiniHoTT_paths]
q:96 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
q:96 [in MetaCoq.PCUIC.PCUICExpandLetsCorrectness]
Q:962 [in MetaCoq.PCUIC.PCUICParallelReduction]
q:970 [in MetaCoq.Translations.MiniHoTT]
Q:973 [in MetaCoq.PCUIC.PCUICParallelReduction]
q:978 [in MetaCoq.Translations.MiniHoTT_paths]
Q:98 [in MetaCoq.PCUIC.PCUICConfluence]
Q:980 [in MetaCoq.Template.utils.All_Forall]
Q:99 [in MetaCoq.Erasure.EWcbvEvalEtaInd]
q:99 [in MetaCoq.PCUIC.utils.PCUICOnOne]
q:99 [in MetaCoq.PCUIC.Syntax.PCUICPosition]
| 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) |