/[mojave]/metaprl/theories/czf/czf_itt_hom.prla
ViewVC logotype

Diff of /metaprl/theories/czf/czf_itt_hom.prla

Parent Directory Parent Directory | Revision Log Revision Log | View Patch Patch

revision 3558 by xiny, Sun Mar 24 08:26:30 2002 UTC revision 3559 by xiny, Tue Apr 2 08:46:33 2002 UTC
# Line 1045  Line 1045 
1045  B       b387    t387  B       b387    t387
1046  T       t388    o b363 b387  T       t388    o b363 b387
1047  B       b388    t388  B       b388    t388
 T       t389    o b361 b388  
 B       b389    t389  
 T       t390    o2 b361 b389 b356  
 B       b390    t390  
 T       t391    o359 b390  
 B       b391    t391  
1048  P       p391    Number 42  P       p391    Number 42
1049  P       p392    Number 63  P       p392    Number 63
1050  O       o392    location p391 p392  O       o392    location p391 p392
# Line 1090  Line 1084 
1084  B       b403    t403  B       b403    t403
1085  T       t404    o b403 b4  T       t404    o b403 b4
1086  B       b404    t404  B       b404    t404
1087  T       t405    o b404 b4  T       t1      o b404 b388
1088  B       b405    t405  B       b1      t1
1089  T       t406    o b402 b405  T       t2      o b402 b1
1090  B       b406    t406  B       b2      t2
1091  T       t407    o b400 b406  T       t3      o b400 b2
1092  B       b407    t407  B       b3      t3
1093  T       t408    o b398 b407  T       t214    o b398 b3
1094  B       b408    t408  B       b214    t214
1095  T       t409    o b396 b408  T       t215    o b396 b214
1096  B       b409    t409  B       b215    t215
1097  T       t410    o b394 b409  T       t218    o b394 b215
1098  B       b410    t410  B       b218    t218
1099  T       t411    o2 b394 b410 b356  T       t219    o b361 b218
1100  B       b411    t411  B       b219    t219
1101  T       t412    o392 b411  T       t229    o2 b361 b219 b356
1102  B       b412    t412  B       b229    t229
1103    T       t230    o359 b229
1104    B       b230    t230
1105    T       t233    o2 b394 b4 b356
1106    B       b233    t233
1107    T       t237    o392 b233
1108    B       b237    t237
1109  P       p412    Number 64  P       p412    Number 64
1110  P       p413    Number 90  P       p413    Number 90
1111  O       o413    location p412 p413  O       o413    location p412 p413
# Line 1337  Line 1337 
1337  B       b512    t512  B       b512    t512
1338  T       t513    o507 b512  T       t513    o507 b512
1339  B       b513    t513  B       b513    t513
1340  P       p513    Number 371  P       p246    Number 370
1341  P       p514    Number 387  P       p514    Number 387
1342  O       o514    location p513 p514  O       o246    location p246 p514
1343  O       o515    str_open p513 p514  O       o247    str_open p246 p514
1344    P       p247    String Simple_print
1345    O       o248    string p247
1346    T       t251    o248
1347    B       b251    t251
1348    T       t256    o b251 b4
1349    B       b256    t256
1350    T       t257    o247 b256
1351    B       b257    t257
1352    T       t265    o420 b257
1353    B       b265    t265
1354    T       t266    o246 b265
1355    B       b266    t266
1356    P       p277    Number 389
1357    P       p279    Number 405
1358    O       o279    location p277 p279
1359    O       o280    str_open p277 p279
1360  P       p515    String Tactic_type  P       p515    String Tactic_type
1361  O       o516    string p515  O       o516    string p515
1362  T       t516    o516  T       t516    o516
1363  B       b516    t516  B       b516    t516
1364  T       t517    o b516 b4  T       t517    o b516 b4
1365  B       b517    t517  B       b517    t517
1366  T       t518    o515 b517  T       t289    o280 b517
1367  B       b518    t518  B       b289    t289
1368  T       t519    o420 b518  T       t290    o420 b289
1369  B       b519    t519  B       b290    t290
1370  T       t520    o514 b519  T       t292    o279 b290
1371  B       b520    t520  B       b292    t292
1372  P       p520    Number 388  P       p294    Number 406
1373  P       p521    Number 414  P       p295    Number 432
1374  O       o521    location p520 p521  O       o295    location p294 p295
1375  O       o522    str_open p520 p521  O       o296    str_open p294 p295
1376  P       p522    String Tacticals  P       p522    String Tacticals
1377  O       o523    string p522  O       o523    string p522
1378  T       t523    o523  T       t523    o523
# Line 1365  Line 1381 
1381  B       b524    t524  B       b524    t524
1382  T       t525    o b516 b524  T       t525    o b516 b524
1383  B       b525    t525  B       b525    t525
1384  T       t526    o522 b525  T       t300    o296 b525
1385  B       b526    t526  B       b300    t300
1386  T       t527    o420 b526  T       t301    o420 b300
1387  B       b527    t527  B       b301    t301
1388  T       t528    o521 b527  T       t304    o295 b301
1389  B       b528    t528  B       b304    t304
1390  P       p528    Number 415  P       p307    Number 433
1391  P       p529    Number 439  P       p322    Number 457
1392  O       o529    location p528 p529  O       o322    location p307 p322
1393  O       o530    str_open p528 p529  O       o323    str_open p307 p322
1394  P       p530    String Sequent  P       p530    String Sequent
1395  O       o531    string p530  O       o531    string p530
1396  T       t531    o531  T       t531    o531
# Line 1383  Line 1399 
1399  B       b532    t532  B       b532    t532
1400  T       t533    o b516 b532  T       t533    o b516 b532
1401  B       b533    t533  B       b533    t533
1402  T       t534    o530 b533  T       t327    o323 b533
1403  B       b534    t534  B       b327    t327
1404  T       t535    o420 b534  T       t331    o420 b327
1405  B       b535    t535  B       b331    t331
1406  T       t536    o529 b535  T       t332    o322 b331
1407  B       b536    t536  B       b332    t332
1408  P       p536    Number 440  P       p337    Number 458
1409  P       p537    Number 470  P       p344    Number 488
1410  O       o537    location p536 p537  O       o344    location p337 p344
1411  O       o538    str_open p536 p537  O       o345    str_open p337 p344
1412  P       p538    String Conversionals  P       p538    String Conversionals
1413  O       o539    string p538  O       o539    string p538
1414  T       t539    o539  T       t539    o539
# Line 1401  Line 1417 
1417  B       b540    t540  B       b540    t540
1418  T       t541    o b516 b540  T       t541    o b516 b540
1419  B       b541    t541  B       b541    t541
1420  T       t542    o538 b541  T       t359    o345 b541
1421  B       b542    t542  B       b359    t359
1422  T       t543    o420 b542  T       t392    o420 b359
1423  B       b543    t543  B       b392    t392
1424  T       t544    o537 b543  T       t413    o344 b392
1425  B       b544    t544  B       b413    t413
1426  P       p544    Number 471  P       p415    Number 489
1427  P       p545    Number 481  P       p416    Number 499
1428  O       o545    location p544 p545  O       o416    location p415 p416
1429  O       o546    str_open p544 p545  O       o417    str_open p415 p416
1430  O       o547    string p131  O       o547    string p131
1431  T       t547    o547  T       t547    o547
1432  B       b547    t547  B       b547    t547
1433  T       t548    o b547 b4  T       t548    o b547 b4
1434  B       b548    t548  B       b548    t548
1435  T       t549    o546 b548  T       t419    o417 b548
1436  B       b549    t549  B       b419    t419
1437  T       t550    o420 b549  T       t420    o420 b419
1438  B       b550    t550  B       b420    t420
1439  T       t551    o545 b550  T       t421    o416 b420
1440  B       b551    t551  B       b421    t421
1441  P       p551    Number 482  P       p422    Number 500
1442  P       p552    Number 490  P       p423    Number 508
1443  O       o552    location p551 p552  O       o423    location p422 p423
1444  O       o553    str_open p551 p552  O       o424    str_open p422 p423
1445  O       o554    string p129  O       o554    string p129
1446  T       t554    o554  T       t554    o554
1447  B       b554    t554  B       b554    t554
1448  T       t555    o b554 b4  T       t555    o b554 b4
1449  B       b555    t555  B       b555    t555
1450  T       t556    o553 b555  T       t427    o424 b555
1451  B       b556    t556  B       b427    t427
1452  T       t557    o420 b556  T       t428    o420 b427
1453  B       b557    t557  B       b428    t428
1454  T       t558    o552 b557  T       t434    o423 b428
1455  B       b558    t558  B       b434    t434
 P       p558    Number 492  
 P       p559    Number 509  
 O       o559    location p558 p559  
 O       o560    str_open p558 p559  
1456  O       o561    string p119  O       o561    string p119
1457  T       t561    o561  T       t561    o561
1458  B       b561    t561  B       b561    t561
1459  T       t562    o b561 b4  T       t562    o b561 b4
1460  B       b562    t562  B       b562    t562
 T       t563    o560 b562  
 B       b563    t563  
 T       t564    o420 b563  
 B       b564    t564  
 T       t565    o559 b564  
 B       b565    t565  
1461  P       p565    Number 510  P       p565    Number 510
1462  P       p566    Number 531  P       p437    Number 527
1463  O       o566    location p565 p566  O       o438    location p565 p437
1464  O       o567    str_open p565 p566  O       o439    str_open p565 p437
1465    T       t444    o439 b562
1466    B       b444    t444
1467    T       t445    o420 b444
1468    B       b445    t445
1469    T       t453    o438 b445
1470    B       b453    t453
1471    P       p455    Number 528
1472    P       p456    Number 549
1473    O       o456    location p455 p456
1474    O       o457    str_open p455 p456
1475  O       o568    string p121  O       o568    string p121
1476  T       t568    o568  T       t568    o568
1477  B       b568    t568  B       b568    t568
1478  T       t569    o b568 b4  T       t569    o b568 b4
1479  B       b569    t569  B       b569    t569
1480  T       t570    o567 b569  T       t462    o457 b569
1481  B       b570    t570  B       b462    t462
1482  T       t571    o420 b570  T       t463    o420 b462
1483  B       b571    t571  B       b463    t463
1484  T       t572    o566 b571  T       t471    o456 b463
1485  B       b572    t572  B       b471    t471
1486  P       p572    Number 533  P       p473    Number 551
1487  P       p573    Number 575  P       p474    Number 583
1488  O       o573    location p572 p573  O       o474    location p473 p474
1489  NSummary!opname opname  opname Summary  NSummary!opname opname  opname Summary
1490  P       p574    String hom  P       p574    String hom
1491  O       o574    opname p574  O       o574    opname p574
# Line 1501  Line 1517 
1517  B       b581    t581  B       b581    t581
1518  T       t582    o580 b581  T       t582    o580 b581
1519  B       b582    t582 x  B       b582    t582 x
1520    T       t480    o575 b576 b577 b582
1521    B       b480    t480
1522    T       t481    o574 b480
1523    B       b481    t481
1524    T       t489    o474 b481
1525    B       b489    t489
1526    P       p491    Number 585
1527    P       p492    Number 709
1528    O       o492    location p491 p492
1529  T       t583    o575 b576 b577 b578 b579 b582  T       t583    o575 b576 b577 b578 b579 b582
1530  B       b583    t583  B       b583    t583
 T       t584    o574 b583  
 B       b584    t584  
 T       t585    o573 b584  
 B       b585    t585  
 P       p585    Number 577  
 P       p586    Number 743  
 O       o586    location p585 p586  
1531  NSummary!dform  dform   dform Summary  NSummary!dform  dform   dform Summary
1532  P       p587    String hom_df  P       p587    String hom_df
1533  O       o587    dform p587  O       o587    dform p587
# Line 1528  Line 1546 
1546  B       b591    t591  B       b591    t591
1547  T       t592    o580  T       t592    o580
1548  B       b592    t592 x  B       b592    t592 x
1549  T       t593    o575 b576 b577 b578 b579 b592  T       t498    o575 b576 b577 b592
1550  B       b593    t593  B       b498    t498
1551  NSummary!df_term        df_term df_term Summary  NSummary!df_term        df_term df_term Summary
1552  O       o593    df_term  O       o593    df_term
1553  NPerv!string    string593       string Perv  NPerv!string    string593       string Perv
# Line 1547  Line 1565 
1565  B       b596    t596  B       b596    t596
1566  T       t597    o595 b577  T       t597    o595 b577
1567  B       b597    t597  B       b597    t597
 T       t598    o595 b578  
 B       b598    t598  
 T       t599    o595 b579  
 B       b599    t599  
1568  B       b600    t592  B       b600    t592
1569  T       t600    o595 b600  T       t600    o595 b600
1570  B       b601    t600  B       b601    t600
# Line 1564  Line 1578 
1578  B       b604    t603  B       b604    t603
1579  T       t604    o b596 b604  T       t604    o b596 b604
1580  B       b605    t604  B       b605    t604
1581  T       t605    o b599 b605  T       t499    o b597 b605
1582  B       b606    t605  B       b499    t499
1583  T       t606    o b596 b606  T       t507    o b596 b499
1584  B       b607    t606  B       b507    t507
1585  T       t607    o b598 b607  T       t508    o b595 b507
1586  B       b608    t607  B       b508    t508
1587  T       t608    o b596 b608  T       t514    o b594 b508
1588  B       b609    t608  B       b514    t514
1589  T       t609    o b597 b609  T       t515    o593 b514
1590  B       b610    t609  B       b515    t515
1591  T       t610    o b596 b610  T       t521    o587 b591 b498 b515
1592  B       b611    t610  B       b521    t521
1593  T       t611    o b595 b611  T       t522    o492 b521
1594  B       b612    t611  B       b522    t522
1595  T       t612    o b594 b612  P       p523    Number 820
1596  B       b613    t612  P       p3      Number 1255
1597  T       t613    o593 b613  O       o6      location p523 p3
 B       b614    t613  
 T       t614    o587 b591 b593 b614  
 B       b615    t614  
 T       t615    o586 b615  
 B       b616    t615  
 P       p616    Number 909  
 P       p617    Number 1275  
 O       o617    location p616 p617  
1598  NSummary!rewrite        rewrite rewrite Summary  NSummary!rewrite        rewrite rewrite Summary
1599  P       p618    String unfold_hom  P       p618    String unfold_hom
1600  O       o618    rewrite p618  O       o618    rewrite p618
# Line 1699  Line 1705 
1705  O       o654    prim  O       o654    prim
1706  T       t655    o654 b4  T       t655    o654 b4
1707  B       b655    t655  B       b655    t655
 T       t656    o618 b583 b654 b655 b4  
 B       b656    t656  
 T       t657    o617 b656  
 B       b657    t657  
 P       p657    Number 1277  
 P       p658    Number 1714  
 O       o658    location p657 p658  
1708  NSummary!rule   rule    rule Summary  NSummary!rule   rule    rule Summary
1709  P       p659    String hom_type  P       p659    String hom_type
1710  O       o659    rule p659  O       o659    rule p659
# Line 1765  Line 1764 
1764  S       s674    t664 h  S       s674    t664 h
1765  G       s674    t622  G       s674    t622
1766  B       b675    s674  B       b675    s674
 T       t675    o662 b675  
 B       b676    t675  
1767  S       s676    t664 h  S       s676    t664 h
1768  G       s676    t623  G       s676    t623
1769  B       b677    s676  B       b677    s676
 T       t677    o662 b677  
 B       b678    t677  
1770  H       h678    x t634  H       h678    x t634
1771  B       b679    t582  B       b679    t582
1772  T       t679    o621 b679  T       t679    o621 b679
# Line 1786  Line 1781 
1781  S       s681    t671 h  S       s681    t671 h
1782  G       s681    t681  G       s681    t681
1783  B       b682    s681  B       b682    s681
 T       t682    o662 b682  
 B       b683    t682  
 T       t683    o661 b681 b683  
 B       b684    t683  
 T       t684    o661 b678 b684  
 B       b685    t684  
 T       t685    o661 b676 b685  
 B       b686    t685  
 T       t686    o661 b674 b686  
 B       b687    t686  
 T       t687    o661 b672 b687  
 B       b688    t687  
 T       t688    o661 b669 b688  
 B       b689    t688  
 T       t689    o661 b667 b689  
 B       b690    t689  
1784  NSummary!interactive    interactive     interactive Summary  NSummary!interactive    interactive     interactive Summary
1785  O       o690    interactive  O       o690    interactive
1786  NSummary!ext_rule       ext_rule        ext_rule Summary  NSummary!ext_rule       ext_rule        ext_rule Summary
 P       p690    String "rwh unfold_hom 0 thenT autoT thenT rwh fold_isset 0 ttca"  
 O       o691    ext_rule p690  
1787  NSummary!status_incomplete      status_incomplete       status_incomplete Summary  NSummary!status_incomplete      status_incomplete       status_incomplete Summary
1788  O       o692    status_incomplete  O       o692    status_incomplete
1789  T       t692    o692  T       t692    o692
# Line 2021  Line 1998 
1998  B       b773    t772  B       b773    t772
1999  T       t773    o704 b706 b4 b773  T       t773    o704 b706 b4 b773
2000  B       b774    t773  B       b774    t773
 T       t774    o b774 b4  
 B       b775    t774  
 T       t775    o693 b704 b775  
 B       b776    t775  
2001  P       p776    String "assumT 7 ttca thenT instHypT [<< op{'g1; 'a; 'b} >>] 4 ttca thenT rwh fold_isset 0 ttca"  P       p776    String "assumT 7 ttca thenT instHypT [<< op{'g1; 'a; 'b} >>] 4 ttca thenT rwh fold_isset 0 ttca"
2002  O       o776    ext_rule p776  O       o776    ext_rule p776
2003  T       t776    o693 b774 b4  T       t776    o693 b774 b4
# Line 2033  Line 2006 
2006  B       b778    t777  B       b778    t777
2007  T       t778    o b778 b4  T       t778    o b778 b4
2008  B       b779    t778  B       b779    t778
 T       t779    o691 b692 b776 b779 b4  
 B       b780    t779  
 T       t780    o690 b780  
 B       b781    t780  
2009  NSummary!resource_defs  resource_defs   resource_defs Summary  NSummary!resource_defs  resource_defs   resource_defs Summary
 P       p781    Number 1301  
 P       p782    Number 1309  
 O       o782    resource_defs p781 p782 p264  
2010  NOcaml!uid      uid     uid Ocaml  NOcaml!uid      uid     uid Ocaml
 P       p783    Number 1307  
 O       o783    uid p783 p782  
2011  P       p784    String []  P       p784    String []
2012  O       o784    uid p784  O       o784    uid p784
2013  T       t784    o784  T       t784    o784
2014  B       b784    t784  B       b784    t784
 T       t785    o783 b784  
 B       b785    t785  
 T       t786    o b785 b4  
 B       b786    t786  
 T       t787    o782 b786  
 B       b787    t787  
 T       t788    o b787 b4  
 B       b788    t788  
 T       t789    o659 b661 b690 b781 b788  
 B       b789    t789  
 T       t790    o658 b789  
 B       b790    t790  
 P       p790    Number 1716  
 P       p791    Number 2490  
 O       o791    location p790 p791  
2015  P       p792    String hom_intro  P       p792    String hom_intro
2016  O       o792    rule p792  O       o792    rule p792
2017  P       p793    Var z  P       p793    Var z
# Line 2075  Line 2024 
2024  S       s795    t671 h  S       s795    t671 h
2025  G       s795    t795  G       s795    t795
2026  B       b795    s795  B       b795    s795
 T       t796    o662 b795  
 B       b796    t796  
2027  T       t797    o629 b581 b624  T       t797    o629 b581 b624
2028  H       h797    y t797  H       h797    y t797
2029  T       t798    o629 b679 b626  T       t798    o629 b679 b626
# Line 2088  Line 2035 
2035  S       s799    t671 h  S       s799    t671 h
2036  G       s799    t625  G       s799    t625
2037  B       b800    s799  B       b800    s799
 T       t800    o662 b800  
 B       b801    t800  
2038  S       s801    t671 h  S       s801    t671 h
2039  G       s801    t627  G       s801    t627
2040  B       b802    s801  B       b802    s801
 T       t802    o662 b802  
 B       b803    t802  
