"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"