matita/matita/contribs/lambdadelta/static_2/names.txt

   1 aaa
   2 aaa_aaa_inv_appl
   3 aaa_aaa_inv_cast
   4 aaa_abbr
   5 aaa_abst
   6 aaa_appl
   7 aaa_cast
   8 aaa_dec
   9 aaa_feqx_conf
  10 aaa_fqu_conf
  11 aaa_fqup_conf
  12 aaa_fquq_conf
  13 aaa_fqus_conf
  14 aaa_inv_abbr
  15 aaa_inv_abbr_aux
  16 aaa_inv_abst
  17 aaa_inv_abst_aux
  18 aaa_inv_appl
  19 aaa_inv_appl_aux
  20 aaa_inv_cast
  21 aaa_inv_cast_aux
  22 aaa_inv_gref
  23 aaa_inv_gref_aux
  24 aaa_inv_lifts
  25 aaa_inv_lref
  26 aaa_inv_lref_aux
  27 aaa_inv_lref_drops
  28 aaa_inv_sort
  29 aaa_inv_sort_aux
  30 aaa_inv_zero
  31 aaa_inv_zero_aux
  32 aaa_lifts
  33 aaa_lref
  34 aaa_lref_drops
  35 aaa_mono
  36 aaa_pair_inv_lref
  37 aaa_sort
  38 aaa_teqx_conf_reqx
  39 aaa_zero
  40 aarity
  41 AAtom
  42 Abbr
  43 Abst
  44 abst_dec
  45 ac
  46 ac_eq
  47 ac_eq_props
  48 ac_le
  49 acle
  50 acle_eq_le
  51 acle_eq_monotonic_le
  52 acle_le_eq
  53 acle_le_monotonic_le
  54 acle_omega
  55 acle_one
  56 ac_le_props
  57 acle_refl
  58 acle_trans
  59 ac_props
  60 acr
  61 acr_aaa
  62 acr_aaa_csubc_lifts
  63 acr_abst
  64 acr_gcr
  65 acr_lifts
  66 ac_top
  67 ac_top_props
  68 APair
  69 append
  70 append_assoc
  71 append_atom
  72 append_atom_sn
  73 append_bind
  74 append_inj_dx
  75 append_inj_length_dx
  76 append_inj_length_sn
  77 append_inj_sn
  78 append_inv_atom3_sn
  79 append_inv_bind3_sn
  80 append_inv_pair_dx
  81 append_inv_refl_dx
  82 append_length
  83 append_shift
  84 Appl
  85 applv
  86 applv_cons
  87 applv_nil
  88 applv_simple
  89 apply_top
  90 bind
  91 bind1
  92 bind2
  93 Bind2
  94 BPair
  95 BUnit
  96 bw
  97 bw_pos
  98 candidate
  99 Cast
 100 cdeq
 101 cdeq_ext
 102 ceq
 103 ceq_ext
 104 ceq_ext_inv_eq
 105 ceq_ext_refl
 106 ceq_ext_trans
 107 ceq_inv_lift_sn
 108 ceq_lift_sn
 109 cext2
 110 cext2_co
 111 cext2_d_liftable2_sn
 112 cext2_sym
 113 cfull
 114 cfull_dec
 115 cfull_lift_sn
 116 cfun
 117 co_dedropable_sn
 118 co_dedropable_sn_CTC
 119 co_dedropable_sn_ltc
 120 co_dropable_dx
 121 co_dropable_dx_CTC
 122 co_dropable_dx_ltc
 123 co_dropable_sn
 124 co_dropable_sn_CTC
 125 co_dropable_sn_ltc
 126 CP0
 127 CP1
 128 CP2
 129 CP3
 130 d1_liftable_liftable_all
 131 d2_deliftable_sn_CTC
 132 d2_deliftable_sn_ltc
 133 d2_liftable_sn_CTC
 134 d2_liftable_sn_ltc
 135 d_appendable_sn
 136 d_deliftable1
 137 d_deliftable1_isuni
 138 d_deliftable2_bi
 139 d_deliftable2_sn
 140 d_deliftable2_sn_bi
 141 dedropable_sn
 142 dedropable_sn_CTC
 143 deg_inv_prec
 144 deg_inv_pred
 145 deg_iter
 146 deg_next_SO
 147 deg_O
 148 deg_SO
 149 deg_SO_gt
 150 deg_SO_inv_succ
 151 deg_SO_inv_succ_aux
 152 deg_SO_refl
 153 deg_SO_succ
 154 deg_SO_zero
 155 deliftable2_bi
 156 deliftable2_dx
 157 deliftable2_sn
 158 deliftable2_sn_bi
 159 deliftable2_sn_dx
 160 destruct_apair_apair_aux
 161 destruct_lbind_lbind_aux
 162 destruct_sort_sort_aux
 163 destruct_tatom_tatom_aux
 164 destruct_tpair_tpair_aux
 165 discr_apair_xy_x
 166 discr_apair_xy_y
 167 discr_lbind_x_xy
 168 discr_lbind_xy_x
 169 discr_tpair_xy_x
 170 discr_tpair_xy_y
 171 d_liftable1
 172 d_liftable1_all
 173 d_liftable1_isuni
 174 d_liftable2_bi
 175 d_liftable2_sn
 176 d_liftable2_sn_bi
 177 dropable_dx
 178 dropable_dx_CTC
 179 dropable_sn
 180 dropable_sn_CTC
 181 drops
 182 drops_after_fwd_drop2
 183 drops_atom
 184 drops_atom2_sex_conf
 185 drops_atom_F
 186 drops_bind2_fwd_rfw
 187 drops_conf
 188 drops_conf_div
 189 drops_conf_div_bind_isuni
 190 drops_conf_div_fcla
 191 drops_conf_div_isuni
 192 drops_conf_skip1
 193 drops_drop
 194 drops_eq_repl_back
 195 drops_eq_repl_fwd
 196 drops_F
 197 drops_fcla_fwd
 198 drops_fcla_fwd_le2
 199 drops_fcla_fwd_lt2
 200 drops_fcla_fwd_lt4
 201 drops_F_uni
 202 drops_fwd_drop2
 203 drops_fwd_drop2_aux
 204 drops_fwd_fcla
 205 drops_fwd_fcla_le2
 206 drops_fwd_fcla_lt2
 207 drops_fwd_isfin
 208 drops_fwd_isid
 209 drops_fwd_length_eq1
 210 drops_fwd_length_eq2
 211 drops_fwd_length_le4
 212 drops_fwd_lw
 213 drops_fwd_lw_lt
 214 drops_gen
 215 drops_inv_atom1
 216 drops_inv_atom1_aux
 217 drops_inv_atom2
 218 drops_inv_bind1_isuni
 219 drops_inv_bind2_isuni
 220 drops_inv_bind2_isuni_next
 221 drops_inv_drop1
 222 drops_inv_drop1_aux
 223 drops_inv_F
 224 drops_inv_gen
 225 drops_inv_isuni
 226 drops_inv_length_eq
 227 drops_inv_skip1
 228 drops_inv_skip1_aux
 229 drops_inv_skip2
 230 drops_inv_skip2_aux
 231 drops_inv_succ
 232 drops_inv_TF
 233 drops_inv_TF_aux
 234 drops_inv_uni
 235 drops_inv_x_bind_xy
 236 drops_isuni_ex
 237 drops_isuni_fwd_drop2
 238 drops_ldec_dec
 239 drops_lsubc_trans
 240 drops_mono
 241 drops_refl
 242 drops_seq_trans_next
 243 drops_sex_trans_next
 244 drops_sex_trans_push
 245 drops_skip
 246 drops_split_div
 247 drops_split_trans
 248 drops_split_trans_bind2
 249 drops_TF
 250 drops_tls_at
 251 drops_trans
 252 drops_trans_skip2
 253 eq_aarity_dec
 254 eq_bind1_dec
 255 eq_bind2_dec
 256 eq_bind_dec
 257 eq_false_inv_tpair_dx
 258 eq_false_inv_tpair_sn
 259 eq_flat2_dec
 260 eq_genv_dec
 261 eq_item0_dec
 262 eq_item2_dec
 263 eq_lenv_dec
 264 eq_term_dec
 265 ext2
 266 ext2_dec
 267 ext2_inv_pair
 268 ext2_inv_pair_dx
 269 ext2_inv_pair_dx_aux
 270 ext2_inv_pair_sn
 271 ext2_inv_pair_sn_aux
 272 ext2_inv_tc
 273 ext2_inv_unit
 274 ext2_inv_unit_dx
 275 ext2_inv_unit_dx_aux
 276 ext2_inv_unit_sn
 277 ext2_inv_unit_sn_aux
 278 ext2_pair
 279 ext2_refl
 280 ext2_sym
 281 ext2_tc
 282 ext2_tc_inj
 283 ext2_tc_pair
 284 ext2_tc_step
 285 ext2_trans
 286 ext2_unit
 287 f_dedropable_sn
 288 f_dropable_dx
 289 f_dropable_sn
 290 feqx
 291 feqx_canc_dx
 292 feqx_canc_sn
 293 feqx_fqus_trans
 294 feqx_intro_dx
 295 feqx_intro_sn
 296 feqx_inv_gen_dx
 297 feqx_inv_gen_sn
 298 feqx_refl
 299 feqx_sym
 300 feqx_tneqx_repl_dx
 301 feqx_trans
 302 flat2
 303 Flat2
 304 fold
 305 fold_atom
 306 fold_pair
 307 fold_unit
 308 fqu
 309 fqu_bind_dx
 310 fqu_clear
 311 fqu_drop
 312 fqu_flat_dx
 313 fqu_fqup
 314 fqu_fquq
 315 fqu_fwd_fw
 316 fqu_fwd_length_lref1
 317 fqu_fwd_length_lref1_aux
 318 fqu_gref
 319 fqu_inv_atom1
 320 fqu_inv_bind1
 321 fqu_inv_bind1_aux
 322 fqu_inv_bind1_true
 323 fqu_inv_flat1
 324 fqu_inv_flat1_aux
 325 fqu_inv_gref1
 326 fqu_inv_gref1_aux
 327 fqu_inv_gref1_bind
 328 fqu_inv_lref1
 329 fqu_inv_lref1_aux
 330 fqu_inv_lref1_bind
 331 fqu_inv_sort1
 332 fqu_inv_sort1_aux
 333 fqu_inv_sort1_bind
 334 fqu_inv_teqx
 335 fqu_inv_teqx_aux
 336 fqu_inv_zero1_pair
 337 fqu_lref_O
 338 fqu_lref_S
 339 fqup
 340 fqu_pair_sn
 341 fqup_bind_dx
 342 fqup_bind_dx_flat_dx
 343 fqup_clear
 344 fqup_drops_strap1
 345 fqup_drops_succ
 346 fqup_flat_dx
 347 fqup_flat_dx_bind_dx
 348 fqup_flat_dx_pair_sn
 349 fqup_fqus
 350 fqup_fqus_trans
 351 fqup_fwd_fw
 352 fqup_ind
 353 fqup_ind_dx
 354 fqup_inv_step_sn
 355 fqup_lref
 356 fqup_pair_sn
 357 fqup_strap1
 358 fqup_strap2
 359 fqup_trans
 360 fqup_wf_ind
 361 fqup_wf_ind_eq
 362 fqup_zeta
 363 fquq
 364 fquq_fqus
 365 fquq_fwd_fw
 366 fquq_fwd_length_lref1
 367 fquq_refl
 368 fqus
 369 fqus_drops
 370 fqus_fqup_trans
 371 fqus_fwd_fw
 372 fqus_ind
 373 fqus_ind_dx
 374 fqus_inv_atom1
 375 fqus_inv_bind1
 376 fqus_inv_bind1_true
 377 fqus_inv_flat1
 378 fqus_inv_fqup
 379 fqus_inv_fqu_sn
 380 fqus_inv_gref1
 381 fqus_inv_gref1_bind
 382 fqus_inv_lref1
 383 fqus_inv_lref1_bind
 384 fqus_inv_refl_atom3
 385 fqus_inv_sort1
 386 fqus_inv_sort1_bind
 387 fqus_inv_zero1_pair
 388 fqu_sort
 389 fqus_refl
 390 fqus_strap1
 391 fqus_strap1_fqu
 392 fqus_strap2
 393 fqus_strap2_fqu
 394 fqus_trans
 395 fqu_teqx_conf
 396 fqu_wf_ind
 397 frees
 398 frees_append_void
 399 frees_atom
 400 frees_atom_drops
 401 frees_bind
 402 frees_bind_void
 403 frees_eq_repl_back
 404 frees_eq_repl_fwd
 405 frees_flat
 406 frees_fwd_coafter
 407 frees_fwd_isfin
 408 frees_gref
 409 frees_ind_void
 410 frees_inv_append_void
 411 frees_inv_append_void_aux
 412 frees_inv_atom
 413 frees_inv_atom_aux
 414 frees_inv_bind
 415 frees_inv_bind_aux
 416 frees_inv_bind_void
 417 frees_inv_drops_next
 418 frees_inv_flat
 419 frees_inv_flat_aux
 420 frees_inv_gref
 421 frees_inv_gref_aux
 422 frees_inv_lifts
 423 frees_inv_lifts_ex
 424 frees_inv_lifts_SO
 425 frees_inv_lref
 426 frees_inv_lref_aux
 427 frees_inv_lref_drops
 428 frees_inv_pair
 429 frees_inv_pair_aux
 430 frees_inv_sort
 431 frees_inv_sort_aux
 432 frees_inv_unit
 433 frees_inv_unit_aux
 434 frees_lifts
 435 frees_lifts_SO
 436 frees_lref
 437 frees_lref_push
 438 frees_lref_pushs
 439 frees_mono
 440 frees_pair
 441 frees_pair_drops
 442 frees_req_conf
 443 frees_reqx_conf
 444 frees_sex_conf
 445 frees_sort
 446 frees_teqx_conf
 447 frees_teqx_conf_reqx
 448 frees_total
 449 frees_unit
 450 frees_unit_drops
 451 fsge_rex_trans
 452 fsle
 453 fsle_bind
 454 fsle_bind_dx_dx
 455 fsle_bind_dx_sn
 456 fsle_bind_eq
 457 fsle_bind_sn_ge
 458 fsle_flat
 459 fsle_flat_dx_dx
 460 fsle_flat_dx_sn
 461 fsle_flat_sn
 462 fsle_frees_trans
 463 fsle_frees_trans_eq
 464 fsle_fwd_pair_sn
 465 fsle_gref
 466 fsle_gref_bi
 467 fsle_inv_frees_eq
 468 fsle_inv_lifts_sn
 469 fsle_lifts_dx
 470 fsle_lifts_sn
 471 fsle_lifts_SO
 472 fsle_lifts_SO_sn
 473 fsle_pair_bi
 474 fsle_refl
 475 fsle_shift
 476 fsle_sort
 477 fsle_sort_bi
 478 fsle_trans_dx
 479 fsle_trans_rc
 480 fsle_trans_sn
 481 fsle_unit_bi
 482 f_transitive_next
 483 fw
 484 fw_clear
 485 fw_lpair_sn
 486 fw_shift
 487 fw_tpair_dx
 488 fw_tpair_sn
 489 GAtom
 490 gcp
 491 gcp2_all
 492 gcr
 493 gcr_aaa
 494 genv
 495 glength
 496 GPair
 497 GRef
 498 gw
 499 gw_pair
 500 is_apear_dec
 501 is_lifts_dec
 502 item0
 503 item2
 504 LAtom
 505 LBind
 506 length
 507 length_atom
 508 length_bind
 509 length_inv_succ_dx
 510 length_inv_succ_dx_ltail
 511 length_inv_succ_sn
 512 length_inv_succ_sn_ltail
 513 length_inv_zero_dx
 514 length_inv_zero_sn
 515 lenv
 516 lenv_case_tail
 517 lenv_ind_tail
 518 lex
 519 lex_atom
 520 lex_bind
 521 lex_bind_refl_dx
 522 lex_co
 523 lex_conf
 524 lex_confluent
 525 lex_CTC
 526 lex_CTC_ind_dx
 527 lex_CTC_ind_sn
 528 lex_CTC_inj
 529 lex_CTC_step_dx
 530 lex_CTC_step_sn
 531 lex_dropable_dx
 532 lex_dropable_sn
 533 lex_drops_conf_pair
 534 lex_drops_trans_pair
 535 lex_fwd_length
 536 lex_ind
 537 lex_inv_atom_dx
 538 lex_inv_atom_sn
 539 lex_inv_bind_dx
 540 lex_inv_bind_sn
 541 lex_inv_CTC
 542 lex_inv_pair
 543 lex_inv_pair_dx
 544 lex_inv_pair_sn
 545 lex_inv_unit_dx
 546 lex_inv_unit_sn
 547 lex_liftable_dedropable_sn
 548 lex_pair
 549 lex_refl
 550 lex_trans
 551 lex_transitive
 552 lex_unit
 553 liftable2_bi
 554 liftable2_dx
 555 liftable2_sn
 556 liftable2_sn_bi
 557 liftable2_sn_dx
 558 lifts
 559 lifts_applv
 560 liftsb
 561 liftsb_conf
 562 liftsb_div3
 563 liftsb_eq_repl_back
 564 liftsb_fwd_bw
 565 liftsb_fwd_isid
 566 lifts_bind
 567 liftsb_inj
 568 liftsb_inv_pair_dx
 569 liftsb_inv_pair_sn
 570 liftsb_inv_unit_dx
 571 liftsb_inv_unit_sn
 572 liftsb_mono
 573 liftsb_refl
 574 liftsb_split_trans
 575 liftsb_total
 576 liftsb_trans
 577 lifts_conf
 578 lifts_div3
 579 lifts_div4
 580 lifts_div4_one
 581 lifts_eq_repl_back
 582 lifts_eq_repl_fwd
 583 lifts_flat
 584 lifts_fwd_isid
 585 lifts_fwd_pair1
 586 lifts_fwd_pair2
 587 lifts_fwd_tw
 588 lifts_gref
 589 lifts_inj
 590 lifts_inv_applv1
 591 lifts_inv_applv2
 592 lifts_inv_atom1
 593 lifts_inv_atom2
 594 lifts_inv_bind1
 595 lifts_inv_bind1_aux
 596 lifts_inv_bind2
 597 lifts_inv_bind2_aux
 598 lifts_inv_flat1
 599 lifts_inv_flat1_aux
 600 lifts_inv_flat2
 601 lifts_inv_flat2_aux
 602 lifts_inv_gref1
 603 lifts_inv_gref1_aux
 604 lifts_inv_gref2
 605 lifts_inv_gref2_aux
 606 lifts_inv_lref1
 607 lifts_inv_lref1_aux
 608 lifts_inv_lref1_uni
 609 lifts_inv_lref2
 610 lifts_inv_lref2_aux
 611 lifts_inv_lref2_uni
 612 lifts_inv_lref2_uni_ge
 613 lifts_inv_lref2_uni_lt
 614 lifts_inv_pair_xy_x
 615 lifts_inv_pair_xy_y
 616 lifts_inv_push_succ_sn
 617 lifts_inv_push_zero_sn
 618 lifts_inv_sort1
 619 lifts_inv_sort1_aux
 620 lifts_inv_sort2
 621 lifts_inv_sort2_aux
 622 lifts_lref
 623 lifts_lref_ge
 624 lifts_lref_ge_minus
 625 lifts_lref_lt
 626 lifts_lref_uni
 627 lifts_mono
 628 lifts_push_lref
 629 lifts_push_zero
 630 lifts_refl
 631 lifts_simple_dx
 632 lifts_simple_sn
 633 lifts_sort
 634 lifts_split_div
 635 lifts_split_trans
 636 lifts_total
 637 lifts_trans
 638 lifts_trans4_one
 639 lifts_trans_uni
 640 lifts_uni
 641 liftsv
 642 liftsv_cons
 643 liftsv_inj
 644 liftsv_inv_cons1
 645 liftsv_inv_cons1_aux
 646 liftsv_inv_cons2
 647 liftsv_inv_cons2_aux
 648 liftsv_inv_nil1
 649 liftsv_inv_nil1_aux
 650 liftsv_inv_nil2
 651 liftsv_inv_nil2_aux
 652 liftsv_mono
 653 liftsv_nil
 654 liftsv_split_trans
 655 liftsv_total
 656 liftsv_trans
 657 LRef
 658 lsuba
 659 lsuba_aaa_conf
 660 lsuba_aaa_trans
 661 lsuba_atom
 662 lsuba_beta
 663 lsuba_bind
 664 lsuba_drops_conf_isuni
 665 lsuba_drops_trans_isuni
 666 lsuba_fwd_lsubr
 667 lsuba_inv_atom1
 668 lsuba_inv_atom1_aux
 669 lsuba_inv_atom2
 670 lsuba_inv_atom2_aux
 671 lsuba_inv_bind1
 672 lsuba_inv_bind1_aux
 673 lsuba_inv_bind2
 674 lsuba_inv_bind2_aux
 675 lsuba_lsubc
 676 lsuba_refl
 677 lsuba_trans
 678 lsubc
 679 lsubc_atom
 680 lsubc_beta
 681 lsubc_bind
 682 lsubc_drops_trans_isuni
 683 lsubc_fwd_lsubr
 684 lsubc_inv_atom1
 685 lsubc_inv_atom1_aux
 686 lsubc_inv_atom2
 687 lsubc_inv_atom2_aux
 688 lsubc_inv_bind1
 689 lsubc_inv_bind1_aux
 690 lsubc_inv_bind2
 691 lsubc_inv_bind2_aux
 692 lsubc_refl
 693 lsubf
 694 lsubf_atom
 695 lsubf_beta
 696 lsubf_beta_tl_dx
 697 lsubf_bind
 698 lsubf_bind_tl_dx
 699 lsubf_eq_repl_back1
 700 lsubf_eq_repl_back2
 701 lsubf_eq_repl_fwd1
 702 lsubf_eq_repl_fwd2
 703 lsubf_frees_trans
 704 lsubf_fwd_bind_tl
 705 lsubf_fwd_isid_dx
 706 lsubf_fwd_isid_sn
 707 lsubf_fwd_lsubr_isdiv
 708 lsubf_fwd_sle
 709 lsubf_inv_atom
 710 lsubf_inv_atom1
 711 lsubf_inv_atom1_aux
 712 lsubf_inv_atom2
 713 lsubf_inv_atom2_aux
 714 lsubf_inv_beta_sn
 715 lsubf_inv_bind_sn
 716 lsubf_inv_pair1
 717 lsubf_inv_pair1_aux
 718 lsubf_inv_pair2
 719 lsubf_inv_pair2_aux
 720 lsubf_inv_push1
 721 lsubf_inv_push1_aux
 722 lsubf_inv_push2
 723 lsubf_inv_push2_aux
 724 lsubf_inv_push_sn
 725 lsubf_inv_refl
 726 lsubf_inv_sor_dx
 727 lsubf_inv_unit1
 728 lsubf_inv_unit1_aux
 729 lsubf_inv_unit2
 730 lsubf_inv_unit2_aux
 731 lsubf_inv_unit_sn
 732 lsubf_push
 733 lsubf_refl
 734 lsubf_refl_eq
 735 lsubf_sor
 736 lsubf_unit
 737 lsubr
 738 lsubr_atom
 739 lsubr_beta
 740 lsubr_bind
 741 lsubr_fwd_bind1
 742 lsubr_fwd_bind2
 743 lsubr_fwd_drops2_abbr
 744 lsubr_fwd_drops2_bind
 745 lsubr_fwd_length
 746 lsubr_inv_abbr2
 747 lsubr_inv_abst1
 748 lsubr_inv_abst2
 749 lsubr_inv_atom1
 750 lsubr_inv_atom1_aux
 751 lsubr_inv_atom2
 752 lsubr_inv_atom2_aux
 753 lsubr_inv_bind1
 754 lsubr_inv_bind1_aux
 755 lsubr_inv_bind2
 756 lsubr_inv_bind2_aux
 757 lsubr_inv_pair2
 758 lsubr_inv_unit1
 759 lsubr_inv_unit2
 760 lsubr_lsubf
 761 lsubr_lsubf_isid
 762 lsubr_refl
 763 lsubr_trans
 764 lsubr_unit
 765 ltail_length
 766 lveq
 767 lveq_atom
 768 lveq_bind
 769 lveq_fwd_abst_bind_length_le
 770 lveq_fwd_bind_abst_length_le
 771 lveq_fwd_gen
 772 lveq_fwd_length
 773 lveq_fwd_length_eq
 774 lveq_fwd_length_le_dx
 775 lveq_fwd_length_le_sn
 776 lveq_fwd_length_minus
 777 lveq_fwd_length_plus
 778 lveq_fwd_pair_dx
 779 lveq_fwd_pair_sn
 780 lveq_inj
 781 lveq_inj_length
 782 lveq_inj_void_dx_le
 783 lveq_inj_void_sn_ge
 784 lveq_inv_atom_atom
 785 lveq_inv_atom_bind
 786 lveq_inv_bind
 787 lveq_inv_bind_atom
 788 lveq_inv_bind_O
 789 lveq_inv_pair_pair
 790 lveq_inv_succ
 791 lveq_inv_succ_aux
 792 lveq_inv_succ_dx
 793 lveq_inv_succ_sn
 794 lveq_inv_succ_sn_aux
 795 lveq_inv_void_dx_length
 796 lveq_inv_void_sn_length
 797 lveq_inv_void_succ_dx
 798 lveq_inv_void_succ_sn
 799 lveq_inv_zero
 800 lveq_inv_zero_aux
 801 lveq_length_eq
 802 lveq_length_fwd_dx
 803 lveq_length_fwd_sn
 804 lveq_refl
 805 lveq_sym
 806 lveq_void_dx
 807 lveq_void_sn
 808 lw
 809 lw_bind
 810 mk_ac
 811 mk_ac_props
 812 mk_gcp
 813 mk_gcr
 814 mk_sd
 815 mk_sd_props
 816 mk_sh
 817 mk_sh_acyclic
 818 mk_sh_decidable
 819 mk_sh_lt
 820 nexts_le
 821 nexts_lt
 822 nf
 823 R_confluent2_rex
 824 req
 825 req_feqx_trans
 826 req_fsle_comp
 827 req_fwd_rex
 828 req_inv_bind
 829 req_inv_flat
 830 req_inv_lifts_bi
 831 req_inv_lref_bind_dx
 832 req_inv_lref_bind_sn
 833 req_inv_zero_pair_dx
 834 req_inv_zero_pair_sn
 835 req_refl
 836 req_reqx
 837 req_reqx_trans
 838 req_rex_trans
 839 req_transitive
 840 reqx
 841 reqx_atom
 842 reqx_bind
 843 reqx_bind_repl_dx
 844 reqx_bind_void
 845 reqx_canc_dx
 846 reqx_canc_sn
 847 reqx_dec
 848 reqx_flat
 849 reqx_fqup_trans
 850 reqx_fquq_trans
 851 reqx_fqus_trans
 852 reqx_fqu_trans
 853 reqx_fsge_comp
 854 reqx_fwd_bind_dx
 855 reqx_fwd_bind_dx_void
 856 reqx_fwd_dx
 857 reqx_fwd_flat_dx
 858 reqx_fwd_length
 859 reqx_fwd_pair_sn
 860 reqx_fwd_zero_pair
 861 reqx_gref
 862 reqx_gref_length
 863 reqx_inv_atom_dx
 864 reqx_inv_atom_sn
 865 reqx_inv_bind
 866 reqx_inv_bind_void
 867 reqx_inv_flat
 868 reqx_inv_lifts_bi
 869 reqx_inv_lifts_dx
 870 reqx_inv_lifts_sn
 871 reqx_inv_lref
 872 reqx_inv_lref_bind_dx
 873 reqx_inv_lref_bind_sn
 874 reqx_inv_lref_pair_bi
 875 reqx_inv_lref_pair_dx
 876 reqx_inv_lref_pair_sn
 877 reqx_inv_zero
 878 reqx_inv_zero_pair_dx
 879 reqx_inv_zero_pair_sn
 880 reqx_lifts_bi
 881 reqx_lifts_sn
 882 reqx_lref
 883 reqx_pair
 884 reqx_pair_refl
 885 reqx_refl
 886 reqx_repl
 887 reqx_rneqx_trans
 888 reqx_sort
 889 reqx_sort_length
 890 reqx_sym
 891 reqx_trans
 892 reqx_unit
 893 reqx_unit_length
 894 rex
 895 rex_atom
 896 rex_bind
 897 rex_bind_dx_split
 898 rex_bind_dx_split_void
 899 rex_bind_repl_dx
 900 rex_bind_void
 901 rex_co
 902 rex_conf
 903 rex_confluent
 904 rex_dec
 905 rex_dropable_dx
 906 rex_dropable_sn
 907 rex_flat
 908 rex_flat_dx_split
 909 rex_fsge_compatible
 910 rex_fsle_compatible
 911 rex_fwd_bind_dx
 912 rex_fwd_bind_dx_void
 913 rex_fwd_dx
 914 rex_fwd_flat_dx
 915 rex_fwd_length
 916 rex_fwd_pair_sn
 917 rex_fwd_zero_pair
 918 rex_gref
 919 rex_gref_length
 920 rex_inv_atom_dx
 921 rex_inv_atom_sn
 922 rex_inv_bind
 923 rex_inv_bind_void
 924 rex_inv_flat
 925 rex_inv_frees
 926 rex_inv_gref
 927 rex_inv_gref_bind_dx
 928 rex_inv_gref_bind_sn
 929 rex_inv_lex_req
 930 rex_inv_lifts_bi
 931 rex_inv_lref
 932 rex_inv_lref_bind_dx
 933 rex_inv_lref_bind_sn
 934 rex_inv_lref_pair_bi
 935 rex_inv_lref_pair_dx
 936 rex_inv_lref_pair_sn
 937 rex_inv_lref_unit_dx
 938 rex_inv_lref_unit_sn
 939 rex_inv_sort
 940 rex_inv_sort_bind_dx
 941 rex_inv_sort_bind_sn
 942 rex_inv_zero
 943 rex_inv_zero_length
 944 rex_inv_zero_pair_dx
 945 rex_inv_zero_pair_sn
 946 rex_inv_zero_unit_dx
 947 rex_inv_zero_unit_sn
 948 rex_isid
 949 rex_lex
 950 rex_liftable_dedropable_sn
 951 rex_lifts_bi
 952 rex_lref
 953 rex_pair
 954 rex_pair_refl
 955 rex_pair_sn_split
 956 rex_refl
 957 rexs
 958 rexs_atom
 959 rexs_co
 960 rexs_fwd_bind_dx
 961 rexs_fwd_bind_dx_void
 962 rexs_fwd_flat_dx
 963 rexs_fwd_length
 964 rexs_fwd_pair_sn
 965 rexs_gref
 966 rexs_ind_dx
 967 rexs_ind_sn
 968 rexs_inv_atom_dx
 969 rexs_inv_atom_sn
 970 rexs_inv_bind
 971 rexs_inv_bind_void
 972 rexs_inv_flat
 973 rexs_inv_gref
 974 rexs_inv_gref_bind_dx
 975 rexs_inv_gref_bind_sn
 976 rexs_inv_lex_req
 977 rexs_inv_sort
 978 rexs_inv_sort_bind_dx
 979 rexs_inv_sort_bind_sn
 980 rexs_lex
 981 rexs_lex_req
 982 rexs_lref
 983 rex_sort
 984 rex_sort_length
 985 rexs_pair
 986 rexs_pair_refl
 987 rexs_refl
 988 rexs_sort
 989 rexs_step_dx
 990 rexs_step_sn
 991 rexs_sym
 992 rexs_tc
 993 rexs_trans
 994 rexs_unit
 995 rex_sym
 996 rex_trans_fsle
 997 rex_transitive
 998 rex_trans_next
 999 rex_unit