2041  H       h803    x t635  H       h803    x t635
2042  H       h804    y t637  H       h804    y t637
2043  S       s804    t671 h h704 h705 h803 h804  S       s804    t671 h h704 h705 h803 h804
2044  G       s804    t642  G       s804    t642
2045  B       b804    s804  B       b804    s804
 T       t804    o662 b804  
 B       b805    t804  
2046  S       s805    t671 h  S       s805    t671 h
2047  G       s805    t583  G       s805    t583
2048  B       b806    s805  B       b806    s805
 T       t806    o662 b806  
 B       b807    t806  
 T       t807    o661 b805 b807  
 B       b808    t807  
 T       t808    o661 b803 b808  
 B       b809    t808  
 T       t809    o661 b801 b809  
 B       b810    t809  
 T       t810    o661 b678 b810  
 B       b811    t810  
 T       t811    o661 b676 b811  
 B       b812    t811  
 T       t812    o661 b799 b812  
 B       b813    t812  
 T       t813    o661 b796 b813  
 B       b814    t813  
 T       t814    o661 b674 b814  
 B       b815    t814  
 T       t815    o661 b672 b815  
 B       b816    t815  
 T       t816    o661 b669 b816  
 B       b817    t816  
 T       t817    o661 b667 b817  
 B       b818    t817  
2049  P       p818    String "rwh unfold_hom 0 thenT autoT"  P       p818    String "rwh unfold_hom 0 thenT autoT"
2050  O       o818    ext_rule p818  O       o818    ext_rule p818
2051  T       t818    o b804 b4  T       t818    o b804 b4
# Line 2216  Line 2133 
2133  T       t855    o695 b855 b829  T       t855    o695 b855 b829
2134  B       b856    t855  B       b856    t855
2135  B       b857    t632  B       b857    t632
2136    T       t529    o635 b635 b857
2137    B       b529    t529 a
2138    T       t530    o633 b634 b529
2139    B       b530    t530
2140    NCzf_itt_group!eqG      eqG     eqG Czf_itt_group
2141    O       o532    eqG
2142    T       t537    o532 b577
2143    B       b537    t537
2144    T       t538    o623 b626 b537 b639 b641
2145    B       b538    t538
2146    T       t545    o635 b637 b538
2147    B       b545    t545
2148    T       t546    o635 b635 b545
2149    B       b546    t546 b
2150    T       t552    o633 b634 b546
2151    B       b552    t552 a
2152    T       t553    o633 b634 b552
2153    B       b553    t553
2154    T       t559    o619 b530 b553
2155    B       b559    t559
2156    T       t560    o619 b628 b559
2157    B       b560    t560
2158    T       t566    o619 b621 b560
2159    B       b566    t566
2160    T       t567    o619 b620 b566
2161    B       b567    t567
2162    T       t586    o681 b480
2163    S       s586    t671 h
2164    G       s586    t586
2165    B       b586    s586
2166    T       t587    o662 b586
2167    B       b587    t587
2168    T       t616    o661 b681 b587
2169    B       b617    t616
2170    T       t617    o661 b669 b617
2171    B       b618    t617
2172    T       t618    o661 b667 b618
2173    B       b619    t618
2174    T       t619    o b668 b695
2175    B       b629    t619
2176    T       t629    o b666 b629
2177    B       b658    t629
2178    T       t658    o695 b586 b658
2179    B       b659    t658
2180    T       t659    o694 b659 b4 b703
2181    B       b662    t659
2182    T       t662    o695 b705 b658
2183    B       b664    t662
2184    T       t674    o681 b538
2185    S       s675    t664 h h704 h705
2186    G       s675    t674
2187    B       b691    s675
2188    T       t691    o695 b691 b658
2189    B       b693    t691
2190    T       t693    o681 b545
2191    S       s693    t664 h h704 h705
2192    G       s693    t693
2193    B       b694    s693
2194    T       t694    o695 b694 b658
2195    B       b782    t694
2196    B       b783    t546
2197    T       t783    o681 b783
2198    S       s783    t664 h h704 h705
2199    G       s783    t783
2200    B       b791    s783
2201    T       t791    o695 b791 b658
2202    B       b792    t791
2203    B       b797    t552
2204    T       t801    o681 b797
2205    S       s802    t664 h h704
2206    G       s802    t801
2207    B       b898    s802
2208    T       t898    o695 b898 b658
2209    B       b905    t898
2210    T       t905    o681 b553
2211    S       s905    t664 h
2212    G       s905    t905
2213    B       b952    s905
2214    T       t952    o695 b952 b658
2215    B       b955    t952
2216    T       t970    o681 b559
2217    S       s970    t664 h
2218    G       s970    t970
2219    B       b1034   s970
2220    T       t1034   o695 b1034 b658
2221    B       b1035   t1034
2222    T       t1035   o681 b560
2223    S       s1035   t664 h
2224    G       s1035   t1035
2225    B       b1036   s1035
2226    T       t1054   o695 b1036 b658
2227    B       b1144   t1054
2228    T       t1144   o681 b566
2229    S       s1144   t664 h
2230    G       s1144   t1144
2231    B       b1145   s1144
2232    T       t1145   o695 b1145 b658
2233    B       b1146   t1145
2234    T       t1146   o681 b567
2235    S       s1146   t664 h
2236    G       s1146   t1146
2237    B       b1147   s1146
2238    T       t1147   o695 b1147 b658
2239    B       b1148   t1147
2240    B       b1149   t1146
2241    T       t1149   o737 b1149
2242    S       s1149   t664 h
2243    G       s1149   t1149
2244    B       b1315   s1149
2245    T       t1315   o695 b1315 b658
2246    B       b1316   t1315
2247    S       s1316   t671 h
2248    G       s1316   t1146
2249    B       b1317   s1316
2250    T       t1317   o695 b1317 b658
2251    B       b1318   t1317
2252    T       t1318   o2 b662
2253    B       b1319   t1318
2254    T       t1319   o694 b1318 b4 b1319
2255    B       b1420   t1319
2256    T       t1427   o2 b1420
2257    B       b1427   t1427
2258    T       t1428   o694 b1316 b4 b1427
2259    B       b1428   t1428
2260    T       t1429   o2 b1428
2261    B       b1429   t1429
2262    T       t1430   o694 b1148 b711 b1429
2263    B       b1430   t1430
2264    T       t1436   o2 b1430
2265    B       b1552   t1436
2266    T       t1552   o704 b1146 b711 b1552
2267    B       b1559   t1552
2268    T       t1559   o2 b1559
2269    B       b1693   t1559
2270    T       t1697   o704 b1144 b711 b1693
2271    B       b1832   t1697
2272    T       t1832   o2 b1832
2273    B       b1833   t1832
2274    T       t1833   o704 b1035 b711 b1833
2275    B       b1864   t1833
2276    T       t1864   o2 b1864
2277    B       b1865   t1864
2278    T       t1865   o704 b955 b711 b1865
2279    B       b1866   t1865
2280    T       t1866   o2 b1866
2281    B       b1867   t1866
2282    T       t1867   o704 b905 b711 b1867
2283    B       b1868   t1867
2284    T       t1868   o2 b1868
2285    B       b1869   t1868
2286    T       t1869   o704 b792 b711 b1869
2287    B       b1870   t1869
2288    T       t1870   o2 b1870
2289    B       b1871   t1870
2290    T       t1871   o704 b782 b711 b1871
2291    B       b1872   t1871
2292    T       t1872   o2 b1872
2293    B       b1873   t1872
2294    T       t1873   o704 b693 b711 b1873
2295    B       b1879   t1873
2296    T       t1890   o2 b1879
2297    B       b2177   t1890
2298    T       t2177   o704 b664 b4 b2177
2299    B       b2178   t2177
2300    P       p2461   String "assumT 3 ttca thenT instHypT [<< op{'g1; 'a; 'b} >>] 4 ttca thenT rwh fold_isset 0 ttca"
2301    O       o2461   ext_rule p2461
2302    T       t2466   o693 b2178 b4
2303    B       b2574   t2466
2304    T       t2579   o2461 b692 b2574 b4 b4
2305    B       b2617   t2579
2306    T       t2617   o b2617 b4
2307    B       b2638   t2617
2308    S       s2706   t671 h
2309    G       s2706   t480
2310    B       b2707   s2706
2311    T       t2707   o662 b2707
2312    B       b2708   t2707
2313  T       t857    o681 b857  T       t857    o681 b857
2314  S       s857    t664 h h704  S       s857    t664 h h704
2315  G       s857    t857  G       s857    t857
# Line 2273  Line 2367 
2367  B       b881    t880  B       b881    t880
2368  T       t881    o704 b856 b4 b881  T       t881    o704 b856 b4 b881
2369  B       b882    t881  B       b882    t881
 T       t882    o b882 b4  
 B       b883    t882  
 T       t883    o b854 b883  
 B       b884    t883  
 T       t884    o b847 b884  
 B       b885    t884  
 T       t885    o693 b831 b885  
 B       b886    t885  
2370  P       p886    String "rwh unfold_isset 0 thenT autoT thenT rwh fold_isset 0 thenT autoT"  P       p886    String "rwh unfold_isset 0 thenT autoT thenT rwh fold_isset 0 thenT autoT"
2371  O       o886    ext_rule p886  O       o886    ext_rule p886
2372  T       t886    o693 b847 b4  T       t886    o693 b847 b4
# Line 2303  Line 2389 
2389  B       b894    t893  B       b894    t893
2390  T       t894    o b888 b894  T       t894    o b888 b894
2391  B       b895    t894  B       b895    t894
 T       t895    o818 b692 b886 b895 b4  
 B       b896    t895  
 T       t896    o690 b896  
 B       b897    t896  
 P       p897    Number 1741  
 P       p898    Number 1749  
 O       o898    resource_defs p897 p898 p264  
 P       p899    Number 1747  
 O       o899    uid p899 p898  
 T       t899    o899 b784  
 B       b899    t899  
 T       t900    o b899 b4  
 B       b900    t900  
 T       t901    o898 b900  
 B       b901    t901  
 T       t902    o b901 b4  
 B       b902    t902  
 T       t903    o792 b661 b818 b897 b902  
 B       b903    t903  
 T       t904    o791 b903  
 B       b904    t904  
 P       p904    Number 2492  
 P       p905    Number 3193  
 O       o905    location p904 p905  
 P       p906    String hom_fun  
 O       o906    rule p906  
 T       t906    o579 b793  
 B       b906    t906 z  
 T       t907    o627 b906  
 S       s907    t671 h  
 G       s907    t907  
 B       b907    s907  
 T       t908    o662 b907  
 B       b908    t908  
 T       t909    o578 b793  
 B       b909    t909 z  
 T       t910    o627 b909  
 S       s910    t671 h  
 G       s910    t910  
 B       b910    s910  
 T       t911    o662 b910  
 B       b911    t911  
2392  H       h911    z t634  H       h911    z t634
2393  T       t912    o580 b793 b581  T       t912    o580 b793 b581
 B       b912    t912 x  
 T       t913    o627 b912  
 S       s913    t671 h h911  
 G       s913    t913  
 B       b913    s913  
 T       t914    o662 b913  
 B       b914    t914  
 T       t915    o580 b581 b793  
 B       b915    t915 x  
 T       t916    o627 b915  
 S       s916    t671 h h911  
 G       s916    t916  
 B       b916    s916  
 T       t917    o662 b916  
 B       b917    t917  
2394  B       b918    t912  B       b918    t912
2395  T       t918    o621 b918  T       t918    o621 b918
2396  S       s918    t664 h h911 h678  S       s918    t664 h h911 h678
# Line 2369  Line 2398 
2398  B       b919    s918  B       b919    s918
2399  T       t919    o662 b919  T       t919    o662 b919
2400  B       b920    t919  B       b920    t919
 T       t920    o629 b918 b626  
 S       s920    t671 h h911 h678 h797  
 G       s920    t920  
 B       b921    s920  
 T       t921    o662 b921  
 B       b922    t921  
2401  NCzf_itt_eq!fun_prop    fun_prop        fun_prop Czf_itt_eq  NCzf_itt_eq!fun_prop    fun_prop        fun_prop Czf_itt_eq
2402  O       o922    fun_prop  O       o922    fun_prop
 B       b923    t909  
 B       b924    t906  
2403  P       p924    Var y  P       p924    Var y
2404  O       o924    var p924  O       o924    var p924
2405  T       t924    o924  T       t924    o924
2406  B       b925    t924  B       b925    t924
2407  T       t925    o580 b793 b925  T       t925    o580 b793 b925
2408  B       b926    t925 y  B       b926    t925 y
2409  T       t926    o575 b576 b577 b923 b924 b926  T       t2735   o575 b576 b577 b926
2410  B       b927    t926 z  B       b2735   t2735 z
 T       t927    o922 b927  
 S       s927    t671 h  
 G       s927    t927  
 B       b928    s927  
 T       t928    o662 b928  
 B       b929    t928  
 T       t929    o661 b922 b929  
 B       b930    t929  
 T       t930    o661 b920 b930  
 B       b931    t930  
 T       t931    o661 b917 b931  
 B       b932    t931  
 T       t932    o661 b914 b932  
 B       b933    t932  
 T       t933    o661 b911 b933  
 B       b934    t933  
 T       t934    o661 b908 b934  
 B       b935    t934  
 T       t935    o661 b674 b935  
 B       b936    t935  
 T       t936    o661 b672 b936  
 B       b937    t936  
 T       t937    o661 b669 b937  
 B       b938    t937  
 T       t938    o661 b667 b938  
 B       b939    t938  
 P       p939    String "rwh unfold_fun_prop 0 thenT dT 0 ttca thenT dT 0 ttca thenT dT 0 ttca thenT dT 0 ttca thenT dT 0 ttca"  
 O       o939    ext_rule p939  
 T       t939    o b921 b4  
 B       b940    t939  
 T       t940    o b919 b940  
 B       b941    t940  
 T       t941    o b916 b941  
 B       b942    t941  
 T       t942    o b913 b942  
 B       b943    t942  
 T       t943    o b910 b943  
 B       b944    t943  
 T       t944    o b907 b944  
 B       b945    t944  
 T       t945    o b673 b945  
 B       b946    t945  
 T       t946    o b671 b946  
 B       b947    t946  
 T       t947    o b668 b947  
 B       b948    t947  
 T       t948    o b666 b948  
 B       b949    t948  
 T       t949    o695 b928 b949  
 B       b950    t949  
 T       t950    o694 b950 b4 b703  
 B       b951    t950  
2411  H       h951    s1 t634  H       h951    s1 t634
2412  H       h952    s2 t634  H       h952    s2 t634
2413  NCzf_itt_eq!equal       equal952        equal Czf_itt_eq  NCzf_itt_eq!equal       equal952        equal Czf_itt_eq
# Line 2452  Line 2421 
2421  T       t954    o954  T       t954    o954
2422  B       b954    t954  B       b954    t954
2423  T       t955    o952 b953 b954  T       t955    o952 b953 b954
2424  H       h955    x t955  B       b970    t955
2425  T       t956    o578 b953  H       h1033   y t620
2426    H       h1034   y_1 t621
2427    NCzf_itt_eq!eq  eq      eq Czf_itt_eq
2428    O       o1049   eq
2429    P       p1080   String eq
2430    O       o1080   tactic_arg p1080
2431    P       p1201   String thin
2432    O       o1201   arg_named p1201
2433    P       p1202   String false
2434    O       o1202   arg_bool p1202
2435    T       t1202   o1202
2436    B       b1202   t1202
2437    T       t1203   o1201 b1202
2438    B       b1203   t1203
2439    T       t1204   o b1203 b4
2440    B       b1204   t1204
2441    P       p1206   String with
2442    O       o1206   arg_named p1206
2443    NSummary!arg_term_list  arg_term_list   arg_term_list Summary
2444    O       o1207   arg_term_list
2445    T       t1207   o b636 b4
2446    B       b1207   t1207
2447    T       t1208   o1207 b1207
2448    B       b1208   t1208
2449    T       t1209   o1206 b1208
2450    B       b1209   t1209
2451    T       t1210   o b1209 b1204
2452    B       b1210   t1210
2453    T       t1211   o b630 b4
2454    B       b1211   t1211
2455    T       t1212   o1207 b1211
2456    B       b1212   t1212
2457    T       t1213   o1206 b1212
2458    B       b1213   t1213
2459    T       t1214   o b1213 b1204
2460    B       b1214   t1214
2461    T       t1281   o621 b626
2462    B       b1282   t1281
2463    NCzf_itt_pair   Czf_itt_pair    Czf_itt_pair NIL
2464    NCzf_itt_pair!pair      pair    pair Czf_itt_pair
2465    O       o1292   pair
2466    NCzf_itt_group!id       id      id Czf_itt_group
2467    O       o1560   id
2468    T       t1560   o1560 b577
2469    B       b1560   t1560
2470    T       t3025   o621 b537
2471    B       b3026   t3025
2472    NCzf_itt_equiv!equiv_fun_prop   equiv_fun_prop  equiv_fun_prop Czf_itt_equiv
2473    O       o1656   equiv_fun_prop
2474    NSummary!term_param     term_param      term_param Summary
2475    O       o1834   term_param
2476    T       t3190   o1834 b480
2477    B       b3190   t3190
2478    T       t3191   o b3190 b4
2479    B       b3191   t3191
2480    T       t3192   o b660 b3191
2481    B       b3192   t3192
2482    T       t3216   o532 b576
2483    B       b3216   t3216
2484    P       p2266   String assertion
2485    O       o2266   tactic_arg p2266
2486    T       t2443   o621 b630
2487    T       t3864   o623 b624 b3216
2488    T       t3865   o623 b624 b3216 b630 b636
2489    B       b3875   t3865
2490    T       t238    o623 b626 b537 b631 b640
2491    B       b238    t238
2492    T       t239    o635 b3875 b238
2493    B       b239    t239
2494    T       t242    o635 b637 b239
2495    B       b242    t242
2496    T       t243    o635 b635 b242
2497    B       b243    t243 b
2498    T       t268    o633 b634 b243
2499    B       b268    t268 a
2500    T       t269    o633 b634 b268
2501    B       b269    t269
2502    T       t270    o619 b269 b553
2503    B       b270    t270
2504    T       t273    o619 b530 b270
2505    B       b273    t273
2506    T       t274    o619 b621 b273
2507    B       b274    t274
2508    T       t309    o619 b620 b274
2509    B       b309    t309
2510    T       t310    o618 b480 b309 b655 b4
2511    B       b310    t310
2512    T       t315    o6 b310
2513    B       b315    t315
2514    P       p323    Number 1257
2515    P       p324    Number 1508
2516    O       o324    location p323 p324
2517    T       t316    o681 b270
2518    S       s316    t664 h
2519    G       s316    t316
2520    B       b316    s316
2521    T       t318    o695 b316 b658
2522    B       b318    t318
2523    T       t320    o681 b273
2524    S       s320    t664 h
2525    G       s320    t320
2526    B       b320    s320
2527    T       t335    o695 b320 b658
2528    B       b335    t335
2529    T       t339    o681 b274
2530    S       s339    t664 h
2531    G       s339    t339
2532    B       b339    s339
2533    T       t340    o695 b339 b658
2534    B       b340    t340
2535    T       t408    o681 b309
2536    S       s408    t664 h
2537    G       s408    t408
2538    B       b408    s408
2539    T       t564    o695 b408 b658
2540    B       b564    t564
2541    B       b565    t408
2542    T       t565    o737 b565
2543    S       s565    t664 h
2544    G       s565    t565
2545    B       b573    s565
2546    T       t573    o695 b573 b658
2547    B       b574    t573
2548    S       s574    t671 h
2549    G       s574    t408
2550    B       b585    s574
2551    T       t585    o695 b585 b658
2552    B       b598    t585
2553    T       t608    o694 b598 b4 b1319
2554    B       b609    t608
2555    T       t609    o2 b609
2556    B       b610    t609
2557    T       t610    o694 b574 b4 b610
2558    B       b616    t610
2559    T       t677    o2 b616
2560    B       b906    t677
2561    T       t906    o694 b564 b711 b906
2562    B       b907    t906
2563    T       t907    o2 b907
2564    B       b909    t907
2565    T       t909    o704 b340 b711 b909
2566    B       b910    t909
2567    T       t910    o2 b910
2568    B       b912    t910
2569    T       t913    o704 b335 b711 b912
2570    B       b913    t913
2571    T       t914    o2 b913
2572    B       b914    t914
2573    T       t915    o704 b318 b711 b914
2574    B       b915    t915
2575    T       t916    o2 b915
2576    B       b916    t916
2577    T       t917    o704 b955 b711 b916
2578    B       b917    t917
2579    T       t920    o2 b917
2580    B       b921    t920
2581    T       t921    o704 b905 b711 b921
2582    B       b922    t921
2583    T       t922    o2 b922
2584    B       b923    t922
2585    T       t923    o704 b792 b711 b923
2586    B       b924    t923
2587    T       t926    o2 b924
2588    B       b927    t926
2589    T       t927    o704 b782 b711 b927
2590    B       b928    t927
2591    T       t928    o2 b928
2592    B       b940    t928
2593    T       t940    o704 b693 b711 b940
2594    B       b941    t940
2595    T       t941    o2 b941
2596    B       b942    t941
2597    T       t942    o704 b664 b4 b942
2598    B       b943    t942
2599    T       t943    o b943 b4
2600    B       b944    t943
2601    T       t944    o693 b662 b944
2602    B       b945    t944
2603    T       t945    o818 b692 b945 b2638 b779
2604    B       b946    t945
2605    T       t946    o690 b946
2606    B       b947    t946
2607    P       p325    Number 1281
2608    P       p329    Number 1289
2609    O       o329    resource_defs p325 p329 p264
2610    P       p345    Number 1287
2611    O       o346    uid p345 p329
2612    T       t389    o346 b784
2613    B       b389    t389
2614    T       t390    o b389 b4
2615    B       b390    t390
2616    T       t391    o329 b390
2617    B       b391    t391
2618    T       t405    o b391 b4
2619    B       b405    t405
2620    T       t947    o659 b661 b619 b947 b405
2621    B       b948    t947
2622    T       t948    o324 b948
2623    B       b949    t948
2624    P       p407    Number 1510
2625    P       p408    Number 2208
2626    O       o408    location p407 p408
2627    H       h408    c t634
2628    H       h409    d t634
2629    P       p409    Var c
2630    O       o409    var p409
2631    T       t409    o409
2632    B       b409    t409
2633    T       t410    o629 b409 b624
2634    H       h410    x1 t410
2635    P       p410    Var d
2636    O       o410    var p410
2637    T       t411    o410
2638    B       b411    t411
2639    T       t412    o629 b411 b624
2640    H       h412    y1 t412
2641    T       t435    o623 b624 b3216 b409 b411
2642    H       h435    u t435
2643    T       t454    o580 b409
2644    B       b454    t454
2645    T       t472    o580 b411
2646    B       b472    t472
2647    T       t490    o623 b626 b537 b454 b472
2648    S       s490    t671 h h408 h409 h410 h412 h435
2649    G       s490    t490
2650    B       b490    s490
2651    T       t518    o662 b490
2652    B       b518    t518
2653    H       h518    e t634
2654    H       h519    g t634
2655    P       p519    Var e
2656    O       o519    var p519
2657    T       t519    o519
2658    B       b519    t519
2659    T       t520    o629 b519 b624
2660    H       h520    x2 t520
2661    P       p520    Var g
2662    O       o520    var p520
2663    T       t526    o520
2664    B       b526    t526
2665    T       t527    o629 b526 b624
2666    H       h527    y2 t527
2667    T       t528    o637 b576 b519 b526
2668    B       b528    t528
2669    T       t534    o580 b528
2670    B       b534    t534
2671    T       t535    o580 b519
2672    B       b535    t535
2673    T       t536    o580 b526
2674    B       b536    t536
2675    T       t542    o637 b577 b535 b536
2676    B       b542    t542
2677    T       t543    o623 b626 b537 b534 b542
2678    S       s543    t671 h h518 h519 h520 h527
2679    G       s543    t543
2680    B       b543    s543
2681    T       t544    o662 b543
2682    B       b544    t544
2683    T       t549    o661 b544 b2708
2684    B       b549    t549
2685    T       t550    o661 b518 b549
2686    B       b550    t550
2687    T       t551    o661 b799 b550
2688    B       b551    t551
2689    T       t556    o661 b674 b551
2690    B       b556    t556
2691    T       t557    o661 b672 b556
2692    B       b557    t557
2693    T       t558    o661 b669 b557
2694    B       b558    t558
2695    T       t563    o661 b667 b558
2696    B       b563    t563
2697    T       t949    o b543 b4
2698    B       b950    t949
2699    T       t950    o b490 b950
2700    B       b951    t950
2701    T       t956    o b798 b951
2702  B       b956    t956  B       b956    t956
2703  T       t957    o621 b956  T       t957    o b673 b956
2704  S       s957    t664 h h951 h952 h955  B       b957    t957
2705  G       s957    t957  T       t958    o b671 b957
 B       b957    s957  
 T       t958    o695 b957 b949  
