X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Fnames.txt;h=5785291157ce7d70fc6270dff0f85c41a65eefc7;hb=a1ae862976f2489107dd107937f5e05d0aaa7144;hp=6af48b1ca3b1964e59794a726afa98207fbb3dde;hpb=076439def28e649ec384fae038ed021dadd5f75c;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/static_2/names.txt b/matita/matita/contribs/lambdadelta/static_2/names.txt
index 6af48b1ca..578529115 100644
--- a/matita/matita/contribs/lambdadelta/static_2/names.txt
+++ b/matita/matita/contribs/lambdadelta/static_2/names.txt
@@ -1,1276 +1,1276 @@
-aaa
-aaa_aaa_inv_appl
-aaa_aaa_inv_cast
-aaa_abbr
-aaa_abst
-aaa_appl
-aaa_cast
-aaa_dec
-aaa_feqx_conf
-aaa_fqu_conf
-aaa_fqup_conf
-aaa_fquq_conf
-aaa_fqus_conf
-aaa_inv_abbr
-aaa_inv_abbr_aux
-aaa_inv_abst
-aaa_inv_abst_aux
-aaa_inv_appl
-aaa_inv_appl_aux
-aaa_inv_cast
-aaa_inv_cast_aux
-aaa_inv_gref
-aaa_inv_gref_aux
-aaa_inv_lifts
-aaa_inv_lref
-aaa_inv_lref_aux
-aaa_inv_lref_drops
-aaa_inv_sort
-aaa_inv_sort_aux
-aaa_inv_zero
-aaa_inv_zero_aux
-aaa_lifts
-aaa_lref
-aaa_lref_drops
-aaa_mono
-aaa_pair_inv_lref
-aaa_sort
-aaa_teqx_conf_reqx
-aaa_zero
-aarity
-AAtom
-Abbr
-Abst
-abst_dec
-ac
-ac_eq
-ac_eq_props
-ac_le
-acle
-acle_eq_le
-acle_eq_monotonic_le
-acle_le_eq
-acle_le_monotonic_le
-acle_omega
-acle_one
-ac_le_props
-acle_refl
-acle_trans
-ac_props
-acr
-acr_aaa
-acr_aaa_csubc_lifts
-acr_abst
-acr_gcr
-acr_lifts
-ac_top
-ac_top_props
-APair
-append
-append_assoc
-append_atom
-append_atom_sn
-append_bind
-append_inj_dx
-append_inj_length_dx
-append_inj_length_sn
-append_inj_sn
-append_inv_atom3_sn
-append_inv_bind3_sn
-append_inv_pair_dx
-append_inv_refl_dx
-append_length
-append_shift
-Appl
-applv
-applv_cons
-applv_nil
-applv_simple
-apply_top
-bind
-bind1
-bind2
-Bind2
-BPair
-BUnit
-bw
-bw_pos
-candidate
-Cast
-cdeq
-cdeq_ext
-ceq
-ceq_ext
-ceq_ext_inv_eq
-ceq_ext_refl
-ceq_ext_trans
-ceq_inv_lift_sn
-ceq_lift_sn
-cext2
-cext2_co
-cext2_d_liftable2_sn
-cext2_sym
-cfull
-cfull_dec
-cfull_lift_sn
-cfun
-co_dedropable_sn
-co_dedropable_sn_CTC
-co_dedropable_sn_ltc
-co_dropable_dx
-co_dropable_dx_CTC
-co_dropable_dx_ltc
-co_dropable_sn
-co_dropable_sn_CTC
-co_dropable_sn_ltc
-CP0
-CP1
-CP2
-CP3
-d1_liftable_liftable_all
-d2_deliftable_sn_CTC
-d2_deliftable_sn_ltc
-d2_liftable_sn_CTC
-d2_liftable_sn_ltc
-d_appendable_sn
-d_deliftable1
-d_deliftable1_isuni
-d_deliftable2_bi
-d_deliftable2_sn
-d_deliftable2_sn_bi
-dedropable_sn
-dedropable_sn_CTC
-deg_inv_prec
-deg_inv_pred
-deg_iter
-deg_next_SO
-deg_O
-deg_SO
-deg_SO_gt
-deg_SO_inv_succ
-deg_SO_inv_succ_aux
-deg_SO_refl
-deg_SO_succ
-deg_SO_zero
-deliftable2_bi
-deliftable2_dx
-deliftable2_sn
-deliftable2_sn_bi
-deliftable2_sn_dx
-destruct_apair_apair_aux
-destruct_lbind_lbind_aux
-destruct_sort_sort_aux
-destruct_tatom_tatom_aux
-destruct_tpair_tpair_aux
-discr_apair_xy_x
-discr_apair_xy_y
-discr_lbind_x_xy
-discr_lbind_xy_x
-discr_tpair_xy_x
-discr_tpair_xy_y
-d_liftable1
-d_liftable1_all
-d_liftable1_isuni
-d_liftable2_bi
-d_liftable2_sn
-d_liftable2_sn_bi
-dropable_dx
-dropable_dx_CTC
-dropable_sn
-dropable_sn_CTC
-drops
-drops_after_fwd_drop2
-drops_atom
-drops_atom2_sex_conf
-drops_atom_F
-drops_bind2_fwd_rfw
-drops_conf
-drops_conf_div
-drops_conf_div_bind_isuni
-drops_conf_div_fcla
-drops_conf_div_isuni
-drops_conf_skip1
-drops_drop
-drops_eq_repl_back
-drops_eq_repl_fwd
-drops_F
-drops_fcla_fwd
-drops_fcla_fwd_le2
-drops_fcla_fwd_lt2
-drops_fcla_fwd_lt4
-drops_F_uni
-drops_fwd_drop2
-drops_fwd_drop2_aux
-drops_fwd_fcla
-drops_fwd_fcla_le2
-drops_fwd_fcla_lt2
-drops_fwd_isfin
-drops_fwd_isid
-drops_fwd_length_eq1
-drops_fwd_length_eq2
-drops_fwd_length_le4
-drops_fwd_lw
-drops_fwd_lw_lt
-drops_gen
-drops_inv_atom1
-drops_inv_atom1_aux
-drops_inv_atom2
-drops_inv_bind1_isuni
-drops_inv_bind2_isuni
-drops_inv_bind2_isuni_next
-drops_inv_drop1
-drops_inv_drop1_aux
-drops_inv_F
-drops_inv_gen
-drops_inv_isuni
-drops_inv_length_eq
-drops_inv_skip1
-drops_inv_skip1_aux
-drops_inv_skip2
-drops_inv_skip2_aux
-drops_inv_succ
-drops_inv_TF
-drops_inv_TF_aux
-drops_inv_uni
-drops_inv_x_bind_xy
-drops_isuni_ex
-drops_isuni_fwd_drop2
-drops_ldec_dec
-drops_lsubc_trans
-drops_mono
-drops_refl
-drops_seq_trans_next
-drops_sex_trans_next
-drops_sex_trans_push
-drops_skip
-drops_split_div
-drops_split_trans
-drops_split_trans_bind2
-drops_TF
-drops_tls_at
-drops_trans
-drops_trans_skip2
-eq_aarity_dec
-eq_bind1_dec
-eq_bind2_dec
-eq_bind_dec
-eq_false_inv_tpair_dx
-eq_false_inv_tpair_sn
-eq_flat2_dec
-eq_genv_dec
-eq_item0_dec
-eq_item2_dec
-eq_lenv_dec
-eq_term_dec
-ext2
-ext2_dec
-ext2_inv_pair
-ext2_inv_pair_dx
-ext2_inv_pair_dx_aux
-ext2_inv_pair_sn
-ext2_inv_pair_sn_aux
-ext2_inv_tc
-ext2_inv_unit
-ext2_inv_unit_dx
-ext2_inv_unit_dx_aux
-ext2_inv_unit_sn
-ext2_inv_unit_sn_aux
-ext2_pair
-ext2_refl
-ext2_sym
-ext2_tc
-ext2_tc_inj
-ext2_tc_pair
-ext2_tc_step
-ext2_trans
-ext2_unit
-f_dedropable_sn
-f_dropable_dx
-f_dropable_sn
-feqx
-feqx_canc_dx
-feqx_canc_sn
-feqx_fqus_trans
-feqx_intro_dx
-feqx_intro_sn
-feqx_inv_gen_dx
-feqx_inv_gen_sn
-feqx_refl
-feqx_sym
-feqx_tneqx_repl_dx
-feqx_trans
-flat2
-Flat2
-fold
-fold_atom
-fold_pair
-fold_unit
-fqu
-fqu_bind_dx
-fqu_clear
-fqu_drop
-fqu_flat_dx
-fqu_fqup
-fqu_fquq
-fqu_fwd_fw
-fqu_fwd_length_lref1
-fqu_fwd_length_lref1_aux
-fqu_gref
-fqu_inv_atom1
-fqu_inv_bind1
-fqu_inv_bind1_aux
-fqu_inv_bind1_true
-fqu_inv_flat1
-fqu_inv_flat1_aux
-fqu_inv_gref1
-fqu_inv_gref1_aux
-fqu_inv_gref1_bind
-fqu_inv_lref1
-fqu_inv_lref1_aux
-fqu_inv_lref1_bind
-fqu_inv_sort1
-fqu_inv_sort1_aux
-fqu_inv_sort1_bind
-fqu_inv_teqx
-fqu_inv_teqx_aux
-fqu_inv_zero1_pair
-fqu_lref_O
-fqu_lref_S
-fqup
-fqu_pair_sn
-fqup_bind_dx
-fqup_bind_dx_flat_dx
-fqup_clear
-fqup_drops_strap1
-fqup_drops_succ
-fqup_flat_dx
-fqup_flat_dx_bind_dx
-fqup_flat_dx_pair_sn
-fqup_fqus
-fqup_fqus_trans
-fqup_fwd_fw
-fqup_ind
-fqup_ind_dx
-fqup_inv_step_sn
-fqup_lref
-fqup_pair_sn
-fqup_strap1
-fqup_strap2
-fqup_trans
-fqup_wf_ind
-fqup_wf_ind_eq
-fqup_zeta
-fquq
-fquq_fqus
-fquq_fwd_fw
-fquq_fwd_length_lref1
-fquq_refl
-fqus
-fqus_drops
-fqus_fqup_trans
-fqus_fwd_fw
-fqus_ind
-fqus_ind_dx
-fqus_inv_atom1
-fqus_inv_bind1
-fqus_inv_bind1_true
-fqus_inv_flat1
-fqus_inv_fqup
-fqus_inv_fqu_sn
-fqus_inv_gref1
-fqus_inv_gref1_bind
-fqus_inv_lref1
-fqus_inv_lref1_bind
-fqus_inv_refl_atom3
-fqus_inv_sort1
-fqus_inv_sort1_bind
-fqus_inv_zero1_pair
-fqu_sort
-fqus_refl
-fqus_strap1
-fqus_strap1_fqu
-fqus_strap2
-fqus_strap2_fqu
-fqus_trans
-fqu_teqx_conf
-fqu_wf_ind
-frees
-frees_append_void
-frees_atom
-frees_atom_drops
-frees_bind
-frees_bind_void
-frees_eq_repl_back
-frees_eq_repl_fwd
-frees_flat
-frees_fwd_coafter
-frees_fwd_isfin
-frees_gref
-frees_ind_void
-frees_inv_append_void
-frees_inv_append_void_aux
-frees_inv_atom
-frees_inv_atom_aux
-frees_inv_bind
-frees_inv_bind_aux
-frees_inv_bind_void
-frees_inv_drops_next
-frees_inv_flat
-frees_inv_flat_aux
-frees_inv_gref
-frees_inv_gref_aux
-frees_inv_lifts
-frees_inv_lifts_ex
-frees_inv_lifts_SO
-frees_inv_lref
-frees_inv_lref_aux
-frees_inv_lref_drops
-frees_inv_pair
-frees_inv_pair_aux
-frees_inv_sort
-frees_inv_sort_aux
-frees_inv_unit
-frees_inv_unit_aux
-frees_lifts
-frees_lifts_SO
-frees_lref
-frees_lref_push
-frees_lref_pushs
-frees_mono
-frees_pair
-frees_pair_drops
-frees_req_conf
-frees_reqx_conf
-frees_sex_conf
-frees_sort
-frees_teqx_conf
-frees_teqx_conf_reqx
-frees_total
-frees_unit
-frees_unit_drops
-fsge_rex_trans
-fsle
-fsle_bind
-fsle_bind_dx_dx
-fsle_bind_dx_sn
-fsle_bind_eq
-fsle_bind_sn_ge
-fsle_flat
-fsle_flat_dx_dx
-fsle_flat_dx_sn
-fsle_flat_sn
-fsle_frees_trans
-fsle_frees_trans_eq
-fsle_fwd_pair_sn
-fsle_gref
-fsle_gref_bi
-fsle_inv_frees_eq
-fsle_inv_lifts_sn
-fsle_lifts_dx
-fsle_lifts_sn
-fsle_lifts_SO
-fsle_lifts_SO_sn
-fsle_pair_bi
-fsle_refl
-fsle_shift
-fsle_sort
-fsle_sort_bi
-fsle_trans_dx
-fsle_trans_rc
-fsle_trans_sn
-fsle_unit_bi
-f_transitive_next
-fw
-fw_clear
-fw_lpair_sn
-fw_shift
-fw_tpair_dx
-fw_tpair_sn
-GAtom
-gcp
-gcp2_all
-gcr
-gcr_aaa
-genv
-glength
-GPair
-GRef
-gw
-gw_pair
-is_apear_dec
-is_lifts_dec
-item0
-item2
-LAtom
-LBind
-length
-length_atom
-length_bind
-length_inv_succ_dx
-length_inv_succ_dx_ltail
-length_inv_succ_sn
-length_inv_succ_sn_ltail
-length_inv_zero_dx
-length_inv_zero_sn
-lenv
-lenv_case_tail
-lenv_ind_tail
-lex
-lex_atom
-lex_bind
-lex_bind_refl_dx
-lex_co
-lex_conf
-lex_confluent
-lex_CTC
-lex_CTC_ind_dx
-lex_CTC_ind_sn
-lex_CTC_inj
-lex_CTC_step_dx
-lex_CTC_step_sn
-lex_dropable_dx
-lex_dropable_sn
-lex_drops_conf_pair
-lex_drops_trans_pair
-lex_fwd_length
-lex_ind
-lex_inv_atom_dx
-lex_inv_atom_sn
-lex_inv_bind_dx
-lex_inv_bind_sn
-lex_inv_CTC
-lex_inv_pair
-lex_inv_pair_dx
-lex_inv_pair_sn
-lex_inv_unit_dx
-lex_inv_unit_sn
-lex_liftable_dedropable_sn
-lex_pair
-lex_refl
-lex_trans
-lex_transitive
-lex_unit
-liftable2_bi
-liftable2_dx
-liftable2_sn
-liftable2_sn_bi
-liftable2_sn_dx
-lifts
-lifts_applv
-liftsb
-liftsb_conf
-liftsb_div3
-liftsb_eq_repl_back
-liftsb_fwd_bw
-liftsb_fwd_isid
-lifts_bind
-liftsb_inj
-liftsb_inv_pair_dx
-liftsb_inv_pair_sn
-liftsb_inv_unit_dx
-liftsb_inv_unit_sn
-liftsb_mono
-liftsb_refl
-liftsb_split_trans
-liftsb_total
-liftsb_trans
-lifts_conf
-lifts_div3
-lifts_div4
-lifts_div4_one
-lifts_eq_repl_back
-lifts_eq_repl_fwd
-lifts_flat
-lifts_fwd_isid
-lifts_fwd_pair1
-lifts_fwd_pair2
-lifts_fwd_tw
-lifts_gref
-lifts_inj
-lifts_inv_applv1
-lifts_inv_applv2
-lifts_inv_atom1
-lifts_inv_atom2
-lifts_inv_bind1
-lifts_inv_bind1_aux
-lifts_inv_bind2
-lifts_inv_bind2_aux
-lifts_inv_flat1
-lifts_inv_flat1_aux
-lifts_inv_flat2
-lifts_inv_flat2_aux
-lifts_inv_gref1
-lifts_inv_gref1_aux
-lifts_inv_gref2
-lifts_inv_gref2_aux
-lifts_inv_lref1
-lifts_inv_lref1_aux
-lifts_inv_lref1_uni
-lifts_inv_lref2
-lifts_inv_lref2_aux
-lifts_inv_lref2_uni
-lifts_inv_lref2_uni_ge
-lifts_inv_lref2_uni_lt
-lifts_inv_pair_xy_x
-lifts_inv_pair_xy_y
-lifts_inv_push_succ_sn
-lifts_inv_push_zero_sn
-lifts_inv_sort1
-lifts_inv_sort1_aux
-lifts_inv_sort2
-lifts_inv_sort2_aux
-lifts_lref
-lifts_lref_ge
-lifts_lref_ge_minus
-lifts_lref_lt
-lifts_lref_uni
-lifts_mono
-lifts_push_lref
-lifts_push_zero
-lifts_refl
-lifts_simple_dx
-lifts_simple_sn
-lifts_sort
-lifts_split_div
-lifts_split_trans
-lifts_total
-lifts_trans
-lifts_trans4_one
-lifts_trans_uni
-lifts_uni
-liftsv
-liftsv_cons
-liftsv_inj
-liftsv_inv_cons1
-liftsv_inv_cons1_aux
-liftsv_inv_cons2
-liftsv_inv_cons2_aux
-liftsv_inv_nil1
-liftsv_inv_nil1_aux
-liftsv_inv_nil2
-liftsv_inv_nil2_aux
-liftsv_mono
-liftsv_nil
-liftsv_split_trans
-liftsv_total
-liftsv_trans
-LRef
-lsuba
-lsuba_aaa_conf
-lsuba_aaa_trans
-lsuba_atom
-lsuba_beta
-lsuba_bind
-lsuba_drops_conf_isuni
-lsuba_drops_trans_isuni
-lsuba_fwd_lsubr
-lsuba_inv_atom1
-lsuba_inv_atom1_aux
-lsuba_inv_atom2
-lsuba_inv_atom2_aux
-lsuba_inv_bind1
-lsuba_inv_bind1_aux
-lsuba_inv_bind2
-lsuba_inv_bind2_aux
-lsuba_lsubc
-lsuba_refl
-lsuba_trans
-lsubc
-lsubc_atom
-lsubc_beta
-lsubc_bind
-lsubc_drops_trans_isuni
-lsubc_fwd_lsubr
-lsubc_inv_atom1
-lsubc_inv_atom1_aux
-lsubc_inv_atom2
-lsubc_inv_atom2_aux
-lsubc_inv_bind1
-lsubc_inv_bind1_aux
-lsubc_inv_bind2
-lsubc_inv_bind2_aux
-lsubc_refl
-lsubf
-lsubf_atom
-lsubf_beta
-lsubf_beta_tl_dx
-lsubf_bind
-lsubf_bind_tl_dx
-lsubf_eq_repl_back1
-lsubf_eq_repl_back2
-lsubf_eq_repl_fwd1
-lsubf_eq_repl_fwd2
-lsubf_frees_trans
-lsubf_fwd_bind_tl
-lsubf_fwd_isid_dx
-lsubf_fwd_isid_sn
-lsubf_fwd_lsubr_isdiv
-lsubf_fwd_sle
-lsubf_inv_atom
-lsubf_inv_atom1
-lsubf_inv_atom1_aux
-lsubf_inv_atom2
-lsubf_inv_atom2_aux
-lsubf_inv_beta_sn
-lsubf_inv_bind_sn
-lsubf_inv_pair1
-lsubf_inv_pair1_aux
-lsubf_inv_pair2
-lsubf_inv_pair2_aux
-lsubf_inv_push1
-lsubf_inv_push1_aux
-lsubf_inv_push2
-lsubf_inv_push2_aux
-lsubf_inv_push_sn
-lsubf_inv_refl
-lsubf_inv_sor_dx
-lsubf_inv_unit1
-lsubf_inv_unit1_aux
-lsubf_inv_unit2
-lsubf_inv_unit2_aux
-lsubf_inv_unit_sn
-lsubf_push
-lsubf_refl
-lsubf_refl_eq
-lsubf_sor
-lsubf_unit
-lsubr
-lsubr_atom
-lsubr_beta
-lsubr_bind
-lsubr_fwd_bind1
-lsubr_fwd_bind2
-lsubr_fwd_drops2_abbr
-lsubr_fwd_drops2_bind
-lsubr_fwd_length
-lsubr_inv_abbr2
-lsubr_inv_abst1
-lsubr_inv_abst2
-lsubr_inv_atom1
-lsubr_inv_atom1_aux
-lsubr_inv_atom2
-lsubr_inv_atom2_aux
-lsubr_inv_bind1
-lsubr_inv_bind1_aux
-lsubr_inv_bind2
-lsubr_inv_bind2_aux
-lsubr_inv_pair2
-lsubr_inv_unit1
-lsubr_inv_unit2
-lsubr_lsubf
-lsubr_lsubf_isid
-lsubr_refl
-lsubr_trans
-lsubr_unit
-ltail_length
-lveq
-lveq_atom
-lveq_bind
-lveq_fwd_abst_bind_length_le
-lveq_fwd_bind_abst_length_le
-lveq_fwd_gen
-lveq_fwd_length
-lveq_fwd_length_eq
-lveq_fwd_length_le_dx
-lveq_fwd_length_le_sn
-lveq_fwd_length_minus
-lveq_fwd_length_plus
-lveq_fwd_pair_dx
-lveq_fwd_pair_sn
-lveq_inj
-lveq_inj_length
-lveq_inj_void_dx_le
-lveq_inj_void_sn_ge
-lveq_inv_atom_atom
-lveq_inv_atom_bind
-lveq_inv_bind
-lveq_inv_bind_atom
-lveq_inv_bind_O
-lveq_inv_pair_pair
-lveq_inv_succ
-lveq_inv_succ_aux
-lveq_inv_succ_dx
-lveq_inv_succ_sn
-lveq_inv_succ_sn_aux
-lveq_inv_void_dx_length
-lveq_inv_void_sn_length
-lveq_inv_void_succ_dx
-lveq_inv_void_succ_sn
-lveq_inv_zero
-lveq_inv_zero_aux
-lveq_length_eq
-lveq_length_fwd_dx
-lveq_length_fwd_sn
-lveq_refl
-lveq_sym
-lveq_void_dx
-lveq_void_sn
-lw
-lw_bind
-mk_ac
-mk_ac_props
-mk_gcp
-mk_gcr
-mk_sd
-mk_sd_props
-mk_sh
-mk_sh_acyclic
-mk_sh_decidable
-mk_sh_lt
-nexts_le
-nexts_lt
-nf
-R_confluent2_rex
-req
-req_feqx_trans
-req_fsle_comp
-req_fwd_rex
-req_inv_bind
-req_inv_flat
-req_inv_lifts_bi
-req_inv_lref_bind_dx
-req_inv_lref_bind_sn
-req_inv_zero_pair_dx
-req_inv_zero_pair_sn
-req_refl
-req_reqx
-req_reqx_trans
-req_rex_trans
-req_transitive
-reqx
-reqx_atom
-reqx_bind
-reqx_bind_repl_dx
-reqx_bind_void
-reqx_canc_dx
-reqx_canc_sn
-reqx_dec
-reqx_flat
-reqx_fqup_trans
-reqx_fquq_trans
-reqx_fqus_trans
-reqx_fqu_trans
-reqx_fsge_comp
-reqx_fwd_bind_dx
-reqx_fwd_bind_dx_void
-reqx_fwd_dx
-reqx_fwd_flat_dx
-reqx_fwd_length
-reqx_fwd_pair_sn
-reqx_fwd_zero_pair
-reqx_gref
-reqx_gref_length
-reqx_inv_atom_dx
-reqx_inv_atom_sn
-reqx_inv_bind
-reqx_inv_bind_void
-reqx_inv_flat
-reqx_inv_lifts_bi
-reqx_inv_lifts_dx
-reqx_inv_lifts_sn
-reqx_inv_lref
-reqx_inv_lref_bind_dx
-reqx_inv_lref_bind_sn
-reqx_inv_lref_pair_bi
-reqx_inv_lref_pair_dx
-reqx_inv_lref_pair_sn
-reqx_inv_zero
-reqx_inv_zero_pair_dx
-reqx_inv_zero_pair_sn
-reqx_lifts_bi
-reqx_lifts_sn
-reqx_lref
-reqx_pair
-reqx_pair_refl
-reqx_refl
-reqx_repl
-reqx_rneqx_trans
-reqx_sort
-reqx_sort_length
-reqx_sym
-reqx_trans
-reqx_unit
-reqx_unit_length
-rex
-rex_atom
-rex_bind
-rex_bind_dx_split
-rex_bind_dx_split_void
-rex_bind_repl_dx
-rex_bind_void
-rex_co
-rex_conf
-rex_confluent
-rex_dec
-rex_dropable_dx
-rex_dropable_sn
-rex_flat
-rex_flat_dx_split
-rex_fsge_compatible
-rex_fsle_compatible
-rex_fwd_bind_dx
-rex_fwd_bind_dx_void
-rex_fwd_dx
-rex_fwd_flat_dx
-rex_fwd_length
-rex_fwd_pair_sn
-rex_fwd_zero_pair
-rex_gref
-rex_gref_length
-rex_inv_atom_dx
-rex_inv_atom_sn
-rex_inv_bind
-rex_inv_bind_void
-rex_inv_flat
-rex_inv_frees
-rex_inv_gref
-rex_inv_gref_bind_dx
-rex_inv_gref_bind_sn
-rex_inv_lex_req
-rex_inv_lifts_bi
-rex_inv_lref
-rex_inv_lref_bind_dx
-rex_inv_lref_bind_sn
-rex_inv_lref_pair_bi
-rex_inv_lref_pair_dx
-rex_inv_lref_pair_sn
-rex_inv_lref_unit_dx
-rex_inv_lref_unit_sn
-rex_inv_sort
-rex_inv_sort_bind_dx
-rex_inv_sort_bind_sn
-rex_inv_zero
-rex_inv_zero_length
-rex_inv_zero_pair_dx
-rex_inv_zero_pair_sn
-rex_inv_zero_unit_dx
-rex_inv_zero_unit_sn
-rex_isid
-rex_lex
-rex_liftable_dedropable_sn
-rex_lifts_bi
-rex_lref
-rex_pair
-rex_pair_refl
-rex_pair_sn_split
-rex_refl
-rexs
-rexs_atom
-rexs_co
-rexs_fwd_bind_dx
-rexs_fwd_bind_dx_void
-rexs_fwd_flat_dx
-rexs_fwd_length
-rexs_fwd_pair_sn
-rexs_gref
-rexs_ind_dx
-rexs_ind_sn
-rexs_inv_atom_dx
-rexs_inv_atom_sn
-rexs_inv_bind
-rexs_inv_bind_void
-rexs_inv_flat
-rexs_inv_gref
-rexs_inv_gref_bind_dx
-rexs_inv_gref_bind_sn
-rexs_inv_lex_req
-rexs_inv_sort
-rexs_inv_sort_bind_dx
-rexs_inv_sort_bind_sn
-rexs_lex
-rexs_lex_req
-rexs_lref
-rex_sort
-rex_sort_length
-rexs_pair
-rexs_pair_refl
-rexs_refl
-rexs_sort
-rexs_step_dx
-rexs_step_sn
-rexs_sym
-rexs_tc
-rexs_trans
-rexs_unit
-rex_sym
-rex_trans_fsle
-rex_transitive
-rex_trans_next
-rex_unit
-rex_unit_length
-rex_unit_sn
-R_fsge_compatible
-rfw
-rfw_clear
-rfw_lpair_dx
-rfw_lpair_sn
-rfw_shift
-rfw_tpair_dx
-rfw_tpair_sn
-rneqx_inv_bind
-rneqx_inv_bind_void
-rneqx_inv_flat
-rneqx_reqx_canc_dx
-rneqx_reqx_div
-rnex_inv_bind
-rnex_inv_bind_void
-rnex_inv_flat
-R_pw_confluent2_sex
-S1
-S2
-S3
-S5
-S6
-S7
-sd
-sd_d
-sd_d_correct
-sd_d_props
-sd_d_SS
-sd_O
-sd_O_props
-sd_props
-sd_SO
-sd_SO_props
-seq
-seq_canc_dx
-seq_canc_sn
-seq_co_dedropable_sn
-seq_co_dropable_dx
-seq_co_dropable_sn
-seq_drops_conf_next
-seq_drops_trans_next
-seq_eq_repl_back
-seq_eq_repl_fwd
-seq_fwd_length
-seq_inv_atom1
-seq_inv_atom2
-seq_inv_next
-seq_inv_next1
-seq_inv_next2
-seq_inv_push
-seq_inv_push1
-seq_inv_push2
-seq_inv_tl
-seq_join
-seq_meet
-seq_refl
-seq_sym
-seq_trans
-sex
-sex_atom
-sex_canc_dx
-sex_canc_sn
-sex_co
-sex_co_dropable_dx
-sex_co_dropable_sn
-sex_co_isid
-sex_conf
-sex_dec
-sex_dropable_dx_aux
-sex_drops_conf_next
-sex_drops_conf_push
-sex_drops_trans_next
-sex_drops_trans_push
-sex_eq_repl_back
-sex_eq_repl_fwd
-sex_fwd_bind
-sex_fwd_length
-sex_inv_atom1
-sex_inv_atom1_aux
-sex_inv_atom2
-sex_inv_atom2_aux
-sex_inv_next
-sex_inv_next1
-sex_inv_next1_aux
-sex_inv_next2
-sex_inv_next2_aux
-sex_inv_push
-sex_inv_push1
-sex_inv_push1_aux
-sex_inv_push2
-sex_inv_push2_aux
-sex_inv_tc_dx
-sex_inv_tc_sn
-sex_inv_tl
-sex_join
-sex_length_cfull
-sex_length_isid
-sex_liftable_co_dedropable_bi
-sex_liftable_co_dedropable_sn
-sex_meet
-sex_next
-sex_pair_repl
-sex_push
-sex_refl
-sex_sdj
-sex_sdj_split
-sex_sle_split
-sex_sym
-sex_tc_dx
-sex_tc_inj_dx
-sex_tc_inj_sn
-sex_tc_next
-sex_tc_next_dx
-sex_tc_next_sn
-sex_tc_push
-sex_tc_push_dx
-sex_tc_push_sn
-sex_tc_refl
-sex_tc_step_dx
-sex_trans
-sex_trans_gen
-sex_trans_id_cfull
-sex_transitive
-sh
-sh_acyclic
-sh_decidable
-sh_lt
-sh_lt_acyclic
-sh_lt_dec
-sh_lt_nexts_inv_lt
-simple
-simple_atom
-simple_dec_ex
-simple_flat
-simple_inv_bind
-simple_inv_bind_aux
-simple_inv_pair
-simple_teqo_repl_dx
-simple_teqo_repl_sn
-sle_seq_trans
-sle_sex_conf
-sle_sex_trans
-Sort
-s_rs_transitive_isid
-s_rs_transitive_lex_inv_isid
-TAtom
-tc_f_dedropable_sn
-tc_f_dropable_dx
-tc_f_dropable_sn
-teqo
-teqo_canc_dx
-teqo_canc_sn
-teqo_dec
-teqo_gref
-teqo_inv_applv_bind_simple
-teqo_inv_gref1
-teqo_inv_gref1_aux
-teqo_inv_lifts_bi
-teqo_inv_lref1
-teqo_inv_lref1_aux
-teqo_inv_pair
-teqo_inv_pair1
-teqo_inv_pair1_aux
-teqo_inv_pair2
-teqo_inv_pair2_aux
-teqo_inv_sort1
-teqo_inv_sort1_aux
-teqo_lifts_bi
-teqo_lifts_dx
-teqo_lifts_sn
-teqo_lref
-teqo_pair
-teqo_refl
-teqo_sort
-teqo_sym
-teqo_trans
-teqx
-teqx_canc_dx
-teqx_canc_sn
-teqx_dec
-teqx_ext
-teqx_feqx
-teqx_fqup_trans
-teqx_fquq_trans
-teqx_fqus_trans
-teqx_fqu_trans
-teqx_fwd_atom1
-teqx_gref
-teqx_inv_gref1
-teqx_inv_gref1_aux
-teqx_inv_lifts_bi
-teqx_inv_lifts_dx
-teqx_inv_lifts_sn
-teqx_inv_lref1
-teqx_inv_lref1_aux
-teqx_inv_pair
-teqx_inv_pair1
-teqx_inv_pair1_aux
-teqx_inv_pair2
-teqx_inv_pair_xy_x
-teqx_inv_pair_xy_y
-teqx_inv_sort1
-teqx_inv_sort1_aux
-teqx_inv_sort2
-teqx_lifts_bi
-teqx_lifts_dx
-teqx_lifts_inv_pair_sn
-teqx_lifts_sn
-teqx_lref
-teqx_pair
-teqx_refl
-teqx_repl
-teqx_reqx_conf
-teqx_reqx_div
-teqx_rex_conf
-teqx_rex_div
-teqx_sort
-teqx_sym
-teqx_teqo
-teqx_tneqx_trans
-teqx_trans
-teqx_tweq
-term
-tneqx_inv_pair
-tneqx_teqx_canc_dx
-TPair
-tw
-tweq
-tweq_abbr
-tweq_abbr_neg
-tweq_abbr_pos
-tweq_abst
-tweq_appl
-tweq_canc_dx
-tweq_canc_sn
-tweq_cast
-tweq_dec
-tweq_fwd_pair_bi
-tweq_fwd_pair_sn
-tweq_gref
-tweq_inv_abbr_neg_sn
-tweq_inv_abbr_pos_bi
-tweq_inv_abbr_pos_sn
-tweq_inv_abbr_pos_x_lifts_y_y
-tweq_inv_abbr_sn
-tweq_inv_abbr_sn_aux
-tweq_inv_abst_sn
-tweq_inv_abst_sn_aux
-tweq_inv_appl_bi
-tweq_inv_appl_sn
-tweq_inv_appl_sn_aux
-tweq_inv_cast_bi
-tweq_inv_cast_sn
-tweq_inv_cast_sn_aux
-tweq_inv_cast_xy_y
-tweq_inv_gref_sn
-tweq_inv_gref_sn_aux
-tweq_inv_lifts_bi
-tweq_inv_lref_sn
-tweq_inv_lref_sn_aux
-tweq_inv_sort_sn
-tweq_inv_sort_sn_aux
-tweq_lifts_bi
-tweq_lifts_dx
-tweq_lifts_sn
-tweq_lref
-tweq_refl
-tweq_repl
-tweq_simple_trans
-tweq_sort
-tweq_sym
-tweq_trans
-tw_le_pair_dx
-tw_pos
-Void
+"aaa"
+"aaa_aaa_inv_appl"
+"aaa_aaa_inv_cast"
+"aaa_abbr"
+"aaa_abst"
+"aaa_appl"
+"aaa_cast"
+"aaa_dec"
+"aaa_feqx_conf"
+"aaa_fqu_conf"
+"aaa_fqup_conf"
+"aaa_fquq_conf"
+"aaa_fqus_conf"
+"aaa_inv_abbr"
+"aaa_inv_abbr_aux"
+"aaa_inv_abst"
+"aaa_inv_abst_aux"
+"aaa_inv_appl"
+"aaa_inv_appl_aux"
+"aaa_inv_cast"
+"aaa_inv_cast_aux"
+"aaa_inv_gref"
+"aaa_inv_gref_aux"
+"aaa_inv_lifts"
+"aaa_inv_lref"
+"aaa_inv_lref_aux"
+"aaa_inv_lref_drops"
+"aaa_inv_sort"
+"aaa_inv_sort_aux"
+"aaa_inv_zero"
+"aaa_inv_zero_aux"
+"aaa_lifts"
+"aaa_lref"
+"aaa_lref_drops"
+"aaa_mono"
+"aaa_pair_inv_lref"
+"aaa_sort"
+"aaa_teqx_conf_reqx"
+"aaa_zero"
+"aarity"
+"AAtom"
+"Abbr"
+"Abst"
+"abst_dec"
+"ac"
+"ac_eq"
+"ac_eq_props"
+"ac_le"
+"acle"
+"acle_eq_le"
+"acle_eq_monotonic_le"
+"acle_le_eq"
+"acle_le_monotonic_le"
+"acle_omega"
+"acle_one"
+"ac_le_props"
+"acle_refl"
+"acle_trans"
+"ac_props"
+"acr"
+"acr_aaa"
+"acr_aaa_csubc_lifts"
+"acr_abst"
+"acr_gcr"
+"acr_lifts"
+"ac_top"
+"ac_top_props"
+"APair"
+"append"
+"append_assoc"
+"append_atom"
+"append_atom_sn"
+"append_bind"
+"append_inj_dx"
+"append_inj_length_dx"
+"append_inj_length_sn"
+"append_inj_sn"
+"append_inv_atom3_sn"
+"append_inv_bind3_sn"
+"append_inv_pair_dx"
+"append_inv_refl_dx"
+"append_length"
+"append_shift"
+"Appl"
+"applv"
+"applv_cons"
+"applv_nil"
+"applv_simple"
+"apply_top"
+"bind"
+"bind1"
+"bind2"
+"Bind2"
+"BPair"
+"BUnit"
+"bw"
+"bw_pos"
+"candidate"
+"Cast"
+"cdeq"
+"cdeq_ext"
+"ceq"
+"ceq_ext"
+"ceq_ext_inv_eq"
+"ceq_ext_refl"
+"ceq_ext_trans"
+"ceq_inv_lift_sn"
+"ceq_lift_sn"
+"cext2"
+"cext2_co"
+"cext2_d_liftable2_sn"
+"cext2_sym"
+"cfull"
+"cfull_dec"
+"cfull_lift_sn"
+"cfun"
+"co_dedropable_sn"
+"co_dedropable_sn_CTC"
+"co_dedropable_sn_ltc"
+"co_dropable_dx"
+"co_dropable_dx_CTC"
+"co_dropable_dx_ltc"
+"co_dropable_sn"
+"co_dropable_sn_CTC"
+"co_dropable_sn_ltc"
+"CP0"
+"CP1"
+"CP2"
+"CP3"
+"d1_liftable_liftable_all"
+"d2_deliftable_sn_CTC"
+"d2_deliftable_sn_ltc"
+"d2_liftable_sn_CTC"
+"d2_liftable_sn_ltc"
+"d_appendable_sn"
+"d_deliftable1"
+"d_deliftable1_isuni"
+"d_deliftable2_bi"
+"d_deliftable2_sn"
+"d_deliftable2_sn_bi"
+"dedropable_sn"
+"dedropable_sn_CTC"
+"deg_inv_prec"
+"deg_inv_pred"
+"deg_iter"
+"deg_next_SO"
+"deg_O"
+"deg_SO"
+"deg_SO_gt"
+"deg_SO_inv_succ"
+"deg_SO_inv_succ_aux"
+"deg_SO_refl"
+"deg_SO_succ"
+"deg_SO_zero"
+"deliftable2_bi"
+"deliftable2_dx"
+"deliftable2_sn"
+"deliftable2_sn_bi"
+"deliftable2_sn_dx"
+"destruct_apair_apair_aux"
+"destruct_lbind_lbind_aux"
+"destruct_sort_sort_aux"
+"destruct_tatom_tatom_aux"
+"destruct_tpair_tpair_aux"
+"discr_apair_xy_x"
+"discr_apair_xy_y"
+"discr_lbind_x_xy"
+"discr_lbind_xy_x"
+"discr_tpair_xy_x"
+"discr_tpair_xy_y"
+"d_liftable1"
+"d_liftable1_all"
+"d_liftable1_isuni"
+"d_liftable2_bi"
+"d_liftable2_sn"
+"d_liftable2_sn_bi"
+"dropable_dx"
+"dropable_dx_CTC"
+"dropable_sn"
+"dropable_sn_CTC"
+"drops"
+"drops_after_fwd_drop2"
+"drops_atom"
+"drops_atom2_sex_conf"
+"drops_atom_F"
+"drops_bind2_fwd_rfw"
+"drops_conf"
+"drops_conf_div"
+"drops_conf_div_bind_isuni"
+"drops_conf_div_fcla"
+"drops_conf_div_isuni"
+"drops_conf_skip1"
+"drops_drop"
+"drops_eq_repl_back"
+"drops_eq_repl_fwd"
+"drops_F"
+"drops_fcla_fwd"
+"drops_fcla_fwd_le2"
+"drops_fcla_fwd_lt2"
+"drops_fcla_fwd_lt4"
+"drops_F_uni"
+"drops_fwd_drop2"
+"drops_fwd_drop2_aux"
+"drops_fwd_fcla"
+"drops_fwd_fcla_le2"
+"drops_fwd_fcla_lt2"
+"drops_fwd_isfin"
+"drops_fwd_isid"
+"drops_fwd_length_eq1"
+"drops_fwd_length_eq2"
+"drops_fwd_length_le4"
+"drops_fwd_lw"
+"drops_fwd_lw_lt"
+"drops_gen"
+"drops_inv_atom1"
+"drops_inv_atom1_aux"
+"drops_inv_atom2"
+"drops_inv_bind1_isuni"
+"drops_inv_bind2_isuni"
+"drops_inv_bind2_isuni_next"
+"drops_inv_drop1"
+"drops_inv_drop1_aux"
+"drops_inv_F"
+"drops_inv_gen"
+"drops_inv_isuni"
+"drops_inv_length_eq"
+"drops_inv_skip1"
+"drops_inv_skip1_aux"
+"drops_inv_skip2"
+"drops_inv_skip2_aux"
+"drops_inv_succ"
+"drops_inv_TF"
+"drops_inv_TF_aux"
+"drops_inv_uni"
+"drops_inv_x_bind_xy"
+"drops_isuni_ex"
+"drops_isuni_fwd_drop2"
+"drops_ldec_dec"
+"drops_lsubc_trans"
+"drops_mono"
+"drops_refl"
+"drops_seq_trans_next"
+"drops_sex_trans_next"
+"drops_sex_trans_push"
+"drops_skip"
+"drops_split_div"
+"drops_split_trans"
+"drops_split_trans_bind2"
+"drops_TF"
+"drops_tls_at"
+"drops_trans"
+"drops_trans_skip2"
+"eq_aarity_dec"
+"eq_bind1_dec"
+"eq_bind2_dec"
+"eq_bind_dec"
+"eq_false_inv_tpair_dx"
+"eq_false_inv_tpair_sn"
+"eq_flat2_dec"
+"eq_genv_dec"
+"eq_item0_dec"
+"eq_item2_dec"
+"eq_lenv_dec"
+"eq_term_dec"
+"ext2"
+"ext2_dec"
+"ext2_inv_pair"
+"ext2_inv_pair_dx"
+"ext2_inv_pair_dx_aux"
+"ext2_inv_pair_sn"
+"ext2_inv_pair_sn_aux"
+"ext2_inv_tc"
+"ext2_inv_unit"
+"ext2_inv_unit_dx"
+"ext2_inv_unit_dx_aux"
+"ext2_inv_unit_sn"
+"ext2_inv_unit_sn_aux"
+"ext2_pair"
+"ext2_refl"
+"ext2_sym"
+"ext2_tc"
+"ext2_tc_inj"
+"ext2_tc_pair"
+"ext2_tc_step"
+"ext2_trans"
+"ext2_unit"
+"f_dedropable_sn"
+"f_dropable_dx"
+"f_dropable_sn"
+"feqx"
+"feqx_canc_dx"
+"feqx_canc_sn"
+"feqx_fqus_trans"
+"feqx_intro_dx"
+"feqx_intro_sn"
+"feqx_inv_gen_dx"
+"feqx_inv_gen_sn"
+"feqx_refl"
+"feqx_sym"
+"feqx_tneqx_repl_dx"
+"feqx_trans"
+"flat2"
+"Flat2"
+"fold"
+"fold_atom"
+"fold_pair"
+"fold_unit"
+"fqu"
+"fqu_bind_dx"
+"fqu_clear"
+"fqu_drop"
+"fqu_flat_dx"
+"fqu_fqup"
+"fqu_fquq"
+"fqu_fwd_fw"
+"fqu_fwd_length_lref1"
+"fqu_fwd_length_lref1_aux"
+"fqu_gref"
+"fqu_inv_atom1"
+"fqu_inv_bind1"
+"fqu_inv_bind1_aux"
+"fqu_inv_bind1_true"
+"fqu_inv_flat1"
+"fqu_inv_flat1_aux"
+"fqu_inv_gref1"
+"fqu_inv_gref1_aux"
+"fqu_inv_gref1_bind"
+"fqu_inv_lref1"
+"fqu_inv_lref1_aux"
+"fqu_inv_lref1_bind"
+"fqu_inv_sort1"
+"fqu_inv_sort1_aux"
+"fqu_inv_sort1_bind"
+"fqu_inv_teqx"
+"fqu_inv_teqx_aux"
+"fqu_inv_zero1_pair"
+"fqu_lref_O"
+"fqu_lref_S"
+"fqup"
+"fqu_pair_sn"
+"fqup_bind_dx"
+"fqup_bind_dx_flat_dx"
+"fqup_clear"
+"fqup_drops_strap1"
+"fqup_drops_succ"
+"fqup_flat_dx"
+"fqup_flat_dx_bind_dx"
+"fqup_flat_dx_pair_sn"
+"fqup_fqus"
+"fqup_fqus_trans"
+"fqup_fwd_fw"
+"fqup_ind"
+"fqup_ind_dx"
+"fqup_inv_step_sn"
+"fqup_lref"
+"fqup_pair_sn"
+"fqup_strap1"
+"fqup_strap2"
+"fqup_trans"
+"fqup_wf_ind"
+"fqup_wf_ind_eq"
+"fqup_zeta"
+"fquq"
+"fquq_fqus"
+"fquq_fwd_fw"
+"fquq_fwd_length_lref1"
+"fquq_refl"
+"fqus"
+"fqus_drops"
+"fqus_fqup_trans"
+"fqus_fwd_fw"
+"fqus_ind"
+"fqus_ind_dx"
+"fqus_inv_atom1"
+"fqus_inv_bind1"
+"fqus_inv_bind1_true"
+"fqus_inv_flat1"
+"fqus_inv_fqup"
+"fqus_inv_fqu_sn"
+"fqus_inv_gref1"
+"fqus_inv_gref1_bind"
+"fqus_inv_lref1"
+"fqus_inv_lref1_bind"
+"fqus_inv_refl_atom3"
+"fqus_inv_sort1"
+"fqus_inv_sort1_bind"
+"fqus_inv_zero1_pair"
+"fqu_sort"
+"fqus_refl"
+"fqus_strap1"
+"fqus_strap1_fqu"
+"fqus_strap2"
+"fqus_strap2_fqu"
+"fqus_trans"
+"fqu_teqx_conf"
+"fqu_wf_ind"
+"frees"
+"frees_append_void"
+"frees_atom"
+"frees_atom_drops"
+"frees_bind"
+"frees_bind_void"
+"frees_eq_repl_back"
+"frees_eq_repl_fwd"
+"frees_flat"
+"frees_fwd_coafter"
+"frees_fwd_isfin"
+"frees_gref"
+"frees_ind_void"
+"frees_inv_append_void"
+"frees_inv_append_void_aux"
+"frees_inv_atom"
+"frees_inv_atom_aux"
+"frees_inv_bind"
+"frees_inv_bind_aux"
+"frees_inv_bind_void"
+"frees_inv_drops_next"
+"frees_inv_flat"
+"frees_inv_flat_aux"
+"frees_inv_gref"
+"frees_inv_gref_aux"
+"frees_inv_lifts"
+"frees_inv_lifts_ex"
+"frees_inv_lifts_SO"
+"frees_inv_lref"
+"frees_inv_lref_aux"
+"frees_inv_lref_drops"
+"frees_inv_pair"
+"frees_inv_pair_aux"
+"frees_inv_sort"
+"frees_inv_sort_aux"
+"frees_inv_unit"
+"frees_inv_unit_aux"
+"frees_lifts"
+"frees_lifts_SO"
+"frees_lref"
+"frees_lref_push"
+"frees_lref_pushs"
+"frees_mono"
+"frees_pair"
+"frees_pair_drops"
+"frees_req_conf"
+"frees_reqx_conf"
+"frees_sex_conf"
+"frees_sort"
+"frees_teqx_conf"
+"frees_teqx_conf_reqx"
+"frees_total"
+"frees_unit"
+"frees_unit_drops"
+"fsge_rex_trans"
+"fsle"
+"fsle_bind"
+"fsle_bind_dx_dx"
+"fsle_bind_dx_sn"
+"fsle_bind_eq"
+"fsle_bind_sn_ge"
+"fsle_flat"
+"fsle_flat_dx_dx"
+"fsle_flat_dx_sn"
+"fsle_flat_sn"
+"fsle_frees_trans"
+"fsle_frees_trans_eq"
+"fsle_fwd_pair_sn"
+"fsle_gref"
+"fsle_gref_bi"
+"fsle_inv_frees_eq"
+"fsle_inv_lifts_sn"
+"fsle_lifts_dx"
+"fsle_lifts_sn"
+"fsle_lifts_SO"
+"fsle_lifts_SO_sn"
+"fsle_pair_bi"
+"fsle_refl"
+"fsle_shift"
+"fsle_sort"
+"fsle_sort_bi"
+"fsle_trans_dx"
+"fsle_trans_rc"
+"fsle_trans_sn"
+"fsle_unit_bi"
+"f_transitive_next"
+"fw"
+"fw_clear"
+"fw_lpair_sn"
+"fw_shift"
+"fw_tpair_dx"
+"fw_tpair_sn"
+"GAtom"
+"gcp"
+"gcp2_all"
+"gcr"
+"gcr_aaa"
+"genv"
+"glength"
+"GPair"
+"GRef"
+"gw"
+"gw_pair"
+"is_apear_dec"
+"is_lifts_dec"
+"item0"
+"item2"
+"LAtom"
+"LBind"
+"length"
+"length_atom"
+"length_bind"
+"length_inv_succ_dx"
+"length_inv_succ_dx_ltail"
+"length_inv_succ_sn"
+"length_inv_succ_sn_ltail"
+"length_inv_zero_dx"
+"length_inv_zero_sn"
+"lenv"
+"lenv_case_tail"
+"lenv_ind_tail"
+"lex"
+"lex_atom"
+"lex_bind"
+"lex_bind_refl_dx"
+"lex_co"
+"lex_conf"
+"lex_confluent"
+"lex_CTC"
+"lex_CTC_ind_dx"
+"lex_CTC_ind_sn"
+"lex_CTC_inj"
+"lex_CTC_step_dx"
+"lex_CTC_step_sn"
+"lex_dropable_dx"
+"lex_dropable_sn"
+"lex_drops_conf_pair"
+"lex_drops_trans_pair"
+"lex_fwd_length"
+"lex_ind"
+"lex_inv_atom_dx"
+"lex_inv_atom_sn"
+"lex_inv_bind_dx"
+"lex_inv_bind_sn"
+"lex_inv_CTC"
+"lex_inv_pair"
+"lex_inv_pair_dx"
+"lex_inv_pair_sn"
+"lex_inv_unit_dx"
+"lex_inv_unit_sn"
+"lex_liftable_dedropable_sn"
+"lex_pair"
+"lex_refl"
+"lex_trans"
+"lex_transitive"
+"lex_unit"
+"liftable2_bi"
+"liftable2_dx"
+"liftable2_sn"
+"liftable2_sn_bi"
+"liftable2_sn_dx"
+"lifts"
+"lifts_applv"
+"liftsb"
+"liftsb_conf"
+"liftsb_div3"
+"liftsb_eq_repl_back"
+"liftsb_fwd_bw"
+"liftsb_fwd_isid"
+"lifts_bind"
+"liftsb_inj"
+"liftsb_inv_pair_dx"
+"liftsb_inv_pair_sn"
+"liftsb_inv_unit_dx"
+"liftsb_inv_unit_sn"
+"liftsb_mono"
+"liftsb_refl"
+"liftsb_split_trans"
+"liftsb_total"
+"liftsb_trans"
+"lifts_conf"
+"lifts_div3"
+"lifts_div4"
+"lifts_div4_one"
+"lifts_eq_repl_back"
+"lifts_eq_repl_fwd"
+"lifts_flat"
+"lifts_fwd_isid"
+"lifts_fwd_pair1"
+"lifts_fwd_pair2"
+"lifts_fwd_tw"
+"lifts_gref"
+"lifts_inj"
+"lifts_inv_applv1"
+"lifts_inv_applv2"
+"lifts_inv_atom1"
+"lifts_inv_atom2"
+"lifts_inv_bind1"
+"lifts_inv_bind1_aux"
+"lifts_inv_bind2"
+"lifts_inv_bind2_aux"
+"lifts_inv_flat1"
+"lifts_inv_flat1_aux"
+"lifts_inv_flat2"
+"lifts_inv_flat2_aux"
+"lifts_inv_gref1"
+"lifts_inv_gref1_aux"
+"lifts_inv_gref2"
+"lifts_inv_gref2_aux"
+"lifts_inv_lref1"
+"lifts_inv_lref1_aux"
+"lifts_inv_lref1_uni"
+"lifts_inv_lref2"
+"lifts_inv_lref2_aux"
+"lifts_inv_lref2_uni"
+"lifts_inv_lref2_uni_ge"
+"lifts_inv_lref2_uni_lt"
+"lifts_inv_pair_xy_x"
+"lifts_inv_pair_xy_y"
+"lifts_inv_push_succ_sn"
+"lifts_inv_push_zero_sn"
+"lifts_inv_sort1"
+"lifts_inv_sort1_aux"
+"lifts_inv_sort2"
+"lifts_inv_sort2_aux"
+"lifts_lref"
+"lifts_lref_ge"
+"lifts_lref_ge_minus"
+"lifts_lref_lt"
+"lifts_lref_uni"
+"lifts_mono"
+"lifts_push_lref"
+"lifts_push_zero"
+"lifts_refl"
+"lifts_simple_dx"
+"lifts_simple_sn"
+"lifts_sort"
+"lifts_split_div"
+"lifts_split_trans"
+"lifts_total"
+"lifts_trans"
+"lifts_trans4_one"
+"lifts_trans_uni"
+"lifts_uni"
+"liftsv"
+"liftsv_cons"
+"liftsv_inj"
+"liftsv_inv_cons1"
+"liftsv_inv_cons1_aux"
+"liftsv_inv_cons2"
+"liftsv_inv_cons2_aux"
+"liftsv_inv_nil1"
+"liftsv_inv_nil1_aux"
+"liftsv_inv_nil2"
+"liftsv_inv_nil2_aux"
+"liftsv_mono"
+"liftsv_nil"
+"liftsv_split_trans"
+"liftsv_total"
+"liftsv_trans"
+"LRef"
+"lsuba"
+"lsuba_aaa_conf"
+"lsuba_aaa_trans"
+"lsuba_atom"
+"lsuba_beta"
+"lsuba_bind"
+"lsuba_drops_conf_isuni"
+"lsuba_drops_trans_isuni"
+"lsuba_fwd_lsubr"
+"lsuba_inv_atom1"
+"lsuba_inv_atom1_aux"
+"lsuba_inv_atom2"
+"lsuba_inv_atom2_aux"
+"lsuba_inv_bind1"
+"lsuba_inv_bind1_aux"
+"lsuba_inv_bind2"
+"lsuba_inv_bind2_aux"
+"lsuba_lsubc"
+"lsuba_refl"
+"lsuba_trans"
+"lsubc"
+"lsubc_atom"
+"lsubc_beta"
+"lsubc_bind"
+"lsubc_drops_trans_isuni"
+"lsubc_fwd_lsubr"
+"lsubc_inv_atom1"
+"lsubc_inv_atom1_aux"
+"lsubc_inv_atom2"
+"lsubc_inv_atom2_aux"
+"lsubc_inv_bind1"
+"lsubc_inv_bind1_aux"
+"lsubc_inv_bind2"
+"lsubc_inv_bind2_aux"
+"lsubc_refl"
+"lsubf"
+"lsubf_atom"
+"lsubf_beta"
+"lsubf_beta_tl_dx"
+"lsubf_bind"
+"lsubf_bind_tl_dx"
+"lsubf_eq_repl_back1"
+"lsubf_eq_repl_back2"
+"lsubf_eq_repl_fwd1"
+"lsubf_eq_repl_fwd2"
+"lsubf_frees_trans"
+"lsubf_fwd_bind_tl"
+"lsubf_fwd_isid_dx"
+"lsubf_fwd_isid_sn"
+"lsubf_fwd_lsubr_isdiv"
+"lsubf_fwd_sle"
+"lsubf_inv_atom"
+"lsubf_inv_atom1"
+"lsubf_inv_atom1_aux"
+"lsubf_inv_atom2"
+"lsubf_inv_atom2_aux"
+"lsubf_inv_beta_sn"
+"lsubf_inv_bind_sn"
+"lsubf_inv_pair1"
+"lsubf_inv_pair1_aux"
+"lsubf_inv_pair2"
+"lsubf_inv_pair2_aux"
+"lsubf_inv_push1"
+"lsubf_inv_push1_aux"
+"lsubf_inv_push2"
+"lsubf_inv_push2_aux"
+"lsubf_inv_push_sn"
+"lsubf_inv_refl"
+"lsubf_inv_sor_dx"
+"lsubf_inv_unit1"
+"lsubf_inv_unit1_aux"
+"lsubf_inv_unit2"
+"lsubf_inv_unit2_aux"
+"lsubf_inv_unit_sn"
+"lsubf_push"
+"lsubf_refl"
+"lsubf_refl_eq"
+"lsubf_sor"
+"lsubf_unit"
+"lsubr"
+"lsubr_atom"
+"lsubr_beta"
+"lsubr_bind"
+"lsubr_fwd_bind1"
+"lsubr_fwd_bind2"
+"lsubr_fwd_drops2_abbr"
+"lsubr_fwd_drops2_bind"
+"lsubr_fwd_length"
+"lsubr_inv_abbr2"
+"lsubr_inv_abst1"
+"lsubr_inv_abst2"
+"lsubr_inv_atom1"
+"lsubr_inv_atom1_aux"
+"lsubr_inv_atom2"
+"lsubr_inv_atom2_aux"
+"lsubr_inv_bind1"
+"lsubr_inv_bind1_aux"
+"lsubr_inv_bind2"
+"lsubr_inv_bind2_aux"
+"lsubr_inv_pair2"
+"lsubr_inv_unit1"
+"lsubr_inv_unit2"
+"lsubr_lsubf"
+"lsubr_lsubf_isid"
+"lsubr_refl"
+"lsubr_trans"
+"lsubr_unit"
+"ltail_length"
+"lveq"
+"lveq_atom"
+"lveq_bind"
+"lveq_fwd_abst_bind_length_le"
+"lveq_fwd_bind_abst_length_le"
+"lveq_fwd_gen"
+"lveq_fwd_length"
+"lveq_fwd_length_eq"
+"lveq_fwd_length_le_dx"
+"lveq_fwd_length_le_sn"
+"lveq_fwd_length_minus"
+"lveq_fwd_length_plus"
+"lveq_fwd_pair_dx"
+"lveq_fwd_pair_sn"
+"lveq_inj"
+"lveq_inj_length"
+"lveq_inj_void_dx_le"
+"lveq_inj_void_sn_ge"
+"lveq_inv_atom_atom"
+"lveq_inv_atom_bind"
+"lveq_inv_bind"
+"lveq_inv_bind_atom"
+"lveq_inv_bind_O"
+"lveq_inv_pair_pair"
+"lveq_inv_succ"
+"lveq_inv_succ_aux"
+"lveq_inv_succ_dx"
+"lveq_inv_succ_sn"
+"lveq_inv_succ_sn_aux"
+"lveq_inv_void_dx_length"
+"lveq_inv_void_sn_length"
+"lveq_inv_void_succ_dx"
+"lveq_inv_void_succ_sn"
+"lveq_inv_zero"
+"lveq_inv_zero_aux"
+"lveq_length_eq"
+"lveq_length_fwd_dx"
+"lveq_length_fwd_sn"
+"lveq_refl"
+"lveq_sym"
+"lveq_void_dx"
+"lveq_void_sn"
+"lw"
+"lw_bind"
+"mk_ac"
+"mk_ac_props"
+"mk_gcp"
+"mk_gcr"
+"mk_sd"
+"mk_sd_props"
+"mk_sh"
+"mk_sh_acyclic"
+"mk_sh_decidable"
+"mk_sh_lt"
+"nexts_le"
+"nexts_lt"
+"nf"
+"R_confluent2_rex"
+"req"
+"req_feqx_trans"
+"req_fsle_comp"
+"req_fwd_rex"
+"req_inv_bind"
+"req_inv_flat"
+"req_inv_lifts_bi"
+"req_inv_lref_bind_dx"
+"req_inv_lref_bind_sn"
+"req_inv_zero_pair_dx"
+"req_inv_zero_pair_sn"
+"req_refl"
+"req_reqx"
+"req_reqx_trans"
+"req_rex_trans"
+"req_transitive"
+"reqx"
+"reqx_atom"
+"reqx_bind"
+"reqx_bind_repl_dx"
+"reqx_bind_void"
+"reqx_canc_dx"
+"reqx_canc_sn"
+"reqx_dec"
+"reqx_flat"
+"reqx_fqup_trans"
+"reqx_fquq_trans"
+"reqx_fqus_trans"
+"reqx_fqu_trans"
+"reqx_fsge_comp"
+"reqx_fwd_bind_dx"
+"reqx_fwd_bind_dx_void"
+"reqx_fwd_dx"
+"reqx_fwd_flat_dx"
+"reqx_fwd_length"
+"reqx_fwd_pair_sn"
+"reqx_fwd_zero_pair"
+"reqx_gref"
+"reqx_gref_length"
+"reqx_inv_atom_dx"
+"reqx_inv_atom_sn"
+"reqx_inv_bind"
+"reqx_inv_bind_void"
+"reqx_inv_flat"
+"reqx_inv_lifts_bi"
+"reqx_inv_lifts_dx"
+"reqx_inv_lifts_sn"
+"reqx_inv_lref"
+"reqx_inv_lref_bind_dx"
+"reqx_inv_lref_bind_sn"
+"reqx_inv_lref_pair_bi"
+"reqx_inv_lref_pair_dx"
+"reqx_inv_lref_pair_sn"
+"reqx_inv_zero"
+"reqx_inv_zero_pair_dx"
+"reqx_inv_zero_pair_sn"
+"reqx_lifts_bi"
+"reqx_lifts_sn"
+"reqx_lref"
+"reqx_pair"
+"reqx_pair_refl"
+"reqx_refl"
+"reqx_repl"
+"reqx_rneqx_trans"
+"reqx_sort"
+"reqx_sort_length"
+"reqx_sym"
+"reqx_trans"
+"reqx_unit"
+"reqx_unit_length"
+"rex"
+"rex_atom"
+"rex_bind"
+"rex_bind_dx_split"
+"rex_bind_dx_split_void"
+"rex_bind_repl_dx"
+"rex_bind_void"
+"rex_co"
+"rex_conf"
+"rex_confluent"
+"rex_dec"
+"rex_dropable_dx"
+"rex_dropable_sn"
+"rex_flat"
+"rex_flat_dx_split"
+"rex_fsge_compatible"
+"rex_fsle_compatible"
+"rex_fwd_bind_dx"
+"rex_fwd_bind_dx_void"
+"rex_fwd_dx"
+"rex_fwd_flat_dx"
+"rex_fwd_length"
+"rex_fwd_pair_sn"
+"rex_fwd_zero_pair"
+"rex_gref"
+"rex_gref_length"
+"rex_inv_atom_dx"
+"rex_inv_atom_sn"
+"rex_inv_bind"
+"rex_inv_bind_void"
+"rex_inv_flat"
+"rex_inv_frees"
+"rex_inv_gref"
+"rex_inv_gref_bind_dx"
+"rex_inv_gref_bind_sn"
+"rex_inv_lex_req"
+"rex_inv_lifts_bi"
+"rex_inv_lref"
+"rex_inv_lref_bind_dx"
+"rex_inv_lref_bind_sn"
+"rex_inv_lref_pair_bi"
+"rex_inv_lref_pair_dx"
+"rex_inv_lref_pair_sn"
+"rex_inv_lref_unit_dx"
+"rex_inv_lref_unit_sn"
+"rex_inv_sort"
+"rex_inv_sort_bind_dx"
+"rex_inv_sort_bind_sn"
+"rex_inv_zero"
+"rex_inv_zero_length"
+"rex_inv_zero_pair_dx"
+"rex_inv_zero_pair_sn"
+"rex_inv_zero_unit_dx"
+"rex_inv_zero_unit_sn"
+"rex_isid"
+"rex_lex"
+"rex_liftable_dedropable_sn"
+"rex_lifts_bi"
+"rex_lref"
+"rex_pair"
+"rex_pair_refl"
+"rex_pair_sn_split"
+"rex_refl"
+"rexs"
+"rexs_atom"
+"rexs_co"
+"rexs_fwd_bind_dx"
+"rexs_fwd_bind_dx_void"
+"rexs_fwd_flat_dx"
+"rexs_fwd_length"
+"rexs_fwd_pair_sn"
+"rexs_gref"
+"rexs_ind_dx"
+"rexs_ind_sn"
+"rexs_inv_atom_dx"
+"rexs_inv_atom_sn"
+"rexs_inv_bind"
+"rexs_inv_bind_void"
+"rexs_inv_flat"
+"rexs_inv_gref"
+"rexs_inv_gref_bind_dx"
+"rexs_inv_gref_bind_sn"
+"rexs_inv_lex_req"
+"rexs_inv_sort"
+"rexs_inv_sort_bind_dx"
+"rexs_inv_sort_bind_sn"
+"rexs_lex"
+"rexs_lex_req"
+"rexs_lref"
+"rex_sort"
+"rex_sort_length"
+"rexs_pair"
+"rexs_pair_refl"
+"rexs_refl"
+"rexs_sort"
+"rexs_step_dx"
+"rexs_step_sn"
+"rexs_sym"
+"rexs_tc"
+"rexs_trans"
+"rexs_unit"
+"rex_sym"
+"rex_trans_fsle"
+"rex_transitive"
+"rex_trans_next"
+"rex_unit"
+"rex_unit_length"
+"rex_unit_sn"
+"R_fsge_compatible"
+"rfw"
+"rfw_clear"
+"rfw_lpair_dx"
+"rfw_lpair_sn"
+"rfw_shift"
+"rfw_tpair_dx"
+"rfw_tpair_sn"
+"rneqx_inv_bind"
+"rneqx_inv_bind_void"
+"rneqx_inv_flat"
+"rneqx_reqx_canc_dx"
+"rneqx_reqx_div"
+"rnex_inv_bind"
+"rnex_inv_bind_void"
+"rnex_inv_flat"
+"R_pw_confluent2_sex"
+"S1"
+"S2"
+"S3"
+"S5"
+"S6"
+"S7"
+"sd"
+"sd_d"
+"sd_d_correct"
+"sd_d_props"
+"sd_d_SS"
+"sd_O"
+"sd_O_props"
+"sd_props"
+"sd_SO"
+"sd_SO_props"
+"seq"
+"seq_canc_dx"
+"seq_canc_sn"
+"seq_co_dedropable_sn"
+"seq_co_dropable_dx"
+"seq_co_dropable_sn"
+"seq_drops_conf_next"
+"seq_drops_trans_next"
+"seq_eq_repl_back"
+"seq_eq_repl_fwd"
+"seq_fwd_length"
+"seq_inv_atom1"
+"seq_inv_atom2"
+"seq_inv_next"
+"seq_inv_next1"
+"seq_inv_next2"
+"seq_inv_push"
+"seq_inv_push1"
+"seq_inv_push2"
+"seq_inv_tl"
+"seq_join"
+"seq_meet"
+"seq_refl"
+"seq_sym"
+"seq_trans"
+"sex"
+"sex_atom"
+"sex_canc_dx"
+"sex_canc_sn"
+"sex_co"
+"sex_co_dropable_dx"
+"sex_co_dropable_sn"
+"sex_co_isid"
+"sex_conf"
+"sex_dec"
+"sex_dropable_dx_aux"
+"sex_drops_conf_next"
+"sex_drops_conf_push"
+"sex_drops_trans_next"
+"sex_drops_trans_push"
+"sex_eq_repl_back"
+"sex_eq_repl_fwd"
+"sex_fwd_bind"
+"sex_fwd_length"
+"sex_inv_atom1"
+"sex_inv_atom1_aux"
+"sex_inv_atom2"
+"sex_inv_atom2_aux"
+"sex_inv_next"
+"sex_inv_next1"
+"sex_inv_next1_aux"
+"sex_inv_next2"
+"sex_inv_next2_aux"
+"sex_inv_push"
+"sex_inv_push1"
+"sex_inv_push1_aux"
+"sex_inv_push2"
+"sex_inv_push2_aux"
+"sex_inv_tc_dx"
+"sex_inv_tc_sn"
+"sex_inv_tl"
+"sex_join"
+"sex_length_cfull"
+"sex_length_isid"
+"sex_liftable_co_dedropable_bi"
+"sex_liftable_co_dedropable_sn"
+"sex_meet"
+"sex_next"
+"sex_pair_repl"
+"sex_push"
+"sex_refl"
+"sex_sdj"
+"sex_sdj_split"
+"sex_sle_split"
+"sex_sym"
+"sex_tc_dx"
+"sex_tc_inj_dx"
+"sex_tc_inj_sn"
+"sex_tc_next"
+"sex_tc_next_dx"
+"sex_tc_next_sn"
+"sex_tc_push"
+"sex_tc_push_dx"
+"sex_tc_push_sn"
+"sex_tc_refl"
+"sex_tc_step_dx"
+"sex_trans"
+"sex_trans_gen"
+"sex_trans_id_cfull"
+"sex_transitive"
+"sh"
+"sh_acyclic"
+"sh_decidable"
+"sh_lt"
+"sh_lt_acyclic"
+"sh_lt_dec"
+"sh_lt_nexts_inv_lt"
+"simple"
+"simple_atom"
+"simple_dec_ex"
+"simple_flat"
+"simple_inv_bind"
+"simple_inv_bind_aux"
+"simple_inv_pair"
+"simple_teqo_repl_dx"
+"simple_teqo_repl_sn"
+"sle_seq_trans"
+"sle_sex_conf"
+"sle_sex_trans"
+"Sort"
+"s_rs_transitive_isid"
+"s_rs_transitive_lex_inv_isid"
+"TAtom"
+"tc_f_dedropable_sn"
+"tc_f_dropable_dx"
+"tc_f_dropable_sn"
+"teqo"
+"teqo_canc_dx"
+"teqo_canc_sn"
+"teqo_dec"
+"teqo_gref"
+"teqo_inv_applv_bind_simple"
+"teqo_inv_gref1"
+"teqo_inv_gref1_aux"
+"teqo_inv_lifts_bi"
+"teqo_inv_lref1"
+"teqo_inv_lref1_aux"
+"teqo_inv_pair"
+"teqo_inv_pair1"
+"teqo_inv_pair1_aux"
+"teqo_inv_pair2"
+"teqo_inv_pair2_aux"
+"teqo_inv_sort1"
+"teqo_inv_sort1_aux"
+"teqo_lifts_bi"
+"teqo_lifts_dx"
+"teqo_lifts_sn"
+"teqo_lref"
+"teqo_pair"
+"teqo_refl"
+"teqo_sort"
+"teqo_sym"
+"teqo_trans"
+"teqx"
+"teqx_canc_dx"
+"teqx_canc_sn"
+"teqx_dec"
+"teqx_ext"
+"teqx_feqx"
+"teqx_fqup_trans"
+"teqx_fquq_trans"
+"teqx_fqus_trans"
+"teqx_fqu_trans"
+"teqx_fwd_atom1"
+"teqx_gref"
+"teqx_inv_gref1"
+"teqx_inv_gref1_aux"
+"teqx_inv_lifts_bi"
+"teqx_inv_lifts_dx"
+"teqx_inv_lifts_sn"
+"teqx_inv_lref1"
+"teqx_inv_lref1_aux"
+"teqx_inv_pair"
+"teqx_inv_pair1"
+"teqx_inv_pair1_aux"
+"teqx_inv_pair2"
+"teqx_inv_pair_xy_x"
+"teqx_inv_pair_xy_y"
+"teqx_inv_sort1"
+"teqx_inv_sort1_aux"
+"teqx_inv_sort2"
+"teqx_lifts_bi"
+"teqx_lifts_dx"
+"teqx_lifts_inv_pair_sn"
+"teqx_lifts_sn"
+"teqx_lref"
+"teqx_pair"
+"teqx_refl"
+"teqx_repl"
+"teqx_reqx_conf"
+"teqx_reqx_div"
+"teqx_rex_conf"
+"teqx_rex_div"
+"teqx_sort"
+"teqx_sym"
+"teqx_teqo"
+"teqx_tneqx_trans"
+"teqx_trans"
+"teqx_tweq"
+"term"
+"tneqx_inv_pair"
+"tneqx_teqx_canc_dx"
+"TPair"
+"tw"
+"tweq"
+"tweq_abbr"
+"tweq_abbr_neg"
+"tweq_abbr_pos"
+"tweq_abst"
+"tweq_appl"
+"tweq_canc_dx"
+"tweq_canc_sn"
+"tweq_cast"
+"tweq_dec"
+"tweq_fwd_pair_bi"
+"tweq_fwd_pair_sn"
+"tweq_gref"
+"tweq_inv_abbr_neg_sn"
+"tweq_inv_abbr_pos_bi"
+"tweq_inv_abbr_pos_sn"
+"tweq_inv_abbr_pos_x_lifts_y_y"
+"tweq_inv_abbr_sn"
+"tweq_inv_abbr_sn_aux"
+"tweq_inv_abst_sn"
+"tweq_inv_abst_sn_aux"
+"tweq_inv_appl_bi"
+"tweq_inv_appl_sn"
+"tweq_inv_appl_sn_aux"
+"tweq_inv_cast_bi"
+"tweq_inv_cast_sn"
+"tweq_inv_cast_sn_aux"
+"tweq_inv_cast_xy_y"
+"tweq_inv_gref_sn"
+"tweq_inv_gref_sn_aux"
+"tweq_inv_lifts_bi"
+"tweq_inv_lref_sn"
+"tweq_inv_lref_sn_aux"
+"tweq_inv_sort_sn"
+"tweq_inv_sort_sn_aux"
+"tweq_lifts_bi"
+"tweq_lifts_dx"
+"tweq_lifts_sn"
+"tweq_lref"
+"tweq_refl"
+"tweq_repl"
+"tweq_simple_trans"
+"tweq_sort"
+"tweq_sym"
+"tweq_trans"
+"tw_le_pair_dx"
+"tw_pos"
+"Void"