1000 rex_unit_length
1001 rex_unit_sn
1002 R_fsge_compatible
1003 rfw
1004 rfw_clear
1005 rfw_lpair_dx
1006 rfw_lpair_sn
1007 rfw_shift
1008 rfw_tpair_dx
1009 rfw_tpair_sn
1010 rneqx_inv_bind
1011 rneqx_inv_bind_void
1012 rneqx_inv_flat
1013 rneqx_reqx_canc_dx
1014 rneqx_reqx_div
1015 rnex_inv_bind
1016 rnex_inv_bind_void
1017 rnex_inv_flat
1018 R_pw_confluent2_sex
1019 S1
1020 S2
1021 S3
1022 S5
1023 S6
1024 S7
1025 sd
1026 sd_d
1027 sd_d_correct
1028 sd_d_props
1029 sd_d_SS
1030 sd_O
1031 sd_O_props
1032 sd_props
1033 sd_SO
1034 sd_SO_props
1035 seq
1036 seq_canc_dx
1037 seq_canc_sn
1038 seq_co_dedropable_sn
1039 seq_co_dropable_dx
1040 seq_co_dropable_sn
1041 seq_drops_conf_next
1042 seq_drops_trans_next
1043 seq_eq_repl_back
1044 seq_eq_repl_fwd
1045 seq_fwd_length
1046 seq_inv_atom1
1047 seq_inv_atom2
1048 seq_inv_next
1049 seq_inv_next1
1050 seq_inv_next2
1051 seq_inv_push
1052 seq_inv_push1
1053 seq_inv_push2
1054 seq_inv_tl
1055 seq_join
1056 seq_meet
1057 seq_refl
1058 seq_sym
1059 seq_trans
1060 sex
1061 sex_atom
1062 sex_canc_dx
1063 sex_canc_sn
1064 sex_co
1065 sex_co_dropable_dx
1066 sex_co_dropable_sn
1067 sex_co_isid
1068 sex_conf
1069 sex_dec
1070 sex_dropable_dx_aux
1071 sex_drops_conf_next
1072 sex_drops_conf_push
1073 sex_drops_trans_next
1074 sex_drops_trans_push
1075 sex_eq_repl_back
1076 sex_eq_repl_fwd
1077 sex_fwd_bind
1078 sex_fwd_length
1079 sex_inv_atom1
1080 sex_inv_atom1_aux
1081 sex_inv_atom2
1082 sex_inv_atom2_aux
1083 sex_inv_next
1084 sex_inv_next1
1085 sex_inv_next1_aux
1086 sex_inv_next2
1087 sex_inv_next2_aux
1088 sex_inv_push
1089 sex_inv_push1
1090 sex_inv_push1_aux
1091 sex_inv_push2
1092 sex_inv_push2_aux
1093 sex_inv_tc_dx
1094 sex_inv_tc_sn
1095 sex_inv_tl
1096 sex_join
1097 sex_length_cfull
1098 sex_length_isid
1099 sex_liftable_co_dedropable_bi
1100 sex_liftable_co_dedropable_sn
1101 sex_meet
1102 sex_next
1103 sex_pair_repl
1104 sex_push
1105 sex_refl
1106 sex_sdj
1107 sex_sdj_split
1108 sex_sle_split
1109 sex_sym
1110 sex_tc_dx
1111 sex_tc_inj_dx
1112 sex_tc_inj_sn
1113 sex_tc_next
1114 sex_tc_next_dx
1115 sex_tc_next_sn
1116 sex_tc_push
1117 sex_tc_push_dx
1118 sex_tc_push_sn
1119 sex_tc_refl
1120 sex_tc_step_dx
1121 sex_trans
1122 sex_trans_gen
1123 sex_trans_id_cfull
1124 sex_transitive
1125 sh
1126 sh_acyclic
1127 sh_decidable
1128 sh_lt
1129 sh_lt_acyclic
1130 sh_lt_dec
1131 sh_lt_nexts_inv_lt
1132 simple
1133 simple_atom
1134 simple_dec_ex
1135 simple_flat
1136 simple_inv_bind
1137 simple_inv_bind_aux
1138 simple_inv_pair
1139 simple_teqo_repl_dx
1140 simple_teqo_repl_sn
1141 sle_seq_trans
1142 sle_sex_conf
1143 sle_sex_trans
1144 Sort
1145 s_rs_transitive_isid
1146 s_rs_transitive_lex_inv_isid
1147 TAtom
1148 tc_f_dedropable_sn
1149 tc_f_dropable_dx
1150 tc_f_dropable_sn
1151 teqo
1152 teqo_canc_dx
1153 teqo_canc_sn
1154 teqo_dec
1155 teqo_gref
1156 teqo_inv_applv_bind_simple
1157 teqo_inv_gref1
1158 teqo_inv_gref1_aux
1159 teqo_inv_lifts_bi
1160 teqo_inv_lref1
1161 teqo_inv_lref1_aux
1162 teqo_inv_pair
1163 teqo_inv_pair1
1164 teqo_inv_pair1_aux
1165 teqo_inv_pair2
1166 teqo_inv_pair2_aux
1167 teqo_inv_sort1
1168 teqo_inv_sort1_aux
1169 teqo_lifts_bi
1170 teqo_lifts_dx
1171 teqo_lifts_sn
1172 teqo_lref
1173 teqo_pair
1174 teqo_refl
1175 teqo_sort
1176 teqo_sym
1177 teqo_trans
1178 teqx
1179 teqx_canc_dx
1180 teqx_canc_sn
1181 teqx_dec
1182 teqx_ext
1183 teqx_feqx
1184 teqx_fqup_trans
1185 teqx_fquq_trans
1186 teqx_fqus_trans
1187 teqx_fqu_trans
1188 teqx_fwd_atom1
1189 teqx_gref
1190 teqx_inv_gref1
1191 teqx_inv_gref1_aux
1192 teqx_inv_lifts_bi
1193 teqx_inv_lifts_dx
1194 teqx_inv_lifts_sn
1195 teqx_inv_lref1
1196 teqx_inv_lref1_aux
1197 teqx_inv_pair
1198 teqx_inv_pair1
1199 teqx_inv_pair1_aux
1200 teqx_inv_pair2
1201 teqx_inv_pair_xy_x
1202 teqx_inv_pair_xy_y
1203 teqx_inv_sort1
1204 teqx_inv_sort1_aux
1205 teqx_inv_sort2
1206 teqx_lifts_bi
1207 teqx_lifts_dx
1208 teqx_lifts_inv_pair_sn
1209 teqx_lifts_sn
1210 teqx_lref
1211 teqx_pair
1212 teqx_refl
1213 teqx_repl
1214 teqx_reqx_conf
1215 teqx_reqx_div
1216 teqx_rex_conf
1217 teqx_rex_div
1218 teqx_sort
1219 teqx_sym
1220 teqx_teqo
1221 teqx_tneqx_trans
1222 teqx_trans
1223 teqx_tweq
1224 term
1225 tneqx_inv_pair
1226 tneqx_teqx_canc_dx
1227 TPair
1228 tw
1229 tweq
1230 tweq_abbr
1231 tweq_abbr_neg
1232 tweq_abbr_pos
1233 tweq_abst
1234 tweq_appl
1235 tweq_canc_dx
1236 tweq_canc_sn
1237 tweq_cast
1238 tweq_dec
1239 tweq_fwd_pair_bi
1240 tweq_fwd_pair_sn
1241 tweq_gref
1242 tweq_inv_abbr_neg_sn
1243 tweq_inv_abbr_pos_bi
1244 tweq_inv_abbr_pos_sn
1245 tweq_inv_abbr_pos_x_lifts_y_y
1246 tweq_inv_abbr_sn
1247 tweq_inv_abbr_sn_aux
1248 tweq_inv_abst_sn
1249 tweq_inv_abst_sn_aux
1250 tweq_inv_appl_bi
1251 tweq_inv_appl_sn
1252 tweq_inv_appl_sn_aux
1253 tweq_inv_cast_bi
1254 tweq_inv_cast_sn
1255 tweq_inv_cast_sn_aux
1256 tweq_inv_cast_xy_y
1257 tweq_inv_gref_sn
1258 tweq_inv_gref_sn_aux
1259 tweq_inv_lifts_bi
1260 tweq_inv_lref_sn
1261 tweq_inv_lref_sn_aux
1262 tweq_inv_sort_sn
1263 tweq_inv_sort_sn_aux
1264 tweq_lifts_bi
1265 tweq_lifts_dx
1266 tweq_lifts_sn
1267 tweq_lref
1268 tweq_refl
1269 tweq_repl
1270 tweq_simple_trans
1271 tweq_sort
1272 tweq_sym
1273 tweq_trans
1274 tw_le_pair_dx
1275 tw_pos
1276 Void