2706  B       b958    t958  B       b958    t958
2707  T       t959    o579 b953  T       t959    o b668 b958
2708  B       b959    t959  B       b959    t959
2709  T       t960    o580 b953 b925  T       t960    o b666 b959
2710  B       b960    t960 y  B       b960    t960
2711  T       t961    o575 b576 b577 b956 b959 b960  T       t961    o695 b2707 b960
2712  B       b961    t961  B       b961    t961
2713  T       t962    o681 b961  T       t962    o694 b961 b4 b703
2714  S       s962    t664 h h951 h952 h955  B       b962    t962
2715  G       s962    t962  T       t963    o693 b962 b4
 B       b962    s962  
 T       t963    o695 b962 b949  
2716  B       b963    t963  B       b963    t963
2717  T       t964    o578 b954  T       t964    o818 b692 b963 b4 b895
2718  B       b964    t964  B       b964    t964
2719  T       t965    o579 b954  T       t965    o690 b964
2720  B       b965    t965  B       b965    t965
2721  T       t966    o580 b954 b925  P       p563    Number 1535
2722  B       b966    t966 y  P       p564    Number 1543
2723  T       t967    o575 b576 b577 b964 b965 b966  O       o564    resource_defs p563 p564 p264
2724    P       p566    Number 1541
2725    O       o566    uid p566 p564
2726    T       t570    o566 b784
2727    B       b570    t570
2728    T       t571    o b570 b4
2729    B       b571    t571
2730    T       t572    o564 b571
2731    B       b572    t572
2732    T       t575    o b572 b4
2733    B       b575    t575
2734    T       t966    o792 b661 b563 b965 b575
2735    B       b966    t966
2736    T       t967    o408 b966
2737  B       b967    t967  B       b967    t967
2738  T       t968    o635 b961 b967  P       p4      Number 2210
2739  S       s968    t671 h h951 h952 h955  P       p6      Number 2662
2740  G       s968    t968  O       o8      location p4 p6
2741  B       b968    s968  P       p8      String hom_fun
2742  T       t969    o695 b968 b949  O       o10     rule p8
2743    H       h586    z1 t634
2744    H       h587    x1 t634
2745    P       p589    Var x1
2746    O       o590    var p589
2747    T       t593    o590
2748    B       b593    t593
2749    T       t598    o629 b593 b624
2750    H       h598    y1 t598
2751    T       t969    o580 b793 b593
2752  B       b969    t969  B       b969    t969
2753  B       b970    t955  T       t971    o629 b969 b626
2754  B       b971    t968  S       s971    t671 h h911 h587 h598
 T       t971    o635 b970 b971  
 S       s971    t671 h h951 h952  
2755  G       s971    t971  G       s971    t971
2756  B       b972    s971  B       b971    s971
2757  T       t972    o695 b972 b949  T       t972    o662 b971
2758  B       b973    t972  B       b972    t972
2759  B       b974    t971 s2  T       t973    o580 b581 b793
2760  T       t974    o633 b634 b974  B       b973    t973 x
2761  S       s974    t671 h h951  T       t974    o627 b973
2762    S       s974    t671 h h911
2763  G       s974    t974  G       s974    t974
2764  B       b975    s974  B       b974    s974
2765  T       t975    o695 b975 b949  T       t975    o662 b974
2766  B       b976    t975  B       b975    t975
2767  B       b977    t974 s1  T       t976    o922 b2735
2768  T       t977    o633 b634 b977  S       s976    t671 h
2769  S       s977    t671 h  G       s976    t976
2770  G       s977    t977  B       b976    s976
2771  B       b978    s977  T       t977    o662 b976
2772  T       t978    o695 b978 b949  B       b977    t977
2773  B       b979    t978  T       t978    o661 b975 b977
2774  T       t979    o2 b951  B       b978    t978
2775  B       b980    t979  T       t979    o661 b972 b978
2776  T       t980    o694 b979 b4 b980  B       b979    t979
2777  B       b981    t980  T       t980    o661 b674 b979
2778  T       t981    o2 b981  B       b980    t980
2779  B       b982    t981  T       t981    o661 b672 b980
2780  T       t982    o694 b976 b4 b982  B       b981    t981
2781  B       b983    t982  T       t982    o661 b669 b981
2782  T       t983    o2 b983  B       b982    t982
2783  B       b984    t983  T       t983    o661 b667 b982
2784  T       t984    o694 b973 b4 b984  B       b983    t983
2785  B       b985    t984  T       t984    o b974 b4
2786  T       t985    o2 b985  B       b984    t984
2787  B       b986    t985  T       t985    o b971 b984
2788  T       t986    o694 b969 b4 b986  B       b985    t985
2789  B       b987    t986  T       t986    o b673 b985
2790  T       t987    o2 b987  B       b986    t986
2791  B       b988    t987  T       t987    o b671 b986
2792  T       t988    o704 b963 b4 b988  B       b987    t987
2793  B       b989    t988  T       t988    o b668 b987
2794  T       t989    o2 b989  B       b988    t988
2795  B       b990    t989  T       t989    o b666 b988
2796  T       t990    o704 b958 b4 b990  B       b989    t989
2797  B       b991    t990  T       t990    o695 b976 b989
2798  T       t991    o621 b959  B       b990    t990
2799  S       s991    t664 h h951 h952 h955  T       t991    o694 b990 b4 b703
2800  G       s991    t991  B       b991    t991
2801  B       b992    s991  H       h991    x t955
2802  T       t992    o695 b992 b949  H       h992    y t634
2803  B       b993    t992  T       t992    o580 b953 b925
2804  T       t993    o704 b993 b4 b990  B       b995    t992 y
2805  B       b994    t993  T       t995    o575 b576 b577 b995
 H       h994    x_1 t961  
 T       t994    o621 b964  
 S       s994    t664 h h951 h952 h955 h994  
 G       s994    t994  
 B       b995    s994  
 T       t995    o695 b995 b949  
2806  B       b996    t995  B       b996    t995
2807  S       s996    t671 h h951 h952 h955 h994  T       t998    o580 b954 b925
2808  G       s996    t967  B       b999    t998 y
2809  B       b997    s996  T       t999    o575 b576 b577 b999
 T       t997    o695 b997 b949  
 B       b998    t997  
 T       t998    o694 b998 b4 b988  
 B       b999    t998  
 T       t999    o2 b999  
2810  B       b1000   t999  B       b1000   t999
2811  T       t1000   o694 b996 b4 b1000  T       t1000   o635 b996 b1000
2812  B       b1001   t1000  B       b1003   t1000
2813  T       t1001   o621 b965  T       t1003   o635 b970 b1003
2814  S       s1001   t664 h h951 h952 h955 h994  B       b1006   t1003 s2
2815  G       s1001   t1001  T       t1006   o633 b634 b1006
2816  B       b1002   s1001  B       b1009   t1006 s1
2817  T       t1002   o695 b1002 b949  T       t1009   o633 b634 b1009
2818  B       b1003   t1002  T       t1011   o2 b991
 T       t1003   o694 b1003 b4 b1000  
 B       b1004   t1003  
 T       t1004   o623 b624 b964  
 S       s1004   t671 h h951 h952 h955 h994  
 G       s1004   t1004  
 B       b1005   s1004  
 T       t1005   o695 b1005 b949  
 B       b1006   t1005  
 T       t1006   o694 b1006 b4 b1000  
 B       b1007   t1006  
 T       t1007   o623 b626 b965  
 S       s1007   t671 h h951 h952 h955 h994  
 G       s1007   t1007  
 B       b1008   s1007  
 T       t1008   o695 b1008 b949  
 B       b1009   t1008  
 T       t1009   o694 b1009 b4 b1000  
 B       b1010   t1009  
 H       h1010   y t635  
 T       t1010   o580 b954 b638  
 B       b1011   t1010  
 T       t1011   o580 b954 b630  
