-aplus/props / aplus_ahead_simpl
-aplus/props / aplus_asort_le_simpl
-aplus/props / aplus_asort_O_simpl
-aplus/props / aplus_asort_simpl
-aplus/props / aplus_assoc
-aplus/props / aplus_asucc
-aplus/props / aplus_asucc_false
-aplus/props / aplus_inj
-aplus/props / aplus_reg_r
-aplus/props / aplus_sort_O_S_simpl
-aplus/props / aplus_sort_S_S_simpl
-aprem/fwd / aprem_gen_head_O
-aprem/fwd / aprem_gen_head_S
-aprem/fwd / aprem_gen_sort
-aprem/props / aprem_asucc
-aprem/props / aprem_repl
-arity/aprem / arity_aprem
-arity/cimp / arity_cimp_conf
-arity/fwd / arity_gen_abst
-arity/fwd / arity_gen_appl
-arity/fwd / arity_gen_appls
-arity/fwd / arity_gen_bind
-arity/fwd / arity_gen_cast
-arity/fwd / arity_gen_lift
-arity/fwd / arity_gen_lref
-arity/fwd / arity_gen_sort
-arity/lift1 / arity_lift1
-arity/pr3 / arity_sred_pr2
-arity/pr3 / arity_sred_pr3
-arity/pr3 / arity_sred_wcpr0_pr0
-arity/pr3 / arity_sred_wcpr0_pr1
-arity/props / arity_appls_abbr
-arity/props / arity_appls_bind
-arity/props / arity_appls_cast
-arity/props / arity_lift
-arity/props / arity_mono
-arity/props / arity_repellent
-arity/props / node_inh
-arity/subst0 / arity_fsubst0
-arity/subst0 / arity_gen_cvoid
-arity/subst0 / arity_gen_cvoid_subst0
-arity/subst0 / arity_subst0
-asucc/fwd / asucc_gen_head
-asucc/fwd / asucc_gen_sort
-cimp/props / cimp_bind
-cimp/props / cimp_flat_dx
-cimp/props / cimp_flat_sx
-cimp/props / cimp_getl_conf
-clear/drop / drop_clear
-clear/drop / drop_clear_O
-clear/drop / drop_clear_S
-clear/fwd / clear_gen_all
-clear/fwd / clear_gen_bind
-clear/fwd / clear_gen_flat
-clear/fwd / clear_gen_flat_r
-clear/fwd / clear_gen_sort
-clear/props / clear_cle
-clear/props / clear_clear
-clear/props / clear_ctail
-clear/props / clear_mono
-clear/props / clear_trans
-clen/getl / getl_ctail_clen
-clen/getl / getl_gen_tail
-cnt/props / cnt_lift
-C/props / chead_ctail
-C/props / clt_cong
-C/props / clt_head
-C/props / clt_thead
-C/props / clt_wf_ind
-C/props clt_wf q_ind
-C/props / c_tail_ind
-csuba/arity / arity_appls_appl
-csuba/arity / csuba_arity
-csuba/arity / csuba_arity_rev
-csuba/clear / csuba_clear_conf
-csuba/clear / csuba_clear_trans
-csuba/drop / csuba_drop_abbr
-csuba/drop / csuba_drop_abbr_rev
-csuba/drop / csuba_drop_abst
-csuba/drop / csuba_drop_abst_rev
-csuba/fwd / csuba_gen_abbr
-csuba/fwd / csuba_gen_abbr_rev
-csuba/fwd / csuba_gen_abst
-csuba/fwd / csuba_gen_abst_rev
-csuba/fwd / csuba_gen_bind
-csuba/fwd / csuba_gen_bind_rev
-csuba/fwd / csuba_gen_flat
-csuba/fwd / csuba_gen_flat_rev
-csuba/fwd / csuba_gen_void
-csuba/fwd / csuba_gen_void_rev
-csuba/getl / csuba_getl_abbr
-csuba/getl / csuba_getl_abbr_rev
-csuba/getl / csuba_getl_abst
-csuba/getl / csuba_getl_abst_rev
-csuba/props / csuba_refl
-csubc/arity / csubc_arity_conf
-csubc/arity / csubc_arity_trans
-csubc/clear / csubc_clear_conf
-csubc/csuba / csubc_csuba
-csubc/drop1 / csubc_drop1_conf_rev
-csubc/drop1 / drop1_csubc_trans
-csubc/drop / csubc_drop_conf_O
-csubc/drop / csubc_drop_conf_rev
-csubc/drop / drop_csubc_trans
-csubc/fwd / csubc_gen_head_l
-csubc/fwd / csubc_gen_head_r
-csubc/fwd / csubc_gen_sort_l
-csubc/fwd / csubc_gen_sort_r
-csubc/getl / csubc_getl_conf
-csubc/props / csubc_refl
-csubst0/clear / csubst0_clear_O
-csubst0/clear / csubst0_clear_O_back
-csubst0/clear / csubst0_clear_S
-csubst0/clear / csubst0_clear_trans
-csubst0/drop / csubst0_drop_eq
-csubst0/drop / csubst0_drop_eq_back
-csubst0/drop / csubst0_drop_gt
-csubst0/drop / csubst0_drop_gt_back
-csubst0/drop / csubst0_drop_lt
-csubst0/drop / csubst0_drop_lt_back
-csubst0/fwd / csubst0_gen_head
-csubst0/fwd / csubst0_gen_S_bind_2
-csubst0/fwd / csubst0_gen_sort
-csubst0/getl / csubst0_getl_ge
-csubst0/getl / csubst0_getl_ge_back
-csubst0/getl / csubst0_getl_lt
-csubst0/getl / csubst0_getl_lt_back
-csubst0/props / csubst0_both_bind
-csubst0/props / csubst0_fst_bind
-csubst0/props / csubst0_snd_bind
-csubst1/fwd / csubst1_gen_head
-csubst1/getl / csubst1_getl_ge
-csubst1/getl / csubst1_getl_ge_back
-csubst1/getl / csubst1_getl_lt
-csubst1/getl / getl_csubst1
-csubst1/props / csubst1_bind
-csubst1/props / csubst1_flat
-csubst1/props / csubst1_head
-csubt/clear / csubt_clear_conf
-csubt/csuba / csubt_csuba
-csubt/drop / csubt_drop_abbr
-csubt/drop / csubt_drop_abst
-csubt/drop / csubt_drop_flat
-csubt/fwd / csubt_gen_abbr
-csubt/fwd / csubt_gen_abst
-csubt/fwd / csubt_gen_bind
-csubt/fwd / csubt_gen_flat
-csubt/getl / csubt_getl_abbr
-csubt/getl / csubt_getl_abst
-csubt/pc3 / csubt_pc3
-csubt/pc3 / csubt_pr2
-csubt/props / csubt_refl
-csubt/ty3 / csubt_ty3
-csubt/ty3 / csubt_ty3_ld
-csubv/clear / csubv_clear_conf
-csubv/clear / csubv_clear_conf_void
-csubv/drop / csubv_drop_conf
-csubv/getl / csubv_getl_conf
-csubv/getl / csubv_getl_conf_void
-csubv/props / csubv_bind_same
-csubv/props / csubv_refl
-drop1/fwd / drop1_gen_pcons
-drop1/fwd / drop1_gen_pnil
-drop1/getl / drop1_getl_trans
-drop1/props / drop1_cons_tail
-drop1/props / drop1_skip_bind
-drop1/props / drop1_trans
-drop/fwd / drop_gen_drop
-drop/fwd / drop_gen_refl
-drop/fwd / drop_gen_skip_l
-drop/fwd / drop_gen_skip_r
-drop/fwd / drop_gen_sort
-drop/props / drop_conf_ge
-drop/props / drop_conf_lt
-drop/props / drop_conf_rev
-drop/props / drop_ctail
-drop/props / drop_mono
-drop/props / drop_S
-drop/props / drop_skip_bind
-drop/props / drop_skip_flat
-drop/props / drop_trans_ge
-drop/props / drop_trans_le
-ex0/props / aplus_gz_ge
-ex0/props / aplus_gz_le
-ex0/props / leq_leqz
-ex0/props / leqz_leq
-ex0/props / next_plus_gz
-ex1/props / ex1_arity
-ex1/props ex1 leq_sort_SS
-ex1/props / ex1_ty3
-ex2/props / ex2_arity
-ex2/props / ex2_nf2
-flt/props / flt_arith0
-flt/props / flt_arith1
-flt/props / flt_arith2
-flt/props / flt_shift
-flt/props / flt_thead_dx
-flt/props / flt_thead_sx
-flt/props / flt_trans
-flt/props / flt_wf_ind
-flt/props flt_wf q_ind
-fsubst0/fwd / fsubst0_gen_base
-getl/clear / clear_getl_trans
-getl/clear / getl_clear_bind
-getl/clear / getl_clear_conf
-getl/clear / getl_clear_trans
-getl/dec / getl_dec
-getl/drop / drop_getl_trans_ge
-getl/drop / drop_getl_trans_le
-getl/drop / drop_getl_trans_lt
-getl/drop / getl_conf_ge_drop
-getl/drop / getl_drop
-getl/drop / getl_drop_conf_ge
-getl/drop / getl_drop_conf_lt
-getl/drop / getl_drop_conf_rev
-getl/drop / getl_drop_trans
-getl/flt / getl_flt
-getl/fwd / getl_gen_2
-getl/fwd / getl_gen_all
-getl/fwd / getl_gen_bind
-getl/fwd / getl_gen_flat
-getl/fwd / getl_gen_O
-getl/fwd / getl_gen_S
-getl/fwd / getl_gen_sort
-getl/getl / getl_conf_le
-getl/getl / getl_trans
-getl/props / getl_ctail
-getl/props / getl_flat
-getl/props / getl_head
-getl/props / getl_mono
-getl/props / getl_refl
-iso/fwd / iso_flats_flat_bind_false
-iso/fwd / iso_flats_lref_bind_false
-iso/fwd / iso_gen_head
-iso/fwd / iso_gen_lref
-iso/fwd / iso_gen_sort
-iso/props / iso_refl
-iso/props / iso_trans
-leq/asucc / asucc_inj
-leq/asucc / asucc_repl
-leq/asucc / leq_ahead_asucc_false
-leq/asucc / leq_asucc
-leq/asucc / leq_asucc_false
-leq/fwd / leq_gen_head1
-leq/fwd / leq_gen_head2
-leq/fwd / leq_gen_sort1
-leq/fwd / leq_gen_sort2
-leq/props / ahead_inj_snd
-leq/props / leq_ahead_false_1
-leq/props / leq_ahead_false_2
-leq/props / leq_eq
-leq/props / leq_refl
-leq/props / leq_sym
-leq/props / leq_trans
-lift1/fwd / lift1_bind
-lift1/fwd / lift1_cons_tail
-lift1/fwd / lift1_flat
-lift1/fwd / lift1_lref
-lift1/fwd / lift1_sort
-lift1/fwd / lifts1_cons
-lift1/fwd / lifts1_flat
-lift1/fwd / lifts1_nil
-lift1/props / lift1_free
-lift1/props / lift1_lift1
-lift1/props / lift1_xhg
-lift1/props / lifts1_xhg
-lift/fwd / lift_bind
-lift/fwd / lift_flat
-lift/fwd / lift_gen_bind
-lift/fwd / lift_gen_flat
-lift/fwd / lift_gen_head
-lift/fwd / lift_gen_lref
-lift/fwd / lift_gen_lref_false
-lift/fwd / lift_gen_lref_ge
-lift/fwd / lift_gen_lref_lt
-lift/fwd / lift_gen_sort
-lift/fwd / lift_head
-lift/fwd / lift_lref_ge
-lift/fwd / lift_lref_lt
-lift/fwd / lift_sort
-lift/props / lift_d
-lift/props / lift_free
-lift/props / lift_gen_lift
-lift/props / lift_inj
-lift/props / lift_lref_gt
-lift/props / lift_r
-lift/props / lifts_inj
-lift/props / lifts_tapp
-lift/props / thead_x_lift_y_y
-lift/tlt / lift_tlt_dx
-lift/tlt / lift_weight
-lift/tlt / lift_weight_add
-lift/tlt / lift_weight_add_O
-lift/tlt / lift_weight_map
-llt/props / llt_head_dx
-llt/props / llt_head_sx
-llt/props / llt_repl
-llt/props / llt_trans
-llt/props / llt_wf_ind
-llt/props llt_wf q_ind
-llt/props / lweight_repl
-next_plus/props / next_plus_assoc
-next_plus/props / next_plus_lt
-next_plus/props / next_plus_next
-nf2/arity / arity_nf2_inv_all
-nf2/dec / nf2_dec
-nf2/fwd / nf2_gen_abbr
-nf2/fwd / nf2_gen_abst
-nf2/fwd / nf2_gen_beta
-nf2/fwd / nf2_gen_cast
-nf2/fwd / nf2_gen_flat
-nf2/fwd / nf2_gen_lref
-nf2/fwd nf2_gen nf2_gen_aux
-nf2/fwd / nf2_gen_void
-nf2/iso / nf2_iso_appls_lref
-nf2/lift1 / nf2_lift1
-nf2/pr3 / nf2_pr3_confluence
-nf2/pr3 / nf2_pr3_unfold
-nf2/props / nf2_abst
-nf2/props / nf2_abst_shift
-nf2/props / nf2_appl_lref
-nf2/props / nf2_appls_lref
-nf2/props / nf2_csort_lref
-nf2/props / nf2_lift
-nf2/props / nf2_lref_abst
-nf2/props / nf2_sort
-nf2/props / nfs2_tapp
-pc1/props / pc1_head
-pc1/props / pc1_head_1
-pc1/props / pc1_head_2
-pc1/props / pc1_pr0_r
-pc1/props / pc1_pr0_u
-pc1/props / pc1_pr0_u2
-pc1/props / pc1_pr0_x
-pc1/props / pc1_refl
-pc1/props / pc1_s
-pc1/props / pc1_t
-pc3/dec / pc3_abst_dec
-pc3/dec / pc3_dec
-pc3/fsubst0 / pc3_fsubst0
-pc3/fsubst0 / pc3_pr2_fsubst0
-pc3/fsubst0 / pc3_pr2_fsubst0_back
-pc3/fwd / pc3_gen_abst
-pc3/fwd / pc3_gen_abst_shift
-pc3/fwd / pc3_gen_lift
-pc3/fwd / pc3_gen_lift_abst
-pc3/fwd / pc3_gen_not_abst
-pc3/fwd / pc3_gen_sort
-pc3/fwd / pc3_gen_sort_abst
-pc3/left / pc3_ind_left
-pc3/left pc3_ind_left pc3_left_pc3
-pc3/left pc3_ind_left pc3_left_pr3
-pc3/left pc3_ind_left pc3_left_sym
-pc3/left pc3_ind_left pc3_left_trans
-pc3/left pc3_ind_left pc3_pc3_left
-pc3/nf2 / pc3_nf2
-pc3/nf2 / pc3_nf2_unfold
-pc3/pc1 / pc3_pc1
-pc3/props / clear_pc3_trans
-pc3/props / pc3_eta
-pc3/props / pc3_head_1
-pc3/props / pc3_head_12
-pc3/props / pc3_head_2
-pc3/props / pc3_head_21
-pc3/props / pc3_lift
-pc3/props / pc3_pr0_pr2_t
-pc3/props / pc3_pr2_pr2_t
-pc3/props / pc3_pr2_pr3_t
-pc3/props / pc3_pr2_r
-pc3/props / pc3_pr2_u
-pc3/props / pc3_pr2_u2
-pc3/props / pc3_pr2_x
-pc3/props / pc3_pr3_conf
-pc3/props / pc3_pr3_pc3_t
-pc3/props / pc3_pr3_r
-pc3/props / pc3_pr3_t
-pc3/props / pc3_pr3_x
-pc3/props / pc3_refl
-pc3/props / pc3_s
-pc3/props / pc3_t
-pc3/props / pc3_thin_dx
-pc3/subst1 / pc3_gen_cabbr
-pc3/wcpr0 / pc3_wcpr0
-pc3/wcpr0 pc3_wcpr0 pc3_wcpr0_t_aux
-pc3/wcpr0 / pc3_wcpr0_t
-pr0/dec / nf0_dec
-pr0/fwd / pr0_gen_abbr
-pr0/fwd / pr0_gen_abst
-pr0/fwd / pr0_gen_appl
-pr0/fwd / pr0_gen_cast
-pr0/fwd / pr0_gen_lift
-pr0/fwd / pr0_gen_lref
-pr0/fwd / pr0_gen_sort
-pr0/fwd / pr0_gen_void
-pr0/pr0 / pr0_confluence
-pr0/pr0 pr0_confluence pr0_cong_delta
-pr0/pr0 pr0_confluence pr0_cong_upsilon_cong
-pr0/pr0 pr0_confluence pr0_cong_upsilon_delta
-pr0/pr0 pr0_confluence pr0_cong_upsilon_refl
-pr0/pr0 pr0_confluence pr0_cong_upsilon_zeta
-pr0/pr0 pr0_confluence pr0_delta_delta
-pr0/pr0 pr0_confluence pr0_delta_tau
-pr0/pr0 pr0_confluence pr0_upsilon_upsilon
-pr0/props / pr0_lift
-pr0/props / pr0_subst0
-pr0/props / pr0_subst0_back
-pr0/props / pr0_subst0_fwd
-pr0/subst1 / pr0_delta1
-pr0/subst1 / pr0_subst1
-pr0/subst1 / pr0_subst1_back
-pr0/subst1 / pr0_subst1_fwd
-pr1/pr1 / pr1_confluence
-pr1/pr1 / pr1_strip
-pr1/props / pr1_comp
-pr1/props / pr1_eta
-pr1/props / pr1_head_1
-pr1/props / pr1_head_2
-pr1/props / pr1_pr0
-pr1/props / pr1_t
-pr2/clen / pr2_gen_cbind
-pr2/clen / pr2_gen_cflat
-pr2/clen / pr2_gen_ctail
-pr2/fwd / pr2_gen_abbr
-pr2/fwd / pr2_gen_abst
-pr2/fwd / pr2_gen_appl
-pr2/fwd / pr2_gen_cast
-pr2/fwd / pr2_gen_csort
-pr2/fwd / pr2_gen_lift
-pr2/fwd / pr2_gen_lref
-pr2/fwd / pr2_gen_sort
-pr2/fwd / pr2_gen_void
-pr2/pr2 / pr2_confluence
-pr2/pr2 pr2_confluence pr2_delta_delta
-pr2/pr2 pr2_confluence pr2_free_delta
-pr2/pr2 pr2_confluence pr2_free_free
-pr2/props / clear_pr2_trans
-pr2/props / pr2_cflat
-pr2/props / pr2_change
-pr2/props / pr2_ctail
-pr2/props / pr2_head_1
-pr2/props / pr2_head_2
-pr2/props / pr2_lift
-pr2/props / pr2_thin_dx
-pr2/subst1 / pr2_delta1
-pr2/subst1 / pr2_gen_cabbr
-pr2/subst1 / pr2_subst1
-pr3/fwd / pr3_gen_abbr
-pr3/fwd / pr3_gen_abst
-pr3/fwd / pr3_gen_appl
-pr3/fwd / pr3_gen_bind
-pr3/fwd / pr3_gen_cast
-pr3/fwd / pr3_gen_lift
-pr3/fwd / pr3_gen_lref
-pr3/fwd / pr3_gen_sort
-pr3/fwd / pr3_gen_void
-pr3/iso / pr3_iso_appl_bind
-pr3/iso / pr3_iso_appls_abbr
-pr3/iso / pr3_iso_appls_appl_bind
-pr3/iso / pr3_iso_appls_beta
-pr3/iso / pr3_iso_appls_bind
-pr3/iso / pr3_iso_appls_cast
-pr3/iso / pr3_iso_beta
-pr3/pr1 / pr3_pr1
-pr3/pr3 / pr3_confluence
-pr3/pr3 / pr3_strip
-pr3/props / clear_pr3_trans
-pr3/props / pr3_cflat
-pr3/props / pr3_eta
-pr3/props / pr3_flat
-pr3/props / pr3_head_1
-pr3/props / pr3_head_12
-pr3/props / pr3_head_2
-pr3/props / pr3_head_21
-pr3/props / pr3_lift
-pr3/props / pr3_pr0_pr2_t
-pr3/props / pr3_pr2
-pr3/props / pr3_pr2_pr2_t
-pr3/props / pr3_pr2_pr3_t
-pr3/props / pr3_pr3_pr3_t
-pr3/props / pr3_t
-pr3/props / pr3_thin_dx
-pr3/subst1 / pr3_gen_cabbr
-pr3/subst1 / pr3_subst1
-pr3/wcpr0 / pr3_wcpr0_t
-r/props / r_arith0
-r/props / r_arith1
-r/props / r_dis
-r/props / r_minus
-r/props / r_plus
-r/props / r_plus_sym
-r/props / r_S
-r/props / s_r
-sc3/arity / sc3_arity
-sc3/arity / sc3_arity_csubc
-sc3/props / sc3_abbr
-sc3/props / sc3_abst
-sc3/props / sc3_appl
-sc3/props / sc3_arity_gen
-sc3/props / sc3_bind
-sc3/props / sc3_cast
-sc3/props / sc3_lift
-sc3/props / sc3_lift1
-sc3/props sc3_props sc3_sn3_abst
-sc3/props / sc3_repl
-sc3/props / sc3_sn3
-sn3/fwd / sn3_gen_bind
-sn3/fwd / sn3_gen_cflat
-sn3/fwd / sn3_gen_flat
-sn3/fwd / sn3_gen_head
-sn3/fwd / sn3_gen_lift
-sn3/lift1 / sns3_lifts1
-sn3/nf2 / nf2_sn3
-sn3/nf2 / sn3_nf2
-sn3/props / sn3_abbr
-sn3/props / sn3_appl_abbr
-sn3/props / sn3_appl_appl
-sn3/props / sn3_appl_appls
-sn3/props / sn3_appl_beta
-sn3/props / sn3_appl_bind
-sn3/props / sn3_appl_cast
-sn3/props / sn3_appl_lref
-sn3/props / sn3_appls_abbr
-sn3/props / sn3_appls_beta
-sn3/props / sn3_appls_bind
-sn3/props / sn3_appls_cast
-sn3/props / sn3_appls_lref
-sn3/props / sn3_beta
-sn3/props / sn3_bind
-sn3/props / sn3_cast
-sn3/props / sn3_cdelta
-sn3/props / sn3_cflat
-sn3/props / sn3_change
-sn3/props / sn3_cpr3_trans
-sn3/props / sn3_gen_def
-sn3/props / sn3_lift
-sn3/props / sn3_pr2_intro
-sn3/props / sn3_pr3_trans
-sn3/props / sn3_shift
-sn3/props / sns3_lifts
-s/props / minus_s_s
-s/props / s_arith0
-s/props / s_arith1
-s/props / s_inc
-s/props / s_inj
-s/props / s_le
-s/props / s_lt
-s/props / s_minus
-s/props / s_plus
-s/props / s_plus_sym
-s/props / s_S
-sty0/fwd / sty0_gen_appl
-sty0/fwd / sty0_gen_bind
-sty0/fwd / sty0_gen_cast
-sty0/fwd / sty0_gen_lref
-sty0/fwd / sty0_gen_sort
-sty0/props / sty0_correct
-sty0/props / sty0_lift
-sty1/cnt / sty1_cnt
-sty1/props / sty1_abbr
-sty1/props / sty1_appl
-sty1/props / sty1_bind
-sty1/props / sty1_cast2
-sty1/props / sty1_correct
-sty1/props / sty1_lift
-sty1/props / sty1_trans
-subst0/dec / dnf_dec
-subst0/dec / dnf_dec2
-subst0/fwd / subst0_gen_head
-subst0/fwd / subst0_gen_lift_false
-subst0/fwd / subst0_gen_lift_ge
-subst0/fwd / subst0_gen_lift_lt
-subst0/fwd / subst0_gen_lref
-subst0/fwd / subst0_gen_sort
-subst0/props / subst0_lift_ge
-subst0/props / subst0_lift_ge_s
-subst0/props / subst0_lift_ge_S
-subst0/props / subst0_lift_lt
-subst0/props / subst0_refl
-subst0/subst0 / subst0_confluence_eq
-subst0/subst0 / subst0_confluence_lift
-subst0/subst0 / subst0_confluence_neq
-subst0/subst0 / subst0_subst0
-subst0/subst0 / subst0_subst0_back
-subst0/subst0 / subst0_trans
-subst0/tlt / subst0_tlt
-subst0/tlt / subst0_tlt_head
-subst0/tlt / subst0_weight_le
-subst0/tlt / subst0_weight_lt
-subst1/fwd / subst1_gen_head
-subst1/fwd / subst1_gen_lift_eq
-subst1/fwd / subst1_gen_lift_ge
-subst1/fwd / subst1_gen_lift_lt
-subst1/fwd / subst1_gen_lref
-subst1/fwd / subst1_gen_sort
-subst1/props / subst1_ex
-subst1/props / subst1_head
-subst1/props / subst1_lift_ge
-subst1/props / subst1_lift_lt
-subst1/props / subst1_lift_S
-subst1/subst1 / subst1_confluence_eq
-subst1/subst1 / subst1_confluence_lift
-subst1/subst1 / subst1_confluence_neq
-subst1/subst1 / subst1_subst1
-subst1/subst1 / subst1_subst1_back
-subst1/subst1 / subst1_trans
-subst/fwd / subst_head
-subst/fwd / subst_lref_eq
-subst/fwd / subst_lref_gt
-subst/fwd / subst_lref_lt
-subst/fwd / subst_sort
-subst/props / subst_lift_SO
-subst/props / subst_subst0
-T/dec / abst_dec
-T/dec / bind_dec_not
-T/dec / binder_dec
-T/dec / term_dec
-T/dec terms_props bind_dec
-T/dec terms_props flat_dec
-T/dec terms_props kind_dec
-tlist/props / tcons_tapp_ex
-tlist/props / theads_tapp
-tlist/props / tlist_ind_rev
-tlist/props / tslt_wf_ind
-tlist/props tslt_wf q_ind
-tlt/props / tlt_head_dx
-tlt/props / tlt_head_sx
-tlt/props / tlt_trans
-tlt/props / tlt_wf_ind
-tlt/props tlt_wf q_ind
-tlt/props / wadd_le
-tlt/props / wadd_lt
-tlt/props / wadd_O
-tlt/props / weight_add_O
-tlt/props / weight_add_S
-tlt/props / weight_eq
-tlt/props / weight_le
-T/props / not_abbr_abst
-T/props / not_abbr_void
-T/props / not_abst_void
-T/props / not_void_abst
-T/props / thead_x_y_y
-T/props / tweight_lt
-ty3/arity / ty3_arity
-ty3/arity_props / ty3_acyclic
-ty3/arity_props / ty3_predicative
-ty3/arity_props / ty3_repellent
-ty3/arity_props / ty3_sn3
-ty3/dec / ty3_inference
-ty3/fsubst0 / ty3_csubst0
-ty3/fsubst0 / ty3_fsubst0
-ty3/fsubst0 / ty3_subst0
-ty3/fwd / ty3_gen_appl
-ty3/fwd / ty3_gen_bind
-ty3/fwd / ty3_gen_cast
-ty3/fwd / ty3_gen_lref
-ty3/fwd / ty3_gen_sort
-ty3/fwd / tys3_gen_cons
-ty3/fwd / tys3_gen_nil
-ty3/fwd_nf2 / ty3_gen_appl_nf2
-ty3/fwd_nf2 / ty3_inv_appls_lref_nf2
-ty3/fwd_nf2 / ty3_inv_lref_lref_nf2
-ty3/fwd_nf2 / ty3_inv_lref_nf2
-ty3/fwd_nf2 / ty3_inv_lref_nf2_pc3
-ty3/nf2 ty3_nf2_gen ty3_nf2_inv_abst_aux
-ty3/nf2 / ty3_nf2_inv_abst
-ty3/nf2 / ty3_nf2_inv_abst_premise_csort
-ty3/nf2 / ty3_nf2_inv_all
-ty3/nf2 / ty3_nf2_inv_sort
-ty3/pr3 / ty3_sred_pr0
-ty3/pr3 / ty3_sred_pr1
-ty3/pr3 / ty3_sred_pr2
-ty3/pr3 / ty3_sred_pr3
-ty3/pr3 / ty3_sred_wcpr0_pr0
-ty3/pr3_props / ty3_cred_pr2
-ty3/pr3_props / ty3_cred_pr3
-ty3/pr3_props / ty3_gen_lift
-ty3/pr3_props / ty3_sconv
-ty3/pr3_props / ty3_sconv_pc3
-ty3/pr3_props / ty3_sred_back
-ty3/pr3_props / ty3_tred
-ty3/props / ty3_correct
-ty3/props / ty3_gen_abst_abst
-ty3/props / ty3_getl_subst0
-ty3/props / ty3_lift
-ty3/props / ty3_typecheck
-ty3/props / ty3_unique
-ty3/sty0 / ty3_sty0
-ty3/subst1 / ty3_gen_cabbr
-ty3/subst1 / ty3_gen_cvoid
-wcpr0/fwd / wcpr0_gen_head
-wcpr0/fwd / wcpr0_gen_sort
-wcpr0/getl / wcpr0_drop
-wcpr0/getl / wcpr0_drop_back
-wcpr0/getl / wcpr0_getl
-wcpr0/getl / wcpr0_getl_back
-wf3/clear / clear_wf3_trans
-wf3/clear / wf3_clear_conf
-wf3/fwd / wf3_gen_bind1
-wf3/fwd / wf3_gen_flat1
-wf3/fwd / wf3_gen_head2
-wf3/fwd / wf3_gen_sort1
-wf3/getl / getl_wf3_trans
-wf3/getl / wf3_getl_conf
-wf3/props / ty3_shift1
-wf3/props / wf3_idem
-wf3/props / wf3_mono
-wf3/props / wf3_total
-wf3/props / wf3_ty3
-wf3/ty3 / wf3_pc3_conf
-wf3/ty3 / wf3_pr2_conf
-wf3/ty3 / wf3_pr3_conf
-wf3/ty3 / wf3_ty3_conf