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