2819  B       b1012   t1011  B       b1012   t1011
2820  T       t1012   o580 b954 b636  T       t1032   o580 b953 b630
2821    B       b1033   t1032
2822    T       t1036   o629 b1033 b626
2823    B       b1038   t1036
2824    T       t1038   o635 b635 b1038
2825    B       b1039   t1038 a
2826    T       t1039   o633 b634 b1039
2827    H       h1039   y_2 t1039
2828    T       t1040   o580 b953 b636
2829    B       b1040   t1040
2830    T       t1041   o623 b626 b537 b1033 b1040
2831    B       b1041   t1041
2832    T       t1042   o635 b3875 b1041
2833    B       b1042   t1042
2834    T       t1043   o635 b637 b1042
2835    B       b1043   t1043
2836    T       t1044   o635 b635 b1043
2837    B       b1044   t1044 b
2838    T       t1045   o633 b634 b1044
2839    B       b1045   t1045 a
2840    T       t1046   o633 b634 b1045
2841    H       h1046   y_3 t1046
2842    T       t1047   o580 b953 b638
2843    B       b1047   t1047
2844    T       t1048   o637 b577 b1033 b1040
2845    B       b1048   t1048
2846    T       t1049   o623 b626 b537 b1047 b1048
2847    B       b1049   t1049
2848    T       t1050   o635 b637 b1049
2849    B       b1050   t1050
2850    T       t1051   o635 b635 b1050
2851    B       b1051   t1051 b
2852    T       t1052   o633 b634 b1051
2853    B       b1052   t1052 a
2854    T       t1053   o633 b634 b1052
2855    H       h1053   z_1 t1053
2856    T       t1055   o580 b954 b409
2857    B       b1055   t1055
2858    T       t1056   o580 b954 b411
2859    B       b1056   t1056
2860    T       t1058   o623 b626 b537 b1055 b1056
2861    B       b1060   t1046
2862    B       b1061   t1053
2863    T       t1061   o619 b1060 b1061
2864    H       h1061   z t1061
2865    B       b1064   t1039
2866    B       b1065   t1061
2867    T       t1065   o619 b1064 b1065
2868    H       h1065   z_1 t1065
2869    B       b1068   t1065
2870    T       t1068   o619 b621 b1068
2871    H       h1068   z t1068
2872    B       b1071   t1068
2873    T       t1071   o619 b620 b1071
2874    H       h1071   x_1 t1071
2875    H       h1073   x_1 t995
2876    T       t1090   o580 b954 b528
2877    B       b1091   t1090
2878    T       t1091   o580 b954 b519
2879    B       b1092   t1091
2880    T       t1092   o580 b954 b526
2881    B       b1093   t1092
2882    T       t1093   o637 b577 b1092 b1093
2883    B       b1094   t1093
2884    T       t1094   o623 b626 b537 b1091 b1094
2885    T       t1123   o580 b953 b409
2886    B       b1124   t1123
2887    T       t1124   o580 b953 b411
2888    B       b1125   t1124
2889    T       t1125   o623 b626 b537 b1124 b1125
2890    H       h1125   y_4 t1125
2891    P       p598    Var z1
2892    O       o598    var p598
2893    T       t599    o598
2894    B       b599    t599
2895    T       t605    o580 b599 b593
2896    B       b606    t605
2897    T       t606    o629 b606 b626
2898    S       s606    t671 h h586 h587 h598
2899    G       s606    t606
2900    B       b607    s606
2901    T       t607    o662 b607
2902    B       b608    t607
2903    H       h615    z3 t634
2904    H       h616    x3 t410
2905    H       h617    y3 t412
2906    H       h618    v t435
2907    P       p619    Var z3
2908    O       o622    var p619
2909    T       t656    o622
2910    B       b656    t656
2911    T       t657    o580 b409 b656
2912    B       b657    t657
2913    T       t675    o580 b411 b656
2914    B       b676    t675
2915    T       t676    o623 b626 b537 b657 b676
2916    S       s677    t671 h h615 h408 h409 h616 h617 h618
2917    G       s677    t676
2918    B       b678    s677
2919    T       t678    o662 b678
2920    B       b683    t678
2921    T       t683    o1656 b624 b3216 b2735
2922    S       s683    t671 h
2923    G       s683    t683
2924    B       b684    s683
2925    T       t684    o662 b684
2926    B       b685    t684
2927    T       t685    o661 b683 b685
2928    B       b686    t685
2929    T       t780    o b678 b4
2930    B       b781    t780
2931    H       h805    x t3864
2932    H       h806    x_1 t3865
2933    T       t806    o580 b630 b925
2934    B       b807    t806 y
2935    T       t807    o575 b576 b577 b807
2936    H       h807    x_2 t807
2937    T       t808    o580 b636 b528
2938    B       b808    t808
2939    T       t809    o580 b636 b519
2940    B       b809    t809
2941    T       t810    o580 b636 b526
2942    B       b810    t810
2943    T       t811    o637 b577 b809 b810
2944    B       b811    t811
2945    T       t812    o623 b626 b537 b808 b811
2946    S       s812    t671 h h704 h705 h805 h806 h807 h518 h519 h520 h527
2947    G       s812    t812
2948    B       b812    s812
2949    T       t814    o580 b636 b925
2950    B       b814    t814 y
2951    T       t815    o575 b576 b577 b814
2952    S       s815    t671 h h704 h705 h805 h806 h807
2953    G       s815    t815
2954    B       b815    s815
2955    B       b817    t807
2956    B       b818    t815
2957    T       t831    o635 b817 b818
2958    S       s832    t671 h h704 h705 h805 h806
2959    G       s832    t831
2960    B       b883    s832
2961    B       b885    t831
2962    T       t885    o635 b3875 b885
2963    S       s885    t671 h h704 h705 h805
2964    G       s885    t885
2965    B       b886    s885
2966    B       b3879   t3864
2967    B       b897    t885
2968    T       t897    o635 b3879 b897
2969    S       s897    t671 h h704 h705
2970    G       s897    t897
2971    B       b899    s897
2972    B       b901    t897 b
2973    T       t901    o633 b634 b901
2974    S       s901    t671 h h704
2975    G       s901    t901
2976    B       b902    s901
2977    B       b904    t901 a
2978    T       t904    o633 b634 b904
2979    S       s904    t671 h
2980    G       s904    t904
2981    B       b908    s904
2982    P       p1023   Var a_1
2983    O       o1023   var p1023
2984    T       t1023   o1023
2985    B       b1023   t1023
2986    T       t1024   o629 b1023 b624
2987    B       b1024   t1024
2988    T       t1033   o580 b630 b1023
2989    B       b1037   t1033
2990    T       t1057   o629 b1037 b626
2991    B       b1421   t1057
2992    T       t1437   o635 b1024 b1421
2993    B       b1550   t1437 a_1
2994    T       t1550   o633 b634 b1550
2995    H       h1550   y_2 t1550
2996    T       t1551   o623 b624 b3216 b1023 b636
2997    B       b1551   t1551
2998    T       t1553   o580 b630 b636
2999    B       b1553   t1553
3000    T       t1554   o623 b626 b537 b1037 b1553
3001    B       b1554   t1554
3002    T       t1555   o635 b1551 b1554
3003    B       b1555   t1555
3004    T       t1556   o635 b637 b1555
3005    B       b1556   t1556
3006    T       t1557   o635 b1024 b1556
3007    B       b1557   t1557 b
3008    T       t1558   o633 b634 b1557
3009    B       b1558   t1558 a_1
3010    T       t1562   o633 b634 b1558
3011    H       h1562   y_3 t1562
3012    T       t1563   o637 b576 b1023 b636
3013    B       b1563   t1563
3014    T       t1564   o580 b630 b1563
3015    B       b1564   t1564
3016    T       t1565   o637 b577 b1037 b1553
3017    B       b1565   t1565
3018    T       t1566   o623 b626 b537 b1564 b1565
3019    B       b1566   t1566
3020    T       t1567   o635 b637 b1566
3021    B       b1567   t1567
3022    T       t1568   o635 b1024 b1567
3023    B       b1568   t1568 b
3024    T       t1569   o633 b634 b1568
3025    B       b1569   t1569 a_1
3026    T       t1570   o633 b634 b1569
3027    H       h1570   z_1 t1570
3028    S       s1570   t671 h h704 h705 h805 h806 h1033 h1034 h1550 h1562 h1570 h518 h519 h520 h527
3029    G       s1570   t812
3030    B       b1570   s1570
3031    B       b1572   t1562
3032    B       b1599   t1570
3033    T       t1599   o619 b1572 b1599
3034    H       h1599   z t1599
3035    S       s1599   t671 h h704 h705 h805 h806 h1033 h1034 h1550 h1599 h518 h519 h520 h527
3036    G       s1599   t812
3037    B       b1600   s1599
3038    B       b1828   t1550
3039    B       b1829   t1599
3040    T       t1829   o619 b1828 b1829
3041    H       h1829   z_1 t1829
3042    S       s1829   t671 h h704 h705 h805 h806 h1033 h1034 h1829 h518 h519 h520 h527
3043    G       s1829   t812
3044    B       b1830   s1829
3045    B       b1834   t1829
3046    T       t1834   o619 b621 b1834
3047    H       h1834   z t1834
3048    S       s1834   t671 h h704 h705 h805 h806 h1033 h1834 h518 h519 h520 h527
3049    G       s1834   t812
3050    B       b1835   s1834
3051    B       b1840   t1834
3052    T       t1840   o619 b620 b1840
3053    H       h1840   x_2 t1840
3054    S       s1840   t671 h h704 h705 h805 h806 h1840 h518 h519 h520 h527
3055    G       s1840   t812
3056    B       b1842   s1840
3057    P       p2575   String "instHypT [<< 'e >>; << 'g >>] 10 thenT autoT thenT dT 15 ttca thenT dT 15 ttca"
3058    O       o2575   ext_rule p2575
3059    T       t2612   o580 b630 b528
3060    B       b2613   t2612
3061    T       t2613   o580 b630 b519
3062    B       b2614   t2613
3063    T       t2614   o580 b630 b526
3064    B       b2615   t2614
3065    T       t2615   o637 b577 b2614 b2615
3066    B       b2616   t2615
3067    T       t2616   o623 b626 b537 b2613 b2616
3068    H       h2616   y_5 t2616
3069    S       s2616   t671 h h704 h705 h805 h806 h1033 h1034 h1550 h1562 h1570 h518 h519 h520 h527 h2616
3070    G       s2616   t812
3071    B       b2621   s2616
3072    B       b2623   t527
3073    B       b2624   t2616
3074    T       t2624   o635 b2623 b2624
3075    H       h2624   y_4 t2624
3076    S       s2624   t671 h h704 h705 h805 h806 h1033 h1034 h1550 h1562 h1570 h518 h519 h520 h527 h2624 h2616
3077    G       s2624   t812
3078    B       b2625   s2624
3079    S       s2626   t671 h h704 h705 h805 h806 h1033 h1034 h1550 h1562 h1570 h518 h519 h520 h527 h2624
3080    G       s2626   t812
3081    B       b2636   s2626
3082    B       b2640   t520
3083    B       b2641   t2624
3084    T       t2641   o635 b2640 b2641
3085    H       h2641   w_1 t2641
3086    S       s2642   t671 h h704 h705 h805 h806 h1033 h1034 h1550 h1562 h1570 h518 h519 h520 h527 h2641 h2624
3087    G       s2642   t812
3088    B       b2649   s2642
3089    S       s2650   t671 h h704 h705 h805 h806 h1033 h1034 h1550 h1562 h1570 h518 h519 h520 h527 h2641
3090    G       s2650   t812
3091    B       b2651   s2650
3092    T       t2652   o637 b576 b519 b636
3093    B       b2653   t2652
3094    T       t2653   o580 b630 b2653
3095    B       b2654   t2653
3096    T       t2654   o637 b577 b2614 b1553
3097    B       b2655   t2654
3098    T       t2655   o623 b626 b537 b2654 b2655
3099    B       b2656   t2655
3100    T       t2656   o635 b637 b2656
3101    B       b2657   t2656
3102    T       t2658   o635 b2640 b2657
3103    B       b2659   t2658 b
3104    T       t2659   o633 b634 b2659
3105    H       h2659   w t2659
3106    S       s2659   t671 h h704 h705 h805 h806 h1033 h1034 h1550 h1562 h1570 h518 h519 h520 h527 h2659 h2641
3107    G       s2659   t812
3108    B       b2660   s2659
3109    S       s2664   t671 h h704 h705 h805 h806 h1033 h1034 h1550 h1562 h1570 h518 h519 h520 h527 h2659
3110    G       s2664   t812
3111    B       b2665   s2664
3112    T       t2666   o b526 b4
3113    B       b2667   t2666
3114    T       t2667   o1207 b2667
3115    B       b2668   t2667
3116    T       t2668   o1206 b2668
3117    B       b2669   t2668
3118    T       t2669   o b2669 b1204
3119    B       b2670   t2669
3120    T       t2670   o b519 b4
3121    B       b2671   t2670
3122    T       t2671   o1207 b2671
3123    B       b2672   t2671
3124    T       t2672   o1206 b2672
3125    B       b2673   t2672
3126    T       t2673   o b2673 b1204
3127    B       b2674   t2673
3128    P       p2691   String "equivSubstT << equiv{car{'g2}; eqG{'g2}; 'f['a; op{'g1; 'e; 'g}]; 'f['b; op{'g1; 'e; 'g}]} >> 15 thenT autoT"
3129    O       o2691   ext_rule p2691
3130    T       t2691   o623 b626 b537 b2613 b808
3131    S       s2691   t671 h h704 h705 h805 h806 h1033 h1034 h1550 h1562 h1570 h518 h519 h520 h527 h2616
3132    G       s2691   t2691
3133    B       b2692   s2691
3134    T       t2695   o623 b626 b537 b808 b2616
3135    H       h2695   z t2695
3136    S       s2695   t671 h h704 h705 h805 h806 h1033 h1034 h1550 h1562 h1570 h518 h519 h520 h527 h2616 h2695
3137    G       s2695   t812
3138    B       b2698   s2695
3139    B       b3214   t410
3140    B       b3215   t412
3141    B       b3221   t435
3142    B       b1128   t1125
3143    T       t1128   o635 b3221 b1128
3144    H       h1128   y_5 t1128
3145    B       b1133   t1128
3146    T       t1133   o635 b3215 b1133
3147    H       h1133   y_4 t1133
3148    B       b1138   t1133
3149    T       t1138   o635 b3214 b1138
3150    H       h1138   w_1 t1138
3151    T       t1142   o623 b624 b3216 b409 b636
3152    B       b1143   t1142
3153    T       t1143   o623 b626 b537 b1124 b1040
3154    B       b1150   t1143
3155    T       t1150   o635 b1143 b1150
3156    B       b1151   t1150
3157    T       t1151   o635 b637 b1151
3158    B       b1152   t1151
3159    T       t1152   o635 b3214 b1152
3160    B       b1153   t1152 b
3161    T       t1153   o633 b634 b1153
3162    H       h1153   w t1153
3163    T       t1157   o b411 b4
3164    B       b1158   t1157
3165    T       t1158   o1207 b1158
3166    B       b1159   t1158
3167    T       t1159   o1206 b1159
3168    B       b1160   t1159
3169    T       t1160   o b1160 b1204
3170    B       b1161   t1160
3171    T       t1161   o b409 b4
3172    B       b1162   t1161
3173    T       t1162   o1207 b1162
3174    B       b1163   t1162
3175    T       t1163   o1206 b1163
3176    B       b1164   t1163
3177    T       t1164   o b1164 b1204
3178    B       b1165   t1164
3179    T       t1188   o952 b1124 b1055
3180    T       t1197   o1049 b1124 b1055
3181    T       t1200   o623 b626 b537 b1055 b1125
3182    T       t1311   o580 b953 b528
3183    B       b1312   t1311
3184    T       t1312   o580 b953 b519
3185    B       b1313   t1312
3186    T       t1313   o580 b953 b526
3187    B       b1314   t1313
3188    T       t1314   o637 b577 b1313 b1314
3189    B       b1320   t1314
3190    T       t1320   o623 b626 b537 b1312 b1320
3191    H       h1320   y_5 t1320
3192    B       b1323   t1320
3193    T       t1323   o635 b2623 b1323
3194    H       h1323   y_4 t1323
3195    B       b1328   t1323
3196    T       t1328   o635 b2640 b1328
3197    H       h1328   w_1 t1328
3198    T       t1332   o580 b953 b2653
3199    B       b1333   t1332
3200    T       t1333   o637 b577 b1313 b1040
3201    B       b1334   t1333
3202    T       t1334   o623 b626 b537 b1333 b1334
3203    B       b1335   t1334
3204    T       t1335   o635 b637 b1335
3205    B       b1336   t1335
3206    T       t1336   o635 b2640 b1336
3207    B       b1337   t1336 b
3208    T       t1337   o633 b634 b1337
3209    H       h1337   w t1337
3210    P       p1358   String "assertT << all x: set. all y: set. isset{'f['x; 'y]} >> thenT autoT"
3211    O       o1358   ext_rule p1358
3212    T       t1358   o580 b581 b925
3213    B       b1359   t1358
3214    T       t1359   o621 b1359
3215    S       s10     t671 h h678 h992
3216    G       s10     t1359
3217    B       b406    s10
3218    T       t406    o695 b406 b989
3219    B       b407    t406
3220    B       b1362   t1359 y
3221    T       t1362   o633 b634 b1362
3222    S       s407    t671 h h678
3223    G       s407    t1362
3224    B       b410    s407
3225    T       t574    o695 b410 b989
3226    B       b580    t574
3227    B       b1365   t1362 x
3228    T       t1365   o633 b634 b1365
3229    S       s580    t671 h
3230    G       s580    t1365
3231    B       b584    s580
3232    T       t584    o695 b584 b989
3233    B       b687    t584
3234    T       t687    o2266 b687 b711 b1012
3235    B       b688    t687
3236    T       t688    o2 b688
3237    B       b689    t688
3238    T       t689    o694 b580 b711 b689
3239    B       b690    t689
3240    T       t690    o2 b690
3241    B       b775    t690
3242    T       t775    o694 b407 b4 b775
3243    B       b776    t775
3244    H       h1373   v t1365
3245    S       s776    t671 h h1373
3246    G       s776    t976
3247    B       b780    s776
3248    T       t782    o695 b780 b989
3249    B       b968    t782
3250    T       t968    o694 b968 b4 b1012
3251    B       b1021   t968
3252    T       t1021   o b1021 b4
3253    B       b1022   t1021
3254    T       t1022   o b776 b1022
3255    B       b1046   t1022
3256    T       t1060   o693 b991 b1046
3257    B       b1437   t1060
3258    P       p1437   String "assumT 6 ttca thenT rwh unfold_fun_set 4 thenT instHypT [<< 'y >>; << 'x >>; << 'x >>] 4 ttca thenT dT 5 ttca thenT rwh unfold_equal 5 ttca"
3259    O       o1437   ext_rule p1437
3260    T       t1507   o693 b776 b4
3261    B       b2179   t1507
3262    T       t2179   o1437 b692 b2179 b4 b4
3263    B       b2461   t2179
3264    P       p2462   String "rwh unfold_fun_prop 0 thenT autoT thenT rwh unfold_hom 6 thenT autoT"
3265    O       o2462   ext_rule p2462
3266    S       s2462   t671 h h1373 h951 h952 h991 h1033 h1034 h1039 h1046 h1053 h408 h409 h410 h412 h435
3267    G       s2462   t1058
3268    B       b2620   s2462
3269    T       t2620   o695 b2620 b989
3270    B       b2627   t2620
3271    S       s2627   t671 h h1373 h951 h952 h991 h1033 h1034 h1039 h1061 h408 h409 h410 h412 h435
3272    G       s2627   t1058
3273    B       b2628   s2627
3274    T       t2628   o695 b2628 b989
3275    B       b2629   t2628
3276    S       s2629   t671 h h1373 h951 h952 h991 h1033 h1034 h1065 h408 h409 h410 h412 h435
3277    G       s2629   t1058
3278    B       b2630   s2629
3279    T       t2630   o695 b2630 b989
3280    B       b2631   t2630
3281    S       s2631   t671 h h1373 h951 h952 h991 h1033 h1068 h408 h409 h410 h412 h435
3282    G       s2631   t1058
3283    B       b2632   s2631
3284    T       t2632   o695 b2632 b989
3285    B       b2633   t2632
3286    S       s2633   t671 h h1373 h951 h952 h991 h1071 h408 h409 h410 h412 h435
3287    G       s2633   t1058
3288    B       b2634   s2633
3289    T       t2634   o695 b2634 b989
3290    B       b2635   t2634
3291    S       s2635   t671 h h1373 h951 h952 h991 h1073 h408 h409 h410 h412 h435
3292    G       s2635   t1058
3293    B       b2696   s2635
3294    T       t2696   o695 b2696 b989
3295    B       b2697   t2696
3296    S       s2697   t671 h h1373 h951 h952 h991 h1073
3297    G       s2697   t999
3298    B       b2705   s2697
3299    T       t2705   o695 b2705 b989
3300    B       b2716   t2705
3301    S       s2716   t671 h h1373 h951 h952 h991
3302    G       s2716   t1000
3303    B       b2717   s2716
3304    T       t2717   o695 b2717 b989
3305    B       b2718   t2717
3306    S       s2718   t671 h h1373 h951 h952
3307    G       s2718   t1003
3308    B       b2719   s2718
3309    T       t2719   o695 b2719 b989
3310    B       b2720   t2719
3311    S       s2720   t671 h h1373 h951
3312    G       s2720   t1006
3313    B       b2721   s2720
3314    T       t2721   o695 b2721 b989
3315    B       b2722   t2721
3316    S       s2722   t671 h h1373
3317    G       s2722   t1009
3318    B       b2723   s2722
3319    T       t2723   o695 b2723 b989
3320    B       b2724   t2723
3321    T       t2724   o2 b1021
3322    B       b2725   t2724
3323    T       t2725   o694 b2724 b711 b2725
3324    B       b2726   t2725
3325    T       t2726   o2 b2726
3326    B       b2727   t2726
3327    T       t2739   o694 b2722 b711 b2727
3328    B       b2801   t2739
3329    T       t2801   o2 b2801
3330    B       b4095   t2801
3331    T       t4095   o694 b2720 b711 b4095
3332    B       b4247   t4095
3333    T       t4247   o2 b4247
3334    B       b4248   t4247
3335    T       t4248   o694 b2718 b711 b4248
3336    B       b4250   t4248
3337    T       t4250   o2 b4250
3338    B       b4251   t4250
3339    T       t4251   o694 b2716 b711 b4251
3340    B       b4252   t4251
3341    T       t4252   o2 b4252
3342    B       b4253   t4252
3343    T       t4253   o694 b2697 b4 b4253
3344    B       b4254   t4253
3345    T       t4254   o2 b4254
3346    B       b4255   t4254
3347    T       t4255   o694 b2635 b4 b4255
3348    B       b4264   t4255
3349    T       t4264   o2 b4264
3350    B       b4265   t4264
3351    T       t4265   o694 b2633 b4 b4265
3352    B       b4266   t4265
3353    T       t4266   o2 b4266
3354    B       b4267   t4266
3355    T       t4267   o694 b2631 b4 b4267
3356    B       b4268   t4267
3357    T       t4268   o2 b4268
3358    B       b4269   t4268
3359    T       t4269   o694 b2629 b4 b4269
3360    B       b4270   t4269
3361    T       t4270   o2 b4270
3362    B       b4271   t4270
3363    T       t4271   o694 b2627 b4 b4271
3364    B       b4272   t4271
3365    S       s4272   t671 h h1373 h951 h952 h991 h1033 h1034 h1039 h1046 h1053 h518 h519 h520 h527
3366    G       s4272   t1094
3367    B       b4273   s4272
3368    T       t4273   o695 b4273 b989
3369    B       b4274   t4273
3370    S       s4274   t671 h h1373 h951 h952 h991 h1033 h1034 h1039 h1061 h518 h519 h520 h527
3371    G       s4274   t1094
3372    B       b4275   s4274
3373    T       t4275   o695 b4275 b989
3374    B       b4276   t4275
3375    S       s4276   t671 h h1373 h951 h952 h991 h1033 h1034 h1065 h518 h519 h520 h527
3376    G       s4276   t1094
3377    B       b4277   s4276
3378    T       t4277   o695 b4277 b989
3379    B       b4278   t4277
3380    S       s4278   t671 h h1373 h951 h952 h991 h1033 h1068 h518 h519 h520 h527
3381    G       s4278   t1094
3382    B       b4279   s4278
3383    T       t4279   o695 b4279 b989
3384    B       b4287   t4279
3385    S       s4287   t671 h h1373 h951 h952 h991 h1071 h518 h519 h520 h527
3386    G       s4287   t1094
3387    B       b4290   s4287
3388    T       t4290   o695 b4290 b989
3389    B       b4294   t4290
3390    S       s4294   t671 h h1373 h951 h952 h991 h1073 h518 h519 h520 h527
3391    G       s4294   t1094
3392    B       b4297   s4294
3393    T       t4297   o695 b4297 b989
3394    B       b4300   t4297
3395    T       t4300   o694 b4300 b4 b4253
3396    B       b4303   t4300
3397    T       t4303   o2 b4303
3398    B       b4306   t4303
3399    T       t4306   o694 b4294 b4 b4306
3400    B       b4307   t4306
3401    T       t4307   o2 b4307
3402    B       b4308   t4307
3403    T       t4308   o694 b4287 b4 b4308
3404    B       b4309   t4308
3405    T       t4309   o2 b4309
3406    B       b4310   t4309
3407    T       t4310   o694 b4278 b4 b4310
3408    B       b4311   t4310
3409    T       t4311   o2 b4311
3410    B       b4312   t4311
3411    T       t4312   o694 b4276 b4 b4312
3412    B       b4313   t4312
3413    T       t4313   o2 b4313
3414    B       b4314   t4313
3415    T       t4314   o694 b4274 b4 b4314
3416    B       b4315   t4314
3417    T       t4315   o b4315 b4
3418    B       b4316   t4315
3419    T       t4316   o b4272 b4316
3420    B       b4317   t4316
3421    T       t4317   o693 b1021 b4317
3422    B       b4318   t4317
3423    P       p4318   String "instHypT [<< 'c >>; << 'd >>] 9 thenT autoT thenT dT 16 ttca thenT dT 16 ttca thenT dT 16 ttca"
3424    O       o4318   ext_rule p4318
3425    S       s4318   t671 h h1373 h951 h952 h991 h1033 h1034 h1039 h1046 h1053 h408 h409 h410 h412 h435 h1125
3426    G       s4318   t1058
3427    B       b4319   s4318
3428    T       t4319   o695 b4319 b989
3429    B       b4320   t4319
3430    S       s4320   t671 h h1373 h951 h952 h991 h1033 h1034 h1039 h1046 h1053 h408 h409 h410 h412 h435 h1128 h1125
3431    G       s4320   t1058
3432    B       b4321   s4320
3433    T       t4321   o695 b4321 b989
3434    B       b4322   t4321
3435    S       s4322   t671 h h1373 h951 h952 h991 h1033 h1034 h1039 h1046 h1053 h408 h409 h410 h412 h435 h1128
3436    G       s4322   t1058
3437    B       b4340   s4322
3438    T       t4340   o695 b4340 b989
3439    B       b4344   t4340
3440    S       s4344   t671 h h1373 h951 h952 h991 h1033 h1034 h1039 h1046 h1053 h408 h409 h410 h412 h435 h1133 h1128
3441    G       s4344   t1058
3442    B       b4348   s4344
3443    T       t4348   o695 b4348 b989
3444    B       b4351   t4348
3445    S       s4351   t671 h h1373 h951 h952 h991 h1033 h1034 h1039 h1046 h1053 h408 h409 h410 h412 h435 h1133
3446    G       s4351   t1058
3447    B       b4354   s4351
3448    T       t4354   o695 b4354 b989
3449    B       b4355   t4354
3450    S       s4355   t671 h h1373 h951 h952 h991 h1033 h1034 h1039 h1046 h1053 h408 h409 h410 h412 h435 h1138 h1133
3451    G       s4355   t1058
3452    B       b4356   s4355
3453    T       t4356   o695 b4356 b989
3454    B       b4357   t4356
3455    S       s4357   t671 h h1373 h951 h952 h991 h1033 h1034 h1039 h1046 h1053 h408 h409 h410 h412 h435 h1138
3456    G       s4357   t1058
3457    B       b4358   s4357
3458    T       t4358   o695 b4358 b989
3459    B       b4359   t4358
3460    S       s4359   t671 h h1373 h951 h952 h991 h1033 h1034 h1039 h1046 h1053 h408 h409 h410 h412 h435 h1153 h1138
3461    G       s4359   t1058
3462    B       b4360   s4359
3463    T       t4360   o695 b4360 b989
3464    B       b4361   t4360
3465    S       s4361   t671 h h1373 h951 h952 h991 h1033 h1034 h1039 h1046 h1053 h408 h409 h410 h412 h435 h1153
3466    G       s4361   t1058
3467    B       b4362   s4361
3468    T       t4362   o695 b4362 b989
3469    B       b4363   t4362
3470    T       t4363   o694 b2627 b1165 b4271
3471    B       b4364   t4363
3472    T       t4364   o2 b4364
3473    B       b4365   t4364
3474    T       t4365   o694 b4363 b1161 b4365
3475    B       b4366   t4365
3476    T       t4371   o2 b4366
3477    B       b4372   t4371
3478    T       t4372   o694 b4361 b1204 b4372
3479    B       b4375   t4372
3480    T       t4375   o2 b4375
3481    B       b4377   t4375
3482    T       t4377   o694 b4359 b4 b4377
3483    B       b4380   t4377
3484    T       t4380   o2 b4380
3485    B       b4382   t4380
3486    T       t4388   o694 b4357 b4 b4382
3487    B       b4389   t4388
3488    T       t4389   o2 b4389
3489    B       b4391   t4389
3490    T       t4391   o694 b4355 b4 b4391
3491    B       b4392   t4391
3492    T       t4392   o2 b4392
3493    B       b4393   t4392
3494    T       t4393   o694 b4351 b4 b4393
3495    B       b4394   t4393
3496    T       t4394   o2 b4394
3497    B       b4395   t4394
3498    T       t4395   o694 b4344 b4 b4395
3499    B       b4396   t4395
3500    T       t4396   o2 b4396
3501    B       b4397   t4396
3502    T       t4397   o694 b4322 b4 b4397
3503    B       b4398   t4397
3504    T       t4398   o2 b4398
3505    B       b4399   t4398
3506    T       t4399   o694 b4320 b4 b4399
3507    B       b4400   t4399
3508    T       t4400   o b4400 b4
3509    B       b4401   t4400
3510    T       t4401   o693 b4272 b4401
3511    B       b4402   t4401
3512    P       p4402   String "setSubstT << equal{'f['s1; 'c]; 'f['s2; 'c]} >> 16 thenT autoT"
3513    O       o4402   ext_rule p4402
3514    S       s4402   t671 h h1373 h951 h952 h991 h1033 h1034 h1039 h1046 h1053 h408 h409 h410 h412 h435 h1125
3515    G       s4402   t1197
3516    B       b4403   s4402
3517    T       t4403   o695 b4403 b989
3518    B       b4404   t4403
3519    S       s4404   t671 h h1373 h951 h952 h991 h1033 h1034 h1039 h1046 h1053 h408 h409 h410 h412 h435 h1125
3520    G       s4404   t1188
3521    B       b4405   s4404
3522    T       t4405   o695 b4405 b989
3523    B       b4406   t4405
3524    T       t4406   o2 b4400
3525    B       b4407   t4406
3526    T       t4407   o1080 b4406 b711 b4407
3527    B       b4408   t4407
3528    T       t4409   o2 b4408
3529    B       b4410   t4409
3530    T       t4410   o1080 b4404 b4 b4410
3531    B       b4411   t4410
3532    H       h4411   v_1 t1200
3533    S       s4411   t671 h h1373 h951 h952 h991 h1033 h1034 h1039 h1046 h1053 h408 h409 h410 h412 h435 h1125 h4411
3534    G       s4411   t1058
3535    B       b4412   s4411
3536    T       t4413   o695 b4412 b989
3537    B       b4414   t4413
3538    T       t4414   o694 b4414 b4 b4407
3539    B       b4415   t4414
3540    T       t4415   o b4415 b4
3541    B       b4416   t4415
3542    T       t4416   o b4411 b4416
3543    B       b4417   t4416
3544    T       t4417   o693 b4400 b4417
3545    B       b4418   t4417
3546    T       t1383   o952 b1312 b1091
3547    T       t1389   o621 b1091
3548    T       t1395   o623 b626 b537 b1091 b1320
3549    T       t1441   o1049 b1320 b1094
3550    T       t1443   o952 b1320 b1094
3551    T       t1457   o629 b1091 b626
3552    P       p1464   String "setSubstT << equal{'f['s1; 'e]; 'f['s2; 'e]} >> 0 thenT autoT"
3553    O       o1464   ext_rule p1464
3554    T       t1464   o1049 b1313 b1092
3555    T       t1466   o952 b1313 b1092
3556    T       t1472   o637 b577 b1092 b1314
3557    B       b1473   t1472
3558    T       t1473   o1049 b1473 b1094
3559    P       p1479   String "setSubstT << equal{'s1; 's2} >> 0 ttca"
3560    O       o1479   ext_rule p1479
3561    T       t4418   o693 b4411 b4
3562    B       b4429   t4418
3563    T       t4429   o1479 b692 b4429 b4 b4
3564    B       b4432   t4429
3565    P       p4432   String "setSubstT << equal{'f['s1; 'd]; 'f['s2; 'd]} >> 17 thenT autoT thenT setSubstT << equal{'s1; 's2} >> 0 ttca"
3566    O       o4432   ext_rule p4432
3567    T       t4432   o693 b4415 b4
3568    B       b4434   t4432
3569    T       t4434   o4432 b692 b4434 b4 b4
3570    B       b4437   t4434
3571    T       t4437   o b4437 b4
3572    B       b4439   t4437
3573    T       t4439   o b4432 b4439
3574    B       b4441   t4439
3575    T       t4441   o4402 b692 b4418 b4441 b4
3576    B       b4442   t4441
3577    T       t4442   o b4442 b4
3578    B       b4443   t4442
3579    T       t4443   o4318 b692 b4402 b4443 b4
3580    B       b4444   t4443
3581    S       s4444   t671 h h1373 h951 h952 h991 h1033 h1034 h1039 h1046 h1053 h518 h519 h520 h527 h1320
3582    G       s4444   t1094
3583    B       b4445   s4444
3584    T       t4445   o695 b4445 b989
3585    B       b4446   t4445
3586    S       s4446   t671 h h1373 h951 h952 h991 h1033 h1034 h1039 h1046 h1053 h518 h519 h520 h527 h1323 h1320
3587    G       s4446   t1094
3588    B       b4447   s4446
3589    T       t4447   o695 b4447 b989
3590    B       b4448   t4447
3591    S       s4448   t671 h h1373 h951 h952 h991 h1033 h1034 h1039 h1046 h1053 h518 h519 h520 h527 h1323
3592    G       s4448   t1094
3593    B       b4449   s4448
3594    T       t4449   o695 b4449 b989
3595    B       b4450   t4449
3596    S       s4450   t671 h h1373 h951 h952 h991 h1033 h1034 h1039 h1046 h1053 h518 h519 h520 h527 h1328 h1323
3597    G       s4450   t1094
3598    B       b4451   s4450
3599    T       t4451   o695 b4451 b989
3600    B       b4452   t4451
3601    S       s4452   t671 h h1373 h951 h952 h991 h1033 h1034 h1039 h1046 h1053 h518 h519 h520 h527 h1328
3602    G       s4452   t1094
3603    B       b4453   s4452
3604    T       t4453   o695 b4453 b989
3605    B       b4454   t4453
3606    S       s4454   t671 h h1373 h951 h952 h991 h1033 h1034 h1039 h1046 h1053 h518 h519 h520 h527 h1337 h1328
3607    G       s4454   t1094
3608    B       b4455   s4454
3609    T       t4455   o695 b4455 b989
3610    B       b4456   t4455
3611    S       s4456   t671 h h1373 h951 h952 h991 h1033 h1034 h1039 h1046 h1053 h518 h519 h520 h527 h1337
3612    G       s4456   t1094
3613    B       b4457   s4456
3614    T       t4457   o695 b4457 b989
3615    B       b4458   t4457
3616    T       t4458   o694 b4274 b2674 b4314
3617    B       b4459   t4458
3618    T       t4460   o2 b4459
3619    B       b4461   t4460
3620    T       t4473   o694 b4458 b2670 b4461
3621    B       b4474   t4473
3622    T       t4474   o2 b4474
3623    B       b4475   t4474
3624    T       t4475   o694 b4456 b1204 b4475
3625    B       b4476   t4475
3626    T       t4476   o2 b4476
3627    B       b4477   t4476
3628    T       t4477   o694 b4454 b4 b4477
3629    B       b4478   t4477
3630    T       t4478   o2 b4478
3631    B       b4479   t4478
3632    T       t4479   o694 b4452 b4 b4479
3633    B       b4480   t4479
3634    T       t4480   o2 b4480
3635    B       b4481   t4480
3636    T       t4481   o694 b4450 b4 b4481
3637    B       b4482   t4481
3638    T       t4483   o2 b4482
3639    B       b4484   t4483
3640    T       t4484   o694 b4448 b4 b4484
3641    B       b4485   t4484
3642    T       t4485   o2 b4485
3643    B       b4486   t4485
3644    T       t4487   o694 b4446 b4 b4486
3645    B       b4488   t4487
3646    T       t4490   o b4488 b4
3647    B       b4491   t4490
3648    T       t4491   o693 b4315 b4491
3649    B       b4492   t4491
3650    P       p4492   String "assertT << fun_set{x. 'f['x; op{'g1; 'e; 'g}]} >> thenT autoT"
3651    O       o4492   ext_rule p4492
3652    T       t4492   o580 b581 b528
3653    B       b4493   t4492 x
3654    T       t4493   o627 b4493
3655    S       s4493   t671 h h1373 h951 h952 h991 h1033 h1034 h1039 h1046 h1053 h518 h519 h520 h527 h1320
3656    G       s4493   t4493
3657    B       b4494   s4493
3658    T       t4494   o695 b4494 b989
3659    B       b4495   t4494
3660    T       t4495   o2 b4488
3661    B       b4496   t4495
3662    T       t4496   o2266 b4495 b4 b4496
3663    B       b4497   t4496
3664    H       h4497   v_1 t4493
3665    S       s4497   t671 h h1373 h951 h952 h991 h1033 h1034 h1039 h1046 h1053 h518 h519 h520 h527 h1320 h4497
3666    G       s4497   t1094
3667    B       b4498   s4497
3668    T       t4498   o695 b4498 b989
3669    B       b4499   t4498
3670    T       t4499   o694 b4499 b4 b4496
3671    B       b4500   t4499
3672    T       t4500   o b4500 b4
3673    B       b4501   t4500
3674    T       t4501   o b4497 b4501
3675    B       b4502   t4501
3676    T       t4502   o693 b4488 b4502
3677    B       b4503   t4502
3678    P       p4503   String "assumT 6 ttca thenT withT << op{'g1; 'e; 'g} >> (dT 16) ttca thenT rwh fold_isset 0 ttca"
3679    O       o4503   ext_rule p4503
3680    T       t4503   o693 b4497 b4
3681    B       b4504   t4503
3682    T       t4504   o4503 b692 b4504 b4 b4
3683    B       b4505   t4504
3684    P       p4505   String "setSubstT << equal{'f['s1; op{'g1; 'e; 'g}]; 'f['s2; op{'g1; 'e; 'g}]} >> 15 ttca"
3685    O       o4505   ext_rule p4505
3686    S       s4505   t671 h h1373 h951 h952 h991 h1033 h1034 h1039 h1046 h1053 h518 h519 h520 h527 h1320 h4497
3687    G       s4505   t1383
3688    B       b4506   s4505
3689    T       t4506   o695 b4506 b989
3690    B       b4507   t4506
3691    T       t4507   o2 b4500
3692    B       b4508   t4507
3693    T       t4508   o1080 b4507 b4 b4508
3694    B       b4509   t4508
3695    H       h4509   v_2 t1395
3696    S       s4509   t671 h h1373 h951 h952 h991 h1033 h1034 h1039 h1046 h1053 h518 h519 h520 h527 h1320 h4497 h4509
3697    G       s4509   t1094
3698    B       b4510   s4509
3699    T       t4510   o695 b4510 b989
3700    B       b4511   t4510
3701    T       t4511   o694 b4511 b4 b4508
3702    B       b4512   t4511
3703    T       t4512   o b4512 b4
3704    B       b4513   t4512
3705    T       t4513   o b4509 b4513
3706    B       b4514   t4513
3707    T       t4514   o693 b4500 b4514
3708    B       b4515   t4514
3709    P       p4515   String "rwh unfold_fun_set 16 thenT instHypT [<< 's1 >>; << 's2 >>] 16 ttca thenT dT 17 ttca"
3710    O       o4515   ext_rule p4515
3711    T       t4515   o693 b4509 b4
3712    B       b4516   t4515
3713    T       t4516   o4515 b692 b4516 b4 b4
3714    B       b4518   t4516
3715    P       p4518   String "setSubstT << equal{op{'g2; 'f['s1; 'e]; 'f['s1; 'g]}; op{'g2; 'f['s2; 'e]; 'f['s2; 'g]}} >> 17 thenT autoT thenT rwh unfold_equiv 17 ttca"
3716    O       o4518   ext_rule p4518
3717    B       b4519   t1389
3718    T       t4519   o621 b1320
3719    B       b4520   t4519
3720    T       t4520   o619 b4519 b4520
3721    B       b4521   t4520
3722    T       t4521   o619 b3026 b4521
3723    B       b4522   t4521
3724    T       t4522   o619 b1282 b4522
3725    B       b4523   t4522
3726    B       b4524   t1457
3727    T       t4524   o629 b1320 b626
3728    B       b4526   t4524
3729    T       t4526   o619 b4524 b4526
3730    B       b4528   t4526
3731    T       t4528   o619 b4523 b4528
3732    B       b4530   t4528
3733    T       t4530   o1292 b1091 b1320
3734    B       b4531   t4530
3735    T       t4531   o629 b4531 b537
3736    B       b4532   t4531
3737    T       t4532   o619 b4530 b4532
3738    H       h4532   v_2 t4532
3739    S       s4532   t671 h h1373 h951 h952 h991 h1033 h1034 h1039 h1046 h1053 h518 h519 h520 h527 h1320 h4497 h4532
3740    G       s4532   t1441
3741    B       b4533   s4532
3742    T       t4533   o695 b4533 b989
3743    B       b4534   t4533
3744    S       s4534   t671 h h1373 h951 h952 h991 h1033 h1034 h1039 h1046 h1053 h518 h519 h520 h527 h1320 h4497 h4509
3745    G       s4534   t1441
3746    B       b4535   s4534
3747    T       t4535   o695 b4535 b989
3748    B       b4536   t4535
3749    S       s4536   t671 h h1373 h951 h952 h991 h1033 h1034 h1039 h1046 h1053 h518 h519 h520 h527 h1320 h4497 h4509
3750    G       s4536   t1443
3751    B       b4537   s4536
3752    T       t4537   o695 b4537 b989
3753    B       b4538   t4537
3754    T       t4538   o2 b4512
3755    B       b4539   t4538
3756    T       t4539   o1080 b4538 b711 b4539
3757    B       b4540   t4539
3758    T       t4540   o2 b4540
3759    B       b4541   t4540
3760    T       t4541   o1080 b4536 b4 b4541
3761    B       b4542   t4541
3762    T       t4542   o2 b4542
3763    B       b4543   t4542
3764    T       t4543   o1080 b4534 b4 b4543
3765    B       b4544   t4543
3766    T       t4544   o b4544 b4
3767    B       b4545   t4544
3768    T       t4545   o693 b4512 b4545
3769    B       b4546   t4545
3770    H       h4546   y_7 t1281
3771    H       h4547   y_6 t3025
3772    H       h4548   y_8 t1389
3773    H       h4549   z_2 t4519
3774    H       h4550   y_4 t1457
3775    H       h4551   z_3 t4524
3776    H       h4552   z t4531
3777    S       s4552   t671 h h1373 h951 h952 h991 h1033 h1034 h1039 h1046 h1053 h518 h519 h520 h527 h1320 h4497 h4546 h4547 h4548 h4549 h4550 h4551 h4552
3778    G       s4552   t1464
3779    B       b4552   s4552
3780    T       t4552   o695 b4552 b989
3781    B       b4553   t4552
3782    S       s4553   t671 h h1373 h951 h952 h991 h1033 h1034 h1039 h1046 h1053 h518 h519 h520 h527 h1320 h4497 h4546 h4547 h4548 h4549 h4550 h4551 h4552
3783    G       s4553   t1466
3784    B       b4554   s4553
3785    T       t4554   o695 b4554 b989
3786    B       b4555   t4554
3787    H       h4555   z_4 t4520
3788    S       s4555   t671 h h1373 h951 h952 h991 h1033 h1034 h1039 h1046 h1053 h518 h519 h520 h527 h1320 h4497 h4546 h4547 h4555 h4550 h4551 h4552
3789    G       s4555   t1466
3790    B       b4556   s4555
3791    T       t4556   o695 b4556 b989
3792    B       b4557   t4556
3793    H       h4557   z_2 t4521
3794    S       s4557   t671 h h1373 h951 h952 h991 h1033 h1034 h1039 h1046 h1053 h518 h519 h520 h527 h1320 h4497 h4546 h4557 h4550 h4551 h4552
3795    G       s4557   t1466
3796    B       b4558   s4557
3797    T       t4558   o695 b4558 b989
3798    B       b4559   t4558
3799    H       h4559   y_6 t4522
3800    S       s4559   t671 h h1373 h951 h952 h991 h1033 h1034 h1039 h1046 h1053 h518 h519 h520 h527 h1320 h4497 h4559 h4550 h4551 h4552
3801    G       s4559   t1466
3802    B       b4560   s4559
3803    T       t4560   o695 b4560 b989
3804    B       b4561   t4560
3805    H       h4561   z_2 t4526
3806    S       s4561   t671 h h1373 h951 h952 h991 h1033 h1034 h1039 h1046 h1053 h518 h519 h520 h527 h1320 h4497 h4559 h4561 h4552
3807    G       s4561   t1466
3808    B       b4562   s4561
3809    T       t4562   o695 b4562 b989
3810    B       b4563   t4562
3811    H       h4563   y_4 t4528
3812    S       s4563   t671 h h1373 h951 h952 h991 h1033 h1034 h1039 h1046 h1053 h518 h519 h520 h527 h1320 h4497 h4563 h4552
3813    G       s4563   t1466
3814    B       b4564   s4563
3815    T       t4564   o695 b4564 b989
3816    B       b4637   t4564
3817    S       s4637   t671 h h1373 h951 h952 h991 h1033 h1034 h1039 h1046 h1053 h518 h519 h520 h527 h1320 h4497 h4532
3818    G       s4637   t1466
3819    B       b4897   s4637
3820    T       t4897   o695 b4897 b989
3821    B       b4905   t4897
3822    T       t4905   o2 b4544
3823    B       b4907   t4905
3824    T       t4907   o1080 b4905 b4 b4907
3825    B       b4953   t4907
3826    T       t4954   o2 b4953
3827    B       b4954   t4954
3828    T       t4955   o694 b4637 b4 b4954
3829    B       b4955   t4955
3830    T       t4956   o2 b4955
3831    B       b4956   t4956
3832    T       t4957   o694 b4563 b4 b4956
3833    B       b4957   t4957
3834    T       t4958   o2 b4957
3835    B       b4958   t4958
3836    T       t4959   o694 b4561 b4 b4958
3837    B       b4959   t4959
3838    T       t4960   o2 b4959
3839    B       b4960   t4960
3840    T       t4961   o694 b4559 b4 b4960
3841    B       b4961   t4961
3842    T       t4962   o2 b4961
3843    B       b4962   t4962
3844    T       t4963   o694 b4557 b4 b4962
3845    B       b4963   t4963
3846    T       t4964   o2 b4963
3847    B       b4964   t4964
3848    T       t4965   o694 b4555 b711 b4964
3849    B       b4965   t4965
3850    T       t4966   o2 b4965
3851    B       b4966   t4966
3852    T       t4967   o694 b4553 b4 b4966
3853    B       b4967   t4967
3854    S       s4967   t671 h h1373 h951 h952 h991 h1033 h1034 h1039 h1046 h1053 h518 h519 h520 h527 h1320 h4497 h4546 h4547 h4548 h4549 h4550 h4551 h4552
3855    G       s4967   t1473
3856    B       b4968   s4967
3857    T       t4968   o695 b4968 b989
3858    B       b4969   t4968
3859    S       s4969   t671 h h1373 h951 h952 h991 h1033 h1034 h1039 h1046 h1053 h518 h519 h520 h527 h1320 h4497 h4546 h4547 h4555 h4550 h4551 h4552
3860    G       s4969   t1473
3861    B       b4970   s4969
3862    T       t4970   o695 b4970 b989
3863    B       b4971   t4970
3864    S       s4971   t671 h h1373 h951 h952 h991 h1033 h1034 h1039 h1046 h1053 h518 h519 h520 h527 h1320 h4497 h4546 h4557 h4550 h4551 h4552
3865    G       s4971   t1473
3866    B       b4972   s4971
3867    T       t4972   o695 b4972 b989
3868    B       b4973   t4972
3869    S       s4973   t671 h h1373 h951 h952 h991 h1033 h1034 h1039 h1046 h1053 h518 h519 h520 h527 h1320 h4497 h4559 h4550 h4551 h4552
3870    G       s4973   t1473
3871    B       b4974   s4973
3872    T       t4974   o695 b4974 b989
3873    B       b4975   t4974
3874    S       s4975   t671 h h1373 h951 h952 h991 h1033 h1034 h1039 h1046 h1053 h518 h519 h520 h527 h1320 h4497 h4559 h4561 h4552
3875    G       s4975   t1473
3876    B       b4976   s4975
3877    T       t4976   o695 b4976 b989
3878    B       b4977   t4976
3879    S       s4977   t671 h h1373 h951 h952 h991 h1033 h1034 h1039 h1046 h1053 h518 h519 h520 h527 h1320 h4497 h4563 h4552
3880    G       s4977   t1473
3881    B       b4978   s4977
3882    T       t4978   o695 b4978 b989
3883    B       b4979   t4978
3884    S       s4979   t671 h h1373 h951 h952 h991 h1033 h1034 h1039 h1046 h1053 h518 h519 h520 h527 h1320 h4497 h4532
3885    G       s4979   t1473
3886    B       b4980   s4979
3887    T       t4980   o695 b4980 b989
3888    B       b4981   t4980
3889    T       t4981   o694 b4981 b4 b4907
3890    B       b4982   t4981
3891    T       t4982   o2 b4982
3892    B       b4983   t4982
3893    T       t4983   o694 b4979 b4 b4983
3894    B       b4984   t4983
3895    T       t4984   o2 b4984
3896    B       b4985   t4984
3897    T       t4985   o694 b4977 b4 b4985
3898    B       b4986   t4985
3899    T       t4986   o2 b4986
3900    B       b4987   t4986
3901    T       t4987   o694 b4975 b4 b4987
3902    B       b4988   t4987
3903    T       t4988   o2 b4988
3904    B       b4989   t4988
3905    T       t4989   o694 b4973 b4 b4989
3906    B       b4990   t4989
3907    T       t4990   o2 b4990
3908    B       b4991   t4990
3909    T       t4991   o694 b4971 b4 b4991
3910    B       b4992   t4991
3911    T       t4992   o2 b4992
3912    B       b4993   t4992
3913    T       t4993   o694 b4969 b4 b4993
3914    B       b4994   t4993
3915    T       t4994   o b4994 b4
3916    B       b4995   t4994
3917    T       t4995   o b4967 b4995
3918    B       b4996   t4995
3919    T       t4996   o693 b4544 b4996
3920    B       b4997   t4996
3921    T       t4997   o693 b4967 b4
3922    B       b4998   t4997
3923    T       t4998   o1479 b692 b4998 b4 b4
3924    B       b4999   t4998
3925    P       p1481   String "setSubstT << equal{'f['s1; 'g]; 'f['s2; 'g]} >> 0 thenT autoT"
3926    O       o1481   ext_rule p1481
3927    T       t1481   o1049 b1314 b1093
3928    S       s4999   t671 h h1373 h951 h952 h991 h1033 h1034 h1039 h1046 h1053 h518 h519 h520 h527 h1320 h4497 h4546 h4547 h4548 h4549 h4550 h4551 h4552
3929    G       s4999   t1481
3930    B       b5000   s4999
3931    T       t5000   o695 b5000 b989
3932    B       b5001   t5000
3933    T       t1483   o952 b1314 b1093
3934    S       s5001   t671 h h1373 h951 h952 h991 h1033 h1034 h1039 h1046 h1053 h518 h519 h520 h527 h1320 h4497 h4546 h4547 h4548 h4549 h4550 h4551 h4552
3935    G       s5001   t1483
3936    B       b5002   s5001
3937    T       t5002   o695 b5002 b989
3938    B       b5003   t5002
3939    T       t5003   o2 b4994
3940    B       b5004   t5003
3941    T       t5004   o1080 b5003 b711 b5004
3942    B       b5005   t5004
3943    T       t5005   o2 b5005
3944    B       b5006   t5005
3945    T       t5006   o1080 b5001 b4 b5006
3946    B       b5007   t5006
3947    T       t5007   o b5007 b4
3948    B       b5008   t5007
3949    T       t5008   o693 b4994 b5008
3950    B       b5009   t5008
3951    T       t5009   o693 b5007 b4
3952    B       b5010   t5009
3953    T       t5010   o1479 b692 b5010 b4 b4
3954    B       b5011   t5010
3955    T       t5011   o b5011 b4
3956    B       b5012   t5011
3957    T       t5012   o1481 b692 b5009 b5012 b4
3958    B       b5013   t5012
3959    T       t5013   o b5013 b4
3960    B       b5014   t5013
3961    T       t5014   o b4999 b5014
3962    B       b5015   t5014
3963    T       t5015   o1464 b692 b4997 b5015 b4
3964    B       b5016   t5015
3965    T       t5016   o b5016 b4
3966    B       b5017   t5016
3967    T       t5017   o4518 b692 b4546 b5017 b4
3968    B       b5018   t5017
3969    T       t5018   o b5018 b4
3970    B       b5019   t5018
3971    T       t5019   o b4518 b5019
3972    B       b5020   t5019
3973    T       t5020   o4505 b692 b4515 b5020 b4
3974    B       b5021   t5020
3975    T       t5021   o b5021 b4
3976    B       b5022   t5021
3977    T       t5022   o b4505 b5022
3978    B       b5023   t5022
3979    T       t5023   o4492 b692 b4503 b5023 b4
3980    B       b5024   t5023
3981    T       t5024   o b5024 b4
3982    B       b5025   t5024
3983    T       t5025   o2575 b692 b4492 b5025 b4
3984    B       b5026   t5025
3985    T       t5026   o b5026 b4
3986    B       b5027   t5026
3987    T       t5027   o b4444 b5027
3988    B       b5028   t5027
3989    T       t5028   o2462 b692 b4318 b5028 b4
3990    B       b5029   t5028
3991    T       t5029   o b5029 b4
3992    B       b5030   t5029
3993    T       t5030   o b2461 b5030
3994    B       b5031   t5030
3995    T       t5031   o1358 b692 b1437 b5031 b4
3996    B       b5032   t5031
3997    T       t5032   o690 b5032
3998    B       b5033   t5032
3999    P       p5033   Number 2233
4000    P       p5034   Number 2241
4001    O       o5034   resource_defs p5033 p5034 p264
4002    P       p5035   Number 2239
4003    O       o5035   uid p5035 p5034
4004    T       t5035   o5035 b784
4005    B       b5035   t5035
4006    T       t5036   o b5035 b4
4007    B       b5036   t5036
4008    T       t5037   o5034 b5036
4009    B       b5037   t5037
4010    T       t5038   o b5037 b4
4011    B       b5038   t5038
4012    T       t5039   o10 b661 b983 b5033 b5038
4013    B       b5039   t5039
4014    T       t5040   o8 b5039
4015    B       b5040   t5040
4016    P       p5040   Number 2664
4017    P       p5041   Number 3348
4018    O       o5041   location p5040 p5041
4019    P       p5042   String hom_equiv_fun
4020    O       o5042   rule p5042
4021    B       b3917   t676
4022    T       t3917   o635 b3221 b3917
4023    B       b3918   t3917
4024    T       t3918   o635 b3215 b3918
4025    B       b3919   t3918
4026    T       t3919   o635 b3214 b3919
4027    B       b3920   t3919 d
4028    T       t3920   o633 b634 b3920
4029    B       b4141   t3920 c
4030    T       t4142   o633 b634 b4141
4031    B       b4142   t4142 z3
4032    T       t4143   o633 b634 b4142
4033    H       h4143   v t4143
4034    B       b4143   t2691
4035    T       t4144   o635 b3875 b4143
4036    B       b4144   t4144
4037    T       t4145   o635 b637 b4144
4038    B       b4145   t4145
4039    T       t4146   o635 b635 b4145
4040    H       h4146   w t4146
4041    S       s4146   t671 h h704 h705 h805 h806 h1033 h1034 h1550 h1562 h1570 h518 h519 h520 h527 h2616 h4143 h4146
4042    G       s4146   t2691
4043    B       b4146   s4146
4044    T       t4148   o623 b624 b3216 b630 b411
4045    B       b4148   t4148
4046    T       t4149   o580 b411 b528
4047    B       b4149   t4149
4048    T       t4150   o623 b626 b537 b2613 b4149
4049    B       b4150   t4150
4050    T       t4151   o635 b4148 b4150
4051    B       b4151   t4151
4052    T       t4152   o635 b3215 b4151
4053    B       b4152   t4152
4054    T       t4153   o635 b635 b4152
4055    B       b4153   t4153 d
4056    T       t4154   o633 b634 b4153
4057    H       h4154   w_1 t4154
4058    S       s4154   t671 h h704 h705 h805 h806 h1033 h1034 h1550 h1562 h1570 h518 h519 h520 h527 h2616 h4143 h4154 h4146
4059    G       s4154   t2691
4060    B       b4154   s4154
4061    S       s4155   t671 h h704 h705 h805 h806 h1033 h1034 h1550 h1562 h1570 h518 h519 h520 h527 h2616 h4143 h4154
4062    G       s4155   t2691
4063    B       b4156   s4155
4064    T       t4157   o580 b409 b528
4065    B       b4158   t4157
4066    T       t4158   o623 b626 b537 b4158 b4149
4067    B       b4159   t4158
4068    T       t4159   o635 b3221 b4159
4069    B       b4160   t4159
4070    T       t4160   o635 b3215 b4160
4071    B       b4161   t4160
4072    T       t4161   o635 b3214 b4161
4073    B       b4162   t4161 d
4074    T       t4162   o633 b634 b4162
4075    B       b4163   t4162 c
4076    T       t4163   o633 b634 b4163
4077    H       h4163   w t4163
4078    S       s4163   t671 h h704 h705 h805 h806 h1033 h1034 h1550 h1562 h1570 h518 h519 h520 h527 h2616 h4143 h4163 h4154
4079    G       s4163   t2691
4080    B       b4164   s4163
4081    S       s4165   t671 h h704 h705 h805 h806 h1033 h1034 h1550 h1562 h1570 h518 h519 h520 h527 h2616 h4143 h4163
4082    G       s4165   t2691
4083    B       b4166   s4165
4084    S       s4167   t671 h h704 h705 h805 h806 h1033 h1034 h1550 h1562 h1570 h518 h519 h520 h527 h2616 h4143
4085    G       s4167   t2691
4086    B       b4168   s4167
4087    T       t4169   o b528 b4
4088    B       b4170   t4169
4089    T       t4170   o1207 b4170
4090    B       b4171   t4170
4091    T       t4171   o1206 b4171
4092    B       b4172   t4171
4093    T       t4172   o b4172 b1204
4094    B       b4173   t4172
4095    T       t2808   o661 b608 b686
4096    B       b2808   t2808
4097    T       t2809   o661 b920 b2808
4098    B       b2809   t2809
4099    T       t2810   o661 b674 b2809
4100    B       b2810   t2810
4101    T       t2811   o661 b672 b2810
4102    B       b2811   t2811
4103    T       t2812   o661 b669 b2811
4104    B       b2812   t2812
4105    T       t2813   o661 b667 b2812
4106    B       b2813   t2813
4107    P       p5043   String "rwh unfold_equiv_fun_prop 0 thenT autoT thenT rwh unfold_hom 6 thenT autoT"
4108    O       o5043   ext_rule p5043
4109    T       t2814   o b607 b781
4110    B       b2814   t2814
4111    T       t2815   o b919 b2814
4112    B       b2815   t2815
4113    T       t2816   o b673 b2815
4114    B       b2816   t2816
4115    T       t2817   o b671 b2816
4116    B       b2817   t2817
4117    T       t2818   o b668 b2817
4118    B       b2818   t2818
4119    T       t2819   o b666 b2818
4120    B       b2819   t2819
4121    T       t2820   o695 b684 b2819
4122    B       b2820   t2820
4123    T       t2821   o694 b2820 b4 b703
4124    B       b2821   t2821
4125    T       t2822   o580 b636 b409
4126    B       b2822   t2822
4127    T       t2823   o580 b636 b411
4128    B       b2823   t2823
4129    T       t2824   o623 b626 b537 b2822 b2823
4130    S       s2824   t671 h h704 h705 h805 h806 h807 h408 h409 h410 h412 h435
4131    G       s2824   t2824
4132    B       b2824   s2824
4133    T       t2825   o695 b2824 b2819
4134    B       b2825   t2825
4135    T       t2826   o695 b815 b2819
4136    B       b2826   t2826
4137    T       t2827   o695 b883 b2819
4138    B       b2827   t2827
4139    T       t2828   o695 b886 b2819
4140    B       b2828   t2828
4141    T       t2829   o695 b899 b2819
4142    B       b2829   t2829
4143    T       t2830   o695 b902 b2819
4144    B       b2830   t2830
4145    T       t2831   o695 b908 b2819
4146    B       b2831   t2831
4147    T       t2832   o2 b2821
4148    B       b2832   t2832
4149    T       t2833   o694 b2831 b711 b2832
4150    B       b2833   t2833
4151    T       t2834   o2 b2833
4152    B       b2834   t2834
4153    T       t2835   o694 b2830 b711 b2834
4154    B       b2835   t2835
4155    T       t2836   o2 b2835
4156    B       b2836   t2836
4157    T       t2837   o694 b2829 b711 b2836
4158    B       b2837   t2837
4159    T       t2838   o2 b2837
4160    B       b2838   t2838
4161    T       t2839   o694 b2828 b711 b2838
4162    B       b2839   t2839
4163    T       t2840   o2 b2839
4164    B       b2840   t2840
4165    T       t2841   o694 b2827 b711 b2840
4166    B       b2841   t2841
4167    T       t2842   o2 b2841
4168    B       b2842   t2842
4169    T       t2843   o694 b2826 b711 b2842
4170    B       b2843   t2843
4171    T       t2844   o2 b2843
4172    B       b2844   t2844
4173    T       t2845   o694 b2825 b4 b2844
4174    B       b2845   t2845
4175    T       t2846   o695 b812 b2819
4176    B       b2846   t2846
4177    T       t2847   o694 b2846 b4 b2844
4178    B       b2847   t2847
4179    T       t2851   o580 b630 b409
4180    B       b2851   t2851
4181    T       t2852   o580 b630 b411
4182    B       b2852   t2852
4183    T       t2853   o623 b626 b537 b2851 b2852
4184    H       h2853   y_4 t2853
4185    S       s2853   t671 h h704 h705 h805 h806 h1033 h1034 h1550 h1562 h1570 h408 h409 h410 h412 h435 h2853
4186    G       s2853   t2824
4187    B       b2853   s2853
4188    T       t2854   o695 b2853 b2819
4189    B       b2854   t2854
4190    B       b2855   t2853
4191    T       t2855   o635 b3221 b2855
4192    H       h2855   y_5 t2855
4193    S       s2855   t671 h h704 h705 h805 h806 h1033 h1034 h1550 h1562 h1570 h408 h409 h410 h412 h435 h2855 h2853
4194    G       s2855   t2824
4195    B       b2856   s2855
4196    T       t2856   o695 b2856 b2819
4197    B       b2857   t2856
4198    S       s2857   t671 h h704 h705 h805 h806 h1033 h1034 h1550 h1562 h1570 h408 h409 h410 h412 h435 h2855
4199    G       s2857   t2824
4200    B       b2858   s2857
4201    T       t2858   o695 b2858 b2819
4202    B       b2859   t2858
4203    B       b2860   t2855
4204    T       t2860   o635 b3215 b2860
4205    H       h2860   y_4 t2860
4206    S       s2860   t671 h h704 h705 h805 h806 h1033 h1034 h1550 h1562 h1570 h408 h409 h410 h412 h435 h2860 h2855
4207    G       s2860   t2824
4208    B       b2861   s2860
4209    T       t2861   o695 b2861 b2819
4210    B       b2862   t2861
4211    S       s2862   t671 h h704 h705 h805 h806 h1033 h1034 h1550 h1562 h1570 h408 h409 h410 h412 h435 h2860
4212    G       s2862   t2824
4213    B       b2863   s2862
4214    T       t2863   o695 b2863 b2819
4215    B       b2864   t2863
4216    B       b2865   t2860
4217    T       t2865   o635 b3214 b2865
4218    H       h2865   w_1 t2865
4219    S       s2865   t671 h h704 h705 h805 h806 h1033 h1034 h1550 h1562 h1570 h408 h409 h410 h412 h435 h2865 h2860
4220    G       s2865   t2824
4221    B       b2866   s2865
4222    T       t2866   o695 b2866 b2819
4223    B       b2867   t2866
4224    S       s2867   t671 h h704 h705 h805 h806 h1033 h1034 h1550 h1562 h1570 h408 h409 h410 h412 h435 h2865
4225    G       s2867   t2824
4226    B       b2868   s2867
4227    T       t2868   o695 b2868 b2819
4228    B       b2869   t2868
4229    T       t2869   o623 b626 b537 b2851 b1553
4230    B       b2870   t2869
4231    T       t2870   o635 b1143 b2870
4232    B       b2871   t2870
4233    T       t2871   o635 b637 b2871
4234    B       b2872   t2871
4235    T       t2872   o635 b3214 b2872
4236    B       b2873   t2872 b
4237    T       t2873   o633 b634 b2873
4238    H       h2873   w t2873
4239    S       s2873   t671 h h704 h705 h805 h806 h1033 h1034 h1550 h1562 h1570 h408 h409 h410 h412 h435 h2873 h2865
4240    G       s2873   t2824
4241    B       b2874   s2873
4242    T       t2874   o695 b2874 b2819
4243    B       b2875   t2874
4244    S       s2875   t671 h h704 h705 h805 h806 h1033 h1034 h1550 h1562 h1570 h408 h409 h410 h412 h435 h2873
4245    G       s2875   t2824
4246    B       b2876   s2875
4247    T       t2876   o695 b2876 b2819
4248    B       b2877   t2876
4249    S       s2877   t671 h h704 h705 h805 h806 h1033 h1034 h1550 h1562 h1570 h408 h409 h410 h412 h435
4250    G       s2877   t2824
4251    B       b2878   s2877
4252    T       t2878   o695 b2878 b2819
4253    B       b2879   t2878
4254    S       s2879   t671 h h704 h705 h805 h806 h1033 h1034 h1550 h1599 h408 h409 h410 h412 h435
4255    G       s2879   t2824
4256    B       b2880   s2879
4257    T       t2880   o695 b2880 b2819
4258    B       b2881   t2880
4259    S       s2881   t671 h h704 h705 h805 h806 h1033 h1034 h1829 h408 h409 h410 h412 h435
4260    G       s2881   t2824
4261    B       b2882   s2881
4262    T       t2882   o695 b2882 b2819
4263    B       b2883   t2882
4264    S       s2883   t671 h h704 h705 h805 h806 h1033 h1834 h408 h409 h410 h412 h435
4265    G       s2883   t2824
4266    B       b2884   s2883
4267    T       t2884   o695 b2884 b2819
4268    B       b2885   t2884
4269    S       s2885   t671 h h704 h705 h805 h806 h1840 h408 h409 h410 h412 h435
4270    G       s2885   t2824
4271    B       b2886   s2885
4272    T       t2886   o695 b2886 b2819
4273    B       b2887   t2886
4274    T       t2887   o2 b2845
4275    B       b2888   t2887
4276    T       t2888   o694 b2887 b4 b2888
4277    B       b2889   t2888
4278    T       t2889   o2 b2889
4279    B       b2890   t2889
4280    T       t2890   o694 b2885 b4 b2890
4281    B       b2891   t2890
4282    T       t2891   o2 b2891
4283    B       b2892   t2891
4284    T       t2892   o694 b2883 b4 b2892
4285    B       b2893   t2892
4286    T       t2893   o2 b2893
4287    B       b2894   t2893
4288    T       t2894   o694 b2881 b4 b2894
4289    B       b2895   t2894
4290    T       t2895   o2 b2895
4291    B       b2896   t2895
4292    T       t5043   o694 b2879 b4 b2896
4293    B       b5043   t5043
4294    T       t2896   o694 b2879 b1165 b2896
4295    B       b2897   t2896
4296    T       t2897   o2 b2897
4297    B       b2898   t2897
4298    T       t2898   o694 b2877 b1161 b2898
4299    B       b2899   t2898
4300    T       t2899   o2 b2899
4301    B       b2900   t2899
4302    T       t2900   o694 b2875 b1204 b2900
4303    B       b2901   t2900
4304    T       t2901   o2 b2901
4305    B       b2902   t2901
4306    T       t2902   o694 b2869 b4 b2902
4307    B       b2903   t2902
4308    T       t2903   o2 b2903
4309    B       b2904   t2903
4310    T       t2904   o694 b2867 b4 b2904
4311    B       b2905   t2904
4312    T       t2905   o2 b2905
4313    B       b2906   t2905
4314    T       t2906   o694 b2864 b4 b2906
4315    B       b2907   t2906
4316    T       t2907   o2 b2907
4317    B       b2908   t2907
4318    T       t2908   o694 b2862 b4 b2908
4319    B       b2909   t2908
4320    T       t2909   o2 b2909
4321    B       b2910   t2909
4322    T       t2910   o694 b2859 b4 b2910
4323    B       b2911   t2910
4324    T       t2911   o2 b2911
4325    B       b2912   t2911
4326    T       t2912   o694 b2857 b4 b2912
4327    B       b2913   t2912
4328    T       t2913   o2 b2913
4329    B       b2914   t2913
4330    T       t2914   o694 b2854 b4 b2914
4331    B       b2915   t2914
4332    T       t2915   o b2915 b4
4333    B       b2916   t2915
4334    P       p2917   String "equivTransT << 'f['a; 'd] >> thenT autoT"
4335    O       o2917   ext_rule p2917
4336    T       t2917   o623 b626 b537 b2822 b2852
4337    S       s2917   t671 h h704 h705 h805 h806 h1033 h1034 h1550 h1562 h1570 h408 h409 h410 h412 h435 h2853
4338    G       s2917   t2917
4339    B       b2918   s2917
4340    T       t2918   o695 b2918 b2819
4341    B       b2919   t2918
4342    T       t2919   o2 b2915
4343    B       b2920   t2919
4344    T       t2920   o694 b2919 b4 b2920
4345    B       b2921   t2920
4346    T       t2921   o623 b626 b537 b2852 b2823
4347    S       s2921   t671 h h704 h705 h805 h806 h1033 h1034 h1550 h1562 h1570 h408 h409 h410 h412 h435 h2853
4348    G       s2921   t2921
4349    B       b2922   s2921
4350    T       t2922   o695 b2922 b2819
4351    B       b2923   t2922
4352    T       t2923   o694 b2923 b4 b2920
4353    B       b2924   t2923
4354    T       t2924   o b2924 b4
4355    B       b2925   t2924
4356    T       t2925   o b2921 b2925
4357    B       b2926   t2925
4358    T       t2926   o693 b2915 b2926
4359    B       b2927   t2926
4360    P       p2927   String "equivTransT << 'f['a; 'c] >> thenT autoT"
4361    O       o2927   ext_rule p2927
4362    T       t2927   o623 b626 b537 b2822 b2851
4363    S       s2927   t671 h h704 h705 h805 h806 h1033 h1034 h1550 h1562 h1570 h408 h409 h410 h412 h435 h2853
4364    G       s2927   t2927
4365    B       b2928   s2927
4366    T       t2928   o695 b2928 b2819
4367    B       b2929   t2928
4368    T       t2929   o2 b2921
4369    B       b2930   t2929
4370    T       t2930   o694 b2929 b4 b2930
4371    B       b2931   t2930
4372    T       t2931   o b2931 b4
4373    B       b2932   t2931
4374    T       t2932   o693 b2921 b2932
4375    B       b2933   t2932
4376    P       p2933   String "equivSymT ttca thenT assumT 7 ttca thenT instHypT [<< 'c >>; << 'a >>; << 'b >>] 17 thenT autoT thenT rwh unfold_equiv 5 thenT dT 18 ttca thenT dT 18 ttca thenT dT 18 ttca thenT rwh fold_equiv 5 ttca"
4377    O       o2933   ext_rule p2933
4378    T       t2933   o693 b2931 b4
4379    B       b2934   t2933
4380    T       t2934   o2933 b692 b2934 b4 b4
4381    B       b2936   t2934
4382    T       t2936   o b2936 b4
4383    B       b2937   t2936
4384    T       t2937   o2927 b692 b2933 b2937 b4
4385    B       b2938   t2937
4386    P       p2938   String "assumT 7 ttca thenT instHypT [<< 'd >>; << 'a >>; << 'b >>] 17 thenT autoT thenT rwh unfold_equiv 5 thenT dT 18 ttca thenT dT 18 ttca thenT dT 18 ttca thenT rwh fold_equiv 5 ttca"
4387    O       o2938   ext_rule p2938
4388    T       t2938   o693 b2924 b4
4389    B       b2939   t2938
4390    T       t2939   o2938 b692 b2939 b4 b4
4391    B       b2940   t2939
4392    T       t2940   o b2940 b4
4393    B       b2941   t2940
4394    T       t2941   o b2938 b2941
4395    B       b3089   t2941
4396    T       t3095   o2917 b692 b2927 b3089 b4
4397    B       b3189   t3095
4398    T       t3189   o b3189 b4
4399    B       b4089   t3189
4400    T       t4096   o695 b1570 b2819
4401    B       b4107   t4096
4402    T       t4107   o695 b1600 b2819
4403    B       b4108   t4107
4404    T       t4108   o695 b1830 b2819
4405    B       b4109   t4108
4406    T       t4109   o695 b1835 b2819
4407    B       b4110   t4109
4408    T       t4110   o695 b1842 b2819
4409    B       b4111   t4110
4410    T       t4111   o2 b2847
4411    B       b4112   t4111
4412    T       t4112   o694 b4111 b4 b4112
4413    B       b4113   t4112
4414    T       t4113   o2 b4113
4415    B       b4114   t4113
4416    T       t4114   o694 b4110 b4 b4114
4417    B       b4115   t4114
4418    T       t4115   o2 b4115
4419    B       b4116   t4115
4420    T       t4116   o694 b4109 b4 b4116
4421    B       b4117   t4116
4422    T       t4117   o2 b4117
4423    B       b4118   t4117
4424    T       t4118   o694 b4108 b4 b4118
4425    B       b4119   t4118
4426    T       t4119   o2 b4119
4427    B       b4120   t4119
4428    T       t4120   o694 b4107 b4 b4120
4429    B       b4121   t4120
4430    T       t4121   o b4121 b4
4431    B       b4122   t4121
4432    T       t5044   o b5043 b4122
4433    B       b5044   t5044
4434    T       t5045   o693 b2821 b5044
4435    B       b5045   t5045
4436    T       t5046   o693 b5043 b2916
4437    B       b5046   t5046
4438    T       t5047   o4318 b692 b5046 b4089 b4
4439    B       b5047   t5047
4440    T       t4123   o695 b2621 b2819
4441    B       b4124   t4123
4442    T       t4124   o695 b2625 b2819
4443    B       b4125   t4124
4444    T       t4125   o695 b2636 b2819
4445    B       b4126   t4125
4446    T       t4126   o695 b2649 b2819
4447    B       b4127   t4126
4448    T       t4127   o695 b2651 b2819
4449    B       b4128   t4127
4450    T       t4128   o695 b2660 b2819
4451    B       b4129   t4128
4452    T       t4129   o695 b2665 b2819
4453    B       b4130   t4129
4454    T       t4130   o694 b4107 b2674 b4120
4455    B       b4131   t4130
4456    T       t4131   o2 b4131
4457    B       b4132   t4131
4458    T       t4132   o694 b4130 b2670 b4132
4459    B       b4133   t4132
4460    T       t4133   o2 b4133
4461    B       b4134   t4133
4462    T       t4134   o694 b4129 b1204 b4134
4463    B       b4135   t4134
4464    T       t4135   o2 b4135
4465    B       b4136   t4135
4466    T       t4136   o694 b4128 b4 b4136
4467    B       b4137   t4136
4468    T       t4137   o2 b4137
4469    B       b4138   t4137
4470    T       t4138   o694 b4127 b4 b4138
4471    B       b4139   t4138
4472    T       t4139   o2 b4139
4473    B       b4140   t4139
4474    T       t4140   o694 b4126 b4 b4140
4475    B       b4249   t4140
4476    T       t4249   o2 b4249
4477    B       b4256   t4249
4478    T       t4256   o694 b4125 b4 b4256
4479    B       b4281   t4256
4480    T       t4291   o2 b4281
4481    B       b4332   t4291
4482    T       t4341   o694 b4124 b4 b4332
4483    B       b4517   t4341
4484    T       t4517   o b4517 b4
4485    B       b4525   t4517
4486    T       t4525   o693 b4121 b4525
4487    B       b4527   t4525
4488    T       t4527   o695 b2692 b2819
4489    B       b4529   t4527
4490    T       t4529   o2 b4517
4491    B       b4565   t4529
4492    T       t4566   o694 b4529 b4 b4565
4493    B       b4566   t4566
4494    T       t4567   o695 b2698 b2819
4495    B       b4567   t4567
4496    T       t4568   o694 b4567 b4 b4565
4497    B       b4568   t4568
4498    T       t4569   o b4568 b4
4499    B       b4569   t4569
4500    T       t4570   o b4566 b4569
4501    B       b4570   t4570
4502    T       t4571   o693 b4517 b4570
4503    B       b4571   t4571
4504    P       p4187   String "rwh unfold_equiv 5 thenT dT 17 ttca thenT dT 17 ttca thenT dT 17 ttca thenT rwh fold_equiv 5 ttca"
4505    O       o4187   ext_rule p4187
4506    P       p4191   String "equivSubstT << equiv{car{'g2}; eqG{'g2}; op{'g2; 'f['a; 'e]; 'f['a; 'g]}; op{'g2; 'f['b; 'e]; 'f['b; 'g]}} >> 16 thenT autoT thenT rwh unfold_equiv 16 ttca thenT rwh fold_equiv 16"
4507    O       o4191   ext_rule p4191
4508    T       t4191   o623 b626 b537 b2616 b811
4509    S       s4191   t671 h h704 h705 h805 h806 h1033 h1034 h1550 h1562 h1570 h518 h519 h520 h527 h2616 h2695
4510    G       s4191   t4191
4511    B       b4192   s4191
4512    T       t4193   o621 b808
4513    B       b4194   t4193
4514    T       t4194   o621 b2616
4515    B       b4195   t4194
4516    T       t4195   o619 b4194 b4195
4517    B       b4196   t4195
4518    T       t4196   o619 b3026 b4196
4519    B       b4197   t4196
4520    T       t4197   o619 b1282 b4197
4521    B       b4198   t4197
4522    T       t4198   o629 b808 b626
4523    B       b4199   t4198
4524    T       t4199   o629 b2616 b626
4525    B       b4200   t4199
4526    T       t4200   o619 b4199 b4200
4527    B       b4201   t4200
4528    T       t4201   o619 b4198 b4201
4529    B       b4202   t4201
4530    T       t4202   o1292 b808 b2616
4531    B       b4203   t4202
4532    T       t4203   o629 b4203 b537
4533    B       b4204   t4203
4534    T       t4204   o619 b4202 b4204
4535    H       h4204   z t4204
4536    S       s4204   t671 h h704 h705 h805 h806 h1033 h1034 h1550 h1562 h1570 h518 h519 h520 h527 h2616 h4204
4537    G       s4204   t4191
4538    B       b4205   s4204
4539    P       p4214   String "equivSubstT << equiv{car{'g2}; eqG{'g2}; 'f['a; 'e]; 'f['b; 'e]} >> 0 thenT autoT"
4540    O       o4214   ext_rule p4214
4541    T       t4214   o623 b626 b537 b2614 b809
4542    S       s4214   t671 h h704 h705 h805 h806 h1033 h1034 h1550 h1562 h1570 h518 h519 h520 h527 h2616 h2695
4543    G       s4214   t4214
4544    B       b4215   s4214
4545    T       t4218   o623 b626 b537 b2615 b810
4546    S       s4218   t671 h h704 h705 h805 h806 h1033 h1034 h1550 h1562 h1570 h518 h519 h520 h527 h2616 h2695
4547    G       s4218   t4218
4548    B       b4219   s4218
4549    T       t4220   o637 b577 b809 b2615
4550    B       b4221   t4220
4551    T       t4221   o623 b626 b537 b4221 b811
4552    S       s4221   t671 h h704 h705 h805 h806 h1033 h1034 h1550 h1562 h1570 h518 h519 h520 h527 h2616 h2695
4553    G       s4221   t4221
4554    B       b4222   s4221
4555    P       p4418   String "assumT 7 ttca thenT instHypT [<< op{'g1; 'e; 'g} >>; << 'a >>; << 'b >>] 16 ttca thenT rwh fold_isset 0 ttca"
4556    O       o4418   ext_rule p4418
4557    T       t4572   o695 b4146 b2819
4558    B       b4572   t4572
4559    T       t4573   o695 b4154 b2819
4560    B       b4573   t4573
4561    T       t4574   o695 b4156 b2819
4562    B       b4574   t4574
4563    T       t4575   o695 b4164 b2819
4564    B       b4575   t4575
4565    T       t4576   o695 b4166 b2819
4566    B       b4576   t4576
4567    T       t4577   o695 b4168 b2819
4568    B       b4577   t4577
4569    T       t4578   o2 b4566
4570    B       b4578   t4578
4571    T       t4579   o694 b4577 b4173 b4578
4572    B       b4579   t4579
4573    T       t4580   o2 b4579
4574    B       b4580   t4580
4575    T       t4581   o694 b4576 b1214 b4580
4576    B       b4581   t4581
4577    T       t4582   o2 b4581
4578    B       b4582   t4582
4579    T       t4583   o694 b4575 b1204 b4582
4580    B       b4583   t4583
4581    T       t4584   o2 b4583
4582    B       b4584   t4584
4583    T       t4585   o694 b4574 b1210 b4584
4584    B       b4585   t4585
4585    T       t4586   o2 b4585
4586    B       b4586   t4586
4587    T       t4587   o694 b4573 b1204 b4586
4588    B       b4587   t4587
4589    T       t4588   o2 b4587
4590    B       b4588   t4588
4591    T       t4589   o694 b4572 b4 b4588
4592    B       b4589   t4589
4593    T       t4590   o b4589 b4
4594    B       b4590   t4590
4595    T       t4591   o693 b4566 b4590
4596    B       b4591   t4591
4597    T       t4592   o693 b4589 b4
4598    B       b4592   t4592
4599    T       t4593   o4187 b692 b4592 b4 b4
4600    B       b4593   t4593
4601    T       t4594   o b4593 b4
4602    B       b4594   t4594
4603    T       t4595   o4418 b692 b4591 b4594 b4
4604    B       b4595   t4595
4605    T       t4596   o695 b4192 b2819
4606    B       b4596   t4596
4607    T       t4597   o695 b4205 b2819
4608    B       b4597   t4597
4609    T       t4598   o2 b4568
4610    B       b4598   t4598
4611    T       t4599   o694 b4596 b4 b4598
4612    B       b4599   t4599
4613    T       t4600   o2 b4599
4614    B       b4600   t4600
4615    T       t4601   o694 b4597 b4 b4600
4616    B       b4601   t4601
4617    T       t4602   o2 b4601
4618    B       b4602   t4602
4619    T       t4603   o694 b4596 b4 b4602
4620    B       b4603   t4603
4621    T       t4604   o b4603 b4
4622    B       b4604   t4604
4623    T       t4605   o693 b4568 b4604
4624    B       b4605   t4605
4625    T       t4606   o695 b4215 b2819
4626    B       b4606   t4606
4627    T       t4607   o2 b4603
4628    B       b4607   t4607
4629    T       t4608   o694 b4606 b4 b4607
4630    B       b4608   t4608
4631    T       t4609   o695 b4219 b2819
4632    B       b4609   t4609
4633    T       t4610   o695 b4222 b2819
4634    B       b4610   t4610
4635    T       t4611   o694 b4610 b711 b4607
4636    B       b4611   t4611
4637    T       t4612   o2 b4611
4638    B       b4612   t4612
4639    T       t4613   o694 b4609 b4 b4612
4640    B       b4613   t4613
4641    T       t4614   o b4613 b4
4642    B       b4614   t4614
4643    T       t4615   o b4608 b4614
4644    B       b4615   t4615
4645    T       t4616   o693 b4603 b4615
4646    B       b4616   t4616
4647    P       p4497   String "assumT 7 ttca thenT instHypT [<< 'e >>; << 'a >>; << 'b >>] 17 ttca thenT rwh unfold_equiv 5 thenT dT 18 ttca thenT dT 18 ttca thenT dT 18 ttca thenT rwh fold_equiv 5 ttca"
4648    O       o4497   ext_rule p4497
4649    T       t4617   o693 b4608 b4
4650    B       b4617   t4617
4651    T       t4618   o4497 b692 b4617 b4 b4
4652    B       b4618   t4618
4653    P       p4499   String "assumT 7 ttca thenT instHypT [<< 'g >>; << 'a >>; << 'b >>] 17 ttca thenT rwh unfold_equiv 5 thenT dT 18 ttca thenT dT 18 ttca thenT dT 18 ttca thenT rwh fold_equiv 5 ttca"
4654    O       o4499   ext_rule p4499
4655    T       t4619   o693 b4613 b4
4656    B       b4619   t4619
4657    T       t4620   o4499 b692 b4619 b4 b4
4658    B       b4620   t4620
4659    T       t4621   o b4620 b4
4660    B       b4621   t4621
4661    T       t4622   o b4618 b4621
4662    B       b4622   t4622
4663    T       t4623   o4214 b692 b4616 b4622 b4
4664    B       b4623   t4623
4665    T       t4624   o b4623 b4
4666    B       b4624   t4624
4667    T       t4625   o4191 b692 b4605 b4624 b4
4668    B       b4625   t4625
4669    T       t4626   o b4625 b4
4670    B       b4626   t4626
4671    T       t4627   o b4595 b4626
4672    B       b4627   t4627
4673    T       t4628   o2691 b692 b4571 b4627 b4
4674    B       b4628   t4628
4675    T       t4629   o b4628 b4
4676    B       b4629   t4629
4677    T       t4630   o2575 b692 b4527 b4629 b4
4678    B       b4630   t4630
4679    T       t4631   o b4630 b4
4680    B       b4631   t4631
4681    T       t5048   o b5047 b4631
4682    B       b5048   t5048
4683    T       t5049   o5043 b692 b5045 b5048 b4
4684    B       b5049   t5049
4685    T       t5050   o690 b5049
4686    B       b5050   t5050
4687    P       p5050   Number 2693
4688    P       p5051   Number 2701
4689    O       o5051   resource_defs p5050 p5051 p264
4690    P       p5052   Number 2699
4691    O       o5052   uid p5052 p5051
4692    T       t5052   o5052 b784
4693    B       b5052   t5052
4694    T       t5053   o b5052 b4
4695    B       b5053   t5053
4696    T       t5054   o5051 b5053
4697    B       b5054   t5054
4698    T       t5055   o b5054 b4
4699    B       b5055   t5055
4700    T       t5056   o5042 b661 b2813 b5050 b5055
4701    B       b5056   t5056
4702    T       t5057   o5041 b5056
4703    B       b5057   t5057
4704    P       p14     Number 3580
4705    P       p16     Number 3946
4706    O       o16     location p14 p16
4707    P       p18     String trivial_hom
4708    O       o18     rule p18
4709    T       t611    o623 b626 b537 b679 b1560
4710    S       s611    t671 h h678 h797
4711    G       s611    t611
4712    B       b796    s611
4713    T       t796    o662 b796
4714    B       b997    t796
4715    T       t997    o661 b997 b2708
4716    B       b998    t997
4717    T       t1001   o661 b674 b998
4718    B       b1001   t1001
4719    T       t1002   o661 b672 b1001
4720    B       b1002   t1002
4721    T       t1004   o661 b669 b1002
4722    B       b1004   t1004
4723    T       t1005   o661 b667 b1004
4724    B       b1005   t1005
4725    P       p1005   String "assumT 5 thenT autoT"
4726    O       o1005   ext_rule p1005
4727    T       t1007   o b796 b4
4728    B       b1007   t1007
4729    T       t1008   o b673 b1007
4730    B       b1008   t1008
4731    T       t1010   o b671 b1008
4732    B       b1010   t1010
4733    T       t1012   o b668 b1010
4734  B       b1013   t1012  B       b1013   t1012
4735  T       t1013   o637 b577 b1012 b1013  T       t1013   o b666 b1013
4736  B       b1014   t1013  B       b1014   t1013
4737  T       t1014   o623 b626 b965 b1011 b1014  T       t1014   o695 b2707 b1014
4738  S       s1014   t671 h h951 h952 h955 h994 h704 h705 h1010 h804  B       b1015   t1014
4739  G       s1014   t1014  T       t1015   o694 b1015 b4 b703
 B       b1015   s1014  
 T       t1015   o695 b1015 b949  
