matita/matita/contribs/lambdadelta/basic_2/basic_1.orig

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