matita/matita/contribs/lambdadelta/basic_1A/names.txt

   1 A
   2 Abbr
   3 Abst
   4 abst_dec
   5 AHead
   6 ahead_inj_snd
   7 aplus
   8 aplus_ahead_simpl
   9 aplus_asort_le_simpl
  10 aplus_asort_O_simpl
  11 aplus_asort_simpl
  12 aplus_assoc
  13 aplus_asucc
  14 aplus_asucc_false
  15 aplus_gz_ge
  16 aplus_gz_le
  17 aplus_inj
  18 aplus_reg_r
  19 aplus_sort_O_S_simpl
  20 aplus_sort_S_S_simpl
  21 app1
  22 Appl
  23 aprem
  24 aprem_asucc
  25 aprem_gen_head_O
  26 aprem_gen_head_S
  27 aprem_gen_sort
  28 aprem_repl
  29 aprem_succ
  30 aprem_zero
  31 arity
  32 arity_abbr
  33 arity_abst
  34 arity_appl
  35 arity_appls_abbr
  36 arity_appls_appl
  37 arity_appls_bind
  38 arity_appls_cast
  39 arity_aprem
  40 arity_bind
  41 arity_cast
  42 arity_cimp_conf
  43 arity_fsubst0
  44 arity_gen_abst
  45 arity_gen_appl
  46 arity_gen_appls
  47 arity_gen_bind
  48 arity_gen_cast
  49 arity_gen_cvoid
  50 arity_gen_cvoid_subst0
  51 arity_gen_lift
  52 arity_gen_lref
  53 arity_gen_sort
  54 arity_head
  55 arity_lift
  56 arity_lift1
  57 arity_mono
  58 arity_nf2_inv_all
  59 arity_repellent
  60 arity_repl
  61 arity_sort
  62 arity_sred_pr2
  63 arity_sred_pr3
  64 arity_sred_wcpr0_pr0
  65 arity_sred_wcpr0_pr1
  66 arity_subst0
  67 ASort
  68 asucc
  69 asucc_gen_head
  70 asucc_gen_sort
  71 asucc_inj
  72 asucc_repl
  73 B
  74 Bind
  75 bind_dec_not
  76 binder_dec
  77 C
  78 Cast
  79 cbk
  80 CHead
  81 chead_ctail
  82 cimp
  83 cimp_bind
  84 cimp_flat_dx
  85 cimp_flat_sx
  86 cimp_getl_conf
  87 cle
  88 clear
  89 clear_bind
  90 clear_cle
  91 clear_clear
  92 clear_ctail
  93 clear_flat
  94 clear_gen_all
  95 clear_gen_bind
  96 clear_gen_flat
  97 clear_gen_flat_r
  98 clear_gen_sort
  99 clear_getl_trans
 100 clear_mono
 101 clear_pc3_trans
 102 clear_pr2_trans
 103 clear_pr3_trans
 104 clear_trans
 105 clear_wf3_trans
 106 cle_flt_trans
 107 cle_head
 108 clen
 109 cle_r
 110 cle_trans_head
 111 clt
 112 clt_cong
 113 clt_head
 114 clt_thead
 115 clt_wf_ind
 116 clt_wf__q_ind
 117 cnt
 118 cnt_head
 119 cnt_lift
 120 cnt_sort
 121 CSort
 122 csuba
 123 csuba_abst
 124 csuba_arity
 125 csuba_arity_rev
 126 csuba_clear_conf
 127 csuba_clear_trans
 128 csuba_drop_abbr
 129 csuba_drop_abbr_rev
 130 csuba_drop_abst
 131 csuba_drop_abst_rev
 132 csuba_gen_abbr
 133 csuba_gen_abbr_rev
 134 csuba_gen_abst
 135 csuba_gen_abst_rev
 136 csuba_gen_bind
 137 csuba_gen_bind_rev
 138 csuba_gen_flat
 139 csuba_gen_flat_rev
 140 csuba_gen_void
 141 csuba_gen_void_rev
 142 csuba_getl_abbr
 143 csuba_getl_abbr_rev
 144 csuba_getl_abst
 145 csuba_getl_abst_rev
 146 csuba_head
 147 csuba_refl
 148 csuba_sort
 149 csuba_void
 150 csubc
 151 csubc_abst
 152 csubc_arity_conf
 153 csubc_arity_trans
 154 csubc_clear_conf
 155 csubc_csuba
 156 csubc_drop1_conf_rev
 157 csubc_drop_conf_O
 158 csubc_drop_conf_rev
 159 csubc_gen_head_l
 160 csubc_gen_head_r
 161 csubc_gen_sort_l
 162 csubc_gen_sort_r
 163 csubc_getl_conf
 164 csubc_head
 165 csubc_refl
 166 csubc_sort
 167 csubc_void
 168 csubst0
 169 csubst0_both
 170 csubst0_both_bind
 171 csubst0_clear_O
 172 csubst0_clear_O_back
 173 csubst0_clear_S
 174 csubst0_clear_trans
 175 csubst0_drop_eq
 176 csubst0_drop_eq_back
 177 csubst0_drop_gt
 178 csubst0_drop_gt_back
 179 csubst0_drop_lt
 180 csubst0_drop_lt_back
 181 csubst0_fst
 182 csubst0_fst_bind
 183 csubst0_gen_head
 184 csubst0_gen_S_bind_2
 185 csubst0_gen_sort
 186 csubst0_getl_ge
 187 csubst0_getl_ge_back
 188 csubst0_getl_lt
 189 csubst0_getl_lt_back
 190 csubst0_snd
 191 csubst0_snd_bind
 192 csubst1
 193 csubst1_bind
 194 csubst1_flat
 195 csubst1_gen_head
 196 csubst1_getl_ge
 197 csubst1_getl_ge_back
 198 csubst1_getl_lt
 199 csubst1_head
 200 csubst1_refl
 201 csubst1_sing
 202 csubt
 203 csubt_abst
 204 csubt_clear_conf
 205 csubt_csuba
 206 csubt_drop_abbr
 207 csubt_drop_abst
 208 csubt_drop_flat
 209 csubt_gen_abbr
 210 csubt_gen_abst
 211 csubt_gen_bind
 212 csubt_gen_flat
 213 csubt_getl_abbr
 214 csubt_getl_abst
 215 csubt_head
 216 csubt_pc3
 217 csubt_pr2
 218 csubt_refl
 219 csubt_sort
 220 csubt_ty3
 221 csubt_ty3_ld
 222 csubt_void
 223 csubv
 224 csubv_bind
 225 csubv_bind_same
 226 csubv_clear_conf
 227 csubv_clear_conf_void
 228 csubv_drop_conf
 229 csubv_flat
 230 csubv_getl_conf
 231 csubv_getl_conf_void
 232 csubv_refl
 233 csubv_sort
 234 csubv_void
 235 CTail
 236 c_tail_ind
 237 cweight
 238 dnf_dec
 239 dnf_dec2
 240 drop
 241 drop1
 242 drop1_cons
 243 drop1_cons_tail
 244 drop1_csubc_trans
 245 drop1_gen_pcons
 246 drop1_gen_pnil
 247 drop1_getl_trans
 248 drop1_nil
 249 drop1_skip_bind
 250 drop1_trans
 251 drop_clear
 252 drop_clear_O
 253 drop_clear_S
 254 drop_conf_ge
 255 drop_conf_lt
 256 drop_conf_rev
 257 drop_csubc_trans
 258 drop_ctail
 259 drop_drop
 260 drop_gen_drop
 261 drop_gen_refl
 262 drop_gen_skip_l
 263 drop_gen_skip_r
 264 drop_gen_sort
 265 drop_getl_trans_ge
 266 drop_getl_trans_le
 267 drop_getl_trans_lt
 268 drop_mono
 269 drop_refl
 270 drop_S
 271 drop_skip
 272 drop_skip_bind
 273 drop_skip_flat
 274 drop_trans_ge
 275 drop_trans_le
 276 ex1_arity
 277 ex1_c
 278 ex1__leq_sort_SS
 279 ex1_t
 280 ex1_ty3
 281 ex2_arity
 282 ex2_c
 283 ex2_nf2
 284 ex2_t
 285 F
 286 Flat
 287 flt
 288 flt_arith0
 289 flt_arith1
 290 flt_arith2
 291 flt_shift
 292 flt_thead_dx
 293 flt_thead_sx
 294 flt_trans
 295 flt_wf_ind
 296 flt_wf__q_ind
 297 fsubst0
 298 fsubst0_both
 299 fsubst0_fst
 300 fsubst0_gen_base
 301 fsubst0_snd
 302 fweight
 303 G
 304 getl
 305 getl_clear_bind
 306 getl_clear_conf
 307 getl_clear_trans
 308 getl_conf_ge_drop
 309 getl_conf_le
 310 getl_csubst1
 311 getl_ctail
 312 getl_ctail_clen
 313 getl_dec
 314 getl_drop
 315 getl_drop_conf_ge
 316 getl_drop_conf_lt
 317 getl_drop_conf_rev
 318 getl_drop_trans
 319 getl_flat
 320 getl_flt
 321 getl_gen_2
 322 getl_gen_all
 323 getl_gen_bind
 324 getl_gen_flat
 325 getl_gen_O
 326 getl_gen_S
 327 getl_gen_sort
 328 getl_gen_tail
 329 getl_head
 330 getl_intro
 331 getl_mono
 332 getl_refl
 333 getl_trans
 334 getl_wf3_trans
 335 gz
 336 iso
 337 iso_flats_flat_bind_false
 338 iso_flats_lref_bind_false
 339 iso_gen_head
 340 iso_gen_lref
 341 iso_gen_sort
 342 iso_head
 343 iso_lref
 344 iso_refl
 345 iso_sort
 346 iso_trans
 347 K
 348 leq
 349 leq_ahead_asucc_false
 350 leq_ahead_false_1
 351 leq_ahead_false_2
 352 leq_asucc
 353 leq_asucc_false
 354 leq_eq
 355 leq_gen_head1
 356 leq_gen_head2
 357 leq_gen_sort1
 358 leq_gen_sort2
 359 leq_head
 360 leq_leqz
 361 leq_refl
 362 leq_sort
 363 leq_sym
 364 leq_trans
 365 leqz
 366 leqz_head
 367 leqz_leq
 368 leqz_sort
 369 lift
 370 lift1
 371 lift1_bind
 372 lift1_cons_tail
 373 lift1_flat
 374 lift1_free
 375 lift1_lift1
 376 lift1_lref
 377 lift1_sort
 378 lift1_xhg
 379 lift_bind
 380 lift_d
 381 lift_flat
 382 lift_free
 383 lift_free_sym
 384 lift_gen_bind
 385 lift_gen_flat
 386 lift_gen_head
 387 lift_gen_lift
 388 lift_gen_lref
 389 lift_gen_lref_false
 390 lift_gen_lref_ge
 391 lift_gen_lref_lt
 392 lift_gen_sort
 393 lift_head
 394 lift_inj
 395 lift_lref_ge
 396 lift_lref_gt
 397 lift_lref_lt
 398 lift_r
 399 lifts
 400 lifts1
 401 lifts1_cons
 402 lifts1_flat
 403 lifts1_nil
 404 lifts1_xhg
 405 lifts_inj
 406 lift_sort
 407 lifts_tapp
 408 lift_tle
 409 lift_tlt_dx
 410 lift_weight
 411 lift_weight_add
 412 lift_weight_add_O
 413 lift_weight_map
 414 llt
 415 llt_head_dx
 416 llt_head_sx
 417 llt_repl
 418 llt_trans
 419 llt_wf_ind
 420 llt_wf__q_ind
 421 lref_map
 422 lweight
 423 lweight_repl
 424 minus_s_s
 425 mk_G
 426 next_plus
 427 next_plus_assoc
 428 next_plus_gz
 429 next_plus_lt
 430 next_plus_next
 431 nf0_dec
 432 nf2
 433 nf2_abst
 434 nf2_abst_shift
 435 nf2_appl_lref
 436 nf2_appls_lref
 437 nf2_csort_lref
 438 nf2_dec
 439 nf2_gen_abbr
 440 nf2_gen_abst
 441 nf2_gen_beta
 442 nf2_gen_cast
 443 nf2_gen_flat
 444 nf2_gen_lref
 445 nf2_gen__nf2_gen_aux
 446 nf2_gen_void
 447 nf2_iso_appls_lref
 448 nf2_lift
 449 nf2_lift1
 450 nf2_lref_abst
 451 nf2_pr3_confluence
 452 nf2_pr3_unfold
 453 nf2_sn3
 454 nf2_sort
 455 nfs2
 456 nfs2_tapp
 457 node_inh
 458 not_abbr_abst
 459 not_abbr_void
 460 not_abst_void
 461 not_void_abst
 462 pc1
 463 pc1_head
 464 pc1_head_1
 465 pc1_head_2
 466 pc1_pr0_r
 467 pc1_pr0_u
 468 pc1_pr0_u2
 469 pc1_pr0_x
 470 pc1_refl
 471 pc1_s
 472 pc1_t
 473 pc3
 474 pc3_abst_dec
 475 pc3_dec
 476 pc3_eta
 477 pc3_fsubst0
 478 pc3_gen_abst
 479 pc3_gen_abst_shift
 480 pc3_gen_appls_lref_abst
 481 pc3_gen_appls_lref_sort
 482 pc3_gen_appls_sort_abst
 483 pc3_gen_cabbr
 484 pc3_gen_lift
 485 pc3_gen_lift_abst
 486 pc3_gen_not_abst
 487 pc3_gen_sort
 488 pc3_gen_sort_abst
 489 pc3_head_1
 490 pc3_head_12
 491 pc3_head_2
 492 pc3_head_21
 493 pc3_ind_left
 494 pc3_ind_left__pc3_left_pc3
 495 pc3_ind_left__pc3_left_pr3
 496 pc3_ind_left__pc3_left_sym
 497 pc3_ind_left__pc3_left_trans
 498 pc3_ind_left__pc3_pc3_left
 499 pc3_left
 500 pc3_left_r
 501 pc3_left_ur
 502 pc3_left_ux
 503 pc3_lift
 504 pc3_nf2
 505 pc3_nf2_unfold
 506 pc3_pc1
 507 pc3_pr0_pr2_t
 508 pc3_pr2_fsubst0
 509 pc3_pr2_fsubst0_back
 510 pc3_pr2_pr2_t
 511 pc3_pr2_pr3_t
 512 pc3_pr2_r
 513 pc3_pr2_u
 514 pc3_pr2_u2
 515 pc3_pr2_x
 516 pc3_pr3_conf
 517 pc3_pr3_pc3_t
 518 pc3_pr3_r
 519 pc3_pr3_t
 520 pc3_pr3_x
 521 pc3_refl
 522 pc3_s
 523 pc3_t
 524 pc3_thin_dx
 525 pc3_wcpr0
 526 pc3_wcpr0__pc3_wcpr0_t_aux
 527 pc3_wcpr0_t
 528 pr0
 529 pr0_beta
 530 pr0_comp
 531 pr0_confluence
 532 pr0_confluence__pr0_cong_delta
 533 pr0_confluence__pr0_cong_upsilon_cong
 534 pr0_confluence__pr0_cong_upsilon_delta
 535 pr0_confluence__pr0_cong_upsilon_refl
 536 pr0_confluence__pr0_cong_upsilon_zeta
 537 pr0_confluence__pr0_delta_delta
 538 pr0_confluence__pr0_delta_tau
 539 pr0_confluence__pr0_upsilon_upsilon
 540 pr0_delta
 541 pr0_delta1
 542 pr0_gen_abbr
 543 pr0_gen_abst
 544 pr0_gen_appl
 545 pr0_gen_cast
 546 pr0_gen_lift
 547 pr0_gen_lref
 548 pr0_gen_sort
 549 pr0_gen_void
 550 pr0_lift
 551 pr0_refl
 552 pr0_subst0
 553 pr0_subst0_back
 554 pr0_subst0_fwd
 555 pr0_subst1
 556 pr0_subst1_back
 557 pr0_subst1_fwd
 558 pr0_tau
 559 pr0_upsilon
 560 pr0_zeta
 561 pr1
 562 pr1_comp
 563 pr1_confluence
 564 pr1_eta
 565 pr1_head_1
 566 pr1_head_2
 567 pr1_pr0
 568 pr1_refl
 569 pr1_sing
 570 pr1_strip
 571 pr1_t
 572 pr2
 573 pr2_cflat
 574 pr2_change
 575 pr2_confluence
 576 pr2_confluence__pr2_delta_delta
 577 pr2_confluence__pr2_free_delta
 578 pr2_confluence__pr2_free_free
 579 pr2_ctail
 580 pr2_delta
 581 pr2_delta1
 582 pr2_free
 583 pr2_gen_abbr
 584 pr2_gen_abst
 585 pr2_gen_appl
 586 pr2_gen_cabbr
 587 pr2_gen_cast
 588 pr2_gen_cbind
 589 pr2_gen_cflat
 590 pr2_gen_csort
 591 pr2_gen_ctail
 592 pr2_gen_lift
 593 pr2_gen_lref
 594 pr2_gen_sort
 595 pr2_gen_void
 596 pr2_head_1
 597 pr2_head_2
 598 pr2_lift
 599 pr2_subst1
 600 pr2_thin_dx
 601 pr3
 602 pr3_cflat
 603 pr3_confluence
 604 pr3_eta
 605 pr3_flat
 606 pr3_gen_abbr
 607 pr3_gen_abst
 608 pr3_gen_appl
 609 pr3_gen_bind
 610 pr3_gen_cabbr
 611 pr3_gen_cast
 612 pr3_gen_lift
 613 pr3_gen_lref
 614 pr3_gen_sort
 615 pr3_gen_void
 616 pr3_head_1
 617 pr3_head_12
 618 pr3_head_2
 619 pr3_head_21
 620 pr3_iso_appl_bind
 621 pr3_iso_appls_abbr
 622 pr3_iso_appls_appl_bind
 623 pr3_iso_appls_beta
 624 pr3_iso_appls_bind
 625 pr3_iso_appls_cast
 626 pr3_iso_beta
 627 pr3_lift
 628 pr3_pr0_pr2_t
 629 pr3_pr1
 630 pr3_pr2
 631 pr3_pr2_pr2_t
 632 pr3_pr2_pr3_t
 633 pr3_pr3_pr3_t
 634 pr3_refl
 635 pr3_sing
 636 pr3_strip
 637 pr3_subst1
 638 pr3_t
 639 pr3_thin_dx
 640 pr3_wcpr0_t
 641 ptrans
 642 r
 643 r_arith0
 644 r_arith1
 645 r_arith2
 646 r_arith3
 647 r_arith4
 648 r_arith5
 649 r_arith6
 650 r_arith7
 651 r_dis
 652 r_minus
 653 r_plus
 654 r_plus_sym
 655 r_S
 656 s
 657 s_arith0
 658 s_arith1
 659 sc3
 660 sc3_abbr
 661 sc3_abst
 662 sc3_appl
 663 sc3_arity
 664 sc3_arity_csubc
 665 sc3_arity_gen
 666 sc3_bind
 667 sc3_cast
 668 sc3_lift
 669 sc3_lift1
 670 sc3_props__sc3_sn3_abst
 671 sc3_repl
 672 sc3_sn3
 673 s_inc
 674 s_inj
 675 s_le
 676 s_le_gen
 677 s_lt
 678 s_lt_gen
 679 s_minus
 680 sn3
 681 sn3_abbr
 682 sn3_appl_abbr
 683 sn3_appl_appl
 684 sn3_appl_appls
 685 sn3_appl_beta
 686 sn3_appl_bind
 687 sn3_appl_cast
 688 sn3_appl_lref
 689 sn3_appls_abbr
 690 sn3_appls_beta
 691 sn3_appls_bind
 692 sn3_appls_cast
 693 sn3_appls_lref
 694 sn3_beta
 695 sn3_bind
 696 sn3_cast
 697 sn3_cdelta
 698 sn3_cflat
 699 sn3_change
 700 sn3_cpr3_trans
 701 sn3_gen_bind
 702 sn3_gen_cflat
 703 sn3_gen_def
 704 sn3_gen_flat
 705 sn3_gen_head
 706 sn3_gen_lift
 707 sn3_lift
 708 sn3_nf2
 709 sn3_pr2_intro
 710 sn3_pr3_trans
 711 sn3_shift
 712 sn3_sing
 713 sns3
 714 sns3_lifts
 715 sns3_lifts1
 716 s_plus
 717 s_plus_sym
 718 s_r
 719 s_S
 720 sty0
 721 sty0_abbr
 722 sty0_abst
 723 sty0_appl
 724 sty0_bind
 725 sty0_cast
 726 sty0_correct
 727 sty0_gen_appl
 728 sty0_gen_bind
 729 sty0_gen_cast
 730 sty0_gen_lref
 731 sty0_gen_sort
 732 sty0_lift
 733 sty0_sort
 734 sty1
 735 sty1_abbr
 736 sty1_appl
 737 sty1_bind
 738 sty1_cast2
 739 sty1_cnt
 740 sty1_correct
 741 sty1_lift
 742 sty1_sing
 743 sty1_sty0
 744 sty1_trans
 745 subst
 746 subst0
 747 subst0_both
 748 subst0_confluence_eq
 749 subst0_confluence_lift
 750 subst0_confluence_neq
 751 subst0_fst
 752 subst0_gen_head
 753 subst0_gen_lift_false
 754 subst0_gen_lift_ge
 755 subst0_gen_lift_lt
 756 subst0_gen_lift_rev_ge
 757 subst0_gen_lref
 758 subst0_gen_sort
 759 subst0_lift_ge
 760 subst0_lift_ge_s
 761 subst0_lift_ge_S
 762 subst0_lift_lt
 763 subst0_lref
 764 subst0_refl
 765 subst0_snd
 766 subst0_subst0
 767 subst0_subst0_back
 768 subst0_tlt
 769 subst0_tlt_head
 770 subst0_trans
 771 subst0_weight_le
 772 subst0_weight_lt
 773 subst1
 774 subst1_confluence_eq
 775 subst1_confluence_lift
 776 subst1_confluence_neq
 777 subst1_ex
 778 subst1_gen_head
 779 subst1_gen_lift_eq
 780 subst1_gen_lift_ge
 781 subst1_gen_lift_lt
 782 subst1_gen_lref
 783 subst1_gen_sort
 784 subst1_head
 785 subst1_lift_ge
 786 subst1_lift_lt
 787 subst1_lift_S
 788 subst1_refl
 789 subst1_single
 790 subst1_subst1
 791 subst1_subst1_back
 792 subst1_trans
 793 subst_head
 794 subst_lift_SO
 795 subst_lref_eq
 796 subst_lref_gt
 797 subst_lref_lt
 798 subst_sort
 799 subst_subst0
 800 T
 801 TApp
 802 TCons
 803 tcons_tapp_ex
 804 term_dec
 805 terms_props__bind_dec
 806 terms_props__flat_dec
 807 terms_props__kind_dec
 808 THead
 809 THeads
 810 theads_tapp
 811 thead_x_lift_y_y
 812 thead_x_y_y
 813 tle
 814 tle_r
 815 TList
 816 tlist_ind_rev
 817 TLRef
 818 tlt
 819 tlt_head_dx
 820 tlt_head_sx
 821 tlt_trans
 822 tlt_wf_ind
 823 tlt_wf__q_ind
 824 TNil
 825 trans
 826 tslen
 827 tslt
 828 tslt_wf_ind
 829 tslt_wf__q_ind
 830 TSort
 831 tweight
 832 tweight_lt
 833 ty3
 834 ty3_abbr
 835 ty3_abst
 836 ty3_acyclic
 837 ty3_appl
 838 ty3_arity
 839 ty3_bind
 840 ty3_cast
 841 ty3_conv
 842 ty3_correct
 843 ty3_cred_pr2
 844 ty3_cred_pr3
 845 ty3_csubst0
 846 ty3_fsubst0
 847 ty3_gen_abst_abst
 848 ty3_gen_appl
 849 ty3_gen_appl_nf2
 850 ty3_gen_bind
 851 ty3_gen_cabbr
 852 ty3_gen_cast
 853 ty3_gen_cvoid
 854 ty3_gen_lift
 855 ty3_gen_lref
 856 ty3_gen_sort
 857 ty3_getl_subst0
 858 ty3_inference
 859 ty3_inv_appls_lref_nf2
 860 ty3_inv_lref_lref_nf2
 861 ty3_inv_lref_nf2
 862 ty3_inv_lref_nf2_pc3
 863 ty3_lift
 864 ty3_nf2_gen__ty3_nf2_inv_abst_aux
 865 ty3_nf2_inv_abst
 866 ty3_nf2_inv_abst_premise
 867 ty3_nf2_inv_abst_premise_csort
 868 ty3_nf2_inv_all
 869 ty3_nf2_inv_sort
 870 ty3_predicative
 871 ty3_repellent
 872 ty3_sconv
 873 ty3_sconv_pc3
 874 ty3_shift1
 875 ty3_sn3
 876 ty3_sort
 877 ty3_sred_back
 878 ty3_sred_pr0
 879 ty3_sred_pr1
 880 ty3_sred_pr2
 881 ty3_sred_pr3
 882 ty3_sred_wcpr0_pr0
 883 ty3_sty0
 884 ty3_subst0
 885 ty3_tred
 886 ty3_typecheck
 887 ty3_unique
 888 tys3
 889 tys3_cons
 890 tys3_gen_cons
 891 tys3_gen_nil
 892 tys3_nil
 893 Void
 894 wadd
 895 wadd_le
 896 wadd_lt
 897 wadd_O
 898 wcpr0
 899 wcpr0_comp
 900 wcpr0_drop
 901 wcpr0_drop_back
 902 wcpr0_gen_head
 903 wcpr0_gen_sort
 904 wcpr0_getl
 905 wcpr0_getl_back
 906 wcpr0_refl
 907 weight
 908 weight_add_O
 909 weight_add_S
 910 weight_eq
 911 weight_le
 912 weight_map
 913 wf3
 914 wf3_bind
 915 wf3_clear_conf
 916 wf3_flat
 917 wf3_gen_bind1
 918 wf3_gen_flat1
 919 wf3_gen_head2
 920 wf3_gen_sort1
 921 wf3_getl_conf
 922 wf3_idem
 923 wf3_mono
 924 wf3_pc3_conf
 925 wf3_pr2_conf
 926 wf3_pr3_conf
 927 wf3_sort
 928 wf3_total
 929 wf3_ty3
 930 wf3_ty3_conf
 931 wf3_void