4740  B       b1016   t1015  B       b1016   t1015
4741  T       t1016   o694 b1016 b4 b1000  B       b1017   t797
4742  B       b1017   t1016  B       b1018   t611
4743  T       t1017   o b1017 b4  T       t1018   o635 b1017 b1018
4744  B       b1018   t1017  B       b1019   t1018 x
4745  T       t1018   o b1010 b1018  T       t1019   o633 b634 b1019
4746  B       b1019   t1018  H       h1019   v t1019
4747  T       t1019   o b1007 b1019  S       s1019   t671 h h1019 h678 h797
4748  B       b1020   t1019  G       s1019   t798
4749  T       t1020   o b1004 b1020  B       b1020   s1019
4750  B       b1021   t1020  T       t1020   o695 b1020 b1014
4751  T       t1021   o b1001 b1021  B       b1025   t1020
4752  B       b1022   t1021  S       s1025   t671 h h1019
4753  T       t1022   o b994 b1022  G       s1025   t480
4754  B       b1023   t1022  B       b1026   s1025
4755  T       t1023   o b991 b1023  T       t1026   o695 b1026 b1014
 B       b1024   t1023  
 T       t1024   o693 b951 b1024  
 B       b1025   t1024  
 T       t1025   o693 b991 b4  
 B       b1026   t1025  
 T       t1026   o890 b692 b1026 b4 b4  
