matita/matita/contribs/lambdadelta/basic_2A/names.txt

   1 aaa
   2 aaa_abbr
   3 aaa_abst
   4 aaa_appl
   5 aaa_cast
   6 aaa_csx
   7 aaa_da
   8 aaa_fqu_conf
   9 aaa_fqup_conf
  10 aaa_fquq_conf
  11 aaa_fqus_conf
  12 aaa_fsb
  13 aaa_fsba
  14 aaa_ind_csx
  15 aaa_ind_csx_alt
  16 aaa_ind_csx_alt_aux
  17 aaa_ind_csx_aux
  18 aaa_ind_fpb
  19 aaa_ind_fpb_aux
  20 aaa_ind_fpbg
  21 aaa_ind_fpbg_aux
  22 aaa_inv_abbr
  23 aaa_inv_abbr_aux
  24 aaa_inv_abst
  25 aaa_inv_abst_aux
  26 aaa_inv_appl
  27 aaa_inv_appl_aux
  28 aaa_inv_cast
  29 aaa_inv_cast_aux
  30 aaa_inv_gref
  31 aaa_inv_gref_aux
  32 aaa_inv_lift
  33 aaa_inv_lref
  34 aaa_inv_lref_aux
  35 aaa_inv_sort
  36 aaa_inv_sort_aux
  37 aaa_lift
  38 aaa_lifts
  39 aaa_lleq_conf
  40 aaa_lref
  41 aaa_lstas
  42 aaa_mono
  43 aaa_sort
  44 aarity
  45 AAtom
  46 Abbr
  47 Abst
  48 acr
  49 acr_aaa
  50 acr_aaa_csubc_lifts
  51 acr_abst
  52 acr_gcr
  53 APair
  54 append
  55 append_assoc
  56 append_atom_sn
  57 append_inj_dx
  58 append_inj_sn
  59 append_inv_pair_dx
  60 append_inv_refl_dx
  61 append_length
  62 Appl
  63 ApplDelta
  64 ApplDelta_lift
  65 ApplOmega1
  66 ApplOmega2
  67 ApplOmega3
  68 applv
  69 applv_simple
  70 at
  71 at_ge
  72 at_inv_cons
  73 at_inv_cons_aux
  74 at_inv_cons_ge
  75 at_inv_cons_lt
  76 at_inv_nil
  77 at_inv_nil_aux
  78 at_lt
  79 at_mono
  80 at_nil
  81 bind2
  82 Bind2
  83 candidate
  84 Cast
  85 ceq
  86 cfun
  87 cir
  88 cir_appl
  89 cir_cnr
  90 cir_gref
  91 cir_ib2
  92 cir_inv_appl
  93 cir_inv_bind
  94 cir_inv_delta
  95 cir_inv_flat
  96 cir_inv_ib2
  97 cir_inv_lift
  98 cir_inv_ri2
  99 cir_lift
 100 cir_sort
 101 cix
 102 cix_appl
 103 cix_cnx
 104 cix_gref
 105 cix_ib2
 106 cix_inv_appl
 107 cix_inv_bind
 108 cix_inv_cir
 109 cix_inv_delta
 110 cix_inv_flat
 111 cix_inv_ib2
 112 cix_inv_lift
 113 cix_inv_ri2
 114 cix_inv_sort
 115 cix_lift
 116 cix_lref
 117 cix_sort
 118 cnr
 119 cnr_abst
 120 cnr_appl_simple
 121 cnr_dec
 122 cnr_inv_abbr
 123 cnr_inv_abst
 124 cnr_inv_appl
 125 cnr_inv_cir
 126 cnr_inv_crr
 127 cnr_inv_delta
 128 cnr_inv_eps
 129 cnr_inv_lift
 130 cnr_inv_zeta
 131 cnr_lift
 132 cnr_lref_abst
 133 cnr_lref_atom
 134 cnr_lref_free
 135 cnr_sort
 136 cnx
 137 cnx_abst
 138 cnx_appl_simple
 139 cnx_csx
 140 cnx_dec
 141 cnx_fwd_cnr
 142 cnx_inv_abbr
 143 cnx_inv_abst
 144 cnx_inv_appl
 145 cnx_inv_cix
 146 cnx_inv_crx
 147 cnx_inv_delta
 148 cnx_inv_eps
 149 cnx_inv_lift
 150 cnx_inv_sort
 151 cnx_inv_zeta
 152 cnx_lift
 153 cnx_lref_atom
 154 cnx_lref_free
 155 cnx_sort
 156 cnx_sort_iter
 157 CP0
 158 CP1
 159 CP2
 160 CP3
 161 cpc
 162 cpc_conf
 163 cpc_cpcs
 164 cpc_fwd_cpr
 165 cpc_refl
 166 cpcs
 167 cpcs_aaa_mono
 168 cpcs_bind1
 169 cpcs_bind2
 170 cpcs_bind_dx
 171 cpcs_bind_sn
 172 cpcs_canc_dx
 173 cpcs_canc_sn
 174 cpcs_cpr_conf
 175 cpcs_cpr_div
 176 cpcs_cprs_conf
 177 cpcs_cprs_div
 178 cpcs_cprs_dx
 179 cpcs_cprs_sn
 180 cpcs_cprs_strap1
 181 cpcs_cprs_strap2
 182 cpcs_cpr_strap1
 183 cpcs_cpr_strap2
 184 cpcs_flat
 185 cpcs_flat_dx_cpr_rev
 186 cpcs_ind
 187 cpcs_ind_dx
 188 cpcs_inv_abst1
 189 cpcs_inv_abst2
 190 cpcs_inv_abst_dx
 191 cpcs_inv_abst_sn
 192 cpcs_inv_cprs
 193 cpcs_inv_lift
 194 cpcs_inv_sort
 195 cpcs_inv_sort_abst
 196 cpcs_lift
 197 cpcs_refl
 198 cpcs_scpes
 199 cpcs_strap1
 200 cpcs_strap2
 201 cpcs_strip
 202 cpcs_sym
 203 cpcs_trans
 204 cpc_sym
 205 cpr
 206 cpr_aaa_conf
 207 cpr_ApplOmega_12
 208 cpr_ApplOmega_23
 209 cpr_atom
 210 cpr_beta
 211 cpr_bind
 212 cpr_bind2
 213 cpr_conf
 214 cpr_conf_lpr
 215 cpr_conf_lpr_atom_atom
 216 cpr_conf_lpr_atom_delta
 217 cpr_conf_lpr_beta_beta
 218 cpr_conf_lpr_bind_bind
 219 cpr_conf_lpr_bind_zeta
 220 cpr_conf_lpr_delta_delta
 221 cpr_conf_lpr_eps_eps
 222 cpr_conf_lpr_flat_beta
 223 cpr_conf_lpr_flat_eps
 224 cpr_conf_lpr_flat_flat
 225 cpr_conf_lpr_flat_theta
 226 cpr_conf_lpr_theta_theta
 227 cpr_conf_lpr_zeta_zeta
 228 cpr_cpcs_dx
 229 cpr_cpcs_sn
 230 cpr_cprs
 231 cpr_cprs_conf_cpcs
 232 cpr_cprs_div
 233 cpr_cpx
 234 cpr_delift
 235 cpr_delta
 236 cpr_div
 237 cpre
 238 cpre_mono
 239 cpr_eps
 240 cpr_flat
 241 cpr_fpb
 242 cpr_fpbq
 243 cpr_fwd_bind1_minus
 244 cpr_fwd_cir
 245 cpr_inv_abbr1
 246 cpr_inv_abst1
 247 cpr_inv_appl1
 248 cpr_inv_appl1_simple
 249 cpr_inv_atom1
 250 cpr_inv_atom1_aux
 251 cpr_inv_bind1
 252 cpr_inv_bind1_aux
 253 cpr_inv_cast1
 254 cpr_inv_flat1
 255 cpr_inv_flat1_aux
 256 cpr_inv_gref1
 257 cpr_inv_lift1
 258 cpr_inv_lref1
 259 cpr_inv_sort1
 260 cpr_lift
 261 cpr_llpx_sn_conf
 262 cpr_lpr_fpbs
 263 cpr_lpr_sta_fpbs
 264 cpr_Omega_12
 265 cpr_Omega_21
 266 cpr_pair_sn
 267 cpr_refl
 268 cprs
 269 cprs_aaa_conf
 270 cprs_beta
 271 cprs_beta_dx
 272 cprs_beta_rc
 273 cprs_bind
 274 cprs_bind2
 275 cprs_bind2_dx
 276 cprs_bind_dx
 277 cprs_conf
 278 cprs_conf_cpcs
 279 cprs_cpr_conf_cpcs
 280 cprs_cpr_div
 281 cprs_cpxs
 282 cprs_delta
 283 cprs_div
 284 cprs_eps
 285 cprs_flat
 286 cprs_flat_dx
 287 cprs_flat_sn
 288 cprs_fpbs
 289 cprs_ind
 290 cprs_ind_dx
 291 cprs_inv_abbr1
 292 cprs_inv_abst
 293 cprs_inv_abst1
 294 cprs_inv_appl1
 295 cprs_inv_cast1
 296 cprs_inv_cnr1
 297 cprs_inv_lift1
 298 cprs_inv_lref1
 299 cprs_inv_sort1
 300 cprs_lift
 301 cprs_lpr_conf_dx
 302 cprs_lpr_conf_sn
 303 cprs_refl
 304 cprs_scpds_div
 305 cprs_strap1
 306 cprs_strap2
 307 cprs_strip
 308 cprs_theta
 309 cprs_theta_dx
 310 cprs_theta_rc
 311 cprs_trans
 312 cprs_zeta
 313 cpr_theta
 314 cpr_zeta
 315 cpx
 316 cpx_aaa_conf
 317 cpx_atom
 318 cpx_beta
 319 cpx_bind
 320 cpx_bind2
 321 cpx_cpxs
 322 cpx_ct
 323 cpx_delift
 324 cpx_delta
 325 cpxe
 326 cpx_eps
 327 cpx_flat
 328 cpx_frees_trans
 329 cpx_fwd_bind1_minus
 330 cpx_fwd_cix
 331 cpx_inv_abbr1
 332 cpx_inv_abst1
 333 cpx_inv_appl1
 334 cpx_inv_appl1_simple
 335 cpx_inv_atom1
 336 cpx_inv_atom1_aux
 337 cpx_inv_bind1
 338 cpx_inv_bind1_aux
 339 cpx_inv_cast1
 340 cpx_inv_flat1
 341 cpx_inv_flat1_aux
 342 cpx_inv_gref1
 343 cpx_inv_lift1
 344 cpx_inv_lref1
 345 cpx_inv_lref1_ge
 346 cpx_inv_sort1
 347 cpx_lift
 348 cpx_lleq_conf
 349 cpx_lleq_conf_dx
 350 cpx_lleq_conf_sn
 351 cpx_llpx_sn_conf
 352 cpx_lpx_aaa_conf
 353 cpx_pair_sn
 354 cpx_refl
 355 cpxs
 356 cpxs_aaa_conf
 357 cpxs_ApplOmega_13
 358 cpxs_beta
 359 cpxs_beta_dx
 360 cpxs_beta_rc
 361 cpxs_bind
 362 cpxs_bind2
 363 cpxs_bind2_dx
 364 cpxs_bind_dx
 365 cpxs_ct
 366 cpxs_delta
 367 cpxs_eps
 368 cpxs_flat
 369 cpxs_flat_dx
 370 cpxs_flat_sn
 371 cpxs_fpbg
 372 cpxs_fpbs
 373 cpxs_fpbs_trans
 374 cpxs_fqup_fpbs
 375 cpxs_fqus_fpbs
 376 cpxs_fqus_lpxs_fpbs
 377 cpxs_fwd_beta
 378 cpxs_fwd_beta_vector
 379 cpxs_fwd_cast
 380 cpxs_fwd_cast_vector
 381 cpxs_fwd_cnx
 382 cpxs_fwd_cnx_vector
 383 cpxs_fwd_delta
 384 cpxs_fwd_delta_vector
 385 cpxs_fwd_sort
 386 cpxs_fwd_sort_vector
 387 cpxs_fwd_theta
 388 cpxs_fwd_theta_vector
 389 cpxs_ind
 390 cpxs_ind_dx
 391 cpxs_inv_abbr1
 392 cpxs_inv_abst1
 393 cpxs_inv_appl1
 394 cpxs_inv_cast1
 395 cpxs_inv_cnx1
 396 cpxs_inv_lift1
 397 cpxs_inv_lref1
 398 cpxs_inv_sort1
 399 cpxs_lift
 400 cpxs_lleq_conf
 401 cpxs_lleq_conf_dx
 402 cpxs_lleq_conf_sn
 403 cpxs_neq_inv_step_sn
 404 cpxs_pair_sn
 405 cpxs_refl
 406 cpxs_sort
 407 cpxs_strap1
 408 cpxs_strap2
 409 cpx_st
 410 cpxs_theta
 411 cpxs_theta_dx
 412 cpxs_theta_rc
 413 cpxs_trans
 414 cpxs_zeta
 415 cpx_theta
 416 cpx_zeta
 417 cpy
 418 cpy_atom
 419 cpy_bind
 420 cpy_conf_eq
 421 cpy_conf_neq
 422 cpy_cpys
 423 cpy_flat
 424 cpy_full
 425 cpy_fwd_nlift2_ge
 426 cpy_fwd_tw
 427 cpy_fwd_up
 428 cpy_inv_atom1
 429 cpy_inv_atom1_aux
 430 cpy_inv_bind1
 431 cpy_inv_bind1_aux
 432 cpy_inv_flat1
 433 cpy_inv_flat1_aux
 434 cpy_inv_gref1
 435 cpy_inv_lift1_be
 436 cpy_inv_lift1_be_up
 437 cpy_inv_lift1_eq
 438 cpy_inv_lift1_ge
 439 cpy_inv_lift1_ge_up
 440 cpy_inv_lift1_le
 441 cpy_inv_lift1_le_up
 442 cpy_inv_lref1
 443 cpy_inv_refl_O2
 444 cpy_inv_refl_O2_aux
 445 cpy_inv_sort1
 446 cpy_lift_be
 447 cpy_lift_ge
 448 cpy_lift_le
 449 cpy_refl
 450 cpys
 451 cpysa
 452 cpysa_atom
 453 cpysa_bind
 454 cpysa_cpy_trans
 455 cpysa_flat
 456 cpysa_inv_cpys
 457 cpys_antisym_eq
 458 cpysa_refl
 459 cpysa_subst
 460 cpys_bind
 461 cpys_conf_eq
 462 cpys_conf_neq
 463 cpys_cpysa
 464 cpys_flat
 465 cpys_fwd_tw
 466 cpys_fwd_up
 467 cpys_ind
 468 cpys_ind_alt
 469 cpys_ind_dx
 470 cpys_inv_atom1
 471 cpys_inv_bind1
 472 cpys_inv_flat1
 473 cpys_inv_gref1
 474 cpys_inv_lift1_be
 475 cpys_inv_lift1_be_up
 476 cpys_inv_lift1_eq
 477 cpys_inv_lift1_ge
 478 cpys_inv_lift1_ge_up
 479 cpys_inv_lift1_le
 480 cpys_inv_lift1_le_up
 481 cpys_inv_lift1_subst
 482 cpys_inv_lift1_up
 483 cpys_inv_lref1
 484 cpys_inv_lref1_drop
 485 cpys_inv_lref1_Y2
 486 cpys_inv_refl_O2
 487 cpys_inv_SO2
 488 cpys_inv_sort1
 489 cpys_lift_be
 490 cpys_lift_ge
 491 cpys_lift_le
 492 cpy_split_down
 493 cpy_split_up
 494 cpys_refl
 495 cpys_split_up
 496 cpys_strap1
 497 cpys_strap1_down
 498 cpys_strap2
 499 cpys_strap2_down
 500 cpys_strip_eq
 501 cpys_strip_neq
 502 cpys_subst
 503 cpys_subst_Y2
 504 cpys_trans_down
 505 cpys_trans_eq
 506 cpy_subst
 507 cpys_weak
 508 cpys_weak_full
 509 cpys_weak_top
 510 cpy_trans_down
 511 cpy_trans_ge
 512 cpy_weak
 513 cpy_weak_full
 514 cpy_weak_top
 515 crr
 516 crr_appl_dx
 517 crr_appl_sn
 518 crr_beta
 519 crr_crx
 520 crr_delta
 521 crr_ib2_dx
 522 crr_ib2_sn
 523 crr_inv_appl
 524 crr_inv_appl_aux
 525 crr_inv_gref
 526 crr_inv_gref_aux
 527 crr_inv_ib2
 528 crr_inv_ib2_aux
 529 crr_inv_lift
 530 crr_inv_lref
 531 crr_inv_lref_aux
 532 crr_inv_sort
 533 crr_inv_sort_aux
 534 crr_lift
 535 crr_ri2
 536 crr_theta
 537 crx
 538 crx_appl_dx
 539 crx_appl_sn
 540 crx_beta
 541 crx_delta
 542 crx_ib2_dx
 543 crx_ib2_sn
 544 crx_inv_appl
 545 crx_inv_appl_aux
 546 crx_inv_gref
 547 crx_inv_gref_aux
 548 crx_inv_ib2
 549 crx_inv_ib2_aux
 550 crx_inv_lift
 551 crx_inv_lref
 552 crx_inv_lref_aux
 553 crx_inv_sort
 554 crx_inv_sort_aux
 555 crx_lift
 556 crx_ri2
 557 crx_sort
 558 crx_theta
 559 csx
 560 csxa
 561 csx_abbr
 562 csx_abst
 563 csxa_cpxs_trans
 564 csxa_csx
 565 csxa_ind
 566 csxa_intro
 567 csxa_intro_aux
 568 csxa_intro_cpx
 569 csx_appl_beta
 570 csx_appl_beta_aux
 571 csx_appl_simple
 572 csx_appl_simple_tsts
 573 csx_appl_theta
 574 csx_appl_theta_aux
 575 csx_applv_beta
 576 csx_applv_cast
 577 csx_applv_cnx
 578 csx_applv_delta
 579 csx_applv_sort
 580 csx_applv_theta
 581 csx_cast
 582 csx_cpre
 583 csx_cpxe
 584 csx_cpxs_trans
 585 csx_cpx_trans
 586 csx_csxa
 587 csx_fpb_conf
 588 csx_fpbs_conf
 589 csx_fqu_conf
 590 csx_fqup_conf
 591 csx_fquq_conf
 592 csx_fqus_conf
 593 csx_fsb
 594 csx_fsb_fpbs
 595 csx_fwd_applv
 596 csx_fwd_bind
 597 csx_fwd_bind_dx
 598 csx_fwd_bind_dx_aux
 599 csx_fwd_flat
 600 csx_fwd_flat_dx
 601 csx_fwd_flat_dx_aux
 602 csx_fwd_pair_sn
 603 csx_fwd_pair_sn_aux
 604 csx_gcp
 605 csx_gcr
 606 csx_ind
 607 csx_ind_alt
 608 csx_ind_fpb
 609 csx_ind_fpbg
 610 csx_intro
 611 csx_intro_cpxs
 612 csx_inv_lift
 613 csx_inv_lref_bind
 614 csx_lift
 615 csx_lleq_conf
 616 csx_lleq_trans
 617 csx_lpx_conf
 618 csx_lpxs_conf
 619 csx_lref_bind
 620 csx_lsx
 621 csx_sort
 622 csxv
 623 csxv_inv_cons
 624 d1_liftable_liftables
 625 d1_liftables_liftables_all
 626 da
 627 da_bind
 628 da_cpr_lpr
 629 da_cpr_lpr_aux
 630 da_cprs_lpr
 631 da_cprs_lpr_aux
 632 da_flat
 633 da_inv_bind
 634 da_inv_bind_aux
 635 da_inv_flat
 636 da_inv_flat_aux
 637 da_inv_gref
 638 da_inv_gref_aux
 639 da_inv_lift
 640 da_inv_lref
 641 da_inv_lref_aux
 642 da_inv_sort
 643 da_inv_sort_aux
 644 da_ldec
 645 da_ldef
 646 da_lift
 647 da_lstas
 648 da_mono
 649 d_appendable_sn
 650 da_scpds_lpr_aux
 651 da_scpes_aux
 652 da_sort
 653 d_deliftable_sn
 654 d_deliftable_sn_llstar
 655 d_deliftable_sn_LTC
 656 dedropable_sn
 657 dedropable_sn_TC
 658 deg_inv_prec
 659 deg_inv_pred
 660 deg_iter
 661 deg_next_SO
 662 deg_O
 663 deg_SO
 664 deg_SO_gt
 665 deg_SO_inv_pos
 666 deg_SO_inv_pos_aux
 667 deg_SO_pos
 668 deg_SO_refl
 669 deg_SO_zero
 670 Delta
 671 Delta_lift
 672 destruct_apair_apair_aux
 673 destruct_lpair_lpair_aux
 674 destruct_sort_sort_aux
 675 destruct_tatom_tatom_aux
 676 destruct_tpair_tpair_aux
 677 discr_apair_xy_x
 678 discr_apair_xy_y
 679 discr_lpair_x_xy
 680 discr_tpair_xy_x
 681 discr_tpair_xy_y
 682 d_liftable
 683 d_liftable1
 684 d_liftable_llstar
 685 d_liftable_LTC
 686 d_liftables1
 687 d_liftables1_all
 688 drop
 689 dropable_dx
 690 dropable_dx_TC
 691 dropable_sn
 692 dropable_sn_TC
 693 drop_atom
 694 drop_conf_be
 695 drop_conf_div
 696 drop_conf_ge
 697 drop_conf_le
 698 drop_conf_lt
 699 drop_drop
 700 drop_drop_lt
 701 drop_FT
 702 drop_fwd_be
 703 drop_fwd_drop2
 704 drop_fwd_length
 705 drop_fwd_length_eq1
 706 drop_fwd_length_eq2
 707 drop_fwd_length_ge
 708 drop_fwd_length_le2
 709 drop_fwd_length_le4
 710 drop_fwd_length_le_ge
 711 drop_fwd_length_le_le
 712 drop_fwd_length_lt2
 713 drop_fwd_length_lt4
 714 drop_fwd_length_minus2
 715 drop_fwd_length_minus4
 716 drop_fwd_lw
 717 drop_fwd_lw_lt
 718 drop_fwd_rfw
 719 drop_gen
 720 drop_inv_atom1
 721 drop_inv_atom1_aux
 722 drop_inv_drop1
 723 drop_inv_drop1_lt
 724 drop_inv_FT
 725 drop_inv_FT_aux
 726 drop_inv_gen
 727 drop_inv_length_eq
 728 drop_inv_O1_gt
 729 drop_inv_O1_pair1
 730 drop_inv_O1_pair1_aux
 731 drop_inv_O1_pair2
 732 drop_inv_O2
 733 drop_inv_O2_aux
 734 drop_inv_pair1
 735 drop_inv_refl
 736 drop_inv_skip1
 737 drop_inv_skip1_aux
 738 drop_inv_skip2
 739 drop_inv_skip2_aux
 740 drop_inv_T
 741 drop_lprs_trans
 742 drop_lpr_trans
 743 drop_lpxs_trans
 744 drop_lpx_trans
 745 drop_lsubc_trans
 746 drop_mono
 747 drop_O1_append_sn_le
 748 drop_O1_append_sn_le_aux
 749 drop_O1_eq
 750 drop_O1_ex
 751 drop_O1_ge
 752 drop_O1_inj
 753 drop_O1_inv_append1_ge
 754 drop_O1_inv_append1_le
 755 drop_O1_le
 756 drop_O1_lt
 757 drop_O1_pair
 758 drop_pair
 759 drop_refl
 760 drop_refl_atom_O2
 761 drops
 762 drops_cons
 763 drops_drop_trans
 764 drops_inv_cons
 765 drops_inv_cons_aux
 766 drops_inv_nil
 767 drops_inv_nil_aux
 768 drops_inv_skip2
 769 drop_skip
 770 drop_skip_lt
 771 drops_lsubc_trans
 772 drops_nil
 773 drop_split
 774 drops_skip
 775 drops_trans
 776 drop_T
 777 drop_trans_ge
 778 drop_trans_ge_comm
 779 drop_trans_le
 780 drop_trans_lt
 781 eq_aarity_dec
 782 eq_bind2_dec
 783 eq_false_inv_tpair_dx
 784 eq_false_inv_tpair_sn
 785 eq_flat2_dec
 786 eq_genv_dec
 787 eq_item0_dec
 788 eq_item2_dec
 789 eq_lenv_dec
 790 eq_term_dec
 791 flat2
 792 Flat2
 793 fleq
 794 fleq_canc_dx
 795 fleq_canc_sn
 796 fleq_fpbg_trans
 797 fleq_fpbq
 798 fleq_fpbs
 799 fleq_fpb_trans
 800 fleq_intro
 801 fleq_inv_gen
 802 fleq_refl
 803 fleq_sym
 804 fleq_trans
 805 fpb
 806 fpb_cpx
 807 fpb_fpbg
 808 fpb_fpbg_trans
 809 fpb_fpbq
 810 fpb_fpbq_alt
 811 fpb_fpbs
 812 fpb_fpbsa_trans
 813 fpb_fqu
 814 fpbg
 815 fpbg_fleq_trans
 816 fpbg_fpbq_trans
 817 fpbg_fpbs_trans
 818 fpbg_fwd_fpbs
 819 fpbg_refl
 820 fpbg_trans
 821 fpb_inv_fleq
 822 fpb_lpx
 823 fpbq
 824 fpbqa
 825 fpbq_aaa_conf
 826 fpbqa_inv_fpbq
 827 fpbq_cpx
 828 fpbq_fpbg_trans
 829 fpbq_fpbqa
 830 fpbq_fpbs
 831 fpbq_fquq
 832 fpbq_ind_alt
 833 fpbq_inv_fpb_alt
 834 fpbq_lleq
 835 fpbq_lpx
 836 fpbq_refl
 837 fpbs
 838 fpbsa
 839 fpbs_aaa_conf
 840 fpbsa_inv_fpbs
 841 fpbs_cpxs_trans
 842 fpbs_cpx_trans_neq
 843 fpbs_fpbg
 844 fpbs_fpbg_trans
 845 fpbs_fpbsa
 846 fpbs_fpb_trans
 847 fpbs_fqup_trans
 848 fpbs_fqus_trans
 849 fpbs_ind
 850 fpbs_ind_dx
 851 fpbs_intro_alt
 852 fpbs_inv_alt
 853 fpbs_lleq_trans
 854 fpbs_lpxs_trans
 855 fpbs_refl
 856 fpbs_strap1
 857 fpbs_strap2
 858 fpbs_trans
 859 fqu
 860 fqu_bind_dx
 861 fqu_cpr_trans_dx
 862 fqu_cpr_trans_sn
 863 fqu_cpxs_trans
 864 fqu_cpxs_trans_neq
 865 fqu_cpx_trans
 866 fqu_cpx_trans_neq
 867 fqu_drop
 868 fqu_drop_lt
 869 fqu_flat_dx
 870 fqu_fqup
 871 fqu_fquq
 872 fqu_fwd_fw
 873 fqu_fwd_length_lref1
 874 fqu_fwd_length_lref1_aux
 875 fqu_inv_eq
 876 fqu_inv_eq_aux
 877 fqu_lpr_trans
 878 fqu_lpx_trans
 879 fqu_lref_O
 880 fqu_lref_S_lt
 881 fqup
 882 fqu_pair_sn
 883 fqup_ApplOmega_13
 884 fqup_bind_dx
 885 fqup_bind_dx_flat_dx
 886 fqup_cpxs_trans
 887 fqup_cpxs_trans_neq
 888 fqup_cpx_trans
 889 fqup_cpx_trans_neq
 890 fqup_drop
 891 fqup_flat_dx
 892 fqup_flat_dx_bind_dx
 893 fqup_flat_dx_pair_sn
 894 fqup_fpbg
 895 fqup_fpbs
 896 fqup_fqus
 897 fqup_fqus_trans
 898 fqup_fwd_fw
 899 fqup_ind
 900 fqup_ind_dx
 901 fqup_inv_step_sn
 902 fqup_lref
 903 fqup_pair_sn
 904 fqup_strap1
 905 fqup_strap2
 906 fqup_trans
 907 fqup_wf_ind
 908 fqup_wf_ind_eq
 909 fquq
 910 fquqa
 911 fquqa_drop
 912 fquqa_inv_fquq
 913 fquqa_refl
 914 fquq_bind_dx
 915 fquq_cpr_trans_dx
 916 fquq_cpr_trans_sn
 917 fquq_cpxs_trans
 918 fquq_cpxs_trans_neq
 919 fquq_cpx_trans
 920 fquq_cpx_trans_neq
 921 fquq_drop
 922 fquq_flat_dx
 923 fquq_fquqa
 924 fquq_fqus
 925 fquq_fwd_fw
 926 fquq_fwd_length_lref1
 927 fquq_fwd_length_lref1_aux
 928 fquq_inv_gen
 929 fquq_lpr_trans
 930 fquq_lpx_trans
 931 fquq_lref_O
 932 fquq_lstas_trans
 933 fquq_pair_sn
 934 fquq_refl
 935 fquq_sta_trans
 936 fqus
 937 fqus_cpxs_trans
 938 fqus_cpxs_trans_neq
 939 fqus_cpx_trans
 940 fqus_cpx_trans_neq
 941 fqus_drop
 942 fqus_fpbs
 943 fqus_fpbs_trans
 944 fqus_fqup_trans
 945 fqus_fwd_fw
 946 fqus_ind
 947 fqus_ind_dx
 948 fqus_inv_gen
 949 fqus_lpxs_fpbs
 950 fqus_lstas_trans
 951 fqus_refl
 952 fqus_strap1
 953 fqus_strap1_fqu
 954 fqus_strap2
 955 fqus_strap2_fqu
 956 fqu_sta_trans
 957 fqus_trans
 958 fqu_wf_ind
 959 frees
 960 frees_append
 961 frees_be
 962 frees_bind_dx
 963 frees_bind_dx_O
 964 frees_bind_sn
 965 frees_dec
 966 frees_eq
 967 frees_flat_dx
 968 frees_flat_sn
 969 frees_inv
 970 frees_inv_append
 971 frees_inv_append_aux
 972 frees_inv_bind
 973 frees_inv_bind_O
 974 frees_inv_flat
 975 frees_inv_gref
 976 frees_inv_lift_be
 977 frees_inv_lift_ge
 978 frees_inv_lref
 979 frees_inv_lref_free
 980 frees_inv_lref_ge
 981 frees_inv_lref_lt
 982 frees_inv_lref_skip
 983 frees_inv_sort
 984 frees_lift_ge
 985 frees_lref_be
 986 frees_lref_eq
 987 frees_lreq_conf
 988 frees_S
 989 frees_trans
 990 frees_weak
 991 fsb
 992 fsba
 993 fsba_fpbs_trans
 994 fsba_ind_alt
 995 fsba_intro
 996 fsba_inv_fsb
 997 fsb_fpbs_trans
 998 fsb_fsba
 999 fsb_ind_alt
