A
Abbr
Abst
abst_dec
AHead
ahead_inj_snd
aplus
aplus_ahead_simpl
aplus_asort_le_simpl
aplus_asort_O_simpl
aplus_asort_simpl
aplus_assoc
aplus_asucc
aplus_asucc_false
aplus_gz_ge
aplus_gz_le
aplus_inj
aplus_reg_r
aplus_sort_O_S_simpl
aplus_sort_S_S_simpl
app1
Appl
aprem
aprem_asucc
aprem_gen_head_O
aprem_gen_head_S
aprem_gen_sort
aprem_repl
aprem_succ
aprem_zero
arity
arity_abbr
arity_abst
arity_appl
arity_appls_abbr
arity_appls_appl
arity_appls_bind
arity_appls_cast
arity_aprem
arity_bind
arity_cast
arity_cimp_conf
arity_fsubst0
arity_gen_abst
arity_gen_appl
arity_gen_appls
arity_gen_bind
arity_gen_cast
arity_gen_cvoid
arity_gen_cvoid_subst0
arity_gen_lift
arity_gen_lref
arity_gen_sort
arity_head
arity_lift
arity_lift1
arity_mono
arity_nf2_inv_all
arity_repellent
arity_repl
arity_sort
arity_sred_pr2
arity_sred_pr3
arity_sred_wcpr0_pr0
arity_sred_wcpr0_pr1
arity_subst0
ASort
asucc
asucc_gen_head
asucc_gen_sort
asucc_inj
asucc_repl
B
Bind
bind_dec_not
binder_dec
C
Cast
cbk
CHead
chead_ctail
cimp
cimp_bind
cimp_flat_dx
cimp_flat_sx
cimp_getl_conf
cle
clear
clear_bind
clear_cle
clear_clear
clear_ctail
clear_flat
clear_gen_all
clear_gen_bind
clear_gen_flat
clear_gen_flat_r
clear_gen_sort
clear_getl_trans
clear_mono
clear_pc3_trans
clear_pr2_trans
clear_pr3_trans
clear_trans
clear_wf3_trans
cle_flt_trans
cle_head
clen
cle_r
cle_trans_head
clt
clt_cong
clt_head
clt_thead
clt_wf_ind
clt_wf__q_ind
cnt
cnt_head
cnt_lift
cnt_sort
CSort
csuba
csuba_abst
csuba_arity
csuba_arity_rev
csuba_clear_conf
csuba_clear_trans
csuba_drop_abbr
csuba_drop_abbr_rev
csuba_drop_abst
csuba_drop_abst_rev
csuba_gen_abbr
csuba_gen_abbr_rev
csuba_gen_abst
csuba_gen_abst_rev
csuba_gen_bind
csuba_gen_bind_rev
csuba_gen_flat
csuba_gen_flat_rev
csuba_gen_void
csuba_gen_void_rev
csuba_getl_abbr
csuba_getl_abbr_rev
csuba_getl_abst
csuba_getl_abst_rev
csuba_head
csuba_refl
csuba_sort
csuba_void
csubc
csubc_abst
csubc_arity_conf
csubc_arity_trans
csubc_clear_conf
csubc_csuba
csubc_drop1_conf_rev
csubc_drop_conf_O
csubc_drop_conf_rev
csubc_gen_head_l
csubc_gen_head_r
csubc_gen_sort_l
csubc_gen_sort_r
csubc_getl_conf
csubc_head
csubc_refl
csubc_sort
csubc_void
csubst0
csubst0_both
csubst0_both_bind
csubst0_clear_O
csubst0_clear_O_back
csubst0_clear_S
csubst0_clear_trans
csubst0_drop_eq
csubst0_drop_eq_back
csubst0_drop_gt
csubst0_drop_gt_back
csubst0_drop_lt
csubst0_drop_lt_back
csubst0_fst
csubst0_fst_bind
csubst0_gen_head
csubst0_gen_S_bind_2
csubst0_gen_sort
csubst0_getl_ge
csubst0_getl_ge_back
csubst0_getl_lt
csubst0_getl_lt_back
csubst0_snd
csubst0_snd_bind
csubst1
csubst1_bind
csubst1_flat
csubst1_gen_head
csubst1_getl_ge
csubst1_getl_ge_back
csubst1_getl_lt
csubst1_head
csubst1_refl
csubst1_sing
csubt
csubt_abst
csubt_clear_conf
csubt_csuba
csubt_drop_abbr
csubt_drop_abst
csubt_drop_flat
csubt_gen_abbr
csubt_gen_abst
csubt_gen_bind
csubt_gen_flat
csubt_getl_abbr
csubt_getl_abst
csubt_head
csubt_pc3
csubt_pr2
csubt_refl
csubt_sort
csubt_ty3
csubt_ty3_ld
csubt_void
csubv
csubv_bind
csubv_bind_same
csubv_clear_conf
csubv_clear_conf_void
csubv_drop_conf
csubv_flat
csubv_getl_conf
csubv_getl_conf_void
csubv_refl
csubv_sort
csubv_void
CTail
c_tail_ind
cweight
dnf_dec
dnf_dec2
drop
drop1
drop1_cons
drop1_cons_tail
drop1_csubc_trans
drop1_gen_pcons
drop1_gen_pnil
drop1_getl_trans
drop1_nil
drop1_skip_bind
drop1_trans
drop_clear
drop_clear_O
drop_clear_S
drop_conf_ge
drop_conf_lt
drop_conf_rev
drop_csubc_trans
drop_ctail
drop_drop
drop_gen_drop
drop_gen_refl
drop_gen_skip_l
drop_gen_skip_r
drop_gen_sort
drop_getl_trans_ge
drop_getl_trans_le
drop_getl_trans_lt
drop_mono
drop_refl
drop_S
drop_skip
drop_skip_bind
drop_skip_flat
drop_trans_ge
drop_trans_le
ex1_arity
ex1_c
ex1__leq_sort_SS
ex1_t
ex1_ty3
ex2_arity
ex2_c
ex2_nf2
ex2_t
F
Flat
flt
flt_arith0
flt_arith1
flt_arith2
flt_shift
flt_thead_dx
flt_thead_sx
flt_trans
flt_wf_ind
flt_wf__q_ind
fsubst0
fsubst0_both
fsubst0_fst
fsubst0_gen_base
fsubst0_snd
fweight
G
getl
getl_clear_bind
getl_clear_conf
getl_clear_trans
getl_conf_ge_drop
getl_conf_le
getl_csubst1
getl_ctail
getl_ctail_clen
getl_dec
getl_drop
getl_drop_conf_ge
getl_drop_conf_lt
getl_drop_conf_rev
getl_drop_trans
getl_flat
getl_flt
getl_gen_2
getl_gen_all
getl_gen_bind
getl_gen_flat
getl_gen_O
getl_gen_S
getl_gen_sort
getl_gen_tail
getl_head
getl_intro
getl_mono
getl_refl
getl_trans
getl_wf3_trans
gz
iso
iso_flats_flat_bind_false
iso_flats_lref_bind_false
iso_gen_head
iso_gen_lref
iso_gen_sort
iso_head
iso_lref
iso_refl
iso_sort
iso_trans
K
leq
leq_ahead_asucc_false
leq_ahead_false_1
leq_ahead_false_2
leq_asucc
leq_asucc_false
leq_eq
leq_gen_head1
leq_gen_head2
leq_gen_sort1
leq_gen_sort2
leq_head
leq_leqz
leq_refl
leq_sort
leq_sym
leq_trans
leqz
leqz_head
leqz_leq
leqz_sort
lift
lift1
lift1_bind
lift1_cons_tail
lift1_flat
lift1_free
lift1_lift1
lift1_lref
lift1_sort
lift1_xhg
lift_bind
lift_d
lift_flat
lift_free
lift_free_sym
lift_gen_bind
lift_gen_flat
lift_gen_head
lift_gen_lift
lift_gen_lref
lift_gen_lref_false
lift_gen_lref_ge
lift_gen_lref_lt
lift_gen_sort
lift_head
lift_inj
lift_lref_ge
lift_lref_gt
lift_lref_lt
lift_r
lifts
lifts1
lifts1_cons
lifts1_flat
lifts1_nil
lifts1_xhg
lifts_inj
lift_sort
lifts_tapp
lift_tle
lift_tlt_dx
lift_weight
lift_weight_add
lift_weight_add_O
lift_weight_map
llt
llt_head_dx
llt_head_sx
llt_repl
llt_trans
llt_wf_ind
llt_wf__q_ind
lref_map
lweight
lweight_repl
minus_s_s
mk_G
next_plus
next_plus_assoc
next_plus_gz
next_plus_lt
next_plus_next
nf0_dec
nf2
nf2_abst
nf2_abst_shift
nf2_appl_lref
nf2_appls_lref
nf2_csort_lref
nf2_dec
nf2_gen_abbr
nf2_gen_abst
nf2_gen_beta
nf2_gen_cast
nf2_gen_flat
nf2_gen_lref
nf2_gen__nf2_gen_aux
nf2_gen_void
nf2_iso_appls_lref
nf2_lift
nf2_lift1
nf2_lref_abst
nf2_pr3_confluence
nf2_pr3_unfold
nf2_sn3
nf2_sort
nfs2
nfs2_tapp
node_inh
not_abbr_abst
not_abbr_void
not_abst_void
not_void_abst
pc1
pc1_head
pc1_head_1
pc1_head_2
pc1_pr0_r
pc1_pr0_u
pc1_pr0_u2
pc1_pr0_x
pc1_refl
pc1_s
pc1_t
pc3
pc3_abst_dec
pc3_dec
pc3_eta
pc3_fsubst0
pc3_gen_abst
pc3_gen_abst_shift
pc3_gen_appls_lref_abst
pc3_gen_appls_lref_sort
pc3_gen_appls_sort_abst
pc3_gen_cabbr
pc3_gen_lift
pc3_gen_lift_abst
pc3_gen_not_abst
pc3_gen_sort
pc3_gen_sort_abst
pc3_head_1
pc3_head_12
pc3_head_2
pc3_head_21
pc3_ind_left
pc3_ind_left__pc3_left_pc3
pc3_ind_left__pc3_left_pr3
pc3_ind_left__pc3_left_sym
pc3_ind_left__pc3_left_trans
pc3_ind_left__pc3_pc3_left
pc3_left
pc3_left_r
pc3_left_ur
pc3_left_ux
pc3_lift
pc3_nf2
pc3_nf2_unfold
pc3_pc1
pc3_pr0_pr2_t
pc3_pr2_fsubst0
pc3_pr2_fsubst0_back
pc3_pr2_pr2_t
pc3_pr2_pr3_t
pc3_pr2_r
pc3_pr2_u
pc3_pr2_u2
pc3_pr2_x
pc3_pr3_conf
pc3_pr3_pc3_t
pc3_pr3_r
pc3_pr3_t
pc3_pr3_x
pc3_refl
pc3_s
pc3_t
pc3_thin_dx
pc3_wcpr0
pc3_wcpr0__pc3_wcpr0_t_aux
pc3_wcpr0_t
pr0
pr0_beta
pr0_comp
pr0_confluence
pr0_confluence__pr0_cong_delta
pr0_confluence__pr0_cong_upsilon_cong
pr0_confluence__pr0_cong_upsilon_delta
pr0_confluence__pr0_cong_upsilon_refl
pr0_confluence__pr0_cong_upsilon_zeta
pr0_confluence__pr0_delta_delta
pr0_confluence__pr0_delta_tau
pr0_confluence__pr0_upsilon_upsilon
pr0_delta
pr0_delta1
pr0_gen_abbr
pr0_gen_abst
pr0_gen_appl
pr0_gen_cast
pr0_gen_lift
pr0_gen_lref
pr0_gen_sort
pr0_gen_void
pr0_lift
pr0_refl
pr0_subst0
pr0_subst0_back
pr0_subst0_fwd
pr0_subst1
pr0_subst1_back
pr0_subst1_fwd
pr0_tau
pr0_upsilon
pr0_zeta
pr1
pr1_comp
pr1_confluence
pr1_eta
pr1_head_1
pr1_head_2
pr1_pr0
pr1_refl
pr1_sing
pr1_strip
pr1_t
pr2
pr2_cflat
pr2_change
pr2_confluence
pr2_confluence__pr2_delta_delta
pr2_confluence__pr2_free_delta
pr2_confluence__pr2_free_free
pr2_ctail
pr2_delta
pr2_delta1
pr2_free
pr2_gen_abbr
pr2_gen_abst
pr2_gen_appl
pr2_gen_cabbr
pr2_gen_cast
pr2_gen_cbind
pr2_gen_cflat
pr2_gen_csort
pr2_gen_ctail
pr2_gen_lift
pr2_gen_lref
pr2_gen_sort
pr2_gen_void
pr2_head_1
pr2_head_2
pr2_lift
pr2_subst1
pr2_thin_dx
pr3
pr3_cflat
pr3_confluence
pr3_eta
pr3_flat
pr3_gen_abbr
pr3_gen_abst
pr3_gen_appl
pr3_gen_bind
pr3_gen_cabbr
pr3_gen_cast
pr3_gen_lift
pr3_gen_lref
pr3_gen_sort
pr3_gen_void
pr3_head_1
pr3_head_12
pr3_head_2
pr3_head_21
pr3_iso_appl_bind
pr3_iso_appls_abbr
pr3_iso_appls_appl_bind
pr3_iso_appls_beta
pr3_iso_appls_bind
pr3_iso_appls_cast
pr3_iso_beta
pr3_lift
pr3_pr0_pr2_t
pr3_pr1
pr3_pr2
pr3_pr2_pr2_t
pr3_pr2_pr3_t
pr3_pr3_pr3_t
pr3_refl
pr3_sing
pr3_strip
pr3_subst1
pr3_t
pr3_thin_dx
pr3_wcpr0_t
ptrans
r
r_arith0
r_arith1
r_arith2
r_arith3
r_arith4
r_arith5
r_arith6
r_arith7
r_dis
r_minus
r_plus
r_plus_sym
r_S
s
s_arith0
s_arith1
sc3
sc3_abbr
sc3_abst
sc3_appl
sc3_arity
sc3_arity_csubc
sc3_arity_gen
sc3_bind
sc3_cast
sc3_lift
sc3_lift1
sc3_props__sc3_sn3_abst
sc3_repl
sc3_sn3
s_inc
s_inj
s_le
s_le_gen
s_lt
s_lt_gen
s_minus
sn3
sn3_abbr
sn3_appl_abbr
sn3_appl_appl
sn3_appl_appls
sn3_appl_beta
sn3_appl_bind
sn3_appl_cast
sn3_appl_lref
sn3_appls_abbr
sn3_appls_beta
sn3_appls_bind
sn3_appls_cast
sn3_appls_lref
sn3_beta
sn3_bind
sn3_cast
sn3_cdelta
sn3_cflat
sn3_change
sn3_cpr3_trans
sn3_gen_bind
sn3_gen_cflat
sn3_gen_def
sn3_gen_flat
sn3_gen_head
sn3_gen_lift
sn3_lift
sn3_nf2
sn3_pr2_intro
sn3_pr3_trans
sn3_shift
sn3_sing
sns3
sns3_lifts
sns3_lifts1
s_plus
s_plus_sym
s_r
s_S
sty0
sty0_abbr
sty0_abst
sty0_appl
sty0_bind
sty0_cast
sty0_correct
sty0_gen_appl
sty0_gen_bind
sty0_gen_cast
sty0_gen_lref
sty0_gen_sort
sty0_lift
sty0_sort
sty1
sty1_abbr
sty1_appl
sty1_bind
sty1_cast2
sty1_cnt
sty1_correct
sty1_lift
sty1_sing
sty1_sty0
sty1_trans
subst
subst0
subst0_both
subst0_confluence_eq
subst0_confluence_lift
subst0_confluence_neq
subst0_fst
subst0_gen_head
subst0_gen_lift_false
subst0_gen_lift_ge
subst0_gen_lift_lt
subst0_gen_lift_rev_ge
subst0_gen_lref
subst0_gen_sort
subst0_lift_ge
subst0_lift_ge_s
subst0_lift_ge_S
subst0_lift_lt
subst0_lref
subst0_refl
subst0_snd
subst0_subst0
subst0_subst0_back
subst0_tlt
subst0_tlt_head
subst0_trans
subst0_weight_le
subst0_weight_lt
subst1
subst1_confluence_eq
subst1_confluence_lift
subst1_confluence_neq
subst1_ex
subst1_gen_head
subst1_gen_lift_eq
subst1_gen_lift_ge
subst1_gen_lift_lt
subst1_gen_lref
subst1_gen_sort
subst1_head
subst1_lift_ge
subst1_lift_lt
subst1_lift_S
subst1_refl
subst1_single
subst1_subst1
subst1_subst1_back
subst1_trans
subst_head
subst_lift_SO
subst_lref_eq
subst_lref_gt
subst_lref_lt
subst_sort
subst_subst0
T
TApp
TCons
tcons_tapp_ex
term_dec
terms_props__bind_dec
terms_props__flat_dec
terms_props__kind_dec
THead
THeads
theads_tapp
thead_x_lift_y_y
thead_x_y_y
tle
tle_r
TList
tlist_ind_rev
TLRef
tlt
tlt_head_dx
tlt_head_sx
tlt_trans
tlt_wf_ind
tlt_wf__q_ind
TNil
trans
tslen
tslt
tslt_wf_ind
tslt_wf__q_ind
TSort
tweight
tweight_lt
ty3
ty3_abbr
ty3_abst
ty3_acyclic
ty3_appl
ty3_arity
ty3_bind
ty3_cast
ty3_conv
ty3_correct
ty3_cred_pr2
ty3_cred_pr3
ty3_csubst0
ty3_fsubst0
ty3_gen_abst_abst
ty3_gen_appl
ty3_gen_appl_nf2
ty3_gen_bind
ty3_gen_cabbr
ty3_gen_cast
ty3_gen_cvoid
ty3_gen_lift
ty3_gen_lref
ty3_gen_sort
ty3_getl_subst0
ty3_inference
ty3_inv_appls_lref_nf2
ty3_inv_lref_lref_nf2
ty3_inv_lref_nf2
ty3_inv_lref_nf2_pc3
ty3_lift
ty3_nf2_gen__ty3_nf2_inv_abst_aux
ty3_nf2_inv_abst
ty3_nf2_inv_abst_premise
ty3_nf2_inv_abst_premise_csort
ty3_nf2_inv_all
ty3_nf2_inv_sort
ty3_predicative
ty3_repellent
ty3_sconv
ty3_sconv_pc3
ty3_shift1
ty3_sn3
ty3_sort
ty3_sred_back
ty3_sred_pr0
ty3_sred_pr1
ty3_sred_pr2
ty3_sred_pr3
ty3_sred_wcpr0_pr0
ty3_sty0
ty3_subst0
ty3_tred
ty3_typecheck
ty3_unique
tys3
tys3_cons
tys3_gen_cons
tys3_gen_nil
tys3_nil
Void
wadd
wadd_le
wadd_lt
wadd_O
wcpr0
wcpr0_comp
wcpr0_drop
wcpr0_drop_back
wcpr0_gen_head
wcpr0_gen_sort
wcpr0_getl
wcpr0_getl_back
wcpr0_refl
weight
weight_add_O
weight_add_S
weight_eq
weight_le
weight_map
wf3
wf3_bind
wf3_clear_conf
wf3_flat
wf3_gen_bind1
wf3_gen_flat1
wf3_gen_head2
wf3_gen_sort1
wf3_getl_conf
wf3_idem
wf3_mono
wf3_pc3_conf
wf3_pr2_conf
wf3_pr3_conf
wf3_sort
wf3_total
wf3_ty3
wf3_ty3_conf
wf3_void