4756  B       b1027   t1026  B       b1027   t1026
4757  T       t1027   o693 b994 b4  T       t1027   o2 b1016
4758  B       b1028   t1027  B       b1028   t1027
4759  T       t1028   o890 b692 b1028 b4 b4  T       t1028   o694 b1027 b711 b1028
4760  B       b1029   t1028  B       b1029   t1028
4761  P       p1029   String "funSetT 3 ttca"  T       t1029   o2 b1029
 O       o1029   ext_rule p1029  
 T       t1029   o693 b1001 b4  
4762  B       b1030   t1029  B       b1030   t1029
4763  T       t1030   o1029 b692 b1030 b4 b4  T       t1030   o694 b1025 b4 b1030
4764  B       b1031   t1030  B       b1031   t1030
4765  T       t1031   o693 b1004 b4  S       s1031   t671 h h1019 h408 h409 h410 h412 h435
4766  B       b1032   t1031  G       s1031   t490
4767  T       t1032   o1029 b692 b1032 b4 b4  B       b1032   s1031
4768  B       b1033   t1032  T       t1037   o695 b1032 b1014
4769  P       p1033   String "rwh unfold_hom 5 thenT setSubstT << equal{'s2; 's1} >> 0 thenT autoT"  B       b1053   t1037
4770  O       o1033   ext_rule p1033  T       t1059   o694 b1053 b4 b1030
4771  H       h1033   y t620  B       b1059   t1059
4772  H       h1034   y_1 t621  S       s1059   t671 h h1019 h518 h519 h520 h527
4773  H       h1035   y_2 t957  G       s1059   t543
4774  H       h1036   y_3 t991  B       b1062   s1059
4775  T       t1036   o623 b624 b956  T       t1062   o695 b1062 b1014
4776  H       h1037   y_4 t1036  B       b1063   t1062
4777  T       t1037   o623 b626 b959  T       t1063   o694 b1063 b4 b1030
4778  H       h1038   y_5 t1037  B       b1066   t1063
4779  T       t1038   o627 b960  T       t1066   o b1066 b4
4780  H       h1039   y_6 t1038  B       b1067   t1066
4781  T       t1039   o580 b953 b630  T       t1067   o b1059 b1067
4782  B       b1039   t1039  B       b1069   t1067
4783  T       t1040   o629 b1039 b626  T       t1069   o b1031 b1069
4784  B       b1040   t1040 a  B       b1070   t1069
4785  T       t1041   o628 b624 b1040  T       t1070   o693 b1016 b1070
4786  H       h1041   y_7 t1041  B       b1072   t1070
4787  T       t1042   o580 b953 b638  P       p1072   String "withT << 'x >> (dT 2) ttca thenT dT 4 ttca thenT rwh unfold_equiv 4 thenT autoT"
4788  B       b1042   t1042  O       o1072   ext_rule p1072
4789  T       t1043   o580 b953 b636  T       t1072   o693 b1031 b4
 B       b1043   t1043  
 T       t1044   o637 b577 b1039 b1043  
 B       b1044   t1044  
 T       t1045   o623 b626 b959 b1042 b1044  
 B       b1045   t1045  
 T       t1046   o635 b637 b1045  
 B       b1046   t1046  
 T       t1047   o635 b635 b1046  
 B       b1047   t1047 b  
 T       t1048   o633 b634 b1047  
 B       b1048   t1048 a  
 T       t1049   o633 b634 b1048  
 H       h1049   z_1 t1049  
 NCzf_itt_eq!eq  eq      eq Czf_itt_eq  
 O       o1049   eq  
 T       t1050   o1049 b954 b953  
 S       s1050   t671 h h951 h952 h955 h1033 h1034 h1035 h1036 h1037 h1038 h1039 h1041 h1049  
 G       s1050   t1050  
 B       b1050   s1050  
 T       t1051   o695 b1050 b949  
 B       b1051   t1051  
 T       t1052   o952 b954 b953  
 S       s1052   t671 h h951 h952 h955 h1033 h1034 h1035 h1036 h1037 h1038 h1039 h1041 h1049  
 G       s1052   t1052  
 B       b1052   s1052  
 T       t1053   o695 b1052 b949  
 B       b1053   t1053  
 B       b1054   t1041  
 B       b1055   t1049  
 T       t1055   o619 b1054 b1055  
 H       h1055   z t1055  
 S       s1055   t671 h h951 h952 h955 h1033 h1034 h1035 h1036 h1037 h1038 h1039 h1055  
 G       s1055   t1052  
 B       b1056   s1055  
 T       t1056   o695 b1056 b949  
 B       b1057   t1056  
 B       b1058   t1038  
 B       b1059   t1055  
 T       t1059   o619 b1058 b1059  
 H       h1059   z_1 t1059  
 S       s1059   t671 h h951 h952 h955 h1033 h1034 h1035 h1036 h1037 h1038 h1059  
 G       s1059   t1052  
 B       b1060   s1059  
 T       t1060   o695 b1060 b949  
 B       b1061   t1060  
 B       b1062   t1037  
 B       b1063   t1059  
 T       t1063   o619 b1062 b1063  
 H       h1063   z t1063  
 S       s1063   t671 h h951 h952 h955 h1033 h1034 h1035 h1036 h1037 h1063  
 G       s1063   t1052  
 B       b1064   s1063  
 T       t1064   o695 b1064 b949  
 B       b1065   t1064  
 B       b1066   t1036  
 B       b1067   t1063  
 T       t1067   o619 b1066 b1067  
 H       h1067   z_1 t1067  
 S       s1067   t671 h h951 h952 h955 h1033 h1034 h1035 h1036 h1067  
 G       s1067   t1052  
 B       b1068   s1067  
 T       t1068   o695 b1068 b949  
 B       b1069   t1068  
 B       b1070   t991  
 B       b1071   t1067  
 T       t1071   o619 b1070 b1071  
 H       h1071   z t1071  
 S       s1071   t671 h h951 h952 h955 h1033 h1034 h1035 h1071  
 G       s1071   t1052  
 B       b1072   s1071  
 T       t1072   o695 b1072 b949  