1000 fsb_ind_fpbg
1001 fsb_intro
1002 fsb_inv_csx
1003 fw
1004 fw_lpair_sn
1005 fw_shift
1006 fw_tpair_dx
1007 fw_tpair_sn
1008 gcp
1009 gcp0_lifts
1010 gcp2_lifts
1011 gcp2_lifts_all
1012 gcr
1013 gcr_aaa
1014 gcr_lift
1015 gcr_lifts
1016 genv
1017 gget
1018 gget_dec
1019 gget_eq
1020 gget_gt
1021 gget_inv_eq
1022 gget_inv_gt
1023 gget_inv_lt
1024 gget_inv_lt_aux
1025 gget_lt
1026 gget_mono
1027 gget_total
1028 GRef
1029 ib2
1030 IH_da_cpr_lpr
1031 IH_lstas_cpr_lpr
1032 IH_snv_cpr_lpr
1033 IH_snv_lstas
1034 is_lift_dec
1035 item0
1036 item2
1037 LAtom
1038 lcosx
1039 lcosx_drop_trans_lt
1040 lcosx_inv_pair
1041 lcosx_inv_succ
1042 lcosx_inv_succ_aux
1043 lcosx_O
1044 lcosx_pair
1045 lcosx_skip
1046 lcosx_sort
1047 length
1048 length_inv_pos_dx
1049 length_inv_pos_dx_ltail
1050 length_inv_pos_sn
1051 length_inv_pos_sn_ltail
1052 length_inv_zero_dx
1053 length_inv_zero_sn
1054 lenv
1055 lenv_ind_alt
1056 lift
1057 lift_bind
1058 lift_conf_be
1059 lift_conf_O1
1060 lift_div_be
1061 lift_div_le
1062 lift_flat
1063 lift_fwd_pair1
1064 lift_fwd_pair2
1065 lift_fwd_tw
1066 lift_gref
1067 lift_inj
1068 lift_inv_bind1
1069 lift_inv_bind1_aux
1070 lift_inv_bind2
1071 lift_inv_bind2_aux
1072 lift_inv_flat1
1073 lift_inv_flat1_aux
1074 lift_inv_flat2
1075 lift_inv_flat2_aux
1076 lift_inv_gref1
1077 lift_inv_gref1_aux
1078 lift_inv_gref2
1079 lift_inv_gref2_aux
1080 lift_inv_lref1
1081 lift_inv_lref1_aux
1082 lift_inv_lref1_ge
1083 lift_inv_lref1_lt
1084 lift_inv_lref2
1085 lift_inv_lref2_aux
1086 lift_inv_lref2_be
1087 lift_inv_lref2_ge
1088 lift_inv_lref2_lt
1089 lift_inv_O2
1090 lift_inv_O2_aux
1091 lift_inv_pair_xy_x
1092 lift_inv_pair_xy_y
1093 lift_inv_sort1
1094 lift_inv_sort1_aux
1095 lift_inv_sort2
1096 lift_inv_sort2_aux
1097 lift_lref_ge
1098 lift_lref_ge_minus
1099 lift_lref_ge_minus_eq
1100 lift_lref_lt
1101 lift_mono
1102 lift_refl
1103 lifts
1104 lifts_applv
1105 lifts_bind
1106 lifts_cons
1107 lifts_flat
1108 lift_simple_dx
1109 lift_simple_sn
1110 lifts_inv_applv1
1111 lifts_inv_bind1
1112 lifts_inv_cons
1113 lifts_inv_cons_aux
1114 lifts_inv_flat1
1115 lifts_inv_gref1
1116 lifts_inv_lref1
1117 lifts_inv_nil
1118 lifts_inv_nil_aux
1119 lifts_inv_sort1
1120 lifts_lift_trans
1121 lifts_lift_trans_le
1122 lifts_nil
1123 lift_sort
1124 lift_split
1125 lifts_simple_dx
1126 lifts_simple_sn
1127 lifts_total
1128 lifts_trans
1129 liftsv
1130 liftsv_cons
1131 liftsv_liftv_trans_le
1132 liftsv_nil
1133 lift_total
1134 lift_trans_be
1135 lift_trans_ge
1136 lift_trans_le
1137 liftv
1138 liftv_cons
1139 liftv_inv_cons1
1140 liftv_inv_cons1_aux
1141 liftv_inv_nil1
1142 liftv_inv_nil1_aux
1143 liftv_mono
1144 liftv_nil
1145 liftv_total
1146 lleq
1147 lleq_aaa_trans
1148 lleq_bind
1149 lleq_bind_O
1150 lleq_bind_repl_O
1151 lleq_bind_repl_SO
1152 lleq_canc_dx
1153 lleq_canc_sn
1154 lleq_cpxs_trans
1155 lleq_cpx_trans
1156 lleq_dec
1157 lleq_flat
1158 lleq_fpbs
1159 lleq_fpbs_trans
1160 lleq_fpb_trans
1161 lleq_fqup_trans
1162 lleq_fquq_trans
1163 lleq_fqus_trans
1164 lleq_fqu_trans
1165 lleq_free
1166 lleq_fwd_bind_dx
1167 lleq_fwd_bind_O_dx
1168 lleq_fwd_bind_sn
1169 lleq_fwd_drop_dx
1170 lleq_fwd_drop_sn
1171 lleq_fwd_flat_dx
1172 lleq_fwd_flat_sn
1173 lleq_fwd_length
1174 lleq_fwd_lref
1175 lleq_fwd_lref_dx
1176 lleq_fwd_lref_sn
1177 lleq_ge
1178 lleq_ge_up
1179 lleq_gref
1180 lleq_ind
1181 lleq_ind_alt_r
1182 lleq_intro_alt
1183 lleq_intro_alt_r
1184 lleq_inv_alt
1185 lleq_inv_alt_r
1186 lleq_inv_bind
1187 lleq_inv_bind_O
1188 lleq_inv_flat
1189 lleq_inv_lift_be
1190 lleq_inv_lift_ge
1191 lleq_inv_lift_le
1192 lleq_inv_lref_ge
1193 lleq_inv_lref_ge_bi
1194 lleq_inv_lref_ge_dx
1195 lleq_inv_lref_ge_sn
1196 lleq_inv_S
1197 lleq_lift_ge
1198 lleq_lift_le
1199 lleq_llpx_sn_conf
1200 lleq_llpx_sn_trans
1201 lleq_lpxs_trans
1202 lleq_lpx_trans
1203 lleq_lref
1204 lleq_lreq_repl
1205 lleq_lreq_trans
1206 lleq_nlleq_trans
1207 lleq_refl
1208 lleq_skip
1209 lleq_sort
1210 lleq_sym
1211 lleq_trans
1212 lleq_transitive
1213 lleq_Y
1214 llor
1215 llor_atom
1216 llor_skip
1217 llor_tail_cofrees
1218 llor_tail_frees
1219 llor_total
1220 llpx_sn
1221 llpx_sn_alt
1222 llpx_sn_alt_inv_llpx_sn
1223 llpx_sn_alt_r
1224 llpx_sn_alt_r_bind
1225 llpx_sn_alt_r_flat
1226 llpx_sn_alt_r_free
1227 llpx_sn_alt_r_fwd_length
1228 llpx_sn_alt_r_fwd_lref
1229 llpx_sn_alt_r_gref
1230 llpx_sn_alt_r_ind_alt
1231 llpx_sn_alt_r_intro
1232 llpx_sn_alt_r_intro_alt
1233 llpx_sn_alt_r_inv_alt
1234 llpx_sn_alt_r_inv_bind
1235 llpx_sn_alt_r_inv_flat
1236 llpx_sn_alt_r_inv_lpx_sn
1237 llpx_sn_alt_r_lref
1238 llpx_sn_alt_r_skip
1239 llpx_sn_alt_r_sort
1240 llpx_sn_bind
1241 llpx_sn_bind_O
1242 llpx_sn_bind_repl_O
1243 llpx_sn_bind_repl_SO
1244 llpx_sn_co
1245 llpx_sn_dec
1246 llpx_sn_drop_conf_O
1247 llpx_sn_drop_trans_O
1248 llpx_sn_flat
1249 llpx_sn_free
1250 llpx_sn_frees_trans
1251 llpx_sn_frees_trans_aux
1252 llpx_sn_fwd_bind_dx
1253 llpx_sn_fwd_bind_O_dx
1254 llpx_sn_fwd_bind_sn
1255 llpx_sn_fwd_drop_dx
1256 llpx_sn_fwd_drop_sn
1257 llpx_sn_fwd_flat_dx
1258 llpx_sn_fwd_flat_sn
1259 llpx_sn_fwd_length
1260 llpx_sn_fwd_lref
1261 llpx_sn_fwd_lref_aux
1262 llpx_sn_fwd_lref_dx
1263 llpx_sn_fwd_lref_sn
1264 llpx_sn_fwd_pair_sn
1265 llpx_sn_ge
1266 llpx_sn_ge_up
1267 llpx_sn_gref
1268 llpx_sn_ind_alt_r
1269 llpx_sn_intro_alt_r
1270 llpx_sn_inv_alt_r
1271 llpx_sn_inv_bind
1272 llpx_sn_inv_bind_aux
1273 llpx_sn_inv_bind_O
1274 llpx_sn_inv_flat
1275 llpx_sn_inv_flat_aux
1276 llpx_sn_inv_lift_be
1277 llpx_sn_inv_lift_ge
1278 llpx_sn_inv_lift_le
1279 llpx_sn_inv_lift_O
1280 llpx_sn_inv_lref_ge_bi
1281 llpx_sn_inv_lref_ge_dx
1282 llpx_sn_inv_lref_ge_sn
1283 llpx_sn_inv_S
1284 llpx_sn_inv_S_aux
1285 llpx_sn_lift_ge
1286 llpx_sn_lift_le
1287 llpx_sn_llor_dx
1288 llpx_sn_llor_dx_sym
1289 llpx_sn_llor_fwd_sn
1290 llpx_sn_llpx_sn_alt
1291 llpx_sn_lpx_sn_alt_r
1292 llpx_sn_lref
1293 llpx_sn_lrefl
1294 llpx_sn_lreq_repl
1295 llpx_sn_lreq_trans
1296 llpx_sn_refl
1297 llpx_sn_skip
1298 llpx_sn_sort
1299 llpx_sn_TC_pair_dx
1300 llpx_sn_Y
1301 LPair
1302 lpair_ltail
1303 lpr
1304 lpr_aaa_conf
1305 lpr_conf
1306 lpr_cpcs_conf
1307 lpr_cpcs_trans
1308 lpr_cpr_conf
1309 lpr_cpr_conf_dx
1310 lpr_cpr_conf_sn
1311 lpr_cprs_conf
1312 lpr_cprs_trans
1313 lpr_cpr_trans
1314 lpr_drop_conf
1315 lpr_drop_trans_O1
1316 lpr_fpb
1317 lpr_fpbq
1318 lpr_fwd_length
1319 lpr_inv_atom1
1320 lpr_inv_atom2
1321 lpr_inv_pair1
1322 lpr_inv_pair2
1323 lpr_lprs
1324 lpr_lpx
1325 lpr_pair
1326 lpr_refl
1327 lprs
1328 lprs_aaa_conf
1329 lprs_conf
1330 lprs_cpcs_trans
1331 lprs_cpr_conf_dx
1332 lprs_cpr_conf_sn
1333 lprs_cprs_conf
1334 lprs_cprs_conf_dx
1335 lprs_cprs_conf_sn
1336 lprs_cprs_trans
1337 lprs_cpr_trans
1338 lprs_drop_conf
1339 lprs_drop_trans_O1
1340 lprs_fpbs
1341 lprs_fwd_length
1342 lprs_ind
1343 lprs_ind_alt
1344 lprs_ind_dx
1345 lprs_inv_atom1
1346 lprs_inv_atom2
1347 lprs_inv_pair1
1348 lprs_inv_pair2
1349 lprs_lpxs
1350 lprs_pair
1351 lprs_pair2
1352 lprs_pair_refl
1353 lprs_refl
1354 lprs_strap1
1355 lprs_strap2
1356 lprs_strip
1357 lprs_trans
1358 lpx
1359 lpx_aaa_conf
1360 lpx_cpx_frees_trans
1361 lpx_cpxs_trans
1362 lpx_cpx_trans
1363 lpx_drop_conf
1364 lpx_drop_trans_O1
1365 lpx_fqup_trans
1366 lpx_fquq_trans
1367 lpx_fqus_trans
1368 lpx_fqu_trans
1369 lpx_frees_trans
1370 lpx_fwd_length
1371 lpx_inv_atom1
1372 lpx_inv_atom2
1373 lpx_inv_pair
1374 lpx_inv_pair1
1375 lpx_inv_pair2
1376 lpx_lleq_fqup_trans
1377 lpx_lleq_fquq_trans
1378 lpx_lleq_fqus_trans
1379 lpx_lleq_fqu_trans
1380 lpx_lpxs
1381 lpx_pair
1382 lpx_refl
1383 lpxs
1384 lpxs_aaa_conf
1385 lpxs_cpxs_trans
1386 lpxs_cpx_trans
1387 lpxs_drop_conf
1388 lpxs_drop_trans_O1
1389 lpxs_fpbg
1390 lpxs_fpbs
1391 lpxs_fpbs_trans
1392 lpxs_fqup_trans
1393 lpxs_fquq_trans
1394 lpxs_fqus_trans
1395 lpxs_fwd_length
1396 lpxs_ind
1397 lpxs_ind_alt
1398 lpxs_ind_dx
1399 lpxs_inv_atom1
1400 lpxs_inv_atom2
1401 lpxs_inv_pair1
1402 lpxs_inv_pair2
1403 lpxs_lleq_fpbs
1404 lpxs_lleq_fqup_trans
1405 lpxs_lleq_fquq_trans
1406 lpxs_lleq_fqus_trans
1407 lpxs_lleq_fqu_trans
1408 lpx_sn
1409 lpx_sn_alt
1410 lpx_sn_alt_atom
1411 lpx_sn_alt_fwd_length
1412 lpx_sn_alt_inv_atom1
1413 lpx_sn_alt_inv_atom2
1414 lpx_sn_alt_inv_lpx_sn
1415 lpx_sn_alt_inv_pair1
1416 lpx_sn_alt_inv_pair2
1417 lpx_sn_alt_pair
1418 lpx_sn_atom
1419 lpx_sn_conf
1420 lpx_sn_confluent
1421 lpx_sn_deliftable_dropable
1422 lpx_sn_dropable
1423 lpx_sn_dropable_aux
1424 lpx_sn_drop_conf
1425 lpx_sn_drop_trans
1426 lpx_sn_fwd_length
1427 lpx_sn_intro_alt
1428 lpx_sn_inv_alt
1429 lpx_sn_inv_atom1
1430 lpx_sn_inv_atom1_aux
1431 lpx_sn_inv_atom2
1432 lpx_sn_inv_atom2_aux
1433 lpx_sn_inv_pair
1434 lpx_sn_inv_pair1
1435 lpx_sn_inv_pair1_aux
1436 lpx_sn_inv_pair2
1437 lpx_sn_inv_pair2_aux
1438 lpx_sn_liftable_dedropable
1439 lpxs_nlleq_inv_step_sn
1440 lpx_sn_llpx_sn
1441 lpx_sn_lpx_sn_alt
1442 lpx_sn_LTC_TC_lpx_sn
1443 lpx_sn_pair
1444 lpx_sn_refl
1445 lpx_sn_trans
1446 lpx_sn_transitive
1447 lpxs_pair
1448 lpxs_pair2
1449 lpxs_pair_refl
1450 lpxs_refl
1451 lpxs_strap1
1452 lpxs_strap2
1453 lpxs_trans
1454 LRef
1455 lreq
1456 lreq_atom
1457 lreq_canc_dx
1458 lreq_canc_sn
1459 lreq_cpxs_trans
1460 lreq_cpx_trans
1461 lreq_drop_conf_be
1462 lreq_drop_trans_be
1463 lreq_frees_trans
1464 lreq_fwd_length
1465 lreq_inv_atom1
1466 lreq_inv_atom1_aux
1467 lreq_inv_atom2
1468 lreq_inv_O_Y
1469 lreq_inv_O_Y_aux
1470 lreq_inv_pair
1471 lreq_inv_pair1
1472 lreq_inv_pair1_aux
1473 lreq_inv_pair2
1474 lreq_inv_succ
1475 lreq_inv_succ1
1476 lreq_inv_succ1_aux
1477 lreq_inv_succ2
1478 lreq_inv_zero1
1479 lreq_inv_zero1_aux
1480 lreq_inv_zero2
1481 lreq_join
1482 lreq_lleq_trans
1483 lreq_llpx_sn_trans
1484 lreq_lpxs_trans_lleq
1485 lreq_lpxs_trans_lleq_aux
1486 lreq_lpx_trans_lleq
1487 lreq_lpx_trans_lleq_aux
1488 lreq_O2
1489 lreq_pair
1490 lreq_pair_lt
1491 lreq_pair_O_Y
1492 lreq_refl
1493 lreq_succ
1494 lreq_succ_lt
1495 lreq_sym
1496 lreq_trans
1497 lreq_zero
1498 lstas
1499 lstas_aaa_conf
1500 lstas_appl
1501 lstas_bind
1502 lstas_cast
1503 lstas_conf
1504 lstas_conf_le
1505 lstas_correct
1506 lstas_cpcs_lpr
1507 lstas_cpr
1508 lstas_cpr_aux
1509 lstas_cpr_lpr
1510 lstas_cpr_lpr_aux
1511 lstas_cprs_lpr
1512 lstas_cprs_lpr_aux
1513 lstas_cpxs
1514 lstas_da_conf
1515 lstas_fpbg
1516 lstas_fpbs
1517 lstas_inv_appl1
1518 lstas_inv_appl1_aux
1519 lstas_inv_bind1
1520 lstas_inv_bind1_aux
1521 lstas_inv_cast1
1522 lstas_inv_cast1_aux
1523 lstas_inv_da
1524 lstas_inv_da_ge
1525 lstas_inv_gref1
1526 lstas_inv_gref1_aux
1527 lstas_inv_lift1
1528 lstas_inv_lref1
1529 lstas_inv_lref1_aux
1530 lstas_inv_lref1_O
1531 lstas_inv_lref1_S
1532 lstas_inv_refl_pos
1533 lstas_inv_sort1
1534 lstas_inv_sort1_aux
1535 lstas_ldef
1536 lstas_lift
1537 lstas_llpx_sn_conf
1538 lstas_lstas
1539 lstas_mono
1540 lstas_scpds
1541 lstas_scpds_aux
1542 lstas_scpds_trans
1543 lstas_scpes_trans
1544 lstas_sort
1545 lstas_split
1546 lstas_split_aux
1547 lstas_succ
1548 lstas_trans
1549 lstas_zero
1550 lsuba
1551 lsuba_aaa_conf
1552 lsuba_aaa_trans
1553 lsuba_atom
1554 lsuba_beta
1555 lsuba_drop_O1_conf
1556 lsuba_drop_O1_trans
1557 lsuba_fwd_lsubr
1558 lsuba_inv_atom1
1559 lsuba_inv_atom1_aux
1560 lsuba_inv_atom2
1561 lsuba_inv_atom2_aux
1562 lsuba_inv_pair1
1563 lsuba_inv_pair1_aux
1564 lsuba_inv_pair2
1565 lsuba_inv_pair2_aux
1566 lsuba_lsubc
1567 lsuba_pair
1568 lsuba_refl
1569 lsuba_trans
1570 lsubc
1571 lsubc_atom
1572 lsubc_beta
1573 lsubc_drop_O1_trans
1574 lsubc_fwd_lsubr
1575 lsubc_inv_atom1
1576 lsubc_inv_atom1_aux
1577 lsubc_inv_atom2
1578 lsubc_inv_atom2_aux
1579 lsubc_inv_pair1
1580 lsubc_inv_pair1_aux
1581 lsubc_inv_pair2
1582 lsubc_inv_pair2_aux
1583 lsubc_pair
1584 lsubc_refl
1585 lsubd
1586 lsubd_atom
1587 lsubd_beta
1588 lsubd_da_conf
1589 lsubd_da_trans
1590 lsubd_drop_O1_conf
1591 lsubd_drop_O1_trans
1592 lsubd_fwd_lsubr
1593 lsubd_inv_atom1
1594 lsubd_inv_atom1_aux
1595 lsubd_inv_atom2
1596 lsubd_inv_atom2_aux
1597 lsubd_inv_pair1
1598 lsubd_inv_pair1_aux
1599 lsubd_inv_pair2
1600 lsubd_inv_pair2_aux
1601 lsubd_pair
1602 lsubd_refl
1603 lsubd_trans
1604 lsubr
1605 lsubr_atom
1606 lsubr_beta
1607 lsubr_cpcs_trans
1608 lsubr_cprs_trans
1609 lsubr_cpr_trans
1610 lsubr_cpxs_trans
1611 lsubr_cpx_trans
1612 lsubr_fwd_drop2_abbr
1613 lsubr_fwd_drop2_pair
1614 lsubr_fwd_length
1615 lsubr_inv_abbr2
1616 lsubr_inv_abbr2_aux
1617 lsubr_inv_abst1
1618 lsubr_inv_abst1_aux
1619 lsubr_inv_atom1
1620 lsubr_inv_atom1_aux
1621 lsubr_inv_pair1
1622 lsubr_inv_pair1_aux
1623 lsubr_pair
1624 lsubr_refl
1625 lsubr_trans
1626 lsubsv
1627 lsubsv_atom
1628 lsubsv_beta
1629 lsubsv_cpcs_trans
1630 lsubsv_cprs_trans
1631 lsubsv_drop_O1_conf
1632 lsubsv_drop_O1_trans
1633 lsubsv_fwd_lsuba
1634 lsubsv_fwd_lsubd
1635 lsubsv_fwd_lsubr
1636 lsubsv_inv_atom1
1637 lsubsv_inv_atom1_aux
1638 lsubsv_inv_atom2
1639 lsubsv_inv_atom2_aux
1640 lsubsv_inv_pair1
1641 lsubsv_inv_pair1_aux
1642 lsubsv_inv_pair2
1643 lsubsv_inv_pair2_aux
1644 lsubsv_lstas_trans
1645 lsubsv_pair
1646 lsubsv_refl
1647 lsubsv_scpds_trans
1648 lsubsv_snv_trans
1649 lsubsv_sta_trans
1650 lsuby
1651 lsuby_atom
1652 lsuby_cpysa_trans
1653 lsuby_cpys_trans
1654 lsuby_cpy_trans
1655 lsuby_drop_trans_be
1656 lsuby_fwd_length
1657 lsuby_inv_atom1
1658 lsuby_inv_atom1_aux
1659 lsuby_inv_pair1
1660 lsuby_inv_pair1_aux
1661 lsuby_inv_pair2
1662 lsuby_inv_pair2_aux
1663 lsuby_inv_succ1
1664 lsuby_inv_succ1_aux
1665 lsuby_inv_succ2
1666 lsuby_inv_succ2_aux
1667 lsuby_inv_zero1
1668 lsuby_inv_zero1_aux
1669 lsuby_inv_zero2
1670 lsuby_inv_zero2_aux
1671 lsuby_O2
1672 lsuby_pair
1673 lsuby_pair_lt
1674 lsuby_pair_O_Y
1675 lsuby_refl
1676 lsuby_succ
1677 lsuby_succ_lt
1678 lsuby_sym
1679 lsuby_trans
1680 lsuby_zero
1681 lsx
1682 lsxa
1683 lsxa_ind
1684 lsxa_intro
1685 lsxa_intro_aux
1686 lsxa_intro_lpx
1687 lsxa_inv_lsx
1688 lsxa_lleq_trans
1689 lsxa_lpxs_trans
1690 lsx_atom
1691 lsx_bind
1692 lsx_bind_lpxs_aux
1693 lsx_cpx_trans_lcosx
1694 lsx_cpx_trans_O
1695 lsx_flat
1696 lsx_flat_lpxs
1697 lsx_fwd_bind_dx
1698 lsx_fwd_bind_sn
1699 lsx_fwd_flat_dx
1700 lsx_fwd_flat_sn
1701 lsx_fwd_lref_be
1702 lsx_fwd_pair_sn
1703 lsx_ge
1704 lsx_ge_up
1705 lsx_gref
1706 lsx_ind
1707 lsx_ind_alt
1708 lsx_intro
1709 lsx_intro_alt
1710 lsx_inv_bind
1711 lsx_inv_flat
1712 lsx_inv_lift_be
1713 lsx_inv_lift_ge
1714 lsx_inv_lift_le
1715 lsx_lift_ge
1716 lsx_lift_le
1717 lsx_lleq_trans
1718 lsx_lpxs_trans
1719 lsx_lpx_trans
1720 lsx_lref_be
1721 lsx_lref_be_lpxs
1722 lsx_lref_free
1723 lsx_lref_skip
1724 lsx_lreq_conf
1725 lsx_lsxa
1726 lsx_sort
1727 ltail_length
1728 lw
1729 lw_pair
1730 minuss
1731 minuss_ge
1732 minuss_inv_cons1
1733 minuss_inv_cons1_aux
1734 minuss_inv_cons1_ge
1735 minuss_inv_cons1_lt
1736 minuss_inv_nil1
1737 minuss_inv_nil1_aux
1738 minuss_lt
1739 minuss_nil
1740 mk_gcp
1741 mk_gcr
1742 mk_sd
1743 mk_sh
1744 nexts_dec
1745 nexts_inj
1746 nexts_le
1747 nexts_lt
1748 nf
1749 nlift_bind_dx
1750 nlift_bind_sn
1751 nlift_flat_dx
1752 nlift_flat_sn
1753 nlift_inv_bind
1754 nlift_inv_flat
1755 nlift_inv_lref_be_SO
1756 nlift_lref_be_SO
1757 nlleq_inv_bind
1758 nlleq_inv_bind_O
1759 nlleq_inv_flat
1760 nlleq_lleq_div
1761 nllpx_sn_inv_bind
1762 nllpx_sn_inv_bind_O
1763 nllpx_sn_inv_flat
1764 Omega1
1765 Omega2
1766 pluss
1767 pluss_inv_cons2
1768 pluss_inv_nil2
1769 rfw
1770 rfw_lpair_dx
1771 rfw_lpair_sn
1772 rfw_shift
1773 rfw_tpair_dx
1774 rfw_tpair_sn
1775 ri2
1776 S1
1777 S2
1778 S3
1779 S4
1780 S5
1781 S6
1782 S7
1783 scpds
1784 scpds_aaa_conf
1785 scpds_conf_eq
1786 scpds_cpr_lpr_aux
1787 scpds_cprs_trans
1788 scpds_div
1789 scpds_fwd_cprs
1790 scpds_fwd_cpxs
1791 scpds_inv_abbr_abst
1792 scpds_inv_abst1
1793 scpds_inv_lift1
1794 scpds_inv_lstas_eq
1795 scpds_lift
1796 scpds_strap1
1797 scpds_strap2
1798 scpes
1799 scpes_aaa_mono
1800 scpes_canc_dx
1801 scpes_canc_sn
1802 scpes_cpr_lpr_aux
1803 scpes_inv_abst2
1804 scpes_inv_lstas_eq
1805 scpes_le_aux
1806 scpes_refl
1807 scpes_sym
1808 scpes_trans
1809 sd
1810 sd_d
1811 sd_d_correct
1812 sd_d_SS
1813 sd_O
1814 sd_SO
1815 sh
1816 sh_N
1817 shnv
1818 shnv_cast
1819 shnv_inv_cast
1820 shnv_inv_cast_aux
1821 shnv_inv_snv
1822 simple
1823 simple_atom
1824 simple_flat
1825 simple_inv_bind
1826 simple_inv_bind_aux
1827 simple_inv_pair
1828 simple_tsts_repl_dx
1829 simple_tsts_repl_sn
1830 snv
1831 snv_appl
1832 snv_bind
1833 snv_cast
1834 snv_cast_scpes
1835 snv_cpr_lpr
1836 snv_cpr_lpr_aux
1837 snv_cprs_lpr
1838 snv_cprs_lpr_aux
1839 snv_extended
1840 snv_fqu_conf
1841 snv_fqup_conf
1842 snv_fquq_conf
1843 snv_fqus_conf
1844 snv_fwd_aaa
1845 snv_fwd_da
1846 snv_fwd_fsb
1847 snv_fwd_lstas
1848 snv_inv_appl
1849 snv_inv_appl_aux
1850 snv_inv_bind
1851 snv_inv_bind_aux
1852 snv_inv_cast
1853 snv_inv_cast_aux
1854 snv_inv_gref
1855 snv_inv_gref_aux
1856 snv_inv_lift
1857 snv_inv_lref
1858 snv_inv_lref_aux
1859 snv_lift
1860 snv_lref
1861 snv_lstas
1862 snv_lstas_aux
1863 snv_preserve
1864 snv_restricted
1865 snv_shnv_cast
1866 snv_sort
1867 Sort
1868 sta_cprs_scpds
1869 sta_cpx
1870 sta_cpx_aux
1871 sta_fpb
1872 sta_fpbg
1873 sta_fpbq
1874 sta_fpbs
1875 sta_ldec
1876 TAtom
1877 TC_lpx_sn_fwd_length
1878 TC_lpx_sn_ind
1879 TC_lpx_sn_inv_atom1
1880 TC_lpx_sn_inv_atom2
1881 TC_lpx_sn_inv_lpx_sn_LTC
1882 TC_lpx_sn_inv_pair1
1883 TC_lpx_sn_inv_pair1_aux
1884 TC_lpx_sn_inv_pair2
1885 TC_lpx_sn_pair
1886 TC_lpx_sn_pair_refl
1887 term
1888 tir_atom
1889 tix_lref
1890 TPair
1891 tpr_cpr
1892 tprs_cprs
1893 trr_inv_atom
1894 trx_inv_atom
1895 tsts
1896 tsts_atom
1897 tsts_canc_dx
1898 tsts_canc_sn
1899 tsts_dec
1900 tsts_inv_atom1
1901 tsts_inv_atom1_aux
1902 tsts_inv_atom2
1903 tsts_inv_atom2_aux
1904 tsts_inv_bind_applv_simple
1905 tsts_inv_pair1
1906 tsts_inv_pair1_aux
1907 tsts_inv_pair2
1908 tsts_inv_pair2_aux
1909 tsts_pair
1910 tsts_refl
1911 tsts_sym
1912 tsts_trans
1913 tw
1914 tw_pos
1915 unfold
1916 unfold_bind
1917 unfold_flat
1918 unfold_lref
1919 unfold_sort