matita/matita/contribs/lambda-delta/Basic-2/Basic-1.txt

   1 # waiting ####################################################################
   2
   3 aplus/props aplus_reg_r
   4 aplus/props aplus_assoc
   5 aplus/props aplus_asucc
   6 aplus/props aplus_sort_O_S_simpl
   7 aplus/props aplus_sort_S_S_simpl
   8 aplus/props aplus_asort_O_simpl
   9 aplus/props aplus_asort_le_simpl
  10 aplus/props aplus_asort_simpl
  11 aplus/props aplus_ahead_simpl
  12 aplus/props aplus_asucc_false
  13 aplus/props aplus_inj
  14 aprem/fwd aprem_gen_sort
  15 aprem/fwd aprem_gen_head_O
  16 aprem/fwd aprem_gen_head_S
  17 aprem/props aprem_repl
  18 aprem/props aprem_asucc
  19 arity/aprem arity_aprem
  20 arity/cimp arity_cimp_conf
  21 arity/fwd arity_gen_sort
  22 arity/fwd arity_gen_lref
  23 arity/fwd arity_gen_bind
  24 arity/fwd arity_gen_abst
  25 arity/fwd arity_gen_appl
  26 arity/fwd arity_gen_cast
  27 arity/fwd arity_gen_appls
  28 arity/fwd arity_gen_lift
  29 arity/lift1 arity_lift1
  30 arity/pr3 arity_sred_wcpr0_pr0
  31 arity/pr3 arity_sred_wcpr0_pr1
  32 arity/pr3 arity_sred_pr2
  33 arity/pr3 arity_sred_pr3
  34 arity/props node_inh
  35 arity/props arity_lift
  36 arity/props arity_mono
  37 arity/props arity_repellent
  38 arity/props arity_appls_cast
  39 arity/props arity_appls_abbr
  40 arity/props arity_appls_bind
  41 arity/subst0 arity_gen_cvoid_subst0
  42 arity/subst0 arity_gen_cvoid
  43 arity/subst0 arity_fsubst0
  44 arity/subst0 arity_subst0
  45 asucc/fwd asucc_gen_sort
  46 asucc/fwd asucc_gen_head
  47
  48 # check ######################################################################
  49
  50 clen/getl getl_ctail_clen
  51 clen/getl getl_gen_tail
  52 cnt/props cnt_lift
  53 C/props clt_cong
  54 C/props clt_head
  55 C/props clt_wf__q_ind
  56 C/props clt_wf_ind
  57 C/props chead_ctail
  58 C/props clt_thead
  59 C/props c_tail_ind
  60
  61 # waiting ####################################################################
  62
  63 csuba/arity csuba_arity
  64 csuba/arity csuba_arity_rev
  65 csuba/arity arity_appls_appl
  66 csuba/clear csuba_clear_conf
  67 csuba/clear csuba_clear_trans
  68 csuba/drop csuba_drop_abbr
  69 csuba/drop csuba_drop_abst
  70 csuba/drop csuba_drop_abst_rev
  71 csuba/drop csuba_drop_abbr_rev
  72 csuba/fwd csuba_gen_abbr
  73 csuba/fwd csuba_gen_void
  74 csuba/fwd csuba_gen_abst
  75 csuba/fwd csuba_gen_flat
  76 csuba/fwd csuba_gen_bind
  77 csuba/fwd csuba_gen_abst_rev
  78 csuba/fwd csuba_gen_void_rev
  79 csuba/fwd csuba_gen_abbr_rev
  80 csuba/fwd csuba_gen_flat_rev
  81 csuba/fwd csuba_gen_bind_rev
  82 csuba/getl csuba_getl_abbr
  83 csuba/getl csuba_getl_abst
  84 csuba/getl csuba_getl_abst_rev
  85 csuba/getl csuba_getl_abbr_rev
  86 csuba/props csuba_refl
  87 csubc/arity csubc_arity_conf
  88 csubc/arity csubc_arity_trans
  89 csubc/clear csubc_clear_conf
  90 csubc/csuba csubc_csuba
  91 csubc/drop1 drop1_csubc_trans
  92 csubc/drop1 csubc_drop1_conf_rev
  93 csubc/drop csubc_drop_conf_O
  94 csubc/drop drop_csubc_trans
  95 csubc/drop csubc_drop_conf_rev
  96 csubc/fwd csubc_gen_sort_l
  97 csubc/fwd csubc_gen_head_l
  98 csubc/fwd csubc_gen_sort_r
  99 csubc/fwd csubc_gen_head_r
 100 csubc/getl csubc_getl_conf
 101 csubc/props csubc_refl
 102 csubst0/clear csubst0_clear_O
 103 csubst0/clear csubst0_clear_O_back
 104 csubst0/clear csubst0_clear_S
 105 csubst0/clear csubst0_clear_trans
 106 csubst0/drop csubst0_drop_gt
 107 csubst0/drop csubst0_drop_gt_back
 108 csubst0/drop csubst0_drop_lt
 109 csubst0/drop csubst0_drop_eq
 110 csubst0/drop csubst0_drop_eq_back
 111 csubst0/drop csubst0_drop_lt_back
 112 csubst0/fwd csubst0_gen_sort
 113 csubst0/fwd csubst0_gen_head
 114 csubst0/fwd csubst0_gen_S_bind_2
 115 csubst0/getl csubst0_getl_ge
 116 csubst0/getl csubst0_getl_lt
 117 csubst0/getl csubst0_getl_ge_back
 118 csubst0/getl csubst0_getl_lt_back
 119 csubst0/props csubst0_snd_bind
 120 csubst0/props csubst0_fst_bind
 121 csubst0/props csubst0_both_bind
 122 csubst1/fwd csubst1_gen_head
 123 csubst1/getl csubst1_getl_ge
 124 csubst1/getl csubst1_getl_lt
 125 csubst1/getl csubst1_getl_ge_back
 126 csubst1/getl getl_csubst1
 127 csubst1/props csubst1_head
 128 csubst1/props csubst1_bind
 129 csubst1/props csubst1_flat
 130 csubt/clear csubt_clear_conf
 131 csubt/csuba csubt_csuba
 132 csubt/drop csubt_drop_flat
 133 csubt/drop csubt_drop_abbr
 134 csubt/drop csubt_drop_abst
 135 csubt/fwd csubt_gen_abbr
 136 csubt/fwd csubt_gen_abst
 137 csubt/fwd csubt_gen_flat
 138 csubt/fwd csubt_gen_bind
 139 csubt/getl csubt_getl_abbr
 140 csubt/getl csubt_getl_abst
 141 csubt/pc3 csubt_pr2
 142 csubt/pc3 csubt_pc3
 143 csubt/props csubt_refl
 144 csubt/ty3 csubt_ty3
 145 csubt/ty3 csubt_ty3_ld
 146 csubv/clear csubv_clear_conf
 147 csubv/clear csubv_clear_conf_void
 148 csubv/drop csubv_drop_conf
 149 csubv/getl csubv_getl_conf
 150 csubv/getl csubv_getl_conf_void
 151 csubv/props csubv_bind_same
 152 csubv/props csubv_refl
 153 drop1/fwd drop1_gen_pnil
 154 drop1/fwd drop1_gen_pcons
 155 drop1/getl drop1_getl_trans
 156 drop1/props drop1_skip_bind
 157 drop1/props drop1_cons_tail
 158 drop1/props drop1_trans
 159
 160 drop/props drop_ctail
 161
 162 ex0/props aplus_gz_le
 163 ex0/props aplus_gz_ge
 164 ex0/props next_plus_gz
 165 ex0/props leqz_leq
 166 ex0/props leq_leqz
 167 ex1/props ex1__leq_sort_SS
 168 ex1/props ex1_arity
 169 ex1/props ex1_ty3
 170 ex2/props ex2_nf2
 171 ex2/props ex2_arity
 172
 173 # check ######################################################################
 174
 175 flt/props flt_thead_sx
 176 flt/props flt_thead_dx
 177 flt/props flt_shift
 178 flt/props flt_arith0
 179 flt/props flt_arith1
 180 flt/props flt_arith2
 181 flt/props flt_trans
 182 flt/props flt_wf__q_ind
 183 flt/props flt_wf_ind
 184 fsubst0/fwd fsubst0_gen_base
 185 getl/clear clear_getl_trans
 186 getl/clear getl_clear_trans
 187 getl/clear getl_clear_bind
 188 getl/clear getl_clear_conf
 189 getl/dec getl_dec
 190 getl/drop getl_drop
 191 getl/drop getl_drop_conf_lt
 192 getl/drop getl_drop_conf_ge
 193 getl/drop getl_conf_ge_drop
 194 getl/drop getl_drop_conf_rev
 195 getl/drop drop_getl_trans_lt
 196 getl/drop drop_getl_trans_le
 197 getl/drop drop_getl_trans_ge
 198 getl/drop getl_drop_trans
 199 getl/flt getl_flt
 200 getl/fwd getl_gen_all
 201 getl/fwd getl_gen_sort
 202 getl/fwd getl_gen_O
 203 getl/fwd getl_gen_S
 204 getl/fwd getl_gen_2
 205 getl/fwd getl_gen_flat
 206 getl/fwd getl_gen_bind
 207 getl/getl getl_conf_le
 208 getl/getl getl_trans
 209 getl/props getl_refl
 210 getl/props getl_head
 211 getl/props getl_flat
 212 getl/props getl_ctail
 213 getl/props getl_mono
 214 iso/fwd iso_gen_sort
 215 iso/fwd iso_gen_lref
 216 iso/fwd iso_gen_head
 217 iso/fwd iso_flats_lref_bind_false
 218 iso/fwd iso_flats_flat_bind_false
 219 iso/props iso_refl
 220 iso/props iso_trans
 221 leq/asucc asucc_repl
 222 leq/asucc asucc_inj
 223 leq/asucc leq_asucc
 224 leq/asucc leq_ahead_asucc_false
 225 leq/asucc leq_asucc_false
 226 leq/fwd leq_gen_sort1
 227 leq/fwd leq_gen_head1
 228 leq/fwd leq_gen_sort2
 229 leq/fwd leq_gen_head2
 230 leq/props ahead_inj_snd
 231 leq/props leq_refl
 232 leq/props leq_eq
 233 leq/props leq_sym
 234 leq/props leq_trans
 235 leq/props leq_ahead_false_1
 236 leq/props leq_ahead_false_2
 237 lift1/fwd lift1_sort
 238 lift1/fwd lift1_lref
 239 lift1/fwd lift1_bind
 240 lift1/fwd lift1_flat
 241 lift1/fwd lift1_cons_tail
 242 lift1/fwd lifts1_flat
 243 lift1/fwd lifts1_nil
 244 lift1/fwd lifts1_cons
 245 lift1/props lift1_lift1
 246 lift1/props lift1_xhg
 247 lift1/props lifts1_xhg
 248 lift1/props lift1_free
 249 lift/fwd lift_sort
 250 lift/fwd lift_lref_lt
 251 lift/fwd lift_lref_ge
 252 lift/fwd lift_head
 253 lift/fwd lift_bind
 254 lift/fwd lift_flat
 255 lift/fwd lift_gen_sort
 256 lift/fwd lift_gen_lref
 257 lift/fwd lift_gen_lref_lt
 258 lift/fwd lift_gen_lref_false
 259 lift/fwd lift_gen_lref_ge
 260 lift/fwd lift_gen_head
 261 lift/fwd lift_gen_bind
 262 lift/fwd lift_gen_flat
 263 lift/props thead_x_lift_y_y
 264 lift/props lift_r
 265 lift/props lift_lref_gt
 266 lift/props lifts_tapp
 267 lift/props lift_inj
 268 lift/props lift_gen_lift
 269 lift/props lifts_inj
 270 lift/props lift_free
 271 lift/props lift_d
 272 lift/tlt lift_weight_map
 273 lift/tlt lift_weight
 274 lift/tlt lift_weight_add
 275 lift/tlt lift_weight_add_O
 276 lift/tlt lift_tlt_dx
 277 llt/props lweight_repl
 278 llt/props llt_repl
 279 llt/props llt_trans
 280 llt/props llt_head_sx
 281 llt/props llt_head_dx
 282 llt/props llt_wf__q_ind
 283 llt/props llt_wf_ind
 284 next_plus/props next_plus_assoc
 285 next_plus/props next_plus_next
 286 next_plus/props next_plus_lt
 287 nf2/arity arity_nf2_inv_all
 288 nf2/dec nf2_dec
 289 nf2/fwd nf2_gen_lref
 290 nf2/fwd nf2_gen_abst
 291 nf2/fwd nf2_gen_cast
 292 nf2/fwd nf2_gen_beta
 293 nf2/fwd nf2_gen_flat
 294 nf2/fwd nf2_gen__nf2_gen_aux
 295 nf2/fwd nf2_gen_abbr
 296 nf2/fwd nf2_gen_void
 297 nf2/iso nf2_iso_appls_lref
 298 nf2/lift1 nf2_lift1
 299 nf2/pr3 nf2_pr3_unfold
 300 nf2/pr3 nf2_pr3_confluence
 301 nf2/props nf2_sort
 302 nf2/props nf2_csort_lref
 303 nf2/props nf2_abst
 304 nf2/props nf2_abst_shift
 305 nf2/props nfs2_tapp
 306 nf2/props nf2_appls_lref
 307 nf2/props nf2_appl_lref
 308 nf2/props nf2_lref_abst
 309 nf2/props nf2_lift
 310 pc1/props pc1_pr0_r
 311 pc1/props pc1_pr0_x
 312 pc1/props pc1_refl
 313 pc1/props pc1_pr0_u
 314 pc1/props pc1_s
 315 pc1/props pc1_head_1
 316 pc1/props pc1_head_2
 317 pc1/props pc1_t
 318 pc1/props pc1_pr0_u2
 319 pc1/props pc1_head
 320 pc3/dec pc3_dec
 321 pc3/dec pc3_abst_dec
 322 pc3/fsubst0 pc3_pr2_fsubst0
 323 pc3/fsubst0 pc3_pr2_fsubst0_back
 324 pc3/fsubst0 pc3_fsubst0
 325 pc3/fwd pc3_gen_sort
 326 pc3/fwd pc3_gen_abst
 327 pc3/fwd pc3_gen_abst_shift
 328 pc3/fwd pc3_gen_lift
 329 pc3/fwd pc3_gen_not_abst
 330 pc3/fwd pc3_gen_lift_abst
 331 pc3/fwd pc3_gen_sort_abst
 332 pc3/left pc3_ind_left__pc3_left_pr3
 333 pc3/left pc3_ind_left__pc3_left_trans
 334 pc3/left pc3_ind_left__pc3_left_sym
 335 pc3/left pc3_ind_left__pc3_left_pc3
 336 pc3/left pc3_ind_left__pc3_pc3_left
 337 pc3/left pc3_ind_left
 338 pc3/nf2 pc3_nf2
 339 pc3/nf2 pc3_nf2_unfold
 340 pc3/pc1 pc3_pc1
 341 pc3/props clear_pc3_trans
 342 pc3/props pc3_pr2_r
 343 pc3/props pc3_pr2_x
 344 pc3/props pc3_pr3_r
 345 pc3/props pc3_pr3_x
 346 pc3/props pc3_pr3_t
 347 pc3/props pc3_refl
 348 pc3/props pc3_s
 349 pc3/props pc3_thin_dx
 350 pc3/props pc3_head_1
 351 pc3/props pc3_head_2
 352 pc3/props pc3_pr2_u
 353 pc3/props pc3_t
 354 pc3/props pc3_pr2_u2
 355 pc3/props pc3_pr3_conf
 356 pc3/props pc3_head_12
 357 pc3/props pc3_head_21
 358 pc3/props pc3_pr0_pr2_t
 359 pc3/props pc3_pr2_pr2_t
 360 pc3/props pc3_pr2_pr3_t
 361 pc3/props pc3_pr3_pc3_t
 362 pc3/props pc3_lift
 363 pc3/props pc3_eta
 364 pc3/subst1 pc3_gen_cabbr
 365 pc3/wcpr0 pc3_wcpr0__pc3_wcpr0_t_aux
 366 pc3/wcpr0 pc3_wcpr0_t
 367 pc3/wcpr0 pc3_wcpr0
 368 pr0/dec nf0_dec
 369 pr0/fwd pr0_gen_sort
 370 pr0/fwd pr0_gen_lref
 371 pr0/fwd pr0_gen_abst
 372 pr0/fwd pr0_gen_appl
 373 pr0/fwd pr0_gen_cast
 374 pr0/fwd pr0_gen_abbr
 375 pr0/fwd pr0_gen_void
 376 pr0/fwd pr0_gen_lift
 377 pr0/pr0 pr0_confluence__pr0_cong_upsilon_refl
 378 pr0/pr0 pr0_confluence__pr0_cong_upsilon_cong
 379 pr0/pr0 pr0_confluence__pr0_cong_upsilon_delta
 380 pr0/pr0 pr0_confluence__pr0_cong_upsilon_zeta
 381 pr0/pr0 pr0_confluence__pr0_cong_delta
 382 pr0/pr0 pr0_confluence__pr0_upsilon_upsilon
 383 pr0/pr0 pr0_confluence__pr0_delta_delta
 384 pr0/pr0 pr0_confluence__pr0_delta_tau
 385 pr0/pr0 pr0_confluence
 386 pr0/props pr0_lift
 387 pr0/props pr0_subst0_back
 388 pr0/props pr0_subst0_fwd
 389 pr0/props pr0_subst0
 390 pr0/subst1 pr0_delta1
 391 pr0/subst1 pr0_subst1_back
 392 pr0/subst1 pr0_subst1_fwd
 393 pr0/subst1 pr0_subst1
 394 pr1/pr1 pr1_strip
 395 pr1/pr1 pr1_confluence
 396 pr1/props pr1_pr0
 397 pr1/props pr1_t
 398 pr1/props pr1_head_1
 399 pr1/props pr1_head_2
 400 pr1/props pr1_comp
 401 pr1/props pr1_eta
 402 pr2/clen pr2_gen_ctail
 403 pr2/clen pr2_gen_cbind
 404 pr2/clen pr2_gen_cflat
 405 pr2/fwd pr2_gen_sort
 406 pr2/fwd pr2_gen_lref
 407 pr2/fwd pr2_gen_abst
 408 pr2/fwd pr2_gen_cast
 409 pr2/fwd pr2_gen_csort
 410 pr2/fwd pr2_gen_appl
 411 pr2/fwd pr2_gen_abbr
 412 pr2/fwd pr2_gen_void
 413 pr2/fwd pr2_gen_lift
 414 pr2/pr2 pr2_confluence__pr2_free_free
 415 pr2/pr2 pr2_confluence__pr2_free_delta
 416 pr2/pr2 pr2_confluence__pr2_delta_delta
 417 pr2/pr2 pr2_confluence
 418 pr2/props pr2_thin_dx
 419 pr2/props pr2_head_1
 420 pr2/props pr2_head_2
 421 pr2/props clear_pr2_trans
 422 pr2/props pr2_cflat
 423 pr2/props pr2_ctail
 424 pr2/props pr2_change
 425 pr2/props pr2_lift
 426 pr2/subst1 pr2_delta1
 427 pr2/subst1 pr2_subst1
 428 pr2/subst1 pr2_gen_cabbr
 429 pr3/fwd pr3_gen_sort
 430 pr3/fwd pr3_gen_abst
 431 pr3/fwd pr3_gen_cast
 432 pr3/fwd pr3_gen_lift
 433 pr3/fwd pr3_gen_lref
 434 pr3/fwd pr3_gen_void
 435 pr3/fwd pr3_gen_abbr
 436 pr3/fwd pr3_gen_appl
 437 pr3/fwd pr3_gen_bind
 438 pr3/iso pr3_iso_appls_abbr
 439 pr3/iso pr3_iso_appls_cast
 440 pr3/iso pr3_iso_appl_bind
 441 pr3/iso pr3_iso_appls_appl_bind
 442 pr3/iso pr3_iso_appls_bind
 443 pr3/iso pr3_iso_beta
 444 pr3/iso pr3_iso_appls_beta
 445 pr3/pr1 pr3_pr1
 446 pr3/pr3 pr3_strip
 447 pr3/pr3 pr3_confluence
 448 pr3/props clear_pr3_trans
 449 pr3/props pr3_pr2
 450 pr3/props pr3_t
 451 pr3/props pr3_thin_dx
 452 pr3/props pr3_head_1
 453 pr3/props pr3_head_2
 454 pr3/props pr3_head_21
 455 pr3/props pr3_head_12
 456 pr3/props pr3_cflat
 457 pr3/props pr3_flat
 458 pr3/props pr3_pr0_pr2_t
 459 pr3/props pr3_pr2_pr2_t
 460 pr3/props pr3_pr2_pr3_t
 461 pr3/props pr3_pr3_pr3_t
 462 pr3/props pr3_lift
 463 pr3/props pr3_eta
 464 pr3/subst1 pr3_subst1
 465 pr3/subst1 pr3_gen_cabbr
 466 pr3/wcpr0 pr3_wcpr0_t
 467 sc3/arity sc3_arity_csubc
 468 sc3/arity sc3_arity
 469 sc3/props sc3_arity_gen
 470 sc3/props sc3_repl
 471 sc3/props sc3_lift
 472 sc3/props sc3_lift1
 473 sc3/props sc3_abbr
 474 sc3/props sc3_cast
 475 sc3/props sc3_props__sc3_sn3_abst
 476 sc3/props sc3_sn3
 477 sc3/props sc3_abst
 478 sc3/props sc3_bind
 479 sc3/props sc3_appl
 480 sn3/fwd sn3_gen_bind
 481 sn3/fwd sn3_gen_flat
 482 sn3/fwd sn3_gen_head
 483 sn3/fwd sn3_gen_cflat
 484 sn3/fwd sn3_gen_lift
 485 sn3/lift1 sns3_lifts1
 486 sn3/nf2 sn3_nf2
 487 sn3/nf2 nf2_sn3
 488 sn3/props sn3_pr3_trans
 489 sn3/props sn3_pr2_intro
 490 sn3/props sn3_cast
 491 sn3/props sn3_cflat
 492 sn3/props sn3_shift
 493 sn3/props sn3_change
 494 sn3/props sn3_gen_def
 495 sn3/props sn3_cdelta
 496 sn3/props sn3_cpr3_trans
 497 sn3/props sn3_bind
 498 sn3/props sn3_beta
 499 sn3/props sn3_appl_lref
 500 sn3/props sn3_appl_abbr
 501 sn3/props sn3_appl_cast
 502 sn3/props sn3_appl_bind
 503 sn3/props sn3_appl_appl
 504 sn3/props sn3_appl_beta
 505 sn3/props sn3_appl_appls
 506 sn3/props sn3_appls_lref
 507 sn3/props sn3_appls_cast
 508 sn3/props sn3_appls_bind
 509 sn3/props sn3_appls_beta
 510 sn3/props sn3_lift
 511 sn3/props sn3_abbr
 512 sn3/props sn3_appls_abbr
 513 sn3/props sns3_lifts
 514 sty0/fwd sty0_gen_sort
 515 sty0/fwd sty0_gen_lref
 516 sty0/fwd sty0_gen_bind
 517 sty0/fwd sty0_gen_appl
 518 sty0/fwd sty0_gen_cast
 519 sty0/props sty0_lift
 520 sty0/props sty0_correct
 521 sty1/cnt sty1_cnt
 522 sty1/props sty1_trans
 523 sty1/props sty1_bind
 524 sty1/props sty1_appl
 525 sty1/props sty1_lift
 526 sty1/props sty1_correct
 527 sty1/props sty1_abbr
 528 sty1/props sty1_cast2
 529 subst0/dec dnf_dec2
 530 subst0/dec dnf_dec
 531 subst0/fwd subst0_gen_sort
 532 subst0/fwd subst0_gen_lref
 533 subst0/fwd subst0_gen_head
 534 subst0/fwd subst0_gen_lift_lt
 535 subst0/fwd subst0_gen_lift_false
 536 subst0/fwd subst0_gen_lift_ge
 537 subst0/props subst0_refl
 538 subst0/props subst0_lift_lt
 539 subst0/props subst0_lift_ge
 540 subst0/props subst0_lift_ge_S
 541 subst0/props subst0_lift_ge_s
 542 subst0/subst0 subst0_subst0
 543 subst0/subst0 subst0_subst0_back
 544 subst0/subst0 subst0_trans
 545 subst0/subst0 subst0_confluence_neq
 546 subst0/subst0 subst0_confluence_eq
 547 subst0/subst0 subst0_confluence_lift
 548 subst0/tlt subst0_weight_le
 549 subst0/tlt subst0_weight_lt
 550 subst0/tlt subst0_tlt_head
 551 subst0/tlt subst0_tlt
 552 subst1/fwd subst1_gen_sort
 553 subst1/fwd subst1_gen_lref
 554 subst1/fwd subst1_gen_head
 555 subst1/fwd subst1_gen_lift_lt
 556 subst1/fwd subst1_gen_lift_eq
 557 subst1/fwd subst1_gen_lift_ge
 558 subst1/props subst1_head
 559 subst1/props subst1_lift_lt
 560 subst1/props subst1_lift_ge
 561 subst1/props subst1_ex
 562 subst1/props subst1_lift_S
 563 subst1/subst1 subst1_subst1
 564 subst1/subst1 subst1_subst1_back
 565 subst1/subst1 subst1_trans
 566 subst1/subst1 subst1_confluence_neq
 567 subst1/subst1 subst1_confluence_eq
 568 subst1/subst1 subst1_confluence_lift
 569 subst/fwd subst_sort
 570 subst/fwd subst_lref_lt
 571 subst/fwd subst_lref_eq
 572 subst/fwd subst_lref_gt
 573 subst/fwd subst_head
 574 subst/props subst_lift_SO
 575 subst/props subst_subst0
 576 T/dec terms_props__bind_dec
 577 T/dec bind_dec_not
 578 T/dec terms_props__flat_dec
 579 T/dec terms_props__kind_dec
 580 T/dec term_dec
 581 T/dec binder_dec
 582 T/dec abst_dec
 583 tlist/props tslt_wf__q_ind
 584 tlist/props tslt_wf_ind
 585 tlist/props theads_tapp
 586 tlist/props tcons_tapp_ex
 587 tlist/props tlist_ind_rev
 588 tlt/props wadd_le
 589 tlt/props wadd_lt
 590 tlt/props wadd_O
 591 tlt/props weight_le
 592 tlt/props weight_eq
 593 tlt/props weight_add_O
 594 tlt/props weight_add_S
 595 tlt/props tlt_trans
 596 tlt/props tlt_head_sx
 597 tlt/props tlt_head_dx
 598 tlt/props tlt_wf__q_ind
 599 tlt/props tlt_wf_ind
 600 T/props not_abbr_abst
 601 T/props not_void_abst
 602 T/props not_abbr_void
 603 T/props not_abst_void
 604 T/props thead_x_y_y
 605 T/props tweight_lt
 606 ty3/arity ty3_arity
 607 ty3/arity_props ty3_predicative
 608 ty3/arity_props ty3_repellent
 609 ty3/arity_props ty3_acyclic
 610 ty3/arity_props ty3_sn3
 611 ty3/dec ty3_inference
 612 ty3/fsubst0 ty3_fsubst0
 613 ty3/fsubst0 ty3_csubst0
 614 ty3/fsubst0 ty3_subst0
 615 ty3/fwd ty3_gen_sort
 616 ty3/fwd ty3_gen_lref
 617 ty3/fwd ty3_gen_bind
 618 ty3/fwd ty3_gen_appl
 619 ty3/fwd ty3_gen_cast
 620 ty3/fwd tys3_gen_nil
 621 ty3/fwd tys3_gen_cons
 622 ty3/fwd_nf2 ty3_gen_appl_nf2
 623 ty3/fwd_nf2 ty3_inv_lref_nf2_pc3
 624 ty3/fwd_nf2 ty3_inv_lref_nf2
 625 ty3/fwd_nf2 ty3_inv_appls_lref_nf2
 626 ty3/fwd_nf2 ty3_inv_lref_lref_nf2
 627 ty3/nf2 ty3_nf2_inv_abst_premise_csort
 628 ty3/nf2 ty3_nf2_inv_all
 629 ty3/nf2 ty3_nf2_inv_sort
 630 ty3/nf2 ty3_nf2_gen__ty3_nf2_inv_abst_aux
 631 ty3/nf2 ty3_nf2_inv_abst
 632 ty3/pr3 ty3_sred_wcpr0_pr0
 633 ty3/pr3 ty3_sred_pr0
 634 ty3/pr3 ty3_sred_pr1
 635 ty3/pr3 ty3_sred_pr2
 636 ty3/pr3 ty3_sred_pr3
 637 ty3/pr3_props ty3_cred_pr2
 638 ty3/pr3_props ty3_cred_pr3
 639 ty3/pr3_props ty3_gen_lift
 640 ty3/pr3_props ty3_tred
 641 ty3/pr3_props ty3_sconv_pc3
 642 ty3/pr3_props ty3_sred_back
 643 ty3/pr3_props ty3_sconv
 644 ty3/props ty3_lift
 645 ty3/props ty3_correct
 646 ty3/props ty3_unique
 647 ty3/props ty3_gen_abst_abst
 648 ty3/props ty3_typecheck
 649 ty3/props ty3_getl_subst0
 650 ty3/sty0 ty3_sty0
 651 ty3/subst1 ty3_gen_cabbr
 652 ty3/subst1 ty3_gen_cvoid
 653 wcpr0/fwd wcpr0_gen_sort
 654 wcpr0/fwd wcpr0_gen_head
 655 wcpr0/getl wcpr0_drop
 656 wcpr0/getl wcpr0_drop_back
 657 wcpr0/getl wcpr0_getl
 658 wcpr0/getl wcpr0_getl_back
 659 wf3/clear wf3_clear_conf
 660 wf3/clear clear_wf3_trans
 661 wf3/fwd wf3_gen_sort1
 662 wf3/fwd wf3_gen_bind1
 663 wf3/fwd wf3_gen_flat1
 664 wf3/fwd wf3_gen_head2
 665 wf3/getl wf3_getl_conf
 666 wf3/getl getl_wf3_trans
 667 wf3/props wf3_mono
 668 wf3/props wf3_total
 669 wf3/props ty3_shift1
 670 wf3/props wf3_idem
 671 wf3/props wf3_ty3
 672 wf3/ty3 wf3_pr2_conf
 673 wf3/ty3 wf3_pr3_conf
 674 wf3/ty3 wf3_pc3_conf
 675 wf3/ty3 wf3_ty3_conf