/usr/share/doc/libaac-tactics-coq/theories/index.html is in libaac-tactics-coq 8.6.1-1.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595 596 597 598 599 600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 617 618 619 620 621 622 623 624 625 626 627 628 629 630 631 632 633 634 635 636 637 638 639 640 641 642 643 644 645 646 647 648 649 650 651 652 653 654 655 656 657 658 659 660 661 662 663 664 665 666 667 668 669 670 671 672 673 674 675 676 677 678 679 680 681 682 683 684 685 686 687 688 689 690 691 692 693 694 695 696 697 698 699 700 701 702 703 704 705 706 707 708 709 710 711 712 713 714 715 716 717 718 719 720 721 722 723 724 725 726 727 728 729 730 731 732 733 734 735 736 737 738 739 740 741 742 743 744 745 746 747 748 749 750 751 752 753 754 755 756 757 758 759 760 761 762 763 764 765 766 767 768 769 770 771 772 773 774 775 776 777 778 779 780 781 782 783 784 785 786 787 788 789 790 791 792 793 794 795 796 797 798 799 800 801 802 803 804 805 806 807 808 809 810 811 812 813 814 815 816 817 818 819 820 821 822 823 824 825 826 827 828 829 830 831 832 833 834 835 836 837 838 839 840 841 842 843 844 845 846 847 848 849 850 851 852 853 854 855 856 857 858 859 860 861 862 863 864 865 866 867 868 869 870 871 872 873 874 875 876 877 878 879 880 881 882 883 884 885 886 887 888 889 890 891 892 893 894 895 896 897 898 899 900 901 902 903 904 905 906 907 908 909 910 911 912 913 914 915 916 917 918 919 920 921 922 923 924 925 926 927 928 929 930 931 932 933 934 935 936 937 938 939 940 941 942 943 944 945 946 947 948 949 950 951 952 953 954 955 956 957 958 959 960 961 962 963 964 965 966 967 968 969 970 971 972 973 974 975 976 977 978 979 980 981 982 983 984 985 986 987 988 989 990 991 992 993 994 995 996 997 998 999 1000 1001 1002 1003 1004 1005 1006 1007 1008 1009 1010 1011 1012 1013 1014 1015 1016 1017 1018 1019 1020 1021 1022 1023 1024 1025 1026 1027 1028 1029 1030 1031 1032 1033 1034 1035 1036 1037 1038 1039 1040 1041 1042 1043 1044 1045 1046 1047 1048 1049 1050 1051 1052 1053 1054 1055 1056 1057 1058 1059 1060 1061 1062 1063 1064 1065 1066 1067 1068 1069 1070 1071 1072 1073 1074 1075 1076 1077 1078 1079 1080 1081 1082 1083 1084 1085 1086 1087 1088 1089 1090 1091 1092 1093 1094 1095 1096 1097 1098 1099 1100 1101 1102 1103 1104 1105 1106 1107 1108 1109 1110 1111 1112 1113 1114 1115 1116 1117 1118 1119 1120 1121 1122 1123 1124 1125 1126 1127 1128 1129 1130 1131 1132 1133 1134 1135 1136 1137 1138 1139 1140 1141 1142 1143 1144 1145 1146 1147 1148 1149 1150 1151 1152 1153 1154 1155 1156 1157 1158 1159 1160 1161 1162 1163 1164 1165 1166 1167 1168 1169 1170 1171 1172 1173 1174 1175 1176 1177 1178 1179 1180 1181 1182 1183 1184 1185 1186 1187 1188 1189 1190 1191 1192 1193 1194 1195 1196 1197 1198 1199 1200 1201 1202 1203 1204 1205 1206 1207 1208 1209 1210 1211 1212 1213 1214 1215 1216 1217 1218 1219 1220 1221 1222 1223 1224 1225 1226 1227 1228 1229 1230 1231 1232 1233 1234 1235 1236 1237 1238 1239 1240 1241 1242 1243 1244 1245 1246 1247 1248 1249 1250 1251 1252 1253 1254 1255 1256 1257 1258 1259 1260 1261 1262 1263 1264 1265 1266 1267 1268 1269 1270 1271 1272 1273 1274 1275 1276 1277 1278 1279 1280 1281 1282 1283 1284 1285 1286 1287 1288 1289 1290 1291 1292 1293 1294 1295 1296 1297 1298 1299 1300 1301 1302 1303 1304 1305 1306 1307 1308 1309 1310 1311 1312 1313 1314 1315 1316 1317 1318 1319 1320 1321 1322 1323 1324 1325 1326 1327 1328 1329 1330 1331 1332 1333 1334 1335 1336 1337 1338 1339 1340 1341 1342 1343 1344 1345 1346 1347 1348 1349 1350 1351 1352 1353 1354 1355 1356 1357 1358 1359 1360 1361 1362 1363 1364 1365 1366 1367 1368 1369 1370 1371 1372 1373 1374 1375 1376 1377 1378 1379 1380 1381 1382 1383 1384 1385 1386 1387 1388 1389 1390 1391 1392 1393 1394 1395 1396 1397 1398 1399 1400 1401 1402 1403 1404 1405 1406 1407 1408 1409 1410 1411 1412 1413 1414 1415 1416 1417 1418 1419 1420 1421 1422 1423 1424 1425 1426 1427 1428 1429 1430 1431 1432 1433 1434 1435 1436 1437 1438 1439 1440 1441 1442 1443 1444 1445 1446 1447 1448 1449 1450 1451 1452 1453 1454 1455 1456 1457 1458 1459 1460 1461 1462 1463 1464 1465 1466 1467 1468 1469 1470 1471 1472 1473 1474 1475 1476 1477 1478 1479 1480 1481 1482 1483 1484 1485 1486 1487 1488 1489 1490 1491 1492 1493 1494 1495 1496 1497 1498 1499 1500 1501 1502 1503 1504 1505 1506 1507 1508 1509 1510 1511 1512 1513 1514 1515 1516 1517 1518 1519 1520 1521 1522 1523 1524 1525 1526 1527 1528 1529 1530 1531 1532 1533 1534 1535 1536 1537 1538 1539 1540 1541 1542 1543 1544 1545 1546 1547 1548 1549 1550 1551 1552 1553 1554 1555 1556 1557 1558 1559 1560 1561 1562 1563 1564 1565 1566 1567 1568 1569 1570 1571 1572 1573 1574 1575 1576 1577 1578 1579 1580 1581 1582 1583 1584 1585 1586 1587 1588 1589 1590 1591 1592 1593 1594 1595 1596 1597 1598 1599 1600 1601 1602 1603 1604 1605 1606 1607 1608 1609 1610 1611 1612 1613 1614 1615 1616 1617 1618 1619 1620 1621 1622 1623 1624 1625 1626 1627 1628 1629 1630 1631 1632 1633 1634 1635 1636 1637 1638 1639 1640 1641 1642 1643 1644 1645 1646 1647 1648 1649 1650 1651 1652 1653 1654 1655 1656 1657 1658 1659 1660 1661 1662 1663 1664 1665 1666 1667 1668 1669 1670 1671 1672 1673 1674 1675 1676 1677 1678 1679 1680 1681 1682 1683 1684 1685 1686 1687 1688 1689 1690 1691 1692 1693 1694 1695 1696 1697 1698 1699 1700 1701 1702 1703 1704 1705 1706 1707 1708 1709 1710 1711 1712 1713 1714 1715 1716 1717 1718 1719 1720 1721 1722 1723 1724 1725 1726 1727 1728 1729 1730 1731 1732 1733 1734 1735 1736 1737 1738 1739 1740 1741 1742 1743 1744 1745 1746 1747 1748 1749 1750 1751 1752 1753 1754 1755 1756 1757 1758 1759 1760 1761 1762 1763 1764 1765 1766 1767 1768 1769 1770 1771 1772 1773 1774 1775 1776 1777 1778 1779 1780 1781 1782 1783 1784 1785 1786 1787 1788 1789 1790 1791 1792 1793 1794 1795 1796 1797 1798 1799 1800 1801 1802 1803 1804 1805 1806 1807 1808 1809 1810 1811 1812 1813 1814 1815 1816 1817 1818 1819 1820 1821 1822 1823 1824 1825 1826 1827 1828 1829 1830 1831 1832 1833 1834 1835 1836 1837 1838 1839 1840 1841 1842 1843 1844 1845 1846 1847 1848 1849 1850 1851 1852 1853 1854 1855 1856 1857 1858 1859 1860 1861 1862 1863 1864 1865 1866 1867 1868 1869 1870 1871 1872 1873 1874 1875 1876 1877 1878 1879 1880 1881 1882 1883 1884 1885 1886 1887 1888 1889 1890 1891 1892 1893 1894 1895 1896 1897 1898 1899 1900 1901 1902 1903 1904 1905 1906 1907 1908 1909 1910 1911 1912 1913 1914 1915 1916 1917 1918 1919 1920 1921 1922 1923 1924 1925 1926 1927 1928 1929 1930 1931 1932 1933 1934 1935 1936 1937 1938 1939 1940 1941 1942 1943 1944 1945 1946 1947 1948 1949 1950 1951 1952 1953 1954 1955 1956 1957 1958 1959 1960 1961 1962 1963 1964 1965 1966 1967 1968 1969 1970 1971 1972 1973 1974 1975 1976 1977 1978 1979 1980 1981 1982 1983 1984 1985 1986 1987 1988 1989 1990 1991 1992 1993 1994 1995 1996 1997 1998 1999 2000 2001 2002 2003 2004 2005 2006 2007 2008 2009 2010 2011 2012 2013 2014 2015 2016 2017 2018 2019 2020 2021 | <!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
<link href="coqdoc.css" rel="stylesheet" type="text/css" />
<title>Index</title>
</head>
<body>
<div id="page">
<div id="header">
</div>
<div id="main">
<table>
<tr>
<td>Global Index</td>
<td><a href="index.html#global_A">A</a></td>
<td><a href="index.html#global_B">B</a></td>
<td><a href="index.html#global_C">C</a></td>
<td>D</td>
<td><a href="index.html#global_E">E</a></td>
<td>F</td>
<td>G</td>
<td><a href="index.html#global_H">H</a></td>
<td><a href="index.html#global_I">I</a></td>
<td>J</td>
<td>K</td>
<td><a href="index.html#global_L">L</a></td>
<td><a href="index.html#global_M">M</a></td>
<td><a href="index.html#global_N">N</a></td>
<td>O</td>
<td><a href="index.html#global_P">P</a></td>
<td><a href="index.html#global_Q">Q</a></td>
<td><a href="index.html#global_R">R</a></td>
<td><a href="index.html#global_S">S</a></td>
<td><a href="index.html#global_T">T</a></td>
<td><a href="index.html#global_U">U</a></td>
<td><a href="index.html#global_V">V</a></td>
<td><a href="index.html#global_W">W</a></td>
<td>X</td>
<td>Y</td>
<td><a href="index.html#global_Z">Z</a></td>
<td>_</td>
<td>other</td>
<td>(489 entries)</td>
</tr>
<tr>
<td>Notation Index</td>
<td>A</td>
<td><a href="index.html#notation_B">B</a></td>
<td>C</td>
<td>D</td>
<td><a href="index.html#notation_E">E</a></td>
<td>F</td>
<td>G</td>
<td>H</td>
<td><a href="index.html#notation_I">I</a></td>
<td>J</td>
<td>K</td>
<td>L</td>
<td>M</td>
<td>N</td>
<td>O</td>
<td><a href="index.html#notation_P">P</a></td>
<td>Q</td>
<td>R</td>
<td>S</td>
<td>T</td>
<td><a href="index.html#notation_U">U</a></td>
<td><a href="index.html#notation_V">V</a></td>
<td>W</td>
<td>X</td>
<td>Y</td>
<td>Z</td>
<td>_</td>
<td>other</td>
<td>(19 entries)</td>
</tr>
<tr>
<td>Module Index</td>
<td><a href="index.html#module_A">A</a></td>
<td><a href="index.html#module_B">B</a></td>
<td>C</td>
<td>D</td>
<td>E</td>
<td>F</td>
<td>G</td>
<td>H</td>
<td><a href="index.html#module_I">I</a></td>
<td>J</td>
<td>K</td>
<td><a href="index.html#module_L">L</a></td>
<td>M</td>
<td><a href="index.html#module_N">N</a></td>
<td>O</td>
<td><a href="index.html#module_P">P</a></td>
<td><a href="index.html#module_Q">Q</a></td>
<td><a href="index.html#module_R">R</a></td>
<td>S</td>
<td>T</td>
<td>U</td>
<td>V</td>
<td>W</td>
<td>X</td>
<td>Y</td>
<td><a href="index.html#module_Z">Z</a></td>
<td>_</td>
<td>other</td>
<td>(13 entries)</td>
</tr>
<tr>
<td>Variable Index</td>
<td><a href="index.html#variable_A">A</a></td>
<td><a href="index.html#variable_B">B</a></td>
<td>C</td>
<td>D</td>
<td><a href="index.html#variable_E">E</a></td>
<td>F</td>
<td>G</td>
<td>H</td>
<td><a href="index.html#variable_I">I</a></td>
<td>J</td>
<td>K</td>
<td>L</td>
<td><a href="index.html#variable_M">M</a></td>
<td>N</td>
<td>O</td>
<td><a href="index.html#variable_P">P</a></td>
<td>Q</td>
<td><a href="index.html#variable_R">R</a></td>
<td>S</td>
<td>T</td>
<td><a href="index.html#variable_U">U</a></td>
<td>V</td>
<td><a href="index.html#variable_W">W</a></td>
<td>X</td>
<td>Y</td>
<td><a href="index.html#variable_Z">Z</a></td>
<td>_</td>
<td>other</td>
<td>(114 entries)</td>
</tr>
<tr>
<td>Library Index</td>
<td><a href="index.html#library_A">A</a></td>
<td>B</td>
<td><a href="index.html#library_C">C</a></td>
<td>D</td>
<td>E</td>
<td>F</td>
<td>G</td>
<td>H</td>
<td><a href="index.html#library_I">I</a></td>
<td>J</td>
<td>K</td>
<td>L</td>
<td>M</td>
<td>N</td>
<td>O</td>
<td>P</td>
<td>Q</td>
<td>R</td>
<td>S</td>
<td><a href="index.html#library_T">T</a></td>
<td>U</td>
<td>V</td>
<td>W</td>
<td>X</td>
<td>Y</td>
<td>Z</td>
<td>_</td>
<td>other</td>
<td>(4 entries)</td>
</tr>
<tr>
<td>Lemma Index</td>
<td>A</td>
<td>B</td>
<td>C</td>
<td>D</td>
<td><a href="index.html#lemma_E">E</a></td>
<td>F</td>
<td>G</td>
<td><a href="index.html#lemma_H">H</a></td>
<td><a href="index.html#lemma_I">I</a></td>
<td>J</td>
<td>K</td>
<td><a href="index.html#lemma_L">L</a></td>
<td>M</td>
<td>N</td>
<td>O</td>
<td>P</td>
<td>Q</td>
<td>R</td>
<td>S</td>
<td>T</td>
<td>U</td>
<td>V</td>
<td>W</td>
<td>X</td>
<td>Y</td>
<td><a href="index.html#lemma_Z">Z</a></td>
<td>_</td>
<td>other</td>
<td>(56 entries)</td>
</tr>
<tr>
<td>Constructor Index</td>
<td>A</td>
<td>B</td>
<td>C</td>
<td>D</td>
<td>E</td>
<td>F</td>
<td>G</td>
<td>H</td>
<td><a href="index.html#constructor_I">I</a></td>
<td>J</td>
<td>K</td>
<td><a href="index.html#constructor_L">L</a></td>
<td>M</td>
<td>N</td>
<td>O</td>
<td>P</td>
<td>Q</td>
<td>R</td>
<td>S</td>
<td>T</td>
<td>U</td>
<td>V</td>
<td>W</td>
<td>X</td>
<td>Y</td>
<td>Z</td>
<td>_</td>
<td>other</td>
<td>(34 entries)</td>
</tr>
<tr>
<td>Inductive Index</td>
<td><a href="index.html#inductive_A">A</a></td>
<td>B</td>
<td><a href="index.html#inductive_C">C</a></td>
<td>D</td>
<td>E</td>
<td>F</td>
<td>G</td>
<td>H</td>
<td><a href="index.html#inductive_I">I</a></td>
<td>J</td>
<td>K</td>
<td>L</td>
<td>M</td>
<td>N</td>
<td>O</td>
<td>P</td>
<td>Q</td>
<td>R</td>
<td>S</td>
<td>T</td>
<td>U</td>
<td>V</td>
<td>W</td>
<td>X</td>
<td>Y</td>
<td>Z</td>
<td>_</td>
<td>other</td>
<td>(13 entries)</td>
</tr>
<tr>
<td>Projection Index</td>
<td><a href="index.html#projection_A">A</a></td>
<td>B</td>
<td>C</td>
<td>D</td>
<td>E</td>
<td>F</td>
<td>G</td>
<td>H</td>
<td><a href="index.html#projection_I">I</a></td>
<td>J</td>
<td>K</td>
<td><a href="index.html#projection_L">L</a></td>
<td>M</td>
<td>N</td>
<td>O</td>
<td>P</td>
<td>Q</td>
<td>R</td>
<td>S</td>
<td>T</td>
<td>U</td>
<td>V</td>
<td>W</td>
<td>X</td>
<td>Y</td>
<td>Z</td>
<td>_</td>
<td>other</td>
<td>(17 entries)</td>
</tr>
<tr>
<td>Section Index</td>
<td><a href="index.html#section_A">A</a></td>
<td><a href="index.html#section_B">B</a></td>
<td>C</td>
<td>D</td>
<td><a href="index.html#section_E">E</a></td>
<td>F</td>
<td>G</td>
<td>H</td>
<td><a href="index.html#section_I">I</a></td>
<td>J</td>
<td>K</td>
<td>L</td>
<td><a href="index.html#section_M">M</a></td>
<td>N</td>
<td>O</td>
<td><a href="index.html#section_P">P</a></td>
<td>Q</td>
<td><a href="index.html#section_R">R</a></td>
<td><a href="index.html#section_S">S</a></td>
<td><a href="index.html#section_T">T</a></td>
<td><a href="index.html#section_U">U</a></td>
<td><a href="index.html#section_V">V</a></td>
<td><a href="index.html#section_W">W</a></td>
<td>X</td>
<td>Y</td>
<td><a href="index.html#section_Z">Z</a></td>
<td>_</td>
<td>other</td>
<td>(37 entries)</td>
</tr>
<tr>
<td>Instance Index</td>
<td><a href="index.html#instance_A">A</a></td>
<td><a href="index.html#instance_B">B</a></td>
<td>C</td>
<td>D</td>
<td>E</td>
<td>F</td>
<td>G</td>
<td>H</td>
<td><a href="index.html#instance_I">I</a></td>
<td>J</td>
<td>K</td>
<td><a href="index.html#instance_L">L</a></td>
<td>M</td>
<td><a href="index.html#instance_N">N</a></td>
<td>O</td>
<td><a href="index.html#instance_P">P</a></td>
<td><a href="index.html#instance_Q">Q</a></td>
<td><a href="index.html#instance_R">R</a></td>
<td>S</td>
<td>T</td>
<td>U</td>
<td>V</td>
<td>W</td>
<td>X</td>
<td>Y</td>
<td><a href="index.html#instance_Z">Z</a></td>
<td>_</td>
<td>other</td>
<td>(119 entries)</td>
</tr>
<tr>
<td>Abbreviation Index</td>
<td>A</td>
<td>B</td>
<td>C</td>
<td>D</td>
<td>E</td>
<td>F</td>
<td>G</td>
<td>H</td>
<td><a href="index.html#abbreviation_I">I</a></td>
<td>J</td>
<td>K</td>
<td>L</td>
<td>M</td>
<td>N</td>
<td>O</td>
<td>P</td>
<td>Q</td>
<td>R</td>
<td>S</td>
<td>T</td>
<td>U</td>
<td>V</td>
<td>W</td>
<td>X</td>
<td>Y</td>
<td>Z</td>
<td>_</td>
<td>other</td>
<td>(4 entries)</td>
</tr>
<tr>
<td>Definition Index</td>
<td>A</td>
<td>B</td>
<td>C</td>
<td>D</td>
<td>E</td>
<td>F</td>
<td>G</td>
<td>H</td>
<td><a href="index.html#definition_I">I</a></td>
<td>J</td>
<td>K</td>
<td>L</td>
<td>M</td>
<td>N</td>
<td>O</td>
<td>P</td>
<td>Q</td>
<td><a href="index.html#definition_R">R</a></td>
<td><a href="index.html#definition_S">S</a></td>
<td>T</td>
<td>U</td>
<td>V</td>
<td>W</td>
<td>X</td>
<td>Y</td>
<td>Z</td>
<td>_</td>
<td>other</td>
<td>(51 entries)</td>
</tr>
<tr>
<td>Record Index</td>
<td><a href="index.html#record_A">A</a></td>
<td>B</td>
<td><a href="index.html#record_C">C</a></td>
<td>D</td>
<td>E</td>
<td>F</td>
<td>G</td>
<td>H</td>
<td><a href="index.html#record_I">I</a></td>
<td>J</td>
<td>K</td>
<td>L</td>
<td>M</td>
<td>N</td>
<td>O</td>
<td>P</td>
<td>Q</td>
<td>R</td>
<td>S</td>
<td>T</td>
<td><a href="index.html#record_U">U</a></td>
<td>V</td>
<td>W</td>
<td>X</td>
<td>Y</td>
<td>Z</td>
<td>_</td>
<td>other</td>
<td>(8 entries)</td>
</tr>
</table>
<hr/>
<h1>Global Index</h1>
<a name="global_A"></a><h2>A </h2>
<a href="AAC_tactics.AAC.html">AAC</a> [library]<br/>
<a href="AAC_tactics.AAC.html#aac_lift_proper">aac_lift_proper</a> [instance, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#aac_lift_subrelation">aac_lift_subrelation</a> [instance, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#aac_list_proper">aac_list_proper</a> [projection, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#aac_lift_equivalence">aac_lift_equivalence</a> [projection, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#AAC_lift">AAC_lift</a> [record, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.Tutorial.html#AAC_normalise.d">AAC_normalise.d</a> [variable, in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#AAC_normalise.c">AAC_normalise.c</a> [variable, in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#AAC_normalise.b">AAC_normalise.b</a> [variable, in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#AAC_normalise.a">AAC_normalise.a</a> [variable, in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#AAC_normalise">AAC_normalise</a> [section, in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#aac_zero_max">aac_zero_max</a> [instance, in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#aac_max_Assoc">aac_max_Assoc</a> [instance, in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#aac_max_Comm">aac_max_Comm</a> [instance, in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#aac_zero_plus">aac_zero_plus</a> [instance, in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#aac_one">aac_one</a> [instance, in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#aac_plus_Comm">aac_plus_Comm</a> [instance, in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#aac_plus_Assoc">aac_plus_Assoc</a> [instance, in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Instances.html#All">All</a> [module, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.AAC.html#Associative">Associative</a> [record, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Associative">Associative</a> [inductive, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<br/><br/><a name="global_B"></a><h2>B </h2>
<a href="AAC_tactics.Tutorial.html#base">base</a> [section, in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#base.both">base.both</a> [section, in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#base.both.a">base.both.a</a> [variable, in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#base.both.b">base.both.b</a> [variable, in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#base.both.c">base.both.c</a> [variable, in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#base.both.d">base.both.d</a> [variable, in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#base.both.H">base.both.H</a> [variable, in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#base.both.H'">base.both.H'</a> [variable, in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#base.dealing_with_units.H'">base.dealing_with_units.H'</a> [variable, in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#base.dealing_with_units.H">base.dealing_with_units.H</a> [variable, in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#base.dealing_with_units.c">base.dealing_with_units.c</a> [variable, in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#base.dealing_with_units.b">base.dealing_with_units.b</a> [variable, in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#base.dealing_with_units.a">base.dealing_with_units.a</a> [variable, in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#base.dealing_with_units">base.dealing_with_units</a> [section, in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#base.morphisms">base.morphisms</a> [section, in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#base.morphisms.a">base.morphisms.a</a> [variable, in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#base.morphisms.b">base.morphisms.b</a> [variable, in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#base.morphisms.f">base.morphisms.f</a> [variable, in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#base.morphisms.g">base.morphisms.g</a> [variable, in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#base.morphisms.H">base.morphisms.H</a> [variable, in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#base.morphisms.Hf">base.morphisms.Hf</a> [variable, in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#base.morphisms.Hg">base.morphisms.Hg</a> [variable, in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#base.occurrence">base.occurrence</a> [section, in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#base.occurrence.a">base.occurrence.a</a> [variable, in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#base.occurrence.f">base.occurrence.f</a> [variable, in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#base.occurrence.H">base.occurrence.H</a> [variable, in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#base.occurrence.Hf">base.occurrence.Hf</a> [variable, in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#base.reminder">base.reminder</a> [section, in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#base.reminder.a">base.reminder.a</a> [variable, in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#base.reminder.b">base.reminder.b</a> [variable, in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#base.reminder.c">base.reminder.c</a> [variable, in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#base.reminder.H">base.reminder.H</a> [variable, in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#base.subst">base.subst</a> [section, in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#base.subst.a">base.subst.a</a> [variable, in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#base.subst.b">base.subst.b</a> [variable, in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#base.subst.c">base.subst.c</a> [variable, in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#base.subst.d">base.subst.d</a> [variable, in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#base.subst.H">base.subst.H</a> [variable, in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#base.subst.H'">base.subst.H'</a> [variable, in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#6936d2dd6d0e30561a0f976fbe32a01e">_ + _</a> [notation, in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#76a4d0ad39ecc64693ea30605872d57f">_ * _</a> [notation, in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#60260ee571313b69c0e257fb5861ad74">_ == _</a> [notation, in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#7724fe03f168a663a0649c3a61a8e05b">0</a> [notation, in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#4e1938e63b33842a33782f78d1cabb84">1</a> [notation, in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Instances.html#Bool">Bool</a> [module, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Bool.aac_false">Bool.aac_false</a> [instance, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Bool.aac_true">Bool.aac_true</a> [instance, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Bool.aac_andb_Comm">Bool.aac_andb_Comm</a> [instance, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Bool.aac_andb_Assoc">Bool.aac_andb_Assoc</a> [instance, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Bool.aac_orb_Comm">Bool.aac_orb_Comm</a> [instance, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Bool.aac_orb_Assoc">Bool.aac_orb_Assoc</a> [instance, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Bool.negb_compat">Bool.negb_compat</a> [instance, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<br/><br/><a name="global_C"></a><h2>C </h2>
<a href="AAC_tactics.Caveats.html">Caveats</a> [library]<br/>
<a href="AAC_tactics.AAC.html#Commutative">Commutative</a> [record, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Commutative">Commutative</a> [inductive, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<br/><br/><a name="global_E"></a><h2>E </h2>
<a href="AAC_tactics.Instances.html#eq_subr">eq_subr</a> [lemma, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Caveats.html#evars">evars</a> [section, in <a href="AAC_tactics.Caveats.html">AAC_tactics.Caveats</a>]<br/>
<a href="AAC_tactics.Caveats.html#evars.H">evars.H</a> [variable, in <a href="AAC_tactics.Caveats.html">AAC_tactics.Caveats</a>]<br/>
<a href="AAC_tactics.Caveats.html#evars.H'">evars.H'</a> [variable, in <a href="AAC_tactics.Caveats.html">AAC_tactics.Caveats</a>]<br/>
<a href="AAC_tactics.Caveats.html#evars.idem">evars.idem</a> [variable, in <a href="AAC_tactics.Caveats.html">AAC_tactics.Caveats</a>]<br/>
<a href="AAC_tactics.Caveats.html#evars.P">evars.P</a> [variable, in <a href="AAC_tactics.Caveats.html">AAC_tactics.Caveats</a>]<br/>
<a href="AAC_tactics.Tutorial.html#Examples">Examples</a> [section, in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#Examples.a">Examples.a</a> [variable, in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#Examples.b">Examples.b</a> [variable, in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#Examples.c">Examples.c</a> [variable, in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#Examples.H">Examples.H</a> [variable, in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#d8e3065e97aca589e2a80c1f162e57a3">_ ^2</a> [notation, in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#5b197bb7aed5bcbb129f3ddff1b1a700">2 â‹… _</a> [notation, in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<br/><br/><a name="global_H"></a><h2>H </h2>
<a href="AAC_tactics.Tutorial.html#Hbin1">Hbin1</a> [lemma, in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#Hbin2">Hbin2</a> [lemma, in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#Hopp">Hopp</a> [lemma, in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<br/><br/><a name="global_I"></a><h2>I </h2>
<a href="AAC_tactics.Caveats.html#ineq">ineq</a> [section, in <a href="AAC_tactics.Caveats.html">AAC_tactics.Caveats</a>]<br/>
<a href="AAC_tactics.Caveats.html#ineq.H">ineq.H</a> [variable, in <a href="AAC_tactics.Caveats.html">AAC_tactics.Caveats</a>]<br/>
<a href="AAC_tactics.Instances.html">Instances</a> [library]<br/>
<a href="AAC_tactics.AAC.html#Internal">Internal</a> [module, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.add_to_prd">Internal.add_to_prd</a> [definition, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.add_to_sum">Internal.add_to_sum</a> [definition, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.appne">Internal.appne</a> [definition, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.assoc">Internal.assoc</a> [instance, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.Bin">Internal.Bin</a> [module, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.Binvalue_Proper">Internal.Binvalue_Proper</a> [instance, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.Binvalue_Associative">Internal.Binvalue_Associative</a> [instance, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.Binvalue_Commutative">Internal.Binvalue_Commutative</a> [instance, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.Bin.assoc">Internal.Bin.assoc</a> [projection, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.Bin.comm">Internal.Bin.comm</a> [projection, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.Bin.compat">Internal.Bin.compat</a> [projection, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.Bin.mk_pack">Internal.Bin.mk_pack</a> [constructor, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.Bin.pack">Internal.Bin.pack</a> [record, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.Bin.t">Internal.Bin.t</a> [section, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.Bin.value">Internal.Bin.value</a> [projection, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.cast">Internal.cast</a> [abbreviation, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.cast_eq">Internal.cast_eq</a> [lemma, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.comp">Internal.comp</a> [definition, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.compare">Internal.compare</a> [definition, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.compare_reflect_eq">Internal.compare_reflect_eq</a> [lemma, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.compare_weak_spec">Internal.compare_weak_spec</a> [inductive, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.compat_prd_Unit">Internal.compat_prd_Unit</a> [instance, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.compat_prd_unit_add">Internal.compat_prd_unit_add</a> [lemma, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.compat_prd_unit_return">Internal.compat_prd_unit_return</a> [lemma, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.compat_prd_unit">Internal.compat_prd_unit</a> [inductive, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.compat_sum_unit_Unit">Internal.compat_sum_unit_Unit</a> [instance, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.compat_sum_unit_add">Internal.compat_sum_unit_add</a> [lemma, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.compat_sum_unit_return">Internal.compat_sum_unit_return</a> [lemma, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.compat_sum_unit">Internal.compat_sum_unit</a> [inductive, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.cons">Internal.cons</a> [constructor, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.copy">Internal.copy</a> [definition, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.copy">Internal.copy</a> [section, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.copy_n_unit">Internal.copy_n_unit</a> [lemma, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.copy_mset_copy">Internal.copy_mset_copy</a> [lemma, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.copy_mset_succ">Internal.copy_mset_succ</a> [lemma, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.copy_mset'">Internal.copy_mset'</a> [lemma, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.copy_mset">Internal.copy_mset</a> [definition, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.copy_compat">Internal.copy_compat</a> [instance, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.copy_Psucc">Internal.copy_Psucc</a> [lemma, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.copy_xH">Internal.copy_xH</a> [lemma, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.copy_plus">Internal.copy_plus</a> [lemma, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.copy'">Internal.copy'</a> [definition, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.cpu_right">Internal.cpu_right</a> [constructor, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.cpu_left">Internal.cpu_left</a> [constructor, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.csu_right">Internal.csu_right</a> [constructor, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.csu_left">Internal.csu_left</a> [constructor, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.decide">Internal.decide</a> [lemma, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.decide_false">Internal.decide_false</a> [constructor, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.decide_true">Internal.decide_true</a> [constructor, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.decide_spec">Internal.decide_spec</a> [inductive, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.dep">Internal.dep</a> [section, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.dep.f">Internal.dep.f</a> [variable, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.dep.T">Internal.dep.T</a> [variable, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.dep.U">Internal.dep.U</a> [variable, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.discr">Internal.discr</a> [inductive, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.eq_idx_spec">Internal.eq_idx_spec</a> [lemma, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.eq_idx_bool">Internal.eq_idx_bool</a> [definition, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.eval">Internal.eval</a> [definition, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.eval_norm_aux">Internal.eval_norm_aux</a> [lemma, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.eval_norm">Internal.eval_norm</a> [lemma, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.eval_norm_lists">Internal.eval_norm_lists</a> [lemma, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.eval_prd_app">Internal.eval_prd_app</a> [lemma, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.eval_prd_cons">Internal.eval_prd_cons</a> [lemma, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.eval_prd_nil">Internal.eval_prd_nil</a> [lemma, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.eval_norm_msets">Internal.eval_norm_msets</a> [lemma, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.eval_merge_bin">Internal.eval_merge_bin</a> [lemma, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.eval_sum_cons">Internal.eval_sum_cons</a> [lemma, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.eval_sum_nil">Internal.eval_sum_nil</a> [lemma, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.eval_aux_compat">Internal.eval_aux_compat</a> [instance, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.eval_aux">Internal.eval_aux</a> [definition, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.fold_map'">Internal.fold_map'</a> [definition, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.fold_map">Internal.fold_map</a> [definition, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.idx">Internal.idx</a> [abbreviation, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.idx_compare_reflect_eq">Internal.idx_compare_reflect_eq</a> [lemma, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.idx_compare">Internal.idx_compare</a> [definition, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.insert">Internal.insert</a> [definition, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.is_prd_spec">Internal.is_prd_spec</a> [lemma, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.is_prd_spec_nothing">Internal.is_prd_spec_nothing</a> [constructor, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.is_prd_spec_unit">Internal.is_prd_spec_unit</a> [constructor, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.is_prd_spec_op">Internal.is_prd_spec_op</a> [constructor, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.is_prd_spec_ind">Internal.is_prd_spec_ind</a> [inductive, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.is_sum_spec">Internal.is_sum_spec</a> [lemma, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.is_sum_spec_nothing">Internal.is_sum_spec_nothing</a> [constructor, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.is_sum_spec_unit">Internal.is_sum_spec_unit</a> [constructor, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.is_sum_spec_op">Internal.is_sum_spec_op</a> [constructor, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.is_sum_spec_ind">Internal.is_sum_spec_ind</a> [inductive, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.is_unit_of_Unit">Internal.is_unit_of_Unit</a> [lemma, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.is_prd">Internal.is_prd</a> [definition, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.is_sum">Internal.is_sum</a> [definition, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.Is_nothing">Internal.Is_nothing</a> [constructor, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.Is_unit">Internal.Is_unit</a> [constructor, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.Is_op">Internal.Is_op</a> [constructor, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.is_commutative">Internal.is_commutative</a> [definition, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.is_unit_of">Internal.is_unit_of</a> [definition, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.left">Internal.left</a> [constructor, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.lex">Internal.lex</a> [abbreviation, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.lift_normalise">Internal.lift_normalise</a> [lemma, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.lists">Internal.lists</a> [section, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.lists.c">Internal.lists.c</a> [section, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.lists.c.A">Internal.lists.c.A</a> [variable, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.lists.c.B">Internal.lists.c.B</a> [variable, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.lists.c.compare">Internal.lists.c.compare</a> [variable, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.lists.list_compare_weak_spec.Hcompare">Internal.lists.list_compare_weak_spec.Hcompare</a> [variable, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.lists.list_compare_weak_spec.compare">Internal.lists.list_compare_weak_spec.compare</a> [variable, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.lists.list_compare_weak_spec.A">Internal.lists.list_compare_weak_spec.A</a> [variable, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.lists.list_compare_weak_spec">Internal.lists.list_compare_weak_spec</a> [section, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.lists.m">Internal.lists.m</a> [section, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.lists.mset_compare_weak_spec.Hcompare">Internal.lists.mset_compare_weak_spec.Hcompare</a> [variable, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.lists.mset_compare_weak_spec.compare">Internal.lists.mset_compare_weak_spec.compare</a> [variable, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.lists.mset_compare_weak_spec.A">Internal.lists.mset_compare_weak_spec.A</a> [variable, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.lists.mset_compare_weak_spec">Internal.lists.mset_compare_weak_spec</a> [section, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.lists.m.A">Internal.lists.m.A</a> [variable, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.lists.m.B">Internal.lists.m.B</a> [variable, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.lists.m.bind">Internal.lists.m.bind</a> [variable, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.lists.m.b2">Internal.lists.m.b2</a> [variable, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.lists.m.compare">Internal.lists.m.compare</a> [variable, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.lists.m.map">Internal.lists.m.map</a> [variable, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.lists.m.merge">Internal.lists.m.merge</a> [variable, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.lists.m.ret">Internal.lists.m.ret</a> [variable, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.list_compare_weak_spec">Internal.list_compare_weak_spec</a> [lemma, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.list_compare">Internal.list_compare</a> [definition, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.m">Internal.m</a> [inductive, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.merge_map">Internal.merge_map</a> [definition, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.merge_msets">Internal.merge_msets</a> [definition, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.mk_unit_pack">Internal.mk_unit_pack</a> [constructor, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.mk_unit_for">Internal.mk_unit_for</a> [constructor, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.mset">Internal.mset</a> [definition, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.mset_compare_weak_spec">Internal.mset_compare_weak_spec</a> [lemma, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.mset_compare">Internal.mset_compare</a> [definition, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.nelist">Internal.nelist</a> [inductive, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.nelist_map">Internal.nelist_map</a> [definition, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.nil">Internal.nil</a> [constructor, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.norm">Internal.norm</a> [definition, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.normalise">Internal.normalise</a> [lemma, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.norm_msets">Internal.norm_msets</a> [definition, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.norm_lists">Internal.norm_lists</a> [definition, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.norm_lists_">Internal.norm_lists_</a> [definition, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.norm_msets_">Internal.norm_msets_</a> [definition, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.pcws_gt">Internal.pcws_gt</a> [constructor, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.pcws_lt">Internal.pcws_lt</a> [constructor, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.pcws_eq">Internal.pcws_eq</a> [constructor, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.pos_compare_weak_spec">Internal.pos_compare_weak_spec</a> [lemma, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.pos_compare">Internal.pos_compare</a> [abbreviation, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.prd">Internal.prd</a> [constructor, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.prd'">Internal.prd'</a> [definition, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.prd'_prd">Internal.prd'_prd</a> [lemma, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.proper">Internal.proper</a> [instance, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.reflect_eqdep_weak_spec">Internal.reflect_eqdep_weak_spec</a> [lemma, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.reflect_eqdep_eq">Internal.reflect_eqdep_eq</a> [lemma, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.reflect_eqdep">Internal.reflect_eqdep</a> [definition, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.return_prd">Internal.return_prd</a> [definition, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.return_sum">Internal.return_sum</a> [definition, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.right">Internal.right</a> [constructor, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.run_msets">Internal.run_msets</a> [definition, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.run_list">Internal.run_list</a> [definition, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.s">Internal.s</a> [section, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.sum">Internal.sum</a> [constructor, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.sum'">Internal.sum'</a> [definition, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.sum'_sum">Internal.sum'_sum</a> [lemma, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.sym">Internal.sym</a> [constructor, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.Sym">Internal.Sym</a> [module, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.Sym.ar">Internal.Sym.ar</a> [projection, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.Sym.mkPack">Internal.Sym.mkPack</a> [constructor, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.Sym.morph">Internal.Sym.morph</a> [projection, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.Sym.null">Internal.Sym.null</a> [definition, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.Sym.pack">Internal.Sym.pack</a> [record, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.Sym.rel_of">Internal.Sym.rel_of</a> [definition, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.Sym.t">Internal.Sym.t</a> [section, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.Sym.type_of">Internal.Sym.type_of</a> [definition, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.Sym.value">Internal.Sym.value</a> [projection, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.s.e_unit">Internal.s.e_unit</a> [variable, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.s.e_bin">Internal.s.e_bin</a> [variable, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.s.e_sym">Internal.s.e_sym</a> [variable, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.s.prds">Internal.s.prds</a> [section, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.s.prds.i">Internal.s.prds.i</a> [variable, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.s.prds.is_unit">Internal.s.prds.is_unit</a> [variable, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.s.prd_correctness.is_unit_prd_Unit">Internal.s.prd_correctness.is_unit_prd_Unit</a> [variable, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.s.prd_correctness.is_unit">Internal.s.prd_correctness.is_unit</a> [variable, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.s.prd_correctness.i">Internal.s.prd_correctness.i</a> [variable, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.s.prd_correctness">Internal.s.prd_correctness</a> [section, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.s.sums">Internal.s.sums</a> [section, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.s.sums.i">Internal.s.sums.i</a> [variable, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.s.sums.is_unit">Internal.s.sums.is_unit</a> [variable, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.s.sum_correctness.comm">Internal.s.sum_correctness.comm</a> [variable, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.s.sum_correctness.is_unit_sum_Unit">Internal.s.sum_correctness.is_unit_sum_Unit</a> [variable, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.s.sum_correctness.is_unit">Internal.s.sum_correctness.is_unit</a> [variable, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.s.sum_correctness.i">Internal.s.sum_correctness.i</a> [variable, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.s.sum_correctness">Internal.s.sum_correctness</a> [section, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#7d8b9d5dff6a6433dbfe2fdd0bd6ac14">_ == _</a> [notation, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.T">Internal.T</a> [inductive, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.tcompare_weak_spec">Internal.tcompare_weak_spec</a> [lemma, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.uf_desc">Internal.uf_desc</a> [projection, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.uf_idx">Internal.uf_idx</a> [projection, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.unit">Internal.unit</a> [constructor, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.unit_pack">Internal.unit_pack</a> [record, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.unit_of">Internal.unit_of</a> [record, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.u_desc">Internal.u_desc</a> [projection, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.u_value">Internal.u_value</a> [projection, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.vcompare">Internal.vcompare</a> [definition, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.vcompare_reflect_eqdep">Internal.vcompare_reflect_eqdep</a> [lemma, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.vcons">Internal.vcons</a> [constructor, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.vnil">Internal.vnil</a> [constructor, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.vnorm">Internal.vnorm</a> [definition, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.vT">Internal.vT</a> [inductive, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.z0">Internal.z0</a> [lemma, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.z0'">Internal.z0'</a> [lemma, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.z1">Internal.z1</a> [lemma, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.z1'">Internal.z1'</a> [lemma, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.z2">Internal.z2</a> [lemma, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.z2'">Internal.z2'</a> [lemma, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#6e6d66d837dfebb520818331d60b61a6">_ ++ _</a> [notation, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#5cf0b7da2659696e8f965ee9cf4229d1">_ :: _</a> [notation, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.Tutorial.html#introduction">introduction</a> [section, in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#introduction.a">introduction.a</a> [variable, in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#introduction.b">introduction.b</a> [variable, in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#introduction.c">introduction.c</a> [variable, in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#introduction.H">introduction.H</a> [variable, in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Caveats.html#inv_unique">inv_unique</a> [lemma, in <a href="AAC_tactics.Caveats.html">AAC_tactics.Caveats</a>]<br/>
<br/><br/><a name="global_L"></a><h2>L </h2>
<a href="AAC_tactics.AAC.html#law_neutral_right">law_neutral_right</a> [projection, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#law_neutral_left">law_neutral_left</a> [projection, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#law_comm">law_comm</a> [projection, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#law_comm">law_comm</a> [constructor, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#law_assoc">law_assoc</a> [projection, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#law_assoc">law_assoc</a> [constructor, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#lift_reflexivity">lift_reflexivity</a> [lemma, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#lift_transitivity_right">lift_transitivity_right</a> [lemma, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#lift_transitivity_left">lift_transitivity_left</a> [lemma, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.Tutorial.html#lift_le_eq">lift_le_eq</a> [instance, in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Instances.html#Lists">Lists</a> [module, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Lists.aac_append_Proper">Lists.aac_append_Proper</a> [instance, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Lists.aac_nil_append">Lists.aac_nil_append</a> [instance, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Lists.aac_append_Assoc">Lists.aac_append_Assoc</a> [instance, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<br/><br/><a name="global_M"></a><h2>M </h2>
<a href="AAC_tactics.Caveats.html#morphism">morphism</a> [section, in <a href="AAC_tactics.Caveats.html">AAC_tactics.Caveats</a>]<br/>
<a href="AAC_tactics.Caveats.html#morphism.H">morphism.H</a> [variable, in <a href="AAC_tactics.Caveats.html">AAC_tactics.Caveats</a>]<br/>
<br/><br/><a name="global_N"></a><h2>N </h2>
<a href="AAC_tactics.Instances.html#N">N</a> [module, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#N.aac_zero_max">N.aac_zero_max</a> [instance, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#N.aac_zero">N.aac_zero</a> [instance, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#N.aac_one">N.aac_one</a> [instance, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#N.aac_Nmax_Assoc">N.aac_Nmax_Assoc</a> [instance, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#N.aac_Nmax_Comm">N.aac_Nmax_Comm</a> [instance, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#N.aac_Nmin_Assoc">N.aac_Nmin_Assoc</a> [instance, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#N.aac_Nmin_Comm">N.aac_Nmin_Comm</a> [instance, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#N.aac_Nmult_Assoc">N.aac_Nmult_Assoc</a> [instance, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#N.aac_Nmult_Comm">N.aac_Nmult_Comm</a> [instance, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#N.aac_Nplus_Comm">N.aac_Nplus_Comm</a> [instance, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#N.aac_Nplus_Assoc">N.aac_Nplus_Assoc</a> [instance, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#N.lift_le_eq">N.lift_le_eq</a> [instance, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#N.preorder_le">N.preorder_le</a> [instance, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<br/><br/><a name="global_P"></a><h2>P </h2>
<a href="AAC_tactics.Instances.html#P">P</a> [module, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Caveats.html#parameters">parameters</a> [section, in <a href="AAC_tactics.Caveats.html">AAC_tactics.Caveats</a>]<br/>
<a href="AAC_tactics.Caveats.html#parameters.f">parameters.f</a> [variable, in <a href="AAC_tactics.Caveats.html">AAC_tactics.Caveats</a>]<br/>
<a href="AAC_tactics.Caveats.html#parameters.g">parameters.g</a> [variable, in <a href="AAC_tactics.Caveats.html">AAC_tactics.Caveats</a>]<br/>
<a href="AAC_tactics.Caveats.html#parameters.H">parameters.H</a> [variable, in <a href="AAC_tactics.Caveats.html">AAC_tactics.Caveats</a>]<br/>
<a href="AAC_tactics.Caveats.html#parameters.Hf">parameters.Hf</a> [variable, in <a href="AAC_tactics.Caveats.html">AAC_tactics.Caveats</a>]<br/>
<a href="AAC_tactics.Caveats.html#parameters.Hf'">parameters.Hf'</a> [variable, in <a href="AAC_tactics.Caveats.html">AAC_tactics.Caveats</a>]<br/>
<a href="AAC_tactics.Caveats.html#parameters.Hg">parameters.Hg</a> [variable, in <a href="AAC_tactics.Caveats.html">AAC_tactics.Caveats</a>]<br/>
<a href="AAC_tactics.Caveats.html#865aacb4bfbdfe7dcbba08b1f8d8679f">_ + _</a> [notation, in <a href="AAC_tactics.Caveats.html">AAC_tactics.Caveats</a>]<br/>
<a href="AAC_tactics.Caveats.html#953f619e9581ca1c8ce1e43486042bdc">_ == _</a> [notation, in <a href="AAC_tactics.Caveats.html">AAC_tactics.Caveats</a>]<br/>
<a href="AAC_tactics.Caveats.html#39582f26c5993dabfed0327fea4b50a7">0</a> [notation, in <a href="AAC_tactics.Caveats.html">AAC_tactics.Caveats</a>]<br/>
<a href="AAC_tactics.Tutorial.html#Peano">Peano</a> [section, in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Caveats.html#Peano">Peano</a> [section, in <a href="AAC_tactics.Caveats.html">AAC_tactics.Caveats</a>]<br/>
<a href="AAC_tactics.Instances.html#Peano">Peano</a> [module, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Tutorial.html#Peano.a">Peano.a</a> [variable, in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Instances.html#Peano.aac_zero_max">Peano.aac_zero_max</a> [instance, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Peano.aac_zero_plus">Peano.aac_zero_plus</a> [instance, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Peano.aac_one">Peano.aac_one</a> [instance, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Peano.aac_max_Assoc">Peano.aac_max_Assoc</a> [instance, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Peano.aac_max_Comm">Peano.aac_max_Comm</a> [instance, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Peano.aac_min_Assoc">Peano.aac_min_Assoc</a> [instance, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Peano.aac_min_Comm">Peano.aac_min_Comm</a> [instance, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Peano.aac_mult_Assoc">Peano.aac_mult_Assoc</a> [instance, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Peano.aac_mult_Comm">Peano.aac_mult_Comm</a> [instance, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Peano.aac_plus_Comm">Peano.aac_plus_Comm</a> [instance, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Peano.aac_plus_Assoc">Peano.aac_plus_Assoc</a> [instance, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Tutorial.html#Peano.b">Peano.b</a> [variable, in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#Peano.c">Peano.c</a> [variable, in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#Peano.H">Peano.H</a> [variable, in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Caveats.html#Peano.H">Peano.H</a> [variable, in <a href="AAC_tactics.Caveats.html">AAC_tactics.Caveats</a>]<br/>
<a href="AAC_tactics.Caveats.html#Peano.H'">Peano.H'</a> [variable, in <a href="AAC_tactics.Caveats.html">AAC_tactics.Caveats</a>]<br/>
<a href="AAC_tactics.Instances.html#Peano.lift_le_eq">Peano.lift_le_eq</a> [instance, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Peano.preorder_le">Peano.preorder_le</a> [instance, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Tutorial.html#Proper_Zplus">Proper_Zplus</a> [instance, in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Instances.html#Prop_ops.lift_impl_iff">Prop_ops.lift_impl_iff</a> [instance, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Prop_ops.aac_not_compat">Prop_ops.aac_not_compat</a> [instance, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Prop_ops.aac_False">Prop_ops.aac_False</a> [instance, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Prop_ops.aac_True">Prop_ops.aac_True</a> [instance, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Prop_ops.aac_and_Comm">Prop_ops.aac_and_Comm</a> [instance, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Prop_ops.aac_and_Assoc">Prop_ops.aac_and_Assoc</a> [instance, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Prop_ops.aac_or_Comm">Prop_ops.aac_or_Comm</a> [instance, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Prop_ops.aac_or_Assoc">Prop_ops.aac_or_Assoc</a> [instance, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Prop_ops">Prop_ops</a> [module, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#P.aac_one_max">P.aac_one_max</a> [instance, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#P.aac_one">P.aac_one</a> [instance, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#P.aac_Pmax_Assoc">P.aac_Pmax_Assoc</a> [instance, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#P.aac_Pmax_Comm">P.aac_Pmax_Comm</a> [instance, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#P.aac_Pmin_Assoc">P.aac_Pmin_Assoc</a> [instance, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#P.aac_Pmin_Comm">P.aac_Pmin_Comm</a> [instance, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#P.aac_Pmult_Assoc">P.aac_Pmult_Assoc</a> [instance, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#P.aac_Pmult_Comm">P.aac_Pmult_Comm</a> [instance, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#P.aac_Pplus_Comm">P.aac_Pplus_Comm</a> [instance, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#P.aac_Pplus_Assoc">P.aac_Pplus_Assoc</a> [instance, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#P.lift_le_eq">P.lift_le_eq</a> [instance, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#P.preorder_le">P.preorder_le</a> [instance, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<br/><br/><a name="global_Q"></a><h2>Q </h2>
<a href="AAC_tactics.Instances.html#Q">Q</a> [module, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Q.aac_zero_Qplus">Q.aac_zero_Qplus</a> [instance, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Q.aac_one">Q.aac_one</a> [instance, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Q.aac_Qmax_Assoc">Q.aac_Qmax_Assoc</a> [instance, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Q.aac_Qmax_Comm">Q.aac_Qmax_Comm</a> [instance, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Q.aac_Qmin_Assoc">Q.aac_Qmin_Assoc</a> [instance, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Q.aac_Qmin_Comm">Q.aac_Qmin_Comm</a> [instance, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Q.aac_Qmult_Assoc">Q.aac_Qmult_Assoc</a> [instance, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Q.aac_Qmult_Comm">Q.aac_Qmult_Comm</a> [instance, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Q.aac_Qplus_Comm">Q.aac_Qplus_Comm</a> [instance, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Q.aac_Qplus_Assoc">Q.aac_Qplus_Assoc</a> [instance, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Q.lift_le_eq">Q.lift_le_eq</a> [instance, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Q.preorder_le">Q.preorder_le</a> [instance, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<br/><br/><a name="global_R"></a><h2>R </h2>
<a href="AAC_tactics.Instances.html#Relations">Relations</a> [module, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Relations.aac_eq">Relations.aac_eq</a> [instance, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Relations.aac_compo">Relations.aac_compo</a> [instance, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Relations.aac_top">Relations.aac_top</a> [instance, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Relations.aac_inter_Assoc">Relations.aac_inter_Assoc</a> [instance, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Relations.aac_inter_Comm">Relations.aac_inter_Comm</a> [instance, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Relations.aac_bot">Relations.aac_bot</a> [instance, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Relations.aac_union_Assoc">Relations.aac_union_Assoc</a> [instance, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Relations.aac_union_Comm">Relations.aac_union_Comm</a> [instance, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Relations.bot">Relations.bot</a> [definition, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Relations.clos_refl_trans_compat">Relations.clos_refl_trans_compat</a> [instance, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Relations.clos_refl_trans_incr">Relations.clos_refl_trans_incr</a> [instance, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Relations.clos_trans_compat">Relations.clos_trans_compat</a> [instance, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Relations.clos_trans_incr">Relations.clos_trans_incr</a> [instance, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Relations.compo">Relations.compo</a> [definition, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Relations.defs">Relations.defs</a> [section, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Relations.defs.R">Relations.defs.R</a> [variable, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Relations.defs.S">Relations.defs.S</a> [variable, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Relations.defs.T">Relations.defs.T</a> [variable, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Relations.eq_same_relation">Relations.eq_same_relation</a> [instance, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Relations.inter">Relations.inter</a> [definition, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Relations.lift_inclusion_same_relation">Relations.lift_inclusion_same_relation</a> [instance, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Relations.negr">Relations.negr</a> [definition, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Relations.negr_compat">Relations.negr_compat</a> [instance, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Relations.preorder_inclusion">Relations.preorder_inclusion</a> [instance, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Relations.top">Relations.top</a> [definition, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Relations.transp_compat">Relations.transp_compat</a> [instance, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<br/><br/><a name="global_S"></a><h2>S </h2>
<a href="AAC_tactics.AAC.html#sigma">sigma</a> [definition, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#sigma">sigma</a> [section, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#sigma_empty">sigma_empty</a> [definition, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#sigma_add">sigma_add</a> [definition, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#sigma_get">sigma_get</a> [definition, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<br/><br/><a name="global_T"></a><h2>T </h2>
<a href="AAC_tactics.AAC.html#t">t</a> [section, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.Tutorial.html">Tutorial</a> [library]<br/>
<br/><br/><a name="global_U"></a><h2>U </h2>
<a href="AAC_tactics.Caveats.html#U">U</a> [section, in <a href="AAC_tactics.Caveats.html">AAC_tactics.Caveats</a>]<br/>
<a href="AAC_tactics.AAC.html#Unit">Unit</a> [record, in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.Caveats.html#U.dot_inv_right">U.dot_inv_right</a> [variable, in <a href="AAC_tactics.Caveats.html">AAC_tactics.Caveats</a>]<br/>
<a href="AAC_tactics.Caveats.html#U.dot_inv_left">U.dot_inv_left</a> [variable, in <a href="AAC_tactics.Caveats.html">AAC_tactics.Caveats</a>]<br/>
<a href="AAC_tactics.Caveats.html#U.f">U.f</a> [variable, in <a href="AAC_tactics.Caveats.html">AAC_tactics.Caveats</a>]<br/>
<a href="AAC_tactics.Caveats.html#U.Hf">U.Hf</a> [variable, in <a href="AAC_tactics.Caveats.html">AAC_tactics.Caveats</a>]<br/>
<a href="AAC_tactics.Caveats.html#773acc4c3d9ce1167eb4c82bc53d74df">_ * _</a> [notation, in <a href="AAC_tactics.Caveats.html">AAC_tactics.Caveats</a>]<br/>
<a href="AAC_tactics.Caveats.html#f4f3989510438ef582b0339145b66238">_ == _</a> [notation, in <a href="AAC_tactics.Caveats.html">AAC_tactics.Caveats</a>]<br/>
<a href="AAC_tactics.Caveats.html#86fd7335fe2a7b1ed5371ca992eb1769">1</a> [notation, in <a href="AAC_tactics.Caveats.html">AAC_tactics.Caveats</a>]<br/>
<br/><br/><a name="global_V"></a><h2>V </h2>
<a href="AAC_tactics.Caveats.html#V">V</a> [section, in <a href="AAC_tactics.Caveats.html">AAC_tactics.Caveats</a>]<br/>
<a href="AAC_tactics.Caveats.html#2c3c7894bbbf323625e13085e960b51f">_ * _</a> [notation, in <a href="AAC_tactics.Caveats.html">AAC_tactics.Caveats</a>]<br/>
<a href="AAC_tactics.Caveats.html#71becd7cd098316abac4e275992982c3">_ == _</a> [notation, in <a href="AAC_tactics.Caveats.html">AAC_tactics.Caveats</a>]<br/>
<a href="AAC_tactics.Caveats.html#abdd3b067b54e6edeb13fd863302ac19">1</a> [notation, in <a href="AAC_tactics.Caveats.html">AAC_tactics.Caveats</a>]<br/>
<br/><br/><a name="global_W"></a><h2>W </h2>
<a href="AAC_tactics.Caveats.html#W">W</a> [section, in <a href="AAC_tactics.Caveats.html">AAC_tactics.Caveats</a>]<br/>
<a href="AAC_tactics.Caveats.html#W.a">W.a</a> [variable, in <a href="AAC_tactics.Caveats.html">AAC_tactics.Caveats</a>]<br/>
<a href="AAC_tactics.Caveats.html#W.b">W.b</a> [variable, in <a href="AAC_tactics.Caveats.html">AAC_tactics.Caveats</a>]<br/>
<a href="AAC_tactics.Caveats.html#W.c">W.c</a> [variable, in <a href="AAC_tactics.Caveats.html">AAC_tactics.Caveats</a>]<br/>
<a href="AAC_tactics.Caveats.html#W.H">W.H</a> [variable, in <a href="AAC_tactics.Caveats.html">AAC_tactics.Caveats</a>]<br/>
<br/><br/><a name="global_Z"></a><h2>Z </h2>
<a href="AAC_tactics.Caveats.html#Z">Z</a> [section, in <a href="AAC_tactics.Caveats.html">AAC_tactics.Caveats</a>]<br/>
<a href="AAC_tactics.Instances.html#Z">Z</a> [module, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Tutorial.html#Zabs_triangle">Zabs_triangle</a> [lemma, in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#Zminus_compat">Zminus_compat</a> [instance, in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#Zplus_opp_r">Zplus_opp_r</a> [lemma, in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Caveats.html#Zplus_incr">Zplus_incr</a> [instance, in <a href="AAC_tactics.Caveats.html">AAC_tactics.Caveats</a>]<br/>
<a href="AAC_tactics.Caveats.html#Z.a">Z.a</a> [variable, in <a href="AAC_tactics.Caveats.html">AAC_tactics.Caveats</a>]<br/>
<a href="AAC_tactics.Instances.html#Z.aac_zero_Zplus">Z.aac_zero_Zplus</a> [instance, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Z.aac_one">Z.aac_one</a> [instance, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Z.aac_Zmax_Assoc">Z.aac_Zmax_Assoc</a> [instance, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Z.aac_Zmax_Comm">Z.aac_Zmax_Comm</a> [instance, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Z.aac_Zmin_Assoc">Z.aac_Zmin_Assoc</a> [instance, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Z.aac_Zmin_Comm">Z.aac_Zmin_Comm</a> [instance, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Z.aac_Zmult_Assoc">Z.aac_Zmult_Assoc</a> [instance, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Z.aac_Zmult_Comm">Z.aac_Zmult_Comm</a> [instance, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Z.aac_Zplus_Comm">Z.aac_Zplus_Comm</a> [instance, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Z.aac_Zplus_Assoc">Z.aac_Zplus_Assoc</a> [instance, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Caveats.html#Z.b">Z.b</a> [variable, in <a href="AAC_tactics.Caveats.html">AAC_tactics.Caveats</a>]<br/>
<a href="AAC_tactics.Caveats.html#Z.c">Z.c</a> [variable, in <a href="AAC_tactics.Caveats.html">AAC_tactics.Caveats</a>]<br/>
<a href="AAC_tactics.Caveats.html#Z.f">Z.f</a> [variable, in <a href="AAC_tactics.Caveats.html">AAC_tactics.Caveats</a>]<br/>
<a href="AAC_tactics.Caveats.html#Z.H">Z.H</a> [variable, in <a href="AAC_tactics.Caveats.html">AAC_tactics.Caveats</a>]<br/>
<a href="AAC_tactics.Caveats.html#Z.H0">Z.H0</a> [variable, in <a href="AAC_tactics.Caveats.html">AAC_tactics.Caveats</a>]<br/>
<a href="AAC_tactics.Caveats.html#Z.H1">Z.H1</a> [variable, in <a href="AAC_tactics.Caveats.html">AAC_tactics.Caveats</a>]<br/>
<a href="AAC_tactics.Instances.html#Z.lift_le_eq">Z.lift_le_eq</a> [instance, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Z.preorder_Zle">Z.preorder_Zle</a> [instance, in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<br/><br/><hr/>
<h1>Notation Index</h1>
<a name="notation_B"></a><h2>B </h2>
<a href="AAC_tactics.Tutorial.html#6936d2dd6d0e30561a0f976fbe32a01e">_ + _</a> [in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#76a4d0ad39ecc64693ea30605872d57f">_ * _</a> [in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#60260ee571313b69c0e257fb5861ad74">_ == _</a> [in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#7724fe03f168a663a0649c3a61a8e05b">0</a> [in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#4e1938e63b33842a33782f78d1cabb84">1</a> [in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<br/><br/><a name="notation_E"></a><h2>E </h2>
<a href="AAC_tactics.Tutorial.html#d8e3065e97aca589e2a80c1f162e57a3">_ ^2</a> [in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#5b197bb7aed5bcbb129f3ddff1b1a700">2 â‹… _</a> [in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<br/><br/><a name="notation_I"></a><h2>I </h2>
<a href="AAC_tactics.AAC.html#7d8b9d5dff6a6433dbfe2fdd0bd6ac14">_ == _</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#6e6d66d837dfebb520818331d60b61a6">_ ++ _</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#5cf0b7da2659696e8f965ee9cf4229d1">_ :: _</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<br/><br/><a name="notation_P"></a><h2>P </h2>
<a href="AAC_tactics.Caveats.html#865aacb4bfbdfe7dcbba08b1f8d8679f">_ + _</a> [in <a href="AAC_tactics.Caveats.html">AAC_tactics.Caveats</a>]<br/>
<a href="AAC_tactics.Caveats.html#953f619e9581ca1c8ce1e43486042bdc">_ == _</a> [in <a href="AAC_tactics.Caveats.html">AAC_tactics.Caveats</a>]<br/>
<a href="AAC_tactics.Caveats.html#39582f26c5993dabfed0327fea4b50a7">0</a> [in <a href="AAC_tactics.Caveats.html">AAC_tactics.Caveats</a>]<br/>
<br/><br/><a name="notation_U"></a><h2>U </h2>
<a href="AAC_tactics.Caveats.html#773acc4c3d9ce1167eb4c82bc53d74df">_ * _</a> [in <a href="AAC_tactics.Caveats.html">AAC_tactics.Caveats</a>]<br/>
<a href="AAC_tactics.Caveats.html#f4f3989510438ef582b0339145b66238">_ == _</a> [in <a href="AAC_tactics.Caveats.html">AAC_tactics.Caveats</a>]<br/>
<a href="AAC_tactics.Caveats.html#86fd7335fe2a7b1ed5371ca992eb1769">1</a> [in <a href="AAC_tactics.Caveats.html">AAC_tactics.Caveats</a>]<br/>
<br/><br/><a name="notation_V"></a><h2>V </h2>
<a href="AAC_tactics.Caveats.html#2c3c7894bbbf323625e13085e960b51f">_ * _</a> [in <a href="AAC_tactics.Caveats.html">AAC_tactics.Caveats</a>]<br/>
<a href="AAC_tactics.Caveats.html#71becd7cd098316abac4e275992982c3">_ == _</a> [in <a href="AAC_tactics.Caveats.html">AAC_tactics.Caveats</a>]<br/>
<a href="AAC_tactics.Caveats.html#abdd3b067b54e6edeb13fd863302ac19">1</a> [in <a href="AAC_tactics.Caveats.html">AAC_tactics.Caveats</a>]<br/>
<br/><br/><hr/>
<h1>Module Index</h1>
<a name="module_A"></a><h2>A </h2>
<a href="AAC_tactics.Instances.html#All">All</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<br/><br/><a name="module_B"></a><h2>B </h2>
<a href="AAC_tactics.Instances.html#Bool">Bool</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<br/><br/><a name="module_I"></a><h2>I </h2>
<a href="AAC_tactics.AAC.html#Internal">Internal</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.Bin">Internal.Bin</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.Sym">Internal.Sym</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<br/><br/><a name="module_L"></a><h2>L </h2>
<a href="AAC_tactics.Instances.html#Lists">Lists</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<br/><br/><a name="module_N"></a><h2>N </h2>
<a href="AAC_tactics.Instances.html#N">N</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<br/><br/><a name="module_P"></a><h2>P </h2>
<a href="AAC_tactics.Instances.html#P">P</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Peano">Peano</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Prop_ops">Prop_ops</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<br/><br/><a name="module_Q"></a><h2>Q </h2>
<a href="AAC_tactics.Instances.html#Q">Q</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<br/><br/><a name="module_R"></a><h2>R </h2>
<a href="AAC_tactics.Instances.html#Relations">Relations</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<br/><br/><a name="module_Z"></a><h2>Z </h2>
<a href="AAC_tactics.Instances.html#Z">Z</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<br/><br/><hr/>
<h1>Variable Index</h1>
<a name="variable_A"></a><h2>A </h2>
<a href="AAC_tactics.Tutorial.html#AAC_normalise.d">AAC_normalise.d</a> [in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#AAC_normalise.c">AAC_normalise.c</a> [in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#AAC_normalise.b">AAC_normalise.b</a> [in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#AAC_normalise.a">AAC_normalise.a</a> [in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<br/><br/><a name="variable_B"></a><h2>B </h2>
<a href="AAC_tactics.Tutorial.html#base.both.a">base.both.a</a> [in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#base.both.b">base.both.b</a> [in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#base.both.c">base.both.c</a> [in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#base.both.d">base.both.d</a> [in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#base.both.H">base.both.H</a> [in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#base.both.H'">base.both.H'</a> [in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#base.dealing_with_units.H'">base.dealing_with_units.H'</a> [in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#base.dealing_with_units.H">base.dealing_with_units.H</a> [in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#base.dealing_with_units.c">base.dealing_with_units.c</a> [in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#base.dealing_with_units.b">base.dealing_with_units.b</a> [in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#base.dealing_with_units.a">base.dealing_with_units.a</a> [in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#base.morphisms.a">base.morphisms.a</a> [in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#base.morphisms.b">base.morphisms.b</a> [in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#base.morphisms.f">base.morphisms.f</a> [in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#base.morphisms.g">base.morphisms.g</a> [in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#base.morphisms.H">base.morphisms.H</a> [in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#base.morphisms.Hf">base.morphisms.Hf</a> [in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#base.morphisms.Hg">base.morphisms.Hg</a> [in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#base.occurrence.a">base.occurrence.a</a> [in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#base.occurrence.f">base.occurrence.f</a> [in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#base.occurrence.H">base.occurrence.H</a> [in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#base.occurrence.Hf">base.occurrence.Hf</a> [in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#base.reminder.a">base.reminder.a</a> [in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#base.reminder.b">base.reminder.b</a> [in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#base.reminder.c">base.reminder.c</a> [in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#base.reminder.H">base.reminder.H</a> [in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#base.subst.a">base.subst.a</a> [in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#base.subst.b">base.subst.b</a> [in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#base.subst.c">base.subst.c</a> [in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#base.subst.d">base.subst.d</a> [in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#base.subst.H">base.subst.H</a> [in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#base.subst.H'">base.subst.H'</a> [in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<br/><br/><a name="variable_E"></a><h2>E </h2>
<a href="AAC_tactics.Caveats.html#evars.H">evars.H</a> [in <a href="AAC_tactics.Caveats.html">AAC_tactics.Caveats</a>]<br/>
<a href="AAC_tactics.Caveats.html#evars.H'">evars.H'</a> [in <a href="AAC_tactics.Caveats.html">AAC_tactics.Caveats</a>]<br/>
<a href="AAC_tactics.Caveats.html#evars.idem">evars.idem</a> [in <a href="AAC_tactics.Caveats.html">AAC_tactics.Caveats</a>]<br/>
<a href="AAC_tactics.Caveats.html#evars.P">evars.P</a> [in <a href="AAC_tactics.Caveats.html">AAC_tactics.Caveats</a>]<br/>
<a href="AAC_tactics.Tutorial.html#Examples.a">Examples.a</a> [in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#Examples.b">Examples.b</a> [in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#Examples.c">Examples.c</a> [in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#Examples.H">Examples.H</a> [in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<br/><br/><a name="variable_I"></a><h2>I </h2>
<a href="AAC_tactics.Caveats.html#ineq.H">ineq.H</a> [in <a href="AAC_tactics.Caveats.html">AAC_tactics.Caveats</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.dep.f">Internal.dep.f</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.dep.T">Internal.dep.T</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.dep.U">Internal.dep.U</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.lists.c.A">Internal.lists.c.A</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.lists.c.B">Internal.lists.c.B</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.lists.c.compare">Internal.lists.c.compare</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.lists.list_compare_weak_spec.Hcompare">Internal.lists.list_compare_weak_spec.Hcompare</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.lists.list_compare_weak_spec.compare">Internal.lists.list_compare_weak_spec.compare</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.lists.list_compare_weak_spec.A">Internal.lists.list_compare_weak_spec.A</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.lists.mset_compare_weak_spec.Hcompare">Internal.lists.mset_compare_weak_spec.Hcompare</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.lists.mset_compare_weak_spec.compare">Internal.lists.mset_compare_weak_spec.compare</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.lists.mset_compare_weak_spec.A">Internal.lists.mset_compare_weak_spec.A</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.lists.m.A">Internal.lists.m.A</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.lists.m.B">Internal.lists.m.B</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.lists.m.bind">Internal.lists.m.bind</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.lists.m.b2">Internal.lists.m.b2</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.lists.m.compare">Internal.lists.m.compare</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.lists.m.map">Internal.lists.m.map</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.lists.m.merge">Internal.lists.m.merge</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.lists.m.ret">Internal.lists.m.ret</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.s.e_unit">Internal.s.e_unit</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.s.e_bin">Internal.s.e_bin</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.s.e_sym">Internal.s.e_sym</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.s.prds.i">Internal.s.prds.i</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.s.prds.is_unit">Internal.s.prds.is_unit</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.s.prd_correctness.is_unit_prd_Unit">Internal.s.prd_correctness.is_unit_prd_Unit</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.s.prd_correctness.is_unit">Internal.s.prd_correctness.is_unit</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.s.prd_correctness.i">Internal.s.prd_correctness.i</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.s.sums.i">Internal.s.sums.i</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.s.sums.is_unit">Internal.s.sums.is_unit</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.s.sum_correctness.comm">Internal.s.sum_correctness.comm</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.s.sum_correctness.is_unit_sum_Unit">Internal.s.sum_correctness.is_unit_sum_Unit</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.s.sum_correctness.is_unit">Internal.s.sum_correctness.is_unit</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.s.sum_correctness.i">Internal.s.sum_correctness.i</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.Tutorial.html#introduction.a">introduction.a</a> [in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#introduction.b">introduction.b</a> [in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#introduction.c">introduction.c</a> [in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#introduction.H">introduction.H</a> [in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<br/><br/><a name="variable_M"></a><h2>M </h2>
<a href="AAC_tactics.Caveats.html#morphism.H">morphism.H</a> [in <a href="AAC_tactics.Caveats.html">AAC_tactics.Caveats</a>]<br/>
<br/><br/><a name="variable_P"></a><h2>P </h2>
<a href="AAC_tactics.Caveats.html#parameters.f">parameters.f</a> [in <a href="AAC_tactics.Caveats.html">AAC_tactics.Caveats</a>]<br/>
<a href="AAC_tactics.Caveats.html#parameters.g">parameters.g</a> [in <a href="AAC_tactics.Caveats.html">AAC_tactics.Caveats</a>]<br/>
<a href="AAC_tactics.Caveats.html#parameters.H">parameters.H</a> [in <a href="AAC_tactics.Caveats.html">AAC_tactics.Caveats</a>]<br/>
<a href="AAC_tactics.Caveats.html#parameters.Hf">parameters.Hf</a> [in <a href="AAC_tactics.Caveats.html">AAC_tactics.Caveats</a>]<br/>
<a href="AAC_tactics.Caveats.html#parameters.Hf'">parameters.Hf'</a> [in <a href="AAC_tactics.Caveats.html">AAC_tactics.Caveats</a>]<br/>
<a href="AAC_tactics.Caveats.html#parameters.Hg">parameters.Hg</a> [in <a href="AAC_tactics.Caveats.html">AAC_tactics.Caveats</a>]<br/>
<a href="AAC_tactics.Tutorial.html#Peano.a">Peano.a</a> [in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#Peano.b">Peano.b</a> [in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#Peano.c">Peano.c</a> [in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#Peano.H">Peano.H</a> [in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Caveats.html#Peano.H">Peano.H</a> [in <a href="AAC_tactics.Caveats.html">AAC_tactics.Caveats</a>]<br/>
<a href="AAC_tactics.Caveats.html#Peano.H'">Peano.H'</a> [in <a href="AAC_tactics.Caveats.html">AAC_tactics.Caveats</a>]<br/>
<br/><br/><a name="variable_R"></a><h2>R </h2>
<a href="AAC_tactics.Instances.html#Relations.defs.R">Relations.defs.R</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Relations.defs.S">Relations.defs.S</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Relations.defs.T">Relations.defs.T</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<br/><br/><a name="variable_U"></a><h2>U </h2>
<a href="AAC_tactics.Caveats.html#U.dot_inv_right">U.dot_inv_right</a> [in <a href="AAC_tactics.Caveats.html">AAC_tactics.Caveats</a>]<br/>
<a href="AAC_tactics.Caveats.html#U.dot_inv_left">U.dot_inv_left</a> [in <a href="AAC_tactics.Caveats.html">AAC_tactics.Caveats</a>]<br/>
<a href="AAC_tactics.Caveats.html#U.f">U.f</a> [in <a href="AAC_tactics.Caveats.html">AAC_tactics.Caveats</a>]<br/>
<a href="AAC_tactics.Caveats.html#U.Hf">U.Hf</a> [in <a href="AAC_tactics.Caveats.html">AAC_tactics.Caveats</a>]<br/>
<br/><br/><a name="variable_W"></a><h2>W </h2>
<a href="AAC_tactics.Caveats.html#W.a">W.a</a> [in <a href="AAC_tactics.Caveats.html">AAC_tactics.Caveats</a>]<br/>
<a href="AAC_tactics.Caveats.html#W.b">W.b</a> [in <a href="AAC_tactics.Caveats.html">AAC_tactics.Caveats</a>]<br/>
<a href="AAC_tactics.Caveats.html#W.c">W.c</a> [in <a href="AAC_tactics.Caveats.html">AAC_tactics.Caveats</a>]<br/>
<a href="AAC_tactics.Caveats.html#W.H">W.H</a> [in <a href="AAC_tactics.Caveats.html">AAC_tactics.Caveats</a>]<br/>
<br/><br/><a name="variable_Z"></a><h2>Z </h2>
<a href="AAC_tactics.Caveats.html#Z.a">Z.a</a> [in <a href="AAC_tactics.Caveats.html">AAC_tactics.Caveats</a>]<br/>
<a href="AAC_tactics.Caveats.html#Z.b">Z.b</a> [in <a href="AAC_tactics.Caveats.html">AAC_tactics.Caveats</a>]<br/>
<a href="AAC_tactics.Caveats.html#Z.c">Z.c</a> [in <a href="AAC_tactics.Caveats.html">AAC_tactics.Caveats</a>]<br/>
<a href="AAC_tactics.Caveats.html#Z.f">Z.f</a> [in <a href="AAC_tactics.Caveats.html">AAC_tactics.Caveats</a>]<br/>
<a href="AAC_tactics.Caveats.html#Z.H">Z.H</a> [in <a href="AAC_tactics.Caveats.html">AAC_tactics.Caveats</a>]<br/>
<a href="AAC_tactics.Caveats.html#Z.H0">Z.H0</a> [in <a href="AAC_tactics.Caveats.html">AAC_tactics.Caveats</a>]<br/>
<a href="AAC_tactics.Caveats.html#Z.H1">Z.H1</a> [in <a href="AAC_tactics.Caveats.html">AAC_tactics.Caveats</a>]<br/>
<br/><br/><hr/>
<h1>Library Index</h1>
<a name="library_A"></a><h2>A </h2>
<a href="AAC_tactics.AAC.html">AAC</a> <br/>
<br/><br/><a name="library_C"></a><h2>C </h2>
<a href="AAC_tactics.Caveats.html">Caveats</a> <br/>
<br/><br/><a name="library_I"></a><h2>I </h2>
<a href="AAC_tactics.Instances.html">Instances</a> <br/>
<br/><br/><a name="library_T"></a><h2>T </h2>
<a href="AAC_tactics.Tutorial.html">Tutorial</a> <br/>
<br/><br/><hr/>
<h1>Lemma Index</h1>
<a name="lemma_E"></a><h2>E </h2>
<a href="AAC_tactics.Instances.html#eq_subr">eq_subr</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<br/><br/><a name="lemma_H"></a><h2>H </h2>
<a href="AAC_tactics.Tutorial.html#Hbin1">Hbin1</a> [in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#Hbin2">Hbin2</a> [in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#Hopp">Hopp</a> [in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<br/><br/><a name="lemma_I"></a><h2>I </h2>
<a href="AAC_tactics.AAC.html#Internal.cast_eq">Internal.cast_eq</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.compare_reflect_eq">Internal.compare_reflect_eq</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.compat_prd_unit_add">Internal.compat_prd_unit_add</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.compat_prd_unit_return">Internal.compat_prd_unit_return</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.compat_sum_unit_add">Internal.compat_sum_unit_add</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.compat_sum_unit_return">Internal.compat_sum_unit_return</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.copy_n_unit">Internal.copy_n_unit</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.copy_mset_copy">Internal.copy_mset_copy</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.copy_mset_succ">Internal.copy_mset_succ</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.copy_mset'">Internal.copy_mset'</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.copy_Psucc">Internal.copy_Psucc</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.copy_xH">Internal.copy_xH</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.copy_plus">Internal.copy_plus</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.decide">Internal.decide</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.eq_idx_spec">Internal.eq_idx_spec</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.eval_norm_aux">Internal.eval_norm_aux</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.eval_norm">Internal.eval_norm</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.eval_norm_lists">Internal.eval_norm_lists</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.eval_prd_app">Internal.eval_prd_app</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.eval_prd_cons">Internal.eval_prd_cons</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.eval_prd_nil">Internal.eval_prd_nil</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.eval_norm_msets">Internal.eval_norm_msets</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.eval_merge_bin">Internal.eval_merge_bin</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.eval_sum_cons">Internal.eval_sum_cons</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.eval_sum_nil">Internal.eval_sum_nil</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.idx_compare_reflect_eq">Internal.idx_compare_reflect_eq</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.is_prd_spec">Internal.is_prd_spec</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.is_sum_spec">Internal.is_sum_spec</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.is_unit_of_Unit">Internal.is_unit_of_Unit</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.lift_normalise">Internal.lift_normalise</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.list_compare_weak_spec">Internal.list_compare_weak_spec</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.mset_compare_weak_spec">Internal.mset_compare_weak_spec</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.normalise">Internal.normalise</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.pos_compare_weak_spec">Internal.pos_compare_weak_spec</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.prd'_prd">Internal.prd'_prd</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.reflect_eqdep_weak_spec">Internal.reflect_eqdep_weak_spec</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.reflect_eqdep_eq">Internal.reflect_eqdep_eq</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.sum'_sum">Internal.sum'_sum</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.tcompare_weak_spec">Internal.tcompare_weak_spec</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.vcompare_reflect_eqdep">Internal.vcompare_reflect_eqdep</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.z0">Internal.z0</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.z0'">Internal.z0'</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.z1">Internal.z1</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.z1'">Internal.z1'</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.z2">Internal.z2</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.z2'">Internal.z2'</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.Caveats.html#inv_unique">inv_unique</a> [in <a href="AAC_tactics.Caveats.html">AAC_tactics.Caveats</a>]<br/>
<br/><br/><a name="lemma_L"></a><h2>L </h2>
<a href="AAC_tactics.AAC.html#lift_reflexivity">lift_reflexivity</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#lift_transitivity_right">lift_transitivity_right</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#lift_transitivity_left">lift_transitivity_left</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<br/><br/><a name="lemma_Z"></a><h2>Z </h2>
<a href="AAC_tactics.Tutorial.html#Zabs_triangle">Zabs_triangle</a> [in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#Zplus_opp_r">Zplus_opp_r</a> [in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<br/><br/><hr/>
<h1>Constructor Index</h1>
<a name="constructor_I"></a><h2>I </h2>
<a href="AAC_tactics.AAC.html#Internal.Bin.mk_pack">Internal.Bin.mk_pack</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.cons">Internal.cons</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.cpu_right">Internal.cpu_right</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.cpu_left">Internal.cpu_left</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.csu_right">Internal.csu_right</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.csu_left">Internal.csu_left</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.decide_false">Internal.decide_false</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.decide_true">Internal.decide_true</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.is_prd_spec_nothing">Internal.is_prd_spec_nothing</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.is_prd_spec_unit">Internal.is_prd_spec_unit</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.is_prd_spec_op">Internal.is_prd_spec_op</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.is_sum_spec_nothing">Internal.is_sum_spec_nothing</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.is_sum_spec_unit">Internal.is_sum_spec_unit</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.is_sum_spec_op">Internal.is_sum_spec_op</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.Is_nothing">Internal.Is_nothing</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.Is_unit">Internal.Is_unit</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.Is_op">Internal.Is_op</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.left">Internal.left</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.mk_unit_pack">Internal.mk_unit_pack</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.mk_unit_for">Internal.mk_unit_for</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.nil">Internal.nil</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.pcws_gt">Internal.pcws_gt</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.pcws_lt">Internal.pcws_lt</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.pcws_eq">Internal.pcws_eq</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.prd">Internal.prd</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.right">Internal.right</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.sum">Internal.sum</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.sym">Internal.sym</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.Sym.mkPack">Internal.Sym.mkPack</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.unit">Internal.unit</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.vcons">Internal.vcons</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.vnil">Internal.vnil</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<br/><br/><a name="constructor_L"></a><h2>L </h2>
<a href="AAC_tactics.AAC.html#law_comm">law_comm</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#law_assoc">law_assoc</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<br/><br/><hr/>
<h1>Inductive Index</h1>
<a name="inductive_A"></a><h2>A </h2>
<a href="AAC_tactics.AAC.html#Associative">Associative</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<br/><br/><a name="inductive_C"></a><h2>C </h2>
<a href="AAC_tactics.AAC.html#Commutative">Commutative</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<br/><br/><a name="inductive_I"></a><h2>I </h2>
<a href="AAC_tactics.AAC.html#Internal.compare_weak_spec">Internal.compare_weak_spec</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.compat_prd_unit">Internal.compat_prd_unit</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.compat_sum_unit">Internal.compat_sum_unit</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.decide_spec">Internal.decide_spec</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.discr">Internal.discr</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.is_prd_spec_ind">Internal.is_prd_spec_ind</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.is_sum_spec_ind">Internal.is_sum_spec_ind</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.m">Internal.m</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.nelist">Internal.nelist</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.T">Internal.T</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.vT">Internal.vT</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<br/><br/><hr/>
<h1>Projection Index</h1>
<a name="projection_A"></a><h2>A </h2>
<a href="AAC_tactics.AAC.html#aac_list_proper">aac_list_proper</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#aac_lift_equivalence">aac_lift_equivalence</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<br/><br/><a name="projection_I"></a><h2>I </h2>
<a href="AAC_tactics.AAC.html#Internal.Bin.assoc">Internal.Bin.assoc</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.Bin.comm">Internal.Bin.comm</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.Bin.compat">Internal.Bin.compat</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.Bin.value">Internal.Bin.value</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.Sym.ar">Internal.Sym.ar</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.Sym.morph">Internal.Sym.morph</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.Sym.value">Internal.Sym.value</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.uf_desc">Internal.uf_desc</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.uf_idx">Internal.uf_idx</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.u_desc">Internal.u_desc</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.u_value">Internal.u_value</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<br/><br/><a name="projection_L"></a><h2>L </h2>
<a href="AAC_tactics.AAC.html#law_neutral_right">law_neutral_right</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#law_neutral_left">law_neutral_left</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#law_comm">law_comm</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#law_assoc">law_assoc</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<br/><br/><hr/>
<h1>Section Index</h1>
<a name="section_A"></a><h2>A </h2>
<a href="AAC_tactics.Tutorial.html#AAC_normalise">AAC_normalise</a> [in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<br/><br/><a name="section_B"></a><h2>B </h2>
<a href="AAC_tactics.Tutorial.html#base">base</a> [in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#base.both">base.both</a> [in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#base.dealing_with_units">base.dealing_with_units</a> [in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#base.morphisms">base.morphisms</a> [in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#base.occurrence">base.occurrence</a> [in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#base.reminder">base.reminder</a> [in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#base.subst">base.subst</a> [in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<br/><br/><a name="section_E"></a><h2>E </h2>
<a href="AAC_tactics.Caveats.html#evars">evars</a> [in <a href="AAC_tactics.Caveats.html">AAC_tactics.Caveats</a>]<br/>
<a href="AAC_tactics.Tutorial.html#Examples">Examples</a> [in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<br/><br/><a name="section_I"></a><h2>I </h2>
<a href="AAC_tactics.Caveats.html#ineq">ineq</a> [in <a href="AAC_tactics.Caveats.html">AAC_tactics.Caveats</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.Bin.t">Internal.Bin.t</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.copy">Internal.copy</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.dep">Internal.dep</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.lists">Internal.lists</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.lists.c">Internal.lists.c</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.lists.list_compare_weak_spec">Internal.lists.list_compare_weak_spec</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.lists.m">Internal.lists.m</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.lists.mset_compare_weak_spec">Internal.lists.mset_compare_weak_spec</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.s">Internal.s</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.Sym.t">Internal.Sym.t</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.s.prds">Internal.s.prds</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.s.prd_correctness">Internal.s.prd_correctness</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.s.sums">Internal.s.sums</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.s.sum_correctness">Internal.s.sum_correctness</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.Tutorial.html#introduction">introduction</a> [in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<br/><br/><a name="section_M"></a><h2>M </h2>
<a href="AAC_tactics.Caveats.html#morphism">morphism</a> [in <a href="AAC_tactics.Caveats.html">AAC_tactics.Caveats</a>]<br/>
<br/><br/><a name="section_P"></a><h2>P </h2>
<a href="AAC_tactics.Caveats.html#parameters">parameters</a> [in <a href="AAC_tactics.Caveats.html">AAC_tactics.Caveats</a>]<br/>
<a href="AAC_tactics.Tutorial.html#Peano">Peano</a> [in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Caveats.html#Peano">Peano</a> [in <a href="AAC_tactics.Caveats.html">AAC_tactics.Caveats</a>]<br/>
<br/><br/><a name="section_R"></a><h2>R </h2>
<a href="AAC_tactics.Instances.html#Relations.defs">Relations.defs</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<br/><br/><a name="section_S"></a><h2>S </h2>
<a href="AAC_tactics.AAC.html#sigma">sigma</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<br/><br/><a name="section_T"></a><h2>T </h2>
<a href="AAC_tactics.AAC.html#t">t</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<br/><br/><a name="section_U"></a><h2>U </h2>
<a href="AAC_tactics.Caveats.html#U">U</a> [in <a href="AAC_tactics.Caveats.html">AAC_tactics.Caveats</a>]<br/>
<br/><br/><a name="section_V"></a><h2>V </h2>
<a href="AAC_tactics.Caveats.html#V">V</a> [in <a href="AAC_tactics.Caveats.html">AAC_tactics.Caveats</a>]<br/>
<br/><br/><a name="section_W"></a><h2>W </h2>
<a href="AAC_tactics.Caveats.html#W">W</a> [in <a href="AAC_tactics.Caveats.html">AAC_tactics.Caveats</a>]<br/>
<br/><br/><a name="section_Z"></a><h2>Z </h2>
<a href="AAC_tactics.Caveats.html#Z">Z</a> [in <a href="AAC_tactics.Caveats.html">AAC_tactics.Caveats</a>]<br/>
<br/><br/><hr/>
<h1>Instance Index</h1>
<a name="instance_A"></a><h2>A </h2>
<a href="AAC_tactics.AAC.html#aac_lift_proper">aac_lift_proper</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#aac_lift_subrelation">aac_lift_subrelation</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.Tutorial.html#aac_zero_max">aac_zero_max</a> [in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#aac_max_Assoc">aac_max_Assoc</a> [in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#aac_max_Comm">aac_max_Comm</a> [in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#aac_zero_plus">aac_zero_plus</a> [in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#aac_one">aac_one</a> [in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#aac_plus_Comm">aac_plus_Comm</a> [in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Tutorial.html#aac_plus_Assoc">aac_plus_Assoc</a> [in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<br/><br/><a name="instance_B"></a><h2>B </h2>
<a href="AAC_tactics.Instances.html#Bool.aac_false">Bool.aac_false</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Bool.aac_true">Bool.aac_true</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Bool.aac_andb_Comm">Bool.aac_andb_Comm</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Bool.aac_andb_Assoc">Bool.aac_andb_Assoc</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Bool.aac_orb_Comm">Bool.aac_orb_Comm</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Bool.aac_orb_Assoc">Bool.aac_orb_Assoc</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Bool.negb_compat">Bool.negb_compat</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<br/><br/><a name="instance_I"></a><h2>I </h2>
<a href="AAC_tactics.AAC.html#Internal.assoc">Internal.assoc</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.Binvalue_Proper">Internal.Binvalue_Proper</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.Binvalue_Associative">Internal.Binvalue_Associative</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.Binvalue_Commutative">Internal.Binvalue_Commutative</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.compat_prd_Unit">Internal.compat_prd_Unit</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.compat_sum_unit_Unit">Internal.compat_sum_unit_Unit</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.copy_compat">Internal.copy_compat</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.eval_aux_compat">Internal.eval_aux_compat</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.proper">Internal.proper</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<br/><br/><a name="instance_L"></a><h2>L </h2>
<a href="AAC_tactics.Tutorial.html#lift_le_eq">lift_le_eq</a> [in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Instances.html#Lists.aac_append_Proper">Lists.aac_append_Proper</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Lists.aac_nil_append">Lists.aac_nil_append</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Lists.aac_append_Assoc">Lists.aac_append_Assoc</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<br/><br/><a name="instance_N"></a><h2>N </h2>
<a href="AAC_tactics.Instances.html#N.aac_zero_max">N.aac_zero_max</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#N.aac_zero">N.aac_zero</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#N.aac_one">N.aac_one</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#N.aac_Nmax_Assoc">N.aac_Nmax_Assoc</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#N.aac_Nmax_Comm">N.aac_Nmax_Comm</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#N.aac_Nmin_Assoc">N.aac_Nmin_Assoc</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#N.aac_Nmin_Comm">N.aac_Nmin_Comm</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#N.aac_Nmult_Assoc">N.aac_Nmult_Assoc</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#N.aac_Nmult_Comm">N.aac_Nmult_Comm</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#N.aac_Nplus_Comm">N.aac_Nplus_Comm</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#N.aac_Nplus_Assoc">N.aac_Nplus_Assoc</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#N.lift_le_eq">N.lift_le_eq</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#N.preorder_le">N.preorder_le</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<br/><br/><a name="instance_P"></a><h2>P </h2>
<a href="AAC_tactics.Instances.html#Peano.aac_zero_max">Peano.aac_zero_max</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Peano.aac_zero_plus">Peano.aac_zero_plus</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Peano.aac_one">Peano.aac_one</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Peano.aac_max_Assoc">Peano.aac_max_Assoc</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Peano.aac_max_Comm">Peano.aac_max_Comm</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Peano.aac_min_Assoc">Peano.aac_min_Assoc</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Peano.aac_min_Comm">Peano.aac_min_Comm</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Peano.aac_mult_Assoc">Peano.aac_mult_Assoc</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Peano.aac_mult_Comm">Peano.aac_mult_Comm</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Peano.aac_plus_Comm">Peano.aac_plus_Comm</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Peano.aac_plus_Assoc">Peano.aac_plus_Assoc</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Peano.lift_le_eq">Peano.lift_le_eq</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Peano.preorder_le">Peano.preorder_le</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Tutorial.html#Proper_Zplus">Proper_Zplus</a> [in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Instances.html#Prop_ops.lift_impl_iff">Prop_ops.lift_impl_iff</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Prop_ops.aac_not_compat">Prop_ops.aac_not_compat</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Prop_ops.aac_False">Prop_ops.aac_False</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Prop_ops.aac_True">Prop_ops.aac_True</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Prop_ops.aac_and_Comm">Prop_ops.aac_and_Comm</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Prop_ops.aac_and_Assoc">Prop_ops.aac_and_Assoc</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Prop_ops.aac_or_Comm">Prop_ops.aac_or_Comm</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Prop_ops.aac_or_Assoc">Prop_ops.aac_or_Assoc</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#P.aac_one_max">P.aac_one_max</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#P.aac_one">P.aac_one</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#P.aac_Pmax_Assoc">P.aac_Pmax_Assoc</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#P.aac_Pmax_Comm">P.aac_Pmax_Comm</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#P.aac_Pmin_Assoc">P.aac_Pmin_Assoc</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#P.aac_Pmin_Comm">P.aac_Pmin_Comm</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#P.aac_Pmult_Assoc">P.aac_Pmult_Assoc</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#P.aac_Pmult_Comm">P.aac_Pmult_Comm</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#P.aac_Pplus_Comm">P.aac_Pplus_Comm</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#P.aac_Pplus_Assoc">P.aac_Pplus_Assoc</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#P.lift_le_eq">P.lift_le_eq</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#P.preorder_le">P.preorder_le</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<br/><br/><a name="instance_Q"></a><h2>Q </h2>
<a href="AAC_tactics.Instances.html#Q.aac_zero_Qplus">Q.aac_zero_Qplus</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Q.aac_one">Q.aac_one</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Q.aac_Qmax_Assoc">Q.aac_Qmax_Assoc</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Q.aac_Qmax_Comm">Q.aac_Qmax_Comm</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Q.aac_Qmin_Assoc">Q.aac_Qmin_Assoc</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Q.aac_Qmin_Comm">Q.aac_Qmin_Comm</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Q.aac_Qmult_Assoc">Q.aac_Qmult_Assoc</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Q.aac_Qmult_Comm">Q.aac_Qmult_Comm</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Q.aac_Qplus_Comm">Q.aac_Qplus_Comm</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Q.aac_Qplus_Assoc">Q.aac_Qplus_Assoc</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Q.lift_le_eq">Q.lift_le_eq</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Q.preorder_le">Q.preorder_le</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<br/><br/><a name="instance_R"></a><h2>R </h2>
<a href="AAC_tactics.Instances.html#Relations.aac_eq">Relations.aac_eq</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Relations.aac_compo">Relations.aac_compo</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Relations.aac_top">Relations.aac_top</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Relations.aac_inter_Assoc">Relations.aac_inter_Assoc</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Relations.aac_inter_Comm">Relations.aac_inter_Comm</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Relations.aac_bot">Relations.aac_bot</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Relations.aac_union_Assoc">Relations.aac_union_Assoc</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Relations.aac_union_Comm">Relations.aac_union_Comm</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Relations.clos_refl_trans_compat">Relations.clos_refl_trans_compat</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Relations.clos_refl_trans_incr">Relations.clos_refl_trans_incr</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Relations.clos_trans_compat">Relations.clos_trans_compat</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Relations.clos_trans_incr">Relations.clos_trans_incr</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Relations.eq_same_relation">Relations.eq_same_relation</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Relations.lift_inclusion_same_relation">Relations.lift_inclusion_same_relation</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Relations.negr_compat">Relations.negr_compat</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Relations.preorder_inclusion">Relations.preorder_inclusion</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Relations.transp_compat">Relations.transp_compat</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<br/><br/><a name="instance_Z"></a><h2>Z </h2>
<a href="AAC_tactics.Tutorial.html#Zminus_compat">Zminus_compat</a> [in <a href="AAC_tactics.Tutorial.html">AAC_tactics.Tutorial</a>]<br/>
<a href="AAC_tactics.Caveats.html#Zplus_incr">Zplus_incr</a> [in <a href="AAC_tactics.Caveats.html">AAC_tactics.Caveats</a>]<br/>
<a href="AAC_tactics.Instances.html#Z.aac_zero_Zplus">Z.aac_zero_Zplus</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Z.aac_one">Z.aac_one</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Z.aac_Zmax_Assoc">Z.aac_Zmax_Assoc</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Z.aac_Zmax_Comm">Z.aac_Zmax_Comm</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Z.aac_Zmin_Assoc">Z.aac_Zmin_Assoc</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Z.aac_Zmin_Comm">Z.aac_Zmin_Comm</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Z.aac_Zmult_Assoc">Z.aac_Zmult_Assoc</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Z.aac_Zmult_Comm">Z.aac_Zmult_Comm</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Z.aac_Zplus_Comm">Z.aac_Zplus_Comm</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Z.aac_Zplus_Assoc">Z.aac_Zplus_Assoc</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Z.lift_le_eq">Z.lift_le_eq</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Z.preorder_Zle">Z.preorder_Zle</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<br/><br/><hr/>
<h1>Abbreviation Index</h1>
<a name="abbreviation_I"></a><h2>I </h2>
<a href="AAC_tactics.AAC.html#Internal.cast">Internal.cast</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.idx">Internal.idx</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.lex">Internal.lex</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.pos_compare">Internal.pos_compare</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<br/><br/><hr/>
<h1>Definition Index</h1>
<a name="definition_I"></a><h2>I </h2>
<a href="AAC_tactics.AAC.html#Internal.add_to_prd">Internal.add_to_prd</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.add_to_sum">Internal.add_to_sum</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.appne">Internal.appne</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.comp">Internal.comp</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.compare">Internal.compare</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.copy">Internal.copy</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.copy_mset">Internal.copy_mset</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.copy'">Internal.copy'</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.eq_idx_bool">Internal.eq_idx_bool</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.eval">Internal.eval</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.eval_aux">Internal.eval_aux</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.fold_map'">Internal.fold_map'</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.fold_map">Internal.fold_map</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.idx_compare">Internal.idx_compare</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.insert">Internal.insert</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.is_prd">Internal.is_prd</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.is_sum">Internal.is_sum</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.is_commutative">Internal.is_commutative</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.is_unit_of">Internal.is_unit_of</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.list_compare">Internal.list_compare</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.merge_map">Internal.merge_map</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.merge_msets">Internal.merge_msets</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.mset">Internal.mset</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.mset_compare">Internal.mset_compare</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.nelist_map">Internal.nelist_map</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.norm">Internal.norm</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.norm_msets">Internal.norm_msets</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.norm_lists">Internal.norm_lists</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.norm_lists_">Internal.norm_lists_</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.norm_msets_">Internal.norm_msets_</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.prd'">Internal.prd'</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.reflect_eqdep">Internal.reflect_eqdep</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.return_prd">Internal.return_prd</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.return_sum">Internal.return_sum</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.run_msets">Internal.run_msets</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.run_list">Internal.run_list</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.sum'">Internal.sum'</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.Sym.null">Internal.Sym.null</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.Sym.rel_of">Internal.Sym.rel_of</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.Sym.type_of">Internal.Sym.type_of</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.vcompare">Internal.vcompare</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.vnorm">Internal.vnorm</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<br/><br/><a name="definition_R"></a><h2>R </h2>
<a href="AAC_tactics.Instances.html#Relations.bot">Relations.bot</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Relations.compo">Relations.compo</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Relations.inter">Relations.inter</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Relations.negr">Relations.negr</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<a href="AAC_tactics.Instances.html#Relations.top">Relations.top</a> [in <a href="AAC_tactics.Instances.html">AAC_tactics.Instances</a>]<br/>
<br/><br/><a name="definition_S"></a><h2>S </h2>
<a href="AAC_tactics.AAC.html#sigma">sigma</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#sigma_empty">sigma_empty</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#sigma_add">sigma_add</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#sigma_get">sigma_get</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<br/><br/><hr/>
<h1>Record Index</h1>
<a name="record_A"></a><h2>A </h2>
<a href="AAC_tactics.AAC.html#AAC_lift">AAC_lift</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Associative">Associative</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<br/><br/><a name="record_C"></a><h2>C </h2>
<a href="AAC_tactics.AAC.html#Commutative">Commutative</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<br/><br/><a name="record_I"></a><h2>I </h2>
<a href="AAC_tactics.AAC.html#Internal.Bin.pack">Internal.Bin.pack</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.Sym.pack">Internal.Sym.pack</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.unit_pack">Internal.unit_pack</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<a href="AAC_tactics.AAC.html#Internal.unit_of">Internal.unit_of</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<br/><br/><a name="record_U"></a><h2>U </h2>
<a href="AAC_tactics.AAC.html#Unit">Unit</a> [in <a href="AAC_tactics.AAC.html">AAC_tactics.AAC</a>]<br/>
<br/><br/><hr/><table>
<tr>
<td>Global Index</td>
<td><a href="index.html#global_A">A</a></td>
<td><a href="index.html#global_B">B</a></td>
<td><a href="index.html#global_C">C</a></td>
<td>D</td>
<td><a href="index.html#global_E">E</a></td>
<td>F</td>
<td>G</td>
<td><a href="index.html#global_H">H</a></td>
<td><a href="index.html#global_I">I</a></td>
<td>J</td>
<td>K</td>
<td><a href="index.html#global_L">L</a></td>
<td><a href="index.html#global_M">M</a></td>
<td><a href="index.html#global_N">N</a></td>
<td>O</td>
<td><a href="index.html#global_P">P</a></td>
<td><a href="index.html#global_Q">Q</a></td>
<td><a href="index.html#global_R">R</a></td>
<td><a href="index.html#global_S">S</a></td>
<td><a href="index.html#global_T">T</a></td>
<td><a href="index.html#global_U">U</a></td>
<td><a href="index.html#global_V">V</a></td>
<td><a href="index.html#global_W">W</a></td>
<td>X</td>
<td>Y</td>
<td><a href="index.html#global_Z">Z</a></td>
<td>_</td>
<td>other</td>
<td>(489 entries)</td>
</tr>
<tr>
<td>Notation Index</td>
<td>A</td>
<td><a href="index.html#notation_B">B</a></td>
<td>C</td>
<td>D</td>
<td><a href="index.html#notation_E">E</a></td>
<td>F</td>
<td>G</td>
<td>H</td>
<td><a href="index.html#notation_I">I</a></td>
<td>J</td>
<td>K</td>
<td>L</td>
<td>M</td>
<td>N</td>
<td>O</td>
<td><a href="index.html#notation_P">P</a></td>
<td>Q</td>
<td>R</td>
<td>S</td>
<td>T</td>
<td><a href="index.html#notation_U">U</a></td>
<td><a href="index.html#notation_V">V</a></td>
<td>W</td>
<td>X</td>
<td>Y</td>
<td>Z</td>
<td>_</td>
<td>other</td>
<td>(19 entries)</td>
</tr>
<tr>
<td>Module Index</td>
<td><a href="index.html#module_A">A</a></td>
<td><a href="index.html#module_B">B</a></td>
<td>C</td>
<td>D</td>
<td>E</td>
<td>F</td>
<td>G</td>
<td>H</td>
<td><a href="index.html#module_I">I</a></td>
<td>J</td>
<td>K</td>
<td><a href="index.html#module_L">L</a></td>
<td>M</td>
<td><a href="index.html#module_N">N</a></td>
<td>O</td>
<td><a href="index.html#module_P">P</a></td>
<td><a href="index.html#module_Q">Q</a></td>
<td><a href="index.html#module_R">R</a></td>
<td>S</td>
<td>T</td>
<td>U</td>
<td>V</td>
<td>W</td>
<td>X</td>
<td>Y</td>
<td><a href="index.html#module_Z">Z</a></td>
<td>_</td>
<td>other</td>
<td>(13 entries)</td>
</tr>
<tr>
<td>Variable Index</td>
<td><a href="index.html#variable_A">A</a></td>
<td><a href="index.html#variable_B">B</a></td>
<td>C</td>
<td>D</td>
<td><a href="index.html#variable_E">E</a></td>
<td>F</td>
<td>G</td>
<td>H</td>
<td><a href="index.html#variable_I">I</a></td>
<td>J</td>
<td>K</td>
<td>L</td>
<td><a href="index.html#variable_M">M</a></td>
<td>N</td>
<td>O</td>
<td><a href="index.html#variable_P">P</a></td>
<td>Q</td>
<td><a href="index.html#variable_R">R</a></td>
<td>S</td>
<td>T</td>
<td><a href="index.html#variable_U">U</a></td>
<td>V</td>
<td><a href="index.html#variable_W">W</a></td>
<td>X</td>
<td>Y</td>
<td><a href="index.html#variable_Z">Z</a></td>
<td>_</td>
<td>other</td>
<td>(114 entries)</td>
</tr>
<tr>
<td>Library Index</td>
<td><a href="index.html#library_A">A</a></td>
<td>B</td>
<td><a href="index.html#library_C">C</a></td>
<td>D</td>
<td>E</td>
<td>F</td>
<td>G</td>
<td>H</td>
<td><a href="index.html#library_I">I</a></td>
<td>J</td>
<td>K</td>
<td>L</td>
<td>M</td>
<td>N</td>
<td>O</td>
<td>P</td>
<td>Q</td>
<td>R</td>
<td>S</td>
<td><a href="index.html#library_T">T</a></td>
<td>U</td>
<td>V</td>
<td>W</td>
<td>X</td>
<td>Y</td>
<td>Z</td>
<td>_</td>
<td>other</td>
<td>(4 entries)</td>
</tr>
<tr>
<td>Lemma Index</td>
<td>A</td>
<td>B</td>
<td>C</td>
<td>D</td>
<td><a href="index.html#lemma_E">E</a></td>
<td>F</td>
<td>G</td>
<td><a href="index.html#lemma_H">H</a></td>
<td><a href="index.html#lemma_I">I</a></td>
<td>J</td>
<td>K</td>
<td><a href="index.html#lemma_L">L</a></td>
<td>M</td>
<td>N</td>
<td>O</td>
<td>P</td>
<td>Q</td>
<td>R</td>
<td>S</td>
<td>T</td>
<td>U</td>
<td>V</td>
<td>W</td>
<td>X</td>
<td>Y</td>
<td><a href="index.html#lemma_Z">Z</a></td>
<td>_</td>
<td>other</td>
<td>(56 entries)</td>
</tr>
<tr>
<td>Constructor Index</td>
<td>A</td>
<td>B</td>
<td>C</td>
<td>D</td>
<td>E</td>
<td>F</td>
<td>G</td>
<td>H</td>
<td><a href="index.html#constructor_I">I</a></td>
<td>J</td>
<td>K</td>
<td><a href="index.html#constructor_L">L</a></td>
<td>M</td>
<td>N</td>
<td>O</td>
<td>P</td>
<td>Q</td>
<td>R</td>
<td>S</td>
<td>T</td>
<td>U</td>
<td>V</td>
<td>W</td>
<td>X</td>
<td>Y</td>
<td>Z</td>
<td>_</td>
<td>other</td>
<td>(34 entries)</td>
</tr>
<tr>
<td>Inductive Index</td>
<td><a href="index.html#inductive_A">A</a></td>
<td>B</td>
<td><a href="index.html#inductive_C">C</a></td>
<td>D</td>
<td>E</td>
<td>F</td>
<td>G</td>
<td>H</td>
<td><a href="index.html#inductive_I">I</a></td>
<td>J</td>
<td>K</td>
<td>L</td>
<td>M</td>
<td>N</td>
<td>O</td>
<td>P</td>
<td>Q</td>
<td>R</td>
<td>S</td>
<td>T</td>
<td>U</td>
<td>V</td>
<td>W</td>
<td>X</td>
<td>Y</td>
<td>Z</td>
<td>_</td>
<td>other</td>
<td>(13 entries)</td>
</tr>
<tr>
<td>Projection Index</td>
<td><a href="index.html#projection_A">A</a></td>
<td>B</td>
<td>C</td>
<td>D</td>
<td>E</td>
<td>F</td>
<td>G</td>
<td>H</td>
<td><a href="index.html#projection_I">I</a></td>
<td>J</td>
<td>K</td>
<td><a href="index.html#projection_L">L</a></td>
<td>M</td>
<td>N</td>
<td>O</td>
<td>P</td>
<td>Q</td>
<td>R</td>
<td>S</td>
<td>T</td>
<td>U</td>
<td>V</td>
<td>W</td>
<td>X</td>
<td>Y</td>
<td>Z</td>
<td>_</td>
<td>other</td>
<td>(17 entries)</td>
</tr>
<tr>
<td>Section Index</td>
<td><a href="index.html#section_A">A</a></td>
<td><a href="index.html#section_B">B</a></td>
<td>C</td>
<td>D</td>
<td><a href="index.html#section_E">E</a></td>
<td>F</td>
<td>G</td>
<td>H</td>
<td><a href="index.html#section_I">I</a></td>
<td>J</td>
<td>K</td>
<td>L</td>
<td><a href="index.html#section_M">M</a></td>
<td>N</td>
<td>O</td>
<td><a href="index.html#section_P">P</a></td>
<td>Q</td>
<td><a href="index.html#section_R">R</a></td>
<td><a href="index.html#section_S">S</a></td>
<td><a href="index.html#section_T">T</a></td>
<td><a href="index.html#section_U">U</a></td>
<td><a href="index.html#section_V">V</a></td>
<td><a href="index.html#section_W">W</a></td>
<td>X</td>
<td>Y</td>
<td><a href="index.html#section_Z">Z</a></td>
<td>_</td>
<td>other</td>
<td>(37 entries)</td>
</tr>
<tr>
<td>Instance Index</td>
<td><a href="index.html#instance_A">A</a></td>
<td><a href="index.html#instance_B">B</a></td>
<td>C</td>
<td>D</td>
<td>E</td>
<td>F</td>
<td>G</td>
<td>H</td>
<td><a href="index.html#instance_I">I</a></td>
<td>J</td>
<td>K</td>
<td><a href="index.html#instance_L">L</a></td>
<td>M</td>
<td><a href="index.html#instance_N">N</a></td>
<td>O</td>
<td><a href="index.html#instance_P">P</a></td>
<td><a href="index.html#instance_Q">Q</a></td>
<td><a href="index.html#instance_R">R</a></td>
<td>S</td>
<td>T</td>
<td>U</td>
<td>V</td>
<td>W</td>
<td>X</td>
<td>Y</td>
<td><a href="index.html#instance_Z">Z</a></td>
<td>_</td>
<td>other</td>
<td>(119 entries)</td>
</tr>
<tr>
<td>Abbreviation Index</td>
<td>A</td>
<td>B</td>
<td>C</td>
<td>D</td>
<td>E</td>
<td>F</td>
<td>G</td>
<td>H</td>
<td><a href="index.html#abbreviation_I">I</a></td>
<td>J</td>
<td>K</td>
<td>L</td>
<td>M</td>
<td>N</td>
<td>O</td>
<td>P</td>
<td>Q</td>
<td>R</td>
<td>S</td>
<td>T</td>
<td>U</td>
<td>V</td>
<td>W</td>
<td>X</td>
<td>Y</td>
<td>Z</td>
<td>_</td>
<td>other</td>
<td>(4 entries)</td>
</tr>
<tr>
<td>Definition Index</td>
<td>A</td>
<td>B</td>
<td>C</td>
<td>D</td>
<td>E</td>
<td>F</td>
<td>G</td>
<td>H</td>
<td><a href="index.html#definition_I">I</a></td>
<td>J</td>
<td>K</td>
<td>L</td>
<td>M</td>
<td>N</td>
<td>O</td>
<td>P</td>
<td>Q</td>
<td><a href="index.html#definition_R">R</a></td>
<td><a href="index.html#definition_S">S</a></td>
<td>T</td>
<td>U</td>
<td>V</td>
<td>W</td>
<td>X</td>
<td>Y</td>
<td>Z</td>
<td>_</td>
<td>other</td>
<td>(51 entries)</td>
</tr>
<tr>
<td>Record Index</td>
<td><a href="index.html#record_A">A</a></td>
<td>B</td>
<td><a href="index.html#record_C">C</a></td>
<td>D</td>
<td>E</td>
<td>F</td>
<td>G</td>
<td>H</td>
<td><a href="index.html#record_I">I</a></td>
<td>J</td>
<td>K</td>
<td>L</td>
<td>M</td>
<td>N</td>
<td>O</td>
<td>P</td>
<td>Q</td>
<td>R</td>
<td>S</td>
<td>T</td>
<td><a href="index.html#record_U">U</a></td>
<td>V</td>
<td>W</td>
<td>X</td>
<td>Y</td>
<td>Z</td>
<td>_</td>
<td>other</td>
<td>(8 entries)</td>
</tr>
</table>
<hr/>This page has been generated by <a href="http://coq.inria.fr/">coqdoc</a>
</div>
</div>
</body>
</html>
|