4790  B       b1073   t1072  B       b1073   t1072
4791  B       b1074   t957  T       t1073   o1072 b692 b1073 b4 b4
4792  B       b1075   t1071  B       b1074   t1073
4793  T       t1075   o619 b1074 b1075  P       p1074   String "instHypT [<< 'c >>] 2 ttca thenT dT 8 ttca thenT instHypT [<< 'd >>] 2 ttca thenT dT 9 ttca thenT equivTransT << id{'g2} >> ttca thenT rwh unfold_equiv 8 thenT copyHypT 9 9 thenT rwh unfold_equiv 9 ttca thenT equivSymT ttca"
4794  H       h1075   z_1 t1075  O       o1074   ext_rule p1074
4795  S       s1075   t671 h h951 h952 h955 h1033 h1034 h1075  T       t1074   o693 b1059 b4
4796  G       s1075   t1052  B       b1075   t1074
4797  B       b1076   s1075  T       t1075   o1074 b692 b1075 b4 b4
4798  T       t1076   o695 b1076 b949  B       b1076   t1075
4799  B       b1077   t1076  P       p1076   String "instHypT [<< 'e >>] 2 ttca thenT dT 7 ttca thenT instHypT [<< 'g >>] 2 ttca thenT dT 8 ttca"
4800  B       b1078   t1075  O       o1076   ext_rule p1076
4801  T       t1078   o619 b621 b1078  T       t1076   o623 b626 b537 b535 b1560
4802  H       h1078   z t1078  H       h1076   y t1076
4803  S       s1078   t671 h h951 h952 h955 h1033 h1078  T       t1077   o623 b626 b537 b536 b1560
4804  G       s1078   t1052  H       h1077   y_1 t1077
4805  B       b1079   s1078  S       s1077   t671 h h1019 h518 h519 h520 h527 h1076 h1077
4806  T       t1079   o695 b1079 b949  G       s1077   t543
4807  B       b1080   t1079  B       b1077   s1077
4808  P       p1080   String eq  T       t1078   o695 b1077 b1014
4809  O       o1080   tactic_arg p1080  B       b1078   t1078
4810  B       b1081   t1078  B       b1079   t1077
4811  T       t1081   o619 b620 b1081  T       t1079   o635 b2623 b1079
4812  H       h1081   x_1 t1081  H       h1079   w t1079
4813  S       s1081   t671 h h951 h952 h955 h1081  S       s1079   t671 h h1019 h518 h519 h520 h527 h1076 h1079 h1077
4814  G       s1081   t1052  G       s1079   t543
4815    B       b1080   s1079
4816    T       t1080   o695 b1080 b1014
4817    B       b1081   t1080
4818    S       s1081   t671 h h1019 h518 h519 h520 h527 h1076 h1079
4819    G       s1081   t543
4820  B       b1082   s1081  B       b1082   s1081
4821  T       t1082   o695 b1082 b949  T       t1082   o695 b1082 b1014
4822  B       b1083   t1082  B       b1083   t1082
4823  S       s1083   t671 h h951 h952 h955 h1081  S       s1083   t671 h h1019 h518 h519 h520 h527 h1076
4824  G       s1083   t1004  G       s1083   t543
4825  B       b1084   s1083  B       b1084   s1083
4826  T       t1084   o695 b1084 b949  T       t1084   o695 b1084 b1014
4827  B       b1085   t1084  B       b1085   t1084
4828  T       t1085   o2 b1007  B       b1086   t1076
4829  B       b1086   t1085  T       t1086   o635 b2640 b1086
4830  T       t1086   o694 b1085 b4 b1086  H       h1086   w t1086
4831  B       b1087   t1086  S       s1086   t671 h h1019 h518 h519 h520 h527 h1086 h1076
4832  T       t1087   o2 b1087  G       s1086   t543
4833    B       b1087   s1086
4834    T       t1087   o695 b1087 b1014
4835  B       b1088   t1087  B       b1088   t1087
4836  T       t1088   o1080 b1083 b4 b1088  S       s1088   t671 h h1019 h518 h519 h520 h527 h1086
4837  B       b1089   t1088  G       s1088   t543
4838  T       t1089   o2 b1089  B       b1089   s1088
4839    T       t1089   o695 b1089 b1014
4840  B       b1090   t1089  B       b1090   t1089
4841  T       t1090   o694 b1080 b4 b1090  T       t1095   o694 b1063 b2674 b1030
4842  B       b1091   t1090  B       b1095   t1095
4843  T       t1091   o2 b1091  T       t1096   o2 b1095
4844  B       b1092   t1091  B       b1096   t1096
4845  T       t1092   o694 b1077 b4 b1092  T       t1097   o694 b1090 b4 b1096
4846  B       b1093   t1092  B       b1097   t1097
4847  T       t1093   o2 b1093  T       t1098   o2 b1097
4848  B       b1094   t1093  B       b1098   t1098
4849  T       t1094   o694 b1073 b4 b1094  T       t1099   o694 b1088 b4 b1098
4850  B       b1095   t1094  B       b1099   t1099
4851  T       t1095   o2 b1095  T       t1100   o2 b1099
4852  B       b1096   t1095  B       b1100   t1100
4853  T       t1096   o694 b1069 b4 b1096  T       t1101   o694 b1085 b2670 b1100
4854  B       b1097   t1096  B       b1101   t1101
4855  T       t1097   o2 b1097  T       t1102   o2 b1101
4856  B       b1098   t1097  B       b1102   t1102
4857  T       t1098   o694 b1065 b4 b1098  T       t1103   o694 b1083 b4 b1102
4858  B       b1099   t1098  B       b1103   t1103
4859  T       t1099   o2 b1099  T       t1104   o2 b1103
4860  B       b1100   t1099  B       b1104   t1104
4861  T       t1100   o694 b1061 b4 b1100  T       t1105   o694 b1081 b4 b1104
4862  B       b1101   t1100  B       b1105   t1105
4863  T       t1101   o2 b1101  T       t1106   o2 b1105
4864  B       b1102   t1101  B       b1106   t1106
4865  T       t1102   o694 b1057 b4 b1102  T       t1107   o694 b1078 b4 b1106
4866  B       b1103   t1102  B       b1107   t1107
4867  T       t1103   o2 b1103  T       t1108   o b1107 b4
4868  B       b1104   t1103  B       b1108   t1108
4869  T       t1104   o694 b1053 b711 b1104  T       t1109   o693 b1066 b1108
4870  B       b1105   t1104  B       b1109   t1109
4871  T       t1105   o2 b1105  P       p1109   String "instHypT [<< op{'g1; 'e; 'g} >>] 2 ttca thenT rwh fold_isset 0 ttca thenT dT 9 ttca"
 B       b1106   t1105  
 T       t1106   o694 b1051 b4 b1106  
 B       b1107   t1106  
 T       t1107   o b1107 b4  
 B       b1108   t1107  
 T       t1108   o693 b1007 b1108  
 B       b1109   t1108  
 P       p1109   String "rwh unfold_equal 4 thenT eqSetSymT ttca"  
4872  O       o1109   ext_rule p1109  O       o1109   ext_rule p1109
4873  T       t1109   o693 b1107 b4  T       t1110   o623 b626 b537 b534 b1560
4874  B       b1110   t1109  H       h1110   y_2 t1110
4875  T       t1110   o1109 b692 b1110 b4 b4  S       s1110   t671 h h1019 h518 h519 h520 h527 h1076 h1077 h1110
4876  B       b1111   t1110  G       s1110   t543
4877  T       t1111   o b1111 b4  B       b1110   s1110
4878  B       b1112   t1111  T       t1111   o695 b1110 b1014
4879  T       t1112   o1033 b692 b1109 b1112 b4  B       b1111   t1111
4880  B       b1113   t1112  T       t1112   o629 b528 b624
4881  S       s1113   t671 h h951 h952 h955 h1081  B       b1112   t1112
4882  G       s1113   t1007  B       b1113   t1110
4883    T       t1113   o635 b1112 b1113
4884    H       h1113   w t1113
4885    S       s1113   t671 h h1019 h518 h519 h520 h527 h1076 h1077 h1113 h1110
4886    G       s1113   t543
4887  B       b1114   s1113  B       b1114   s1113
4888  T       t1114   o695 b1114 b949  T       t1114   o695 b1114 b1014
4889  B       b1115   t1114  B       b1115   t1114
4890  T       t1115   o2 b1010  S       s1115   t671 h h1019 h518 h519 h520 h527 h1076 h1077 h1113
4891  B       b1116   t1115  G       s1115   t543
4892  T       t1116   o694 b1115 b4 b1116  B       b1116   s1115
4893    T       t1116   o695 b1116 b1014
4894  B       b1117   t1116  B       b1117   t1116
4895  T       t1117   o2 b1117  T       t1117   o694 b1078 b4173 b1106
4896  B       b1118   t1117  B       b1118   t1117
4897  T       t1118   o1080 b1083 b4 b1118  T       t1118   o2 b1118
4898  B       b1119   t1118  B       b1119   t1118
4899  T       t1119   o2 b1119  T       t1119   o694 b1117 b4 b1119
4900  B       b1120   t1119  B       b1120   t1119
4901  T       t1120   o694 b1080 b4 b1120  T       t1120   o2 b1120
4902  B       b1121   t1120  B       b1121   t1120
4903  T       t1121   o2 b1121  T       t1121   o694 b1115 b4 b1121
4904  B       b1122   t1121  B       b1122   t1121
4905  T       t1122   o694 b1077 b4 b1122  T       t1122   o2 b1122
4906  B       b1123   t1122  B       b1123   t1122
4907  T       t1123   o2 b1123  T       t1126   o694 b1111 b4 b1123
4908  B       b1124   t1123  B       b1126   t1126
4909  T       t1124   o694 b1073 b4 b1124  T       t1127   o b1126 b4
4910  B       b1125   t1124  B       b1127   t1127
4911