]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/basic_1A/names.txt
update in basic_2 + new tool "roles"
[helm.git] / matita / matita / contribs / lambdadelta / basic_1A / names.txt
index d85e0594506902828726b3ca9c3f05c21dbdf4b7..91031610a0dea1c48cca9161ea33c7d65f3c63e4 100644 (file)
-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
+"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"