X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2A%2Fnames.txt;h=2f23d0fda57d72087ebf2acf24e9a04c5958037d;hb=8f1a123e61ff079b1f9ad63cc915470ec7e6abf3;hp=25e865b6f320ca89ebd457dfbfa6cdae80398d6b;hpb=076439def28e649ec384fae038ed021dadd5f75c;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2A/names.txt b/matita/matita/contribs/lambdadelta/basic_2A/names.txt
index 25e865b6f..2f23d0fda 100644
--- a/matita/matita/contribs/lambdadelta/basic_2A/names.txt
+++ b/matita/matita/contribs/lambdadelta/basic_2A/names.txt
@@ -1,1919 +1,1919 @@
-aaa
-aaa_abbr
-aaa_abst
-aaa_appl
-aaa_cast
-aaa_csx
-aaa_da
-aaa_fqu_conf
-aaa_fqup_conf
-aaa_fquq_conf
-aaa_fqus_conf
-aaa_fsb
-aaa_fsba
-aaa_ind_csx
-aaa_ind_csx_alt
-aaa_ind_csx_alt_aux
-aaa_ind_csx_aux
-aaa_ind_fpb
-aaa_ind_fpb_aux
-aaa_ind_fpbg
-aaa_ind_fpbg_aux
-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_lift
-aaa_inv_lref
-aaa_inv_lref_aux
-aaa_inv_sort
-aaa_inv_sort_aux
-aaa_lift
-aaa_lifts
-aaa_lleq_conf
-aaa_lref
-aaa_lstas
-aaa_mono
-aaa_sort
-aarity
-AAtom
-Abbr
-Abst
-acr
-acr_aaa
-acr_aaa_csubc_lifts
-acr_abst
-acr_gcr
-APair
-append
-append_assoc
-append_atom_sn
-append_inj_dx
-append_inj_sn
-append_inv_pair_dx
-append_inv_refl_dx
-append_length
-Appl
-ApplDelta
-ApplDelta_lift
-ApplOmega1
-ApplOmega2
-ApplOmega3
-applv
-applv_simple
-at
-at_ge
-at_inv_cons
-at_inv_cons_aux
-at_inv_cons_ge
-at_inv_cons_lt
-at_inv_nil
-at_inv_nil_aux
-at_lt
-at_mono
-at_nil
-bind2
-Bind2
-candidate
-Cast
-ceq
-cfun
-cir
-cir_appl
-cir_cnr
-cir_gref
-cir_ib2
-cir_inv_appl
-cir_inv_bind
-cir_inv_delta
-cir_inv_flat
-cir_inv_ib2
-cir_inv_lift
-cir_inv_ri2
-cir_lift
-cir_sort
-cix
-cix_appl
-cix_cnx
-cix_gref
-cix_ib2
-cix_inv_appl
-cix_inv_bind
-cix_inv_cir
-cix_inv_delta
-cix_inv_flat
-cix_inv_ib2
-cix_inv_lift
-cix_inv_ri2
-cix_inv_sort
-cix_lift
-cix_lref
-cix_sort
-cnr
-cnr_abst
-cnr_appl_simple
-cnr_dec
-cnr_inv_abbr
-cnr_inv_abst
-cnr_inv_appl
-cnr_inv_cir
-cnr_inv_crr
-cnr_inv_delta
-cnr_inv_eps
-cnr_inv_lift
-cnr_inv_zeta
-cnr_lift
-cnr_lref_abst
-cnr_lref_atom
-cnr_lref_free
-cnr_sort
-cnx
-cnx_abst
-cnx_appl_simple
-cnx_csx
-cnx_dec
-cnx_fwd_cnr
-cnx_inv_abbr
-cnx_inv_abst
-cnx_inv_appl
-cnx_inv_cix
-cnx_inv_crx
-cnx_inv_delta
-cnx_inv_eps
-cnx_inv_lift
-cnx_inv_sort
-cnx_inv_zeta
-cnx_lift
-cnx_lref_atom
-cnx_lref_free
-cnx_sort
-cnx_sort_iter
-CP0
-CP1
-CP2
-CP3
-cpc
-cpc_conf
-cpc_cpcs
-cpc_fwd_cpr
-cpc_refl
-cpcs
-cpcs_aaa_mono
-cpcs_bind1
-cpcs_bind2
-cpcs_bind_dx
-cpcs_bind_sn
-cpcs_canc_dx
-cpcs_canc_sn
-cpcs_cpr_conf
-cpcs_cpr_div
-cpcs_cprs_conf
-cpcs_cprs_div
-cpcs_cprs_dx
-cpcs_cprs_sn
-cpcs_cprs_strap1
-cpcs_cprs_strap2
-cpcs_cpr_strap1
-cpcs_cpr_strap2
-cpcs_flat
-cpcs_flat_dx_cpr_rev
-cpcs_ind
-cpcs_ind_dx
-cpcs_inv_abst1
-cpcs_inv_abst2
-cpcs_inv_abst_dx
-cpcs_inv_abst_sn
-cpcs_inv_cprs
-cpcs_inv_lift
-cpcs_inv_sort
-cpcs_inv_sort_abst
-cpcs_lift
-cpcs_refl
-cpcs_scpes
-cpcs_strap1
-cpcs_strap2
-cpcs_strip
-cpcs_sym
-cpcs_trans
-cpc_sym
-cpr
-cpr_aaa_conf
-cpr_ApplOmega_12
-cpr_ApplOmega_23
-cpr_atom
-cpr_beta
-cpr_bind
-cpr_bind2
-cpr_conf
-cpr_conf_lpr
-cpr_conf_lpr_atom_atom
-cpr_conf_lpr_atom_delta
-cpr_conf_lpr_beta_beta
-cpr_conf_lpr_bind_bind
-cpr_conf_lpr_bind_zeta
-cpr_conf_lpr_delta_delta
-cpr_conf_lpr_eps_eps
-cpr_conf_lpr_flat_beta
-cpr_conf_lpr_flat_eps
-cpr_conf_lpr_flat_flat
-cpr_conf_lpr_flat_theta
-cpr_conf_lpr_theta_theta
-cpr_conf_lpr_zeta_zeta
-cpr_cpcs_dx
-cpr_cpcs_sn
-cpr_cprs
-cpr_cprs_conf_cpcs
-cpr_cprs_div
-cpr_cpx
-cpr_delift
-cpr_delta
-cpr_div
-cpre
-cpre_mono
-cpr_eps
-cpr_flat
-cpr_fpb
-cpr_fpbq
-cpr_fwd_bind1_minus
-cpr_fwd_cir
-cpr_inv_abbr1
-cpr_inv_abst1
-cpr_inv_appl1
-cpr_inv_appl1_simple
-cpr_inv_atom1
-cpr_inv_atom1_aux
-cpr_inv_bind1
-cpr_inv_bind1_aux
-cpr_inv_cast1
-cpr_inv_flat1
-cpr_inv_flat1_aux
-cpr_inv_gref1
-cpr_inv_lift1
-cpr_inv_lref1
-cpr_inv_sort1
-cpr_lift
-cpr_llpx_sn_conf
-cpr_lpr_fpbs
-cpr_lpr_sta_fpbs
-cpr_Omega_12
-cpr_Omega_21
-cpr_pair_sn
-cpr_refl
-cprs
-cprs_aaa_conf
-cprs_beta
-cprs_beta_dx
-cprs_beta_rc
-cprs_bind
-cprs_bind2
-cprs_bind2_dx
-cprs_bind_dx
-cprs_conf
-cprs_conf_cpcs
-cprs_cpr_conf_cpcs
-cprs_cpr_div
-cprs_cpxs
-cprs_delta
-cprs_div
-cprs_eps
-cprs_flat
-cprs_flat_dx
-cprs_flat_sn
-cprs_fpbs
-cprs_ind
-cprs_ind_dx
-cprs_inv_abbr1
-cprs_inv_abst
-cprs_inv_abst1
-cprs_inv_appl1
-cprs_inv_cast1
-cprs_inv_cnr1
-cprs_inv_lift1
-cprs_inv_lref1
-cprs_inv_sort1
-cprs_lift
-cprs_lpr_conf_dx
-cprs_lpr_conf_sn
-cprs_refl
-cprs_scpds_div
-cprs_strap1
-cprs_strap2
-cprs_strip
-cprs_theta
-cprs_theta_dx
-cprs_theta_rc
-cprs_trans
-cprs_zeta
-cpr_theta
-cpr_zeta
-cpx
-cpx_aaa_conf
-cpx_atom
-cpx_beta
-cpx_bind
-cpx_bind2
-cpx_cpxs
-cpx_ct
-cpx_delift
-cpx_delta
-cpxe
-cpx_eps
-cpx_flat
-cpx_frees_trans
-cpx_fwd_bind1_minus
-cpx_fwd_cix
-cpx_inv_abbr1
-cpx_inv_abst1
-cpx_inv_appl1
-cpx_inv_appl1_simple
-cpx_inv_atom1
-cpx_inv_atom1_aux
-cpx_inv_bind1
-cpx_inv_bind1_aux
-cpx_inv_cast1
-cpx_inv_flat1
-cpx_inv_flat1_aux
-cpx_inv_gref1
-cpx_inv_lift1
-cpx_inv_lref1
-cpx_inv_lref1_ge
-cpx_inv_sort1
-cpx_lift
-cpx_lleq_conf
-cpx_lleq_conf_dx
-cpx_lleq_conf_sn
-cpx_llpx_sn_conf
-cpx_lpx_aaa_conf
-cpx_pair_sn
-cpx_refl
-cpxs
-cpxs_aaa_conf
-cpxs_ApplOmega_13
-cpxs_beta
-cpxs_beta_dx
-cpxs_beta_rc
-cpxs_bind
-cpxs_bind2
-cpxs_bind2_dx
-cpxs_bind_dx
-cpxs_ct
-cpxs_delta
-cpxs_eps
-cpxs_flat
-cpxs_flat_dx
-cpxs_flat_sn
-cpxs_fpbg
-cpxs_fpbs
-cpxs_fpbs_trans
-cpxs_fqup_fpbs
-cpxs_fqus_fpbs
-cpxs_fqus_lpxs_fpbs
-cpxs_fwd_beta
-cpxs_fwd_beta_vector
-cpxs_fwd_cast
-cpxs_fwd_cast_vector
-cpxs_fwd_cnx
-cpxs_fwd_cnx_vector
-cpxs_fwd_delta
-cpxs_fwd_delta_vector
-cpxs_fwd_sort
-cpxs_fwd_sort_vector
-cpxs_fwd_theta
-cpxs_fwd_theta_vector
-cpxs_ind
-cpxs_ind_dx
-cpxs_inv_abbr1
-cpxs_inv_abst1
-cpxs_inv_appl1
-cpxs_inv_cast1
-cpxs_inv_cnx1
-cpxs_inv_lift1
-cpxs_inv_lref1
-cpxs_inv_sort1
-cpxs_lift
-cpxs_lleq_conf
-cpxs_lleq_conf_dx
-cpxs_lleq_conf_sn
-cpxs_neq_inv_step_sn
-cpxs_pair_sn
-cpxs_refl
-cpxs_sort
-cpxs_strap1
-cpxs_strap2
-cpx_st
-cpxs_theta
-cpxs_theta_dx
-cpxs_theta_rc
-cpxs_trans
-cpxs_zeta
-cpx_theta
-cpx_zeta
-cpy
-cpy_atom
-cpy_bind
-cpy_conf_eq
-cpy_conf_neq
-cpy_cpys
-cpy_flat
-cpy_full
-cpy_fwd_nlift2_ge
-cpy_fwd_tw
-cpy_fwd_up
-cpy_inv_atom1
-cpy_inv_atom1_aux
-cpy_inv_bind1
-cpy_inv_bind1_aux
-cpy_inv_flat1
-cpy_inv_flat1_aux
-cpy_inv_gref1
-cpy_inv_lift1_be
-cpy_inv_lift1_be_up
-cpy_inv_lift1_eq
-cpy_inv_lift1_ge
-cpy_inv_lift1_ge_up
-cpy_inv_lift1_le
-cpy_inv_lift1_le_up
-cpy_inv_lref1
-cpy_inv_refl_O2
-cpy_inv_refl_O2_aux
-cpy_inv_sort1
-cpy_lift_be
-cpy_lift_ge
-cpy_lift_le
-cpy_refl
-cpys
-cpysa
-cpysa_atom
-cpysa_bind
-cpysa_cpy_trans
-cpysa_flat
-cpysa_inv_cpys
-cpys_antisym_eq
-cpysa_refl
-cpysa_subst
-cpys_bind
-cpys_conf_eq
-cpys_conf_neq
-cpys_cpysa
-cpys_flat
-cpys_fwd_tw
-cpys_fwd_up
-cpys_ind
-cpys_ind_alt
-cpys_ind_dx
-cpys_inv_atom1
-cpys_inv_bind1
-cpys_inv_flat1
-cpys_inv_gref1
-cpys_inv_lift1_be
-cpys_inv_lift1_be_up
-cpys_inv_lift1_eq
-cpys_inv_lift1_ge
-cpys_inv_lift1_ge_up
-cpys_inv_lift1_le
-cpys_inv_lift1_le_up
-cpys_inv_lift1_subst
-cpys_inv_lift1_up
-cpys_inv_lref1
-cpys_inv_lref1_drop
-cpys_inv_lref1_Y2
-cpys_inv_refl_O2
-cpys_inv_SO2
-cpys_inv_sort1
-cpys_lift_be
-cpys_lift_ge
-cpys_lift_le
-cpy_split_down
-cpy_split_up
-cpys_refl
-cpys_split_up
-cpys_strap1
-cpys_strap1_down
-cpys_strap2
-cpys_strap2_down
-cpys_strip_eq
-cpys_strip_neq
-cpys_subst
-cpys_subst_Y2
-cpys_trans_down
-cpys_trans_eq
-cpy_subst
-cpys_weak
-cpys_weak_full
-cpys_weak_top
-cpy_trans_down
-cpy_trans_ge
-cpy_weak
-cpy_weak_full
-cpy_weak_top
-crr
-crr_appl_dx
-crr_appl_sn
-crr_beta
-crr_crx
-crr_delta
-crr_ib2_dx
-crr_ib2_sn
-crr_inv_appl
-crr_inv_appl_aux
-crr_inv_gref
-crr_inv_gref_aux
-crr_inv_ib2
-crr_inv_ib2_aux
-crr_inv_lift
-crr_inv_lref
-crr_inv_lref_aux
-crr_inv_sort
-crr_inv_sort_aux
-crr_lift
-crr_ri2
-crr_theta
-crx
-crx_appl_dx
-crx_appl_sn
-crx_beta
-crx_delta
-crx_ib2_dx
-crx_ib2_sn
-crx_inv_appl
-crx_inv_appl_aux
-crx_inv_gref
-crx_inv_gref_aux
-crx_inv_ib2
-crx_inv_ib2_aux
-crx_inv_lift
-crx_inv_lref
-crx_inv_lref_aux
-crx_inv_sort
-crx_inv_sort_aux
-crx_lift
-crx_ri2
-crx_sort
-crx_theta
-csx
-csxa
-csx_abbr
-csx_abst
-csxa_cpxs_trans
-csxa_csx
-csxa_ind
-csxa_intro
-csxa_intro_aux
-csxa_intro_cpx
-csx_appl_beta
-csx_appl_beta_aux
-csx_appl_simple
-csx_appl_simple_tsts
-csx_appl_theta
-csx_appl_theta_aux
-csx_applv_beta
-csx_applv_cast
-csx_applv_cnx
-csx_applv_delta
-csx_applv_sort
-csx_applv_theta
-csx_cast
-csx_cpre
-csx_cpxe
-csx_cpxs_trans
-csx_cpx_trans
-csx_csxa
-csx_fpb_conf
-csx_fpbs_conf
-csx_fqu_conf
-csx_fqup_conf
-csx_fquq_conf
-csx_fqus_conf
-csx_fsb
-csx_fsb_fpbs
-csx_fwd_applv
-csx_fwd_bind
-csx_fwd_bind_dx
-csx_fwd_bind_dx_aux
-csx_fwd_flat
-csx_fwd_flat_dx
-csx_fwd_flat_dx_aux
-csx_fwd_pair_sn
-csx_fwd_pair_sn_aux
-csx_gcp
-csx_gcr
-csx_ind
-csx_ind_alt
-csx_ind_fpb
-csx_ind_fpbg
-csx_intro
-csx_intro_cpxs
-csx_inv_lift
-csx_inv_lref_bind
-csx_lift
-csx_lleq_conf
-csx_lleq_trans
-csx_lpx_conf
-csx_lpxs_conf
-csx_lref_bind
-csx_lsx
-csx_sort
-csxv
-csxv_inv_cons
-d1_liftable_liftables
-d1_liftables_liftables_all
-da
-da_bind
-da_cpr_lpr
-da_cpr_lpr_aux
-da_cprs_lpr
-da_cprs_lpr_aux
-da_flat
-da_inv_bind
-da_inv_bind_aux
-da_inv_flat
-da_inv_flat_aux
-da_inv_gref
-da_inv_gref_aux
-da_inv_lift
-da_inv_lref
-da_inv_lref_aux
-da_inv_sort
-da_inv_sort_aux
-da_ldec
-da_ldef
-da_lift
-da_lstas
-da_mono
-d_appendable_sn
-da_scpds_lpr_aux
-da_scpes_aux
-da_sort
-d_deliftable_sn
-d_deliftable_sn_llstar
-d_deliftable_sn_LTC
-dedropable_sn
-dedropable_sn_TC
-deg_inv_prec
-deg_inv_pred
-deg_iter
-deg_next_SO
-deg_O
-deg_SO
-deg_SO_gt
-deg_SO_inv_pos
-deg_SO_inv_pos_aux
-deg_SO_pos
-deg_SO_refl
-deg_SO_zero
-Delta
-Delta_lift
-destruct_apair_apair_aux
-destruct_lpair_lpair_aux
-destruct_sort_sort_aux
-destruct_tatom_tatom_aux
-destruct_tpair_tpair_aux
-discr_apair_xy_x
-discr_apair_xy_y
-discr_lpair_x_xy
-discr_tpair_xy_x
-discr_tpair_xy_y
-d_liftable
-d_liftable1
-d_liftable_llstar
-d_liftable_LTC
-d_liftables1
-d_liftables1_all
-drop
-dropable_dx
-dropable_dx_TC
-dropable_sn
-dropable_sn_TC
-drop_atom
-drop_conf_be
-drop_conf_div
-drop_conf_ge
-drop_conf_le
-drop_conf_lt
-drop_drop
-drop_drop_lt
-drop_FT
-drop_fwd_be
-drop_fwd_drop2
-drop_fwd_length
-drop_fwd_length_eq1
-drop_fwd_length_eq2
-drop_fwd_length_ge
-drop_fwd_length_le2
-drop_fwd_length_le4
-drop_fwd_length_le_ge
-drop_fwd_length_le_le
-drop_fwd_length_lt2
-drop_fwd_length_lt4
-drop_fwd_length_minus2
-drop_fwd_length_minus4
-drop_fwd_lw
-drop_fwd_lw_lt
-drop_fwd_rfw
-drop_gen
-drop_inv_atom1
-drop_inv_atom1_aux
-drop_inv_drop1
-drop_inv_drop1_lt
-drop_inv_FT
-drop_inv_FT_aux
-drop_inv_gen
-drop_inv_length_eq
-drop_inv_O1_gt
-drop_inv_O1_pair1
-drop_inv_O1_pair1_aux
-drop_inv_O1_pair2
-drop_inv_O2
-drop_inv_O2_aux
-drop_inv_pair1
-drop_inv_refl
-drop_inv_skip1
-drop_inv_skip1_aux
-drop_inv_skip2
-drop_inv_skip2_aux
-drop_inv_T
-drop_lprs_trans
-drop_lpr_trans
-drop_lpxs_trans
-drop_lpx_trans
-drop_lsubc_trans
-drop_mono
-drop_O1_append_sn_le
-drop_O1_append_sn_le_aux
-drop_O1_eq
-drop_O1_ex
-drop_O1_ge
-drop_O1_inj
-drop_O1_inv_append1_ge
-drop_O1_inv_append1_le
-drop_O1_le
-drop_O1_lt
-drop_O1_pair
-drop_pair
-drop_refl
-drop_refl_atom_O2
-drops
-drops_cons
-drops_drop_trans
-drops_inv_cons
-drops_inv_cons_aux
-drops_inv_nil
-drops_inv_nil_aux
-drops_inv_skip2
-drop_skip
-drop_skip_lt
-drops_lsubc_trans
-drops_nil
-drop_split
-drops_skip
-drops_trans
-drop_T
-drop_trans_ge
-drop_trans_ge_comm
-drop_trans_le
-drop_trans_lt
-eq_aarity_dec
-eq_bind2_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
-flat2
-Flat2
-fleq
-fleq_canc_dx
-fleq_canc_sn
-fleq_fpbg_trans
-fleq_fpbq
-fleq_fpbs
-fleq_fpb_trans
-fleq_intro
-fleq_inv_gen
-fleq_refl
-fleq_sym
-fleq_trans
-fpb
-fpb_cpx
-fpb_fpbg
-fpb_fpbg_trans
-fpb_fpbq
-fpb_fpbq_alt
-fpb_fpbs
-fpb_fpbsa_trans
-fpb_fqu
-fpbg
-fpbg_fleq_trans
-fpbg_fpbq_trans
-fpbg_fpbs_trans
-fpbg_fwd_fpbs
-fpbg_refl
-fpbg_trans
-fpb_inv_fleq
-fpb_lpx
-fpbq
-fpbqa
-fpbq_aaa_conf
-fpbqa_inv_fpbq
-fpbq_cpx
-fpbq_fpbg_trans
-fpbq_fpbqa
-fpbq_fpbs
-fpbq_fquq
-fpbq_ind_alt
-fpbq_inv_fpb_alt
-fpbq_lleq
-fpbq_lpx
-fpbq_refl
-fpbs
-fpbsa
-fpbs_aaa_conf
-fpbsa_inv_fpbs
-fpbs_cpxs_trans
-fpbs_cpx_trans_neq
-fpbs_fpbg
-fpbs_fpbg_trans
-fpbs_fpbsa
-fpbs_fpb_trans
-fpbs_fqup_trans
-fpbs_fqus_trans
-fpbs_ind
-fpbs_ind_dx
-fpbs_intro_alt
-fpbs_inv_alt
-fpbs_lleq_trans
-fpbs_lpxs_trans
-fpbs_refl
-fpbs_strap1
-fpbs_strap2
-fpbs_trans
-fqu
-fqu_bind_dx
-fqu_cpr_trans_dx
-fqu_cpr_trans_sn
-fqu_cpxs_trans
-fqu_cpxs_trans_neq
-fqu_cpx_trans
-fqu_cpx_trans_neq
-fqu_drop
-fqu_drop_lt
-fqu_flat_dx
-fqu_fqup
-fqu_fquq
-fqu_fwd_fw
-fqu_fwd_length_lref1
-fqu_fwd_length_lref1_aux
-fqu_inv_eq
-fqu_inv_eq_aux
-fqu_lpr_trans
-fqu_lpx_trans
-fqu_lref_O
-fqu_lref_S_lt
-fqup
-fqu_pair_sn
-fqup_ApplOmega_13
-fqup_bind_dx
-fqup_bind_dx_flat_dx
-fqup_cpxs_trans
-fqup_cpxs_trans_neq
-fqup_cpx_trans
-fqup_cpx_trans_neq
-fqup_drop
-fqup_flat_dx
-fqup_flat_dx_bind_dx
-fqup_flat_dx_pair_sn
-fqup_fpbg
-fqup_fpbs
-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
-fquq
-fquqa
-fquqa_drop
-fquqa_inv_fquq
-fquqa_refl
-fquq_bind_dx
-fquq_cpr_trans_dx
-fquq_cpr_trans_sn
-fquq_cpxs_trans
-fquq_cpxs_trans_neq
-fquq_cpx_trans
-fquq_cpx_trans_neq
-fquq_drop
-fquq_flat_dx
-fquq_fquqa
-fquq_fqus
-fquq_fwd_fw
-fquq_fwd_length_lref1
-fquq_fwd_length_lref1_aux
-fquq_inv_gen
-fquq_lpr_trans
-fquq_lpx_trans
-fquq_lref_O
-fquq_lstas_trans
-fquq_pair_sn
-fquq_refl
-fquq_sta_trans
-fqus
-fqus_cpxs_trans
-fqus_cpxs_trans_neq
-fqus_cpx_trans
-fqus_cpx_trans_neq
-fqus_drop
-fqus_fpbs
-fqus_fpbs_trans
-fqus_fqup_trans
-fqus_fwd_fw
-fqus_ind
-fqus_ind_dx
-fqus_inv_gen
-fqus_lpxs_fpbs
-fqus_lstas_trans
-fqus_refl
-fqus_strap1
-fqus_strap1_fqu
-fqus_strap2
-fqus_strap2_fqu
-fqu_sta_trans
-fqus_trans
-fqu_wf_ind
-frees
-frees_append
-frees_be
-frees_bind_dx
-frees_bind_dx_O
-frees_bind_sn
-frees_dec
-frees_eq
-frees_flat_dx
-frees_flat_sn
-frees_inv
-frees_inv_append
-frees_inv_append_aux
-frees_inv_bind
-frees_inv_bind_O
-frees_inv_flat
-frees_inv_gref
-frees_inv_lift_be
-frees_inv_lift_ge
-frees_inv_lref
-frees_inv_lref_free
-frees_inv_lref_ge
-frees_inv_lref_lt
-frees_inv_lref_skip
-frees_inv_sort
-frees_lift_ge
-frees_lref_be
-frees_lref_eq
-frees_lreq_conf
-frees_S
-frees_trans
-frees_weak
-fsb
-fsba
-fsba_fpbs_trans
-fsba_ind_alt
-fsba_intro
-fsba_inv_fsb
-fsb_fpbs_trans
-fsb_fsba
-fsb_ind_alt
-fsb_ind_fpbg
-fsb_intro
-fsb_inv_csx
-fw
-fw_lpair_sn
-fw_shift
-fw_tpair_dx
-fw_tpair_sn
-gcp
-gcp0_lifts
-gcp2_lifts
-gcp2_lifts_all
-gcr
-gcr_aaa
-gcr_lift
-gcr_lifts
-genv
-gget
-gget_dec
-gget_eq
-gget_gt
-gget_inv_eq
-gget_inv_gt
-gget_inv_lt
-gget_inv_lt_aux
-gget_lt
-gget_mono
-gget_total
-GRef
-ib2
-IH_da_cpr_lpr
-IH_lstas_cpr_lpr
-IH_snv_cpr_lpr
-IH_snv_lstas
-is_lift_dec
-item0
-item2
-LAtom
-lcosx
-lcosx_drop_trans_lt
-lcosx_inv_pair
-lcosx_inv_succ
-lcosx_inv_succ_aux
-lcosx_O
-lcosx_pair
-lcosx_skip
-lcosx_sort
-length
-length_inv_pos_dx
-length_inv_pos_dx_ltail
-length_inv_pos_sn
-length_inv_pos_sn_ltail
-length_inv_zero_dx
-length_inv_zero_sn
-lenv
-lenv_ind_alt
-lift
-lift_bind
-lift_conf_be
-lift_conf_O1
-lift_div_be
-lift_div_le
-lift_flat
-lift_fwd_pair1
-lift_fwd_pair2
-lift_fwd_tw
-lift_gref
-lift_inj
-lift_inv_bind1
-lift_inv_bind1_aux
-lift_inv_bind2
-lift_inv_bind2_aux
-lift_inv_flat1
-lift_inv_flat1_aux
-lift_inv_flat2
-lift_inv_flat2_aux
-lift_inv_gref1
-lift_inv_gref1_aux
-lift_inv_gref2
-lift_inv_gref2_aux
-lift_inv_lref1
-lift_inv_lref1_aux
-lift_inv_lref1_ge
-lift_inv_lref1_lt
-lift_inv_lref2
-lift_inv_lref2_aux
-lift_inv_lref2_be
-lift_inv_lref2_ge
-lift_inv_lref2_lt
-lift_inv_O2
-lift_inv_O2_aux
-lift_inv_pair_xy_x
-lift_inv_pair_xy_y
-lift_inv_sort1
-lift_inv_sort1_aux
-lift_inv_sort2
-lift_inv_sort2_aux
-lift_lref_ge
-lift_lref_ge_minus
-lift_lref_ge_minus_eq
-lift_lref_lt
-lift_mono
-lift_refl
-lifts
-lifts_applv
-lifts_bind
-lifts_cons
-lifts_flat
-lift_simple_dx
-lift_simple_sn
-lifts_inv_applv1
-lifts_inv_bind1
-lifts_inv_cons
-lifts_inv_cons_aux
-lifts_inv_flat1
-lifts_inv_gref1
-lifts_inv_lref1
-lifts_inv_nil
-lifts_inv_nil_aux
-lifts_inv_sort1
-lifts_lift_trans
-lifts_lift_trans_le
-lifts_nil
-lift_sort
-lift_split
-lifts_simple_dx
-lifts_simple_sn
-lifts_total
-lifts_trans
-liftsv
-liftsv_cons
-liftsv_liftv_trans_le
-liftsv_nil
-lift_total
-lift_trans_be
-lift_trans_ge
-lift_trans_le
-liftv
-liftv_cons
-liftv_inv_cons1
-liftv_inv_cons1_aux
-liftv_inv_nil1
-liftv_inv_nil1_aux
-liftv_mono
-liftv_nil
-liftv_total
-lleq
-lleq_aaa_trans
-lleq_bind
-lleq_bind_O
-lleq_bind_repl_O
-lleq_bind_repl_SO
-lleq_canc_dx
-lleq_canc_sn
-lleq_cpxs_trans
-lleq_cpx_trans
-lleq_dec
-lleq_flat
-lleq_fpbs
-lleq_fpbs_trans
-lleq_fpb_trans
-lleq_fqup_trans
-lleq_fquq_trans
-lleq_fqus_trans
-lleq_fqu_trans
-lleq_free
-lleq_fwd_bind_dx
-lleq_fwd_bind_O_dx
-lleq_fwd_bind_sn
-lleq_fwd_drop_dx
-lleq_fwd_drop_sn
-lleq_fwd_flat_dx
-lleq_fwd_flat_sn
-lleq_fwd_length
-lleq_fwd_lref
-lleq_fwd_lref_dx
-lleq_fwd_lref_sn
-lleq_ge
-lleq_ge_up
-lleq_gref
-lleq_ind
-lleq_ind_alt_r
-lleq_intro_alt
-lleq_intro_alt_r
-lleq_inv_alt
-lleq_inv_alt_r
-lleq_inv_bind
-lleq_inv_bind_O
-lleq_inv_flat
-lleq_inv_lift_be
-lleq_inv_lift_ge
-lleq_inv_lift_le
-lleq_inv_lref_ge
-lleq_inv_lref_ge_bi
-lleq_inv_lref_ge_dx
-lleq_inv_lref_ge_sn
-lleq_inv_S
-lleq_lift_ge
-lleq_lift_le
-lleq_llpx_sn_conf
-lleq_llpx_sn_trans
-lleq_lpxs_trans
-lleq_lpx_trans
-lleq_lref
-lleq_lreq_repl
-lleq_lreq_trans
-lleq_nlleq_trans
-lleq_refl
-lleq_skip
-lleq_sort
-lleq_sym
-lleq_trans
-lleq_transitive
-lleq_Y
-llor
-llor_atom
-llor_skip
-llor_tail_cofrees
-llor_tail_frees
-llor_total
-llpx_sn
-llpx_sn_alt
-llpx_sn_alt_inv_llpx_sn
-llpx_sn_alt_r
-llpx_sn_alt_r_bind
-llpx_sn_alt_r_flat
-llpx_sn_alt_r_free
-llpx_sn_alt_r_fwd_length
-llpx_sn_alt_r_fwd_lref
-llpx_sn_alt_r_gref
-llpx_sn_alt_r_ind_alt
-llpx_sn_alt_r_intro
-llpx_sn_alt_r_intro_alt
-llpx_sn_alt_r_inv_alt
-llpx_sn_alt_r_inv_bind
-llpx_sn_alt_r_inv_flat
-llpx_sn_alt_r_inv_lpx_sn
-llpx_sn_alt_r_lref
-llpx_sn_alt_r_skip
-llpx_sn_alt_r_sort
-llpx_sn_bind
-llpx_sn_bind_O
-llpx_sn_bind_repl_O
-llpx_sn_bind_repl_SO
-llpx_sn_co
-llpx_sn_dec
-llpx_sn_drop_conf_O
-llpx_sn_drop_trans_O
-llpx_sn_flat
-llpx_sn_free
-llpx_sn_frees_trans
-llpx_sn_frees_trans_aux
-llpx_sn_fwd_bind_dx
-llpx_sn_fwd_bind_O_dx
-llpx_sn_fwd_bind_sn
-llpx_sn_fwd_drop_dx
-llpx_sn_fwd_drop_sn
-llpx_sn_fwd_flat_dx
-llpx_sn_fwd_flat_sn
-llpx_sn_fwd_length
-llpx_sn_fwd_lref
-llpx_sn_fwd_lref_aux
-llpx_sn_fwd_lref_dx
-llpx_sn_fwd_lref_sn
-llpx_sn_fwd_pair_sn
-llpx_sn_ge
-llpx_sn_ge_up
-llpx_sn_gref
-llpx_sn_ind_alt_r
-llpx_sn_intro_alt_r
-llpx_sn_inv_alt_r
-llpx_sn_inv_bind
-llpx_sn_inv_bind_aux
-llpx_sn_inv_bind_O
-llpx_sn_inv_flat
-llpx_sn_inv_flat_aux
-llpx_sn_inv_lift_be
-llpx_sn_inv_lift_ge
-llpx_sn_inv_lift_le
-llpx_sn_inv_lift_O
-llpx_sn_inv_lref_ge_bi
-llpx_sn_inv_lref_ge_dx
-llpx_sn_inv_lref_ge_sn
-llpx_sn_inv_S
-llpx_sn_inv_S_aux
-llpx_sn_lift_ge
-llpx_sn_lift_le
-llpx_sn_llor_dx
-llpx_sn_llor_dx_sym
-llpx_sn_llor_fwd_sn
-llpx_sn_llpx_sn_alt
-llpx_sn_lpx_sn_alt_r
-llpx_sn_lref
-llpx_sn_lrefl
-llpx_sn_lreq_repl
-llpx_sn_lreq_trans
-llpx_sn_refl
-llpx_sn_skip
-llpx_sn_sort
-llpx_sn_TC_pair_dx
-llpx_sn_Y
-LPair
-lpair_ltail
-lpr
-lpr_aaa_conf
-lpr_conf
-lpr_cpcs_conf
-lpr_cpcs_trans
-lpr_cpr_conf
-lpr_cpr_conf_dx
-lpr_cpr_conf_sn
-lpr_cprs_conf
-lpr_cprs_trans
-lpr_cpr_trans
-lpr_drop_conf
-lpr_drop_trans_O1
-lpr_fpb
-lpr_fpbq
-lpr_fwd_length
-lpr_inv_atom1
-lpr_inv_atom2
-lpr_inv_pair1
-lpr_inv_pair2
-lpr_lprs
-lpr_lpx
-lpr_pair
-lpr_refl
-lprs
-lprs_aaa_conf
-lprs_conf
-lprs_cpcs_trans
-lprs_cpr_conf_dx
-lprs_cpr_conf_sn
-lprs_cprs_conf
-lprs_cprs_conf_dx
-lprs_cprs_conf_sn
-lprs_cprs_trans
-lprs_cpr_trans
-lprs_drop_conf
-lprs_drop_trans_O1
-lprs_fpbs
-lprs_fwd_length
-lprs_ind
-lprs_ind_alt
-lprs_ind_dx
-lprs_inv_atom1
-lprs_inv_atom2
-lprs_inv_pair1
-lprs_inv_pair2
-lprs_lpxs
-lprs_pair
-lprs_pair2
-lprs_pair_refl
-lprs_refl
-lprs_strap1
-lprs_strap2
-lprs_strip
-lprs_trans
-lpx
-lpx_aaa_conf
-lpx_cpx_frees_trans
-lpx_cpxs_trans
-lpx_cpx_trans
-lpx_drop_conf
-lpx_drop_trans_O1
-lpx_fqup_trans
-lpx_fquq_trans
-lpx_fqus_trans
-lpx_fqu_trans
-lpx_frees_trans
-lpx_fwd_length
-lpx_inv_atom1
-lpx_inv_atom2
-lpx_inv_pair
-lpx_inv_pair1
-lpx_inv_pair2
-lpx_lleq_fqup_trans
-lpx_lleq_fquq_trans
-lpx_lleq_fqus_trans
-lpx_lleq_fqu_trans
-lpx_lpxs
-lpx_pair
-lpx_refl
-lpxs
-lpxs_aaa_conf
-lpxs_cpxs_trans
-lpxs_cpx_trans
-lpxs_drop_conf
-lpxs_drop_trans_O1
-lpxs_fpbg
-lpxs_fpbs
-lpxs_fpbs_trans
-lpxs_fqup_trans
-lpxs_fquq_trans
-lpxs_fqus_trans
-lpxs_fwd_length
-lpxs_ind
-lpxs_ind_alt
-lpxs_ind_dx
-lpxs_inv_atom1
-lpxs_inv_atom2
-lpxs_inv_pair1
-lpxs_inv_pair2
-lpxs_lleq_fpbs
-lpxs_lleq_fqup_trans
-lpxs_lleq_fquq_trans
-lpxs_lleq_fqus_trans
-lpxs_lleq_fqu_trans
-lpx_sn
-lpx_sn_alt
-lpx_sn_alt_atom
-lpx_sn_alt_fwd_length
-lpx_sn_alt_inv_atom1
-lpx_sn_alt_inv_atom2
-lpx_sn_alt_inv_lpx_sn
-lpx_sn_alt_inv_pair1
-lpx_sn_alt_inv_pair2
-lpx_sn_alt_pair
-lpx_sn_atom
-lpx_sn_conf
-lpx_sn_confluent
-lpx_sn_deliftable_dropable
-lpx_sn_dropable
-lpx_sn_dropable_aux
-lpx_sn_drop_conf
-lpx_sn_drop_trans
-lpx_sn_fwd_length
-lpx_sn_intro_alt
-lpx_sn_inv_alt
-lpx_sn_inv_atom1
-lpx_sn_inv_atom1_aux
-lpx_sn_inv_atom2
-lpx_sn_inv_atom2_aux
-lpx_sn_inv_pair
-lpx_sn_inv_pair1
-lpx_sn_inv_pair1_aux
-lpx_sn_inv_pair2
-lpx_sn_inv_pair2_aux
-lpx_sn_liftable_dedropable
-lpxs_nlleq_inv_step_sn
-lpx_sn_llpx_sn
-lpx_sn_lpx_sn_alt
-lpx_sn_LTC_TC_lpx_sn
-lpx_sn_pair
-lpx_sn_refl
-lpx_sn_trans
-lpx_sn_transitive
-lpxs_pair
-lpxs_pair2
-lpxs_pair_refl
-lpxs_refl
-lpxs_strap1
-lpxs_strap2
-lpxs_trans
-LRef
-lreq
-lreq_atom
-lreq_canc_dx
-lreq_canc_sn
-lreq_cpxs_trans
-lreq_cpx_trans
-lreq_drop_conf_be
-lreq_drop_trans_be
-lreq_frees_trans
-lreq_fwd_length
-lreq_inv_atom1
-lreq_inv_atom1_aux
-lreq_inv_atom2
-lreq_inv_O_Y
-lreq_inv_O_Y_aux
-lreq_inv_pair
-lreq_inv_pair1
-lreq_inv_pair1_aux
-lreq_inv_pair2
-lreq_inv_succ
-lreq_inv_succ1
-lreq_inv_succ1_aux
-lreq_inv_succ2
-lreq_inv_zero1
-lreq_inv_zero1_aux
-lreq_inv_zero2
-lreq_join
-lreq_lleq_trans
-lreq_llpx_sn_trans
-lreq_lpxs_trans_lleq
-lreq_lpxs_trans_lleq_aux
-lreq_lpx_trans_lleq
-lreq_lpx_trans_lleq_aux
-lreq_O2
-lreq_pair
-lreq_pair_lt
-lreq_pair_O_Y
-lreq_refl
-lreq_succ
-lreq_succ_lt
-lreq_sym
-lreq_trans
-lreq_zero
-lstas
-lstas_aaa_conf
-lstas_appl
-lstas_bind
-lstas_cast
-lstas_conf
-lstas_conf_le
-lstas_correct
-lstas_cpcs_lpr
-lstas_cpr
-lstas_cpr_aux
-lstas_cpr_lpr
-lstas_cpr_lpr_aux
-lstas_cprs_lpr
-lstas_cprs_lpr_aux
-lstas_cpxs
-lstas_da_conf
-lstas_fpbg
-lstas_fpbs
-lstas_inv_appl1
-lstas_inv_appl1_aux
-lstas_inv_bind1
-lstas_inv_bind1_aux
-lstas_inv_cast1
-lstas_inv_cast1_aux
-lstas_inv_da
-lstas_inv_da_ge
-lstas_inv_gref1
-lstas_inv_gref1_aux
-lstas_inv_lift1
-lstas_inv_lref1
-lstas_inv_lref1_aux
-lstas_inv_lref1_O
-lstas_inv_lref1_S
-lstas_inv_refl_pos
-lstas_inv_sort1
-lstas_inv_sort1_aux
-lstas_ldef
-lstas_lift
-lstas_llpx_sn_conf
-lstas_lstas
-lstas_mono
-lstas_scpds
-lstas_scpds_aux
-lstas_scpds_trans
-lstas_scpes_trans
-lstas_sort
-lstas_split
-lstas_split_aux
-lstas_succ
-lstas_trans
-lstas_zero
-lsuba
-lsuba_aaa_conf
-lsuba_aaa_trans
-lsuba_atom
-lsuba_beta
-lsuba_drop_O1_conf
-lsuba_drop_O1_trans
-lsuba_fwd_lsubr
-lsuba_inv_atom1
-lsuba_inv_atom1_aux
-lsuba_inv_atom2
-lsuba_inv_atom2_aux
-lsuba_inv_pair1
-lsuba_inv_pair1_aux
-lsuba_inv_pair2
-lsuba_inv_pair2_aux
-lsuba_lsubc
-lsuba_pair
-lsuba_refl
-lsuba_trans
-lsubc
-lsubc_atom
-lsubc_beta
-lsubc_drop_O1_trans
-lsubc_fwd_lsubr
-lsubc_inv_atom1
-lsubc_inv_atom1_aux
-lsubc_inv_atom2
-lsubc_inv_atom2_aux
-lsubc_inv_pair1
-lsubc_inv_pair1_aux
-lsubc_inv_pair2
-lsubc_inv_pair2_aux
-lsubc_pair
-lsubc_refl
-lsubd
-lsubd_atom
-lsubd_beta
-lsubd_da_conf
-lsubd_da_trans
-lsubd_drop_O1_conf
-lsubd_drop_O1_trans
-lsubd_fwd_lsubr
-lsubd_inv_atom1
-lsubd_inv_atom1_aux
-lsubd_inv_atom2
-lsubd_inv_atom2_aux
-lsubd_inv_pair1
-lsubd_inv_pair1_aux
-lsubd_inv_pair2
-lsubd_inv_pair2_aux
-lsubd_pair
-lsubd_refl
-lsubd_trans
-lsubr
-lsubr_atom
-lsubr_beta
-lsubr_cpcs_trans
-lsubr_cprs_trans
-lsubr_cpr_trans
-lsubr_cpxs_trans
-lsubr_cpx_trans
-lsubr_fwd_drop2_abbr
-lsubr_fwd_drop2_pair
-lsubr_fwd_length
-lsubr_inv_abbr2
-lsubr_inv_abbr2_aux
-lsubr_inv_abst1
-lsubr_inv_abst1_aux
-lsubr_inv_atom1
-lsubr_inv_atom1_aux
-lsubr_inv_pair1
-lsubr_inv_pair1_aux
-lsubr_pair
-lsubr_refl
-lsubr_trans
-lsubsv
-lsubsv_atom
-lsubsv_beta
-lsubsv_cpcs_trans
-lsubsv_cprs_trans
-lsubsv_drop_O1_conf
-lsubsv_drop_O1_trans
-lsubsv_fwd_lsuba
-lsubsv_fwd_lsubd
-lsubsv_fwd_lsubr
-lsubsv_inv_atom1
-lsubsv_inv_atom1_aux
-lsubsv_inv_atom2
-lsubsv_inv_atom2_aux
-lsubsv_inv_pair1
-lsubsv_inv_pair1_aux
-lsubsv_inv_pair2
-lsubsv_inv_pair2_aux
-lsubsv_lstas_trans
-lsubsv_pair
-lsubsv_refl
-lsubsv_scpds_trans
-lsubsv_snv_trans
-lsubsv_sta_trans
-lsuby
-lsuby_atom
-lsuby_cpysa_trans
-lsuby_cpys_trans
-lsuby_cpy_trans
-lsuby_drop_trans_be
-lsuby_fwd_length
-lsuby_inv_atom1
-lsuby_inv_atom1_aux
-lsuby_inv_pair1
-lsuby_inv_pair1_aux
-lsuby_inv_pair2
-lsuby_inv_pair2_aux
-lsuby_inv_succ1
-lsuby_inv_succ1_aux
-lsuby_inv_succ2
-lsuby_inv_succ2_aux
-lsuby_inv_zero1
-lsuby_inv_zero1_aux
-lsuby_inv_zero2
-lsuby_inv_zero2_aux
-lsuby_O2
-lsuby_pair
-lsuby_pair_lt
-lsuby_pair_O_Y
-lsuby_refl
-lsuby_succ
-lsuby_succ_lt
-lsuby_sym
-lsuby_trans
-lsuby_zero
-lsx
-lsxa
-lsxa_ind
-lsxa_intro
-lsxa_intro_aux
-lsxa_intro_lpx
-lsxa_inv_lsx
-lsxa_lleq_trans
-lsxa_lpxs_trans
-lsx_atom
-lsx_bind
-lsx_bind_lpxs_aux
-lsx_cpx_trans_lcosx
-lsx_cpx_trans_O
-lsx_flat
-lsx_flat_lpxs
-lsx_fwd_bind_dx
-lsx_fwd_bind_sn
-lsx_fwd_flat_dx
-lsx_fwd_flat_sn
-lsx_fwd_lref_be
-lsx_fwd_pair_sn
-lsx_ge
-lsx_ge_up
-lsx_gref
-lsx_ind
-lsx_ind_alt
-lsx_intro
-lsx_intro_alt
-lsx_inv_bind
-lsx_inv_flat
-lsx_inv_lift_be
-lsx_inv_lift_ge
-lsx_inv_lift_le
-lsx_lift_ge
-lsx_lift_le
-lsx_lleq_trans
-lsx_lpxs_trans
-lsx_lpx_trans
-lsx_lref_be
-lsx_lref_be_lpxs
-lsx_lref_free
-lsx_lref_skip
-lsx_lreq_conf
-lsx_lsxa
-lsx_sort
-ltail_length
-lw
-lw_pair
-minuss
-minuss_ge
-minuss_inv_cons1
-minuss_inv_cons1_aux
-minuss_inv_cons1_ge
-minuss_inv_cons1_lt
-minuss_inv_nil1
-minuss_inv_nil1_aux
-minuss_lt
-minuss_nil
-mk_gcp
-mk_gcr
-mk_sd
-mk_sh
-nexts_dec
-nexts_inj
-nexts_le
-nexts_lt
-nf
-nlift_bind_dx
-nlift_bind_sn
-nlift_flat_dx
-nlift_flat_sn
-nlift_inv_bind
-nlift_inv_flat
-nlift_inv_lref_be_SO
-nlift_lref_be_SO
-nlleq_inv_bind
-nlleq_inv_bind_O
-nlleq_inv_flat
-nlleq_lleq_div
-nllpx_sn_inv_bind
-nllpx_sn_inv_bind_O
-nllpx_sn_inv_flat
-Omega1
-Omega2
-pluss
-pluss_inv_cons2
-pluss_inv_nil2
-rfw
-rfw_lpair_dx
-rfw_lpair_sn
-rfw_shift
-rfw_tpair_dx
-rfw_tpair_sn
-ri2
-S1
-S2
-S3
-S4
-S5
-S6
-S7
-scpds
-scpds_aaa_conf
-scpds_conf_eq
-scpds_cpr_lpr_aux
-scpds_cprs_trans
-scpds_div
-scpds_fwd_cprs
-scpds_fwd_cpxs
-scpds_inv_abbr_abst
-scpds_inv_abst1
-scpds_inv_lift1
-scpds_inv_lstas_eq
-scpds_lift
-scpds_strap1
-scpds_strap2
-scpes
-scpes_aaa_mono
-scpes_canc_dx
-scpes_canc_sn
-scpes_cpr_lpr_aux
-scpes_inv_abst2
-scpes_inv_lstas_eq
-scpes_le_aux
-scpes_refl
-scpes_sym
-scpes_trans
-sd
-sd_d
-sd_d_correct
-sd_d_SS
-sd_O
-sd_SO
-sh
-sh_N
-shnv
-shnv_cast
-shnv_inv_cast
-shnv_inv_cast_aux
-shnv_inv_snv
-simple
-simple_atom
-simple_flat
-simple_inv_bind
-simple_inv_bind_aux
-simple_inv_pair
-simple_tsts_repl_dx
-simple_tsts_repl_sn
-snv
-snv_appl
-snv_bind
-snv_cast
-snv_cast_scpes
-snv_cpr_lpr
-snv_cpr_lpr_aux
-snv_cprs_lpr
-snv_cprs_lpr_aux
-snv_extended
-snv_fqu_conf
-snv_fqup_conf
-snv_fquq_conf
-snv_fqus_conf
-snv_fwd_aaa
-snv_fwd_da
-snv_fwd_fsb
-snv_fwd_lstas
-snv_inv_appl
-snv_inv_appl_aux
-snv_inv_bind
-snv_inv_bind_aux
-snv_inv_cast
-snv_inv_cast_aux
-snv_inv_gref
-snv_inv_gref_aux
-snv_inv_lift
-snv_inv_lref
-snv_inv_lref_aux
-snv_lift
-snv_lref
-snv_lstas
-snv_lstas_aux
-snv_preserve
-snv_restricted
-snv_shnv_cast
-snv_sort
-Sort
-sta_cprs_scpds
-sta_cpx
-sta_cpx_aux
-sta_fpb
-sta_fpbg
-sta_fpbq
-sta_fpbs
-sta_ldec
-TAtom
-TC_lpx_sn_fwd_length
-TC_lpx_sn_ind
-TC_lpx_sn_inv_atom1
-TC_lpx_sn_inv_atom2
-TC_lpx_sn_inv_lpx_sn_LTC
-TC_lpx_sn_inv_pair1
-TC_lpx_sn_inv_pair1_aux
-TC_lpx_sn_inv_pair2
-TC_lpx_sn_pair
-TC_lpx_sn_pair_refl
-term
-tir_atom
-tix_lref
-TPair
-tpr_cpr
-tprs_cprs
-trr_inv_atom
-trx_inv_atom
-tsts
-tsts_atom
-tsts_canc_dx
-tsts_canc_sn
-tsts_dec
-tsts_inv_atom1
-tsts_inv_atom1_aux
-tsts_inv_atom2
-tsts_inv_atom2_aux
-tsts_inv_bind_applv_simple
-tsts_inv_pair1
-tsts_inv_pair1_aux
-tsts_inv_pair2
-tsts_inv_pair2_aux
-tsts_pair
-tsts_refl
-tsts_sym
-tsts_trans
-tw
-tw_pos
-unfold
-unfold_bind
-unfold_flat
-unfold_lref
-unfold_sort
+"aaa"
+"aaa_abbr"
+"aaa_abst"
+"aaa_appl"
+"aaa_cast"
+"aaa_csx"
+"aaa_da"
+"aaa_fqu_conf"
+"aaa_fqup_conf"
+"aaa_fquq_conf"
+"aaa_fqus_conf"
+"aaa_fsb"
+"aaa_fsba"
+"aaa_ind_csx"
+"aaa_ind_csx_alt"
+"aaa_ind_csx_alt_aux"
+"aaa_ind_csx_aux"
+"aaa_ind_fpb"
+"aaa_ind_fpb_aux"
+"aaa_ind_fpbg"
+"aaa_ind_fpbg_aux"
+"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_lift"
+"aaa_inv_lref"
+"aaa_inv_lref_aux"
+"aaa_inv_sort"
+"aaa_inv_sort_aux"
+"aaa_lift"
+"aaa_lifts"
+"aaa_lleq_conf"
+"aaa_lref"
+"aaa_lstas"
+"aaa_mono"
+"aaa_sort"
+"aarity"
+"AAtom"
+"Abbr"
+"Abst"
+"acr"
+"acr_aaa"
+"acr_aaa_csubc_lifts"
+"acr_abst"
+"acr_gcr"
+"APair"
+"append"
+"append_assoc"
+"append_atom_sn"
+"append_inj_dx"
+"append_inj_sn"
+"append_inv_pair_dx"
+"append_inv_refl_dx"
+"append_length"
+"Appl"
+"ApplDelta"
+"ApplDelta_lift"
+"ApplOmega1"
+"ApplOmega2"
+"ApplOmega3"
+"applv"
+"applv_simple"
+"at"
+"at_ge"
+"at_inv_cons"
+"at_inv_cons_aux"
+"at_inv_cons_ge"
+"at_inv_cons_lt"
+"at_inv_nil"
+"at_inv_nil_aux"
+"at_lt"
+"at_mono"
+"at_nil"
+"bind2"
+"Bind2"
+"candidate"
+"Cast"
+"ceq"
+"cfun"
+"cir"
+"cir_appl"
+"cir_cnr"
+"cir_gref"
+"cir_ib2"
+"cir_inv_appl"
+"cir_inv_bind"
+"cir_inv_delta"
+"cir_inv_flat"
+"cir_inv_ib2"
+"cir_inv_lift"
+"cir_inv_ri2"
+"cir_lift"
+"cir_sort"
+"cix"
+"cix_appl"
+"cix_cnx"
+"cix_gref"
+"cix_ib2"
+"cix_inv_appl"
+"cix_inv_bind"
+"cix_inv_cir"
+"cix_inv_delta"
+"cix_inv_flat"
+"cix_inv_ib2"
+"cix_inv_lift"
+"cix_inv_ri2"
+"cix_inv_sort"
+"cix_lift"
+"cix_lref"
+"cix_sort"
+"cnr"
+"cnr_abst"
+"cnr_appl_simple"
+"cnr_dec"
+"cnr_inv_abbr"
+"cnr_inv_abst"
+"cnr_inv_appl"
+"cnr_inv_cir"
+"cnr_inv_crr"
+"cnr_inv_delta"
+"cnr_inv_eps"
+"cnr_inv_lift"
+"cnr_inv_zeta"
+"cnr_lift"
+"cnr_lref_abst"
+"cnr_lref_atom"
+"cnr_lref_free"
+"cnr_sort"
+"cnx"
+"cnx_abst"
+"cnx_appl_simple"
+"cnx_csx"
+"cnx_dec"
+"cnx_fwd_cnr"
+"cnx_inv_abbr"
+"cnx_inv_abst"
+"cnx_inv_appl"
+"cnx_inv_cix"
+"cnx_inv_crx"
+"cnx_inv_delta"
+"cnx_inv_eps"
+"cnx_inv_lift"
+"cnx_inv_sort"
+"cnx_inv_zeta"
+"cnx_lift"
+"cnx_lref_atom"
+"cnx_lref_free"
+"cnx_sort"
+"cnx_sort_iter"
+"CP0"
+"CP1"
+"CP2"
+"CP3"
+"cpc"
+"cpc_conf"
+"cpc_cpcs"
+"cpc_fwd_cpr"
+"cpc_refl"
+"cpcs"
+"cpcs_aaa_mono"
+"cpcs_bind1"
+"cpcs_bind2"
+"cpcs_bind_dx"
+"cpcs_bind_sn"
+"cpcs_canc_dx"
+"cpcs_canc_sn"
+"cpcs_cpr_conf"
+"cpcs_cpr_div"
+"cpcs_cprs_conf"
+"cpcs_cprs_div"
+"cpcs_cprs_dx"
+"cpcs_cprs_sn"
+"cpcs_cprs_strap1"
+"cpcs_cprs_strap2"
+"cpcs_cpr_strap1"
+"cpcs_cpr_strap2"
+"cpcs_flat"
+"cpcs_flat_dx_cpr_rev"
+"cpcs_ind"
+"cpcs_ind_dx"
+"cpcs_inv_abst1"
+"cpcs_inv_abst2"
+"cpcs_inv_abst_dx"
+"cpcs_inv_abst_sn"
+"cpcs_inv_cprs"
+"cpcs_inv_lift"
+"cpcs_inv_sort"
+"cpcs_inv_sort_abst"
+"cpcs_lift"
+"cpcs_refl"
+"cpcs_scpes"
+"cpcs_strap1"
+"cpcs_strap2"
+"cpcs_strip"
+"cpcs_sym"
+"cpcs_trans"
+"cpc_sym"
+"cpr"
+"cpr_aaa_conf"
+"cpr_ApplOmega_12"
+"cpr_ApplOmega_23"
+"cpr_atom"
+"cpr_beta"
+"cpr_bind"
+"cpr_bind2"
+"cpr_conf"
+"cpr_conf_lpr"
+"cpr_conf_lpr_atom_atom"
+"cpr_conf_lpr_atom_delta"
+"cpr_conf_lpr_beta_beta"
+"cpr_conf_lpr_bind_bind"
+"cpr_conf_lpr_bind_zeta"
+"cpr_conf_lpr_delta_delta"
+"cpr_conf_lpr_eps_eps"
+"cpr_conf_lpr_flat_beta"
+"cpr_conf_lpr_flat_eps"
+"cpr_conf_lpr_flat_flat"
+"cpr_conf_lpr_flat_theta"
+"cpr_conf_lpr_theta_theta"
+"cpr_conf_lpr_zeta_zeta"
+"cpr_cpcs_dx"
+"cpr_cpcs_sn"
+"cpr_cprs"
+"cpr_cprs_conf_cpcs"
+"cpr_cprs_div"
+"cpr_cpx"
+"cpr_delift"
+"cpr_delta"
+"cpr_div"
+"cpre"
+"cpre_mono"
+"cpr_eps"
+"cpr_flat"
+"cpr_fpb"
+"cpr_fpbq"
+"cpr_fwd_bind1_minus"
+"cpr_fwd_cir"
+"cpr_inv_abbr1"
+"cpr_inv_abst1"
+"cpr_inv_appl1"
+"cpr_inv_appl1_simple"
+"cpr_inv_atom1"
+"cpr_inv_atom1_aux"
+"cpr_inv_bind1"
+"cpr_inv_bind1_aux"
+"cpr_inv_cast1"
+"cpr_inv_flat1"
+"cpr_inv_flat1_aux"
+"cpr_inv_gref1"
+"cpr_inv_lift1"
+"cpr_inv_lref1"
+"cpr_inv_sort1"
+"cpr_lift"
+"cpr_llpx_sn_conf"
+"cpr_lpr_fpbs"
+"cpr_lpr_sta_fpbs"
+"cpr_Omega_12"
+"cpr_Omega_21"
+"cpr_pair_sn"
+"cpr_refl"
+"cprs"
+"cprs_aaa_conf"
+"cprs_beta"
+"cprs_beta_dx"
+"cprs_beta_rc"
+"cprs_bind"
+"cprs_bind2"
+"cprs_bind2_dx"
+"cprs_bind_dx"
+"cprs_conf"
+"cprs_conf_cpcs"
+"cprs_cpr_conf_cpcs"
+"cprs_cpr_div"
+"cprs_cpxs"
+"cprs_delta"
+"cprs_div"
+"cprs_eps"
+"cprs_flat"
+"cprs_flat_dx"
+"cprs_flat_sn"
+"cprs_fpbs"
+"cprs_ind"
+"cprs_ind_dx"
+"cprs_inv_abbr1"
+"cprs_inv_abst"
+"cprs_inv_abst1"
+"cprs_inv_appl1"
+"cprs_inv_cast1"
+"cprs_inv_cnr1"
+"cprs_inv_lift1"
+"cprs_inv_lref1"
+"cprs_inv_sort1"
+"cprs_lift"
+"cprs_lpr_conf_dx"
+"cprs_lpr_conf_sn"
+"cprs_refl"
+"cprs_scpds_div"
+"cprs_strap1"
+"cprs_strap2"
+"cprs_strip"
+"cprs_theta"
+"cprs_theta_dx"
+"cprs_theta_rc"
+"cprs_trans"
+"cprs_zeta"
+"cpr_theta"
+"cpr_zeta"
+"cpx"
+"cpx_aaa_conf"
+"cpx_atom"
+"cpx_beta"
+"cpx_bind"
+"cpx_bind2"
+"cpx_cpxs"
+"cpx_ct"
+"cpx_delift"
+"cpx_delta"
+"cpxe"
+"cpx_eps"
+"cpx_flat"
+"cpx_frees_trans"
+"cpx_fwd_bind1_minus"
+"cpx_fwd_cix"
+"cpx_inv_abbr1"
+"cpx_inv_abst1"
+"cpx_inv_appl1"
+"cpx_inv_appl1_simple"
+"cpx_inv_atom1"
+"cpx_inv_atom1_aux"
+"cpx_inv_bind1"
+"cpx_inv_bind1_aux"
+"cpx_inv_cast1"
+"cpx_inv_flat1"
+"cpx_inv_flat1_aux"
+"cpx_inv_gref1"
+"cpx_inv_lift1"
+"cpx_inv_lref1"
+"cpx_inv_lref1_ge"
+"cpx_inv_sort1"
+"cpx_lift"
+"cpx_lleq_conf"
+"cpx_lleq_conf_dx"
+"cpx_lleq_conf_sn"
+"cpx_llpx_sn_conf"
+"cpx_lpx_aaa_conf"
+"cpx_pair_sn"
+"cpx_refl"
+"cpxs"
+"cpxs_aaa_conf"
+"cpxs_ApplOmega_13"
+"cpxs_beta"
+"cpxs_beta_dx"
+"cpxs_beta_rc"
+"cpxs_bind"
+"cpxs_bind2"
+"cpxs_bind2_dx"
+"cpxs_bind_dx"
+"cpxs_ct"
+"cpxs_delta"
+"cpxs_eps"
+"cpxs_flat"
+"cpxs_flat_dx"
+"cpxs_flat_sn"
+"cpxs_fpbg"
+"cpxs_fpbs"
+"cpxs_fpbs_trans"
+"cpxs_fqup_fpbs"
+"cpxs_fqus_fpbs"
+"cpxs_fqus_lpxs_fpbs"
+"cpxs_fwd_beta"
+"cpxs_fwd_beta_vector"
+"cpxs_fwd_cast"
+"cpxs_fwd_cast_vector"
+"cpxs_fwd_cnx"
+"cpxs_fwd_cnx_vector"
+"cpxs_fwd_delta"
+"cpxs_fwd_delta_vector"
+"cpxs_fwd_sort"
+"cpxs_fwd_sort_vector"
+"cpxs_fwd_theta"
+"cpxs_fwd_theta_vector"
+"cpxs_ind"
+"cpxs_ind_dx"
+"cpxs_inv_abbr1"
+"cpxs_inv_abst1"
+"cpxs_inv_appl1"
+"cpxs_inv_cast1"
+"cpxs_inv_cnx1"
+"cpxs_inv_lift1"
+"cpxs_inv_lref1"
+"cpxs_inv_sort1"
+"cpxs_lift"
+"cpxs_lleq_conf"
+"cpxs_lleq_conf_dx"
+"cpxs_lleq_conf_sn"
+"cpxs_neq_inv_step_sn"
+"cpxs_pair_sn"
+"cpxs_refl"
+"cpxs_sort"
+"cpxs_strap1"
+"cpxs_strap2"
+"cpx_st"
+"cpxs_theta"
+"cpxs_theta_dx"
+"cpxs_theta_rc"
+"cpxs_trans"
+"cpxs_zeta"
+"cpx_theta"
+"cpx_zeta"
+"cpy"
+"cpy_atom"
+"cpy_bind"
+"cpy_conf_eq"
+"cpy_conf_neq"
+"cpy_cpys"
+"cpy_flat"
+"cpy_full"
+"cpy_fwd_nlift2_ge"
+"cpy_fwd_tw"
+"cpy_fwd_up"
+"cpy_inv_atom1"
+"cpy_inv_atom1_aux"
+"cpy_inv_bind1"
+"cpy_inv_bind1_aux"
+"cpy_inv_flat1"
+"cpy_inv_flat1_aux"
+"cpy_inv_gref1"
+"cpy_inv_lift1_be"
+"cpy_inv_lift1_be_up"
+"cpy_inv_lift1_eq"
+"cpy_inv_lift1_ge"
+"cpy_inv_lift1_ge_up"
+"cpy_inv_lift1_le"
+"cpy_inv_lift1_le_up"
+"cpy_inv_lref1"
+"cpy_inv_refl_O2"
+"cpy_inv_refl_O2_aux"
+"cpy_inv_sort1"
+"cpy_lift_be"
+"cpy_lift_ge"
+"cpy_lift_le"
+"cpy_refl"
+"cpys"
+"cpysa"
+"cpysa_atom"
+"cpysa_bind"
+"cpysa_cpy_trans"
+"cpysa_flat"
+"cpysa_inv_cpys"
+"cpys_antisym_eq"
+"cpysa_refl"
+"cpysa_subst"
+"cpys_bind"
+"cpys_conf_eq"
+"cpys_conf_neq"
+"cpys_cpysa"
+"cpys_flat"
+"cpys_fwd_tw"
+"cpys_fwd_up"
+"cpys_ind"
+"cpys_ind_alt"
+"cpys_ind_dx"
+"cpys_inv_atom1"
+"cpys_inv_bind1"
+"cpys_inv_flat1"
+"cpys_inv_gref1"
+"cpys_inv_lift1_be"
+"cpys_inv_lift1_be_up"
+"cpys_inv_lift1_eq"
+"cpys_inv_lift1_ge"
+"cpys_inv_lift1_ge_up"
+"cpys_inv_lift1_le"
+"cpys_inv_lift1_le_up"
+"cpys_inv_lift1_subst"
+"cpys_inv_lift1_up"
+"cpys_inv_lref1"
+"cpys_inv_lref1_drop"
+"cpys_inv_lref1_Y2"
+"cpys_inv_refl_O2"
+"cpys_inv_SO2"
+"cpys_inv_sort1"
+"cpys_lift_be"
+"cpys_lift_ge"
+"cpys_lift_le"
+"cpy_split_down"
+"cpy_split_up"
+"cpys_refl"
+"cpys_split_up"
+"cpys_strap1"
+"cpys_strap1_down"
+"cpys_strap2"
+"cpys_strap2_down"
+"cpys_strip_eq"
+"cpys_strip_neq"
+"cpys_subst"
+"cpys_subst_Y2"
+"cpys_trans_down"
+"cpys_trans_eq"
+"cpy_subst"
+"cpys_weak"
+"cpys_weak_full"
+"cpys_weak_top"
+"cpy_trans_down"
+"cpy_trans_ge"
+"cpy_weak"
+"cpy_weak_full"
+"cpy_weak_top"
+"crr"
+"crr_appl_dx"
+"crr_appl_sn"
+"crr_beta"
+"crr_crx"
+"crr_delta"
+"crr_ib2_dx"
+"crr_ib2_sn"
+"crr_inv_appl"
+"crr_inv_appl_aux"
+"crr_inv_gref"
+"crr_inv_gref_aux"
+"crr_inv_ib2"
+"crr_inv_ib2_aux"
+"crr_inv_lift"
+"crr_inv_lref"
+"crr_inv_lref_aux"
+"crr_inv_sort"
+"crr_inv_sort_aux"
+"crr_lift"
+"crr_ri2"
+"crr_theta"
+"crx"
+"crx_appl_dx"
+"crx_appl_sn"
+"crx_beta"
+"crx_delta"
+"crx_ib2_dx"
+"crx_ib2_sn"
+"crx_inv_appl"
+"crx_inv_appl_aux"
+"crx_inv_gref"
+"crx_inv_gref_aux"
+"crx_inv_ib2"
+"crx_inv_ib2_aux"
+"crx_inv_lift"
+"crx_inv_lref"
+"crx_inv_lref_aux"
+"crx_inv_sort"
+"crx_inv_sort_aux"
+"crx_lift"
+"crx_ri2"
+"crx_sort"
+"crx_theta"
+"csx"
+"csxa"
+"csx_abbr"
+"csx_abst"
+"csxa_cpxs_trans"
+"csxa_csx"
+"csxa_ind"
+"csxa_intro"
+"csxa_intro_aux"
+"csxa_intro_cpx"
+"csx_appl_beta"
+"csx_appl_beta_aux"
+"csx_appl_simple"
+"csx_appl_simple_tsts"
+"csx_appl_theta"
+"csx_appl_theta_aux"
+"csx_applv_beta"
+"csx_applv_cast"
+"csx_applv_cnx"
+"csx_applv_delta"
+"csx_applv_sort"
+"csx_applv_theta"
+"csx_cast"
+"csx_cpre"
+"csx_cpxe"
+"csx_cpxs_trans"
+"csx_cpx_trans"
+"csx_csxa"
+"csx_fpb_conf"
+"csx_fpbs_conf"
+"csx_fqu_conf"
+"csx_fqup_conf"
+"csx_fquq_conf"
+"csx_fqus_conf"
+"csx_fsb"
+"csx_fsb_fpbs"
+"csx_fwd_applv"
+"csx_fwd_bind"
+"csx_fwd_bind_dx"
+"csx_fwd_bind_dx_aux"
+"csx_fwd_flat"
+"csx_fwd_flat_dx"
+"csx_fwd_flat_dx_aux"
+"csx_fwd_pair_sn"
+"csx_fwd_pair_sn_aux"
+"csx_gcp"
+"csx_gcr"
+"csx_ind"
+"csx_ind_alt"
+"csx_ind_fpb"
+"csx_ind_fpbg"
+"csx_intro"
+"csx_intro_cpxs"
+"csx_inv_lift"
+"csx_inv_lref_bind"
+"csx_lift"
+"csx_lleq_conf"
+"csx_lleq_trans"
+"csx_lpx_conf"
+"csx_lpxs_conf"
+"csx_lref_bind"
+"csx_lsx"
+"csx_sort"
+"csxv"
+"csxv_inv_cons"
+"d1_liftable_liftables"
+"d1_liftables_liftables_all"
+"da"
+"da_bind"
+"da_cpr_lpr"
+"da_cpr_lpr_aux"
+"da_cprs_lpr"
+"da_cprs_lpr_aux"
+"da_flat"
+"da_inv_bind"
+"da_inv_bind_aux"
+"da_inv_flat"
+"da_inv_flat_aux"
+"da_inv_gref"
+"da_inv_gref_aux"
+"da_inv_lift"
+"da_inv_lref"
+"da_inv_lref_aux"
+"da_inv_sort"
+"da_inv_sort_aux"
+"da_ldec"
+"da_ldef"
+"da_lift"
+"da_lstas"
+"da_mono"
+"d_appendable_sn"
+"da_scpds_lpr_aux"
+"da_scpes_aux"
+"da_sort"
+"d_deliftable_sn"
+"d_deliftable_sn_llstar"
+"d_deliftable_sn_LTC"
+"dedropable_sn"
+"dedropable_sn_TC"
+"deg_inv_prec"
+"deg_inv_pred"
+"deg_iter"
+"deg_next_SO"
+"deg_O"
+"deg_SO"
+"deg_SO_gt"
+"deg_SO_inv_pos"
+"deg_SO_inv_pos_aux"
+"deg_SO_pos"
+"deg_SO_refl"
+"deg_SO_zero"
+"Delta"
+"Delta_lift"
+"destruct_apair_apair_aux"
+"destruct_lpair_lpair_aux"
+"destruct_sort_sort_aux"
+"destruct_tatom_tatom_aux"
+"destruct_tpair_tpair_aux"
+"discr_apair_xy_x"
+"discr_apair_xy_y"
+"discr_lpair_x_xy"
+"discr_tpair_xy_x"
+"discr_tpair_xy_y"
+"d_liftable"
+"d_liftable1"
+"d_liftable_llstar"
+"d_liftable_LTC"
+"d_liftables1"
+"d_liftables1_all"
+"drop"
+"dropable_dx"
+"dropable_dx_TC"
+"dropable_sn"
+"dropable_sn_TC"
+"drop_atom"
+"drop_conf_be"
+"drop_conf_div"
+"drop_conf_ge"
+"drop_conf_le"
+"drop_conf_lt"
+"drop_drop"
+"drop_drop_lt"
+"drop_FT"
+"drop_fwd_be"
+"drop_fwd_drop2"
+"drop_fwd_length"
+"drop_fwd_length_eq1"
+"drop_fwd_length_eq2"
+"drop_fwd_length_ge"
+"drop_fwd_length_le2"
+"drop_fwd_length_le4"
+"drop_fwd_length_le_ge"
+"drop_fwd_length_le_le"
+"drop_fwd_length_lt2"
+"drop_fwd_length_lt4"
+"drop_fwd_length_minus2"
+"drop_fwd_length_minus4"
+"drop_fwd_lw"
+"drop_fwd_lw_lt"
+"drop_fwd_rfw"
+"drop_gen"
+"drop_inv_atom1"
+"drop_inv_atom1_aux"
+"drop_inv_drop1"
+"drop_inv_drop1_lt"
+"drop_inv_FT"
+"drop_inv_FT_aux"
+"drop_inv_gen"
+"drop_inv_length_eq"
+"drop_inv_O1_gt"
+"drop_inv_O1_pair1"
+"drop_inv_O1_pair1_aux"
+"drop_inv_O1_pair2"
+"drop_inv_O2"
+"drop_inv_O2_aux"
+"drop_inv_pair1"
+"drop_inv_refl"
+"drop_inv_skip1"
+"drop_inv_skip1_aux"
+"drop_inv_skip2"
+"drop_inv_skip2_aux"
+"drop_inv_T"
+"drop_lprs_trans"
+"drop_lpr_trans"
+"drop_lpxs_trans"
+"drop_lpx_trans"
+"drop_lsubc_trans"
+"drop_mono"
+"drop_O1_append_sn_le"
+"drop_O1_append_sn_le_aux"
+"drop_O1_eq"
+"drop_O1_ex"
+"drop_O1_ge"
+"drop_O1_inj"
+"drop_O1_inv_append1_ge"
+"drop_O1_inv_append1_le"
+"drop_O1_le"
+"drop_O1_lt"
+"drop_O1_pair"
+"drop_pair"
+"drop_refl"
+"drop_refl_atom_O2"
+"drops"
+"drops_cons"
+"drops_drop_trans"
+"drops_inv_cons"
+"drops_inv_cons_aux"
+"drops_inv_nil"
+"drops_inv_nil_aux"
+"drops_inv_skip2"
+"drop_skip"
+"drop_skip_lt"
+"drops_lsubc_trans"
+"drops_nil"
+"drop_split"
+"drops_skip"
+"drops_trans"
+"drop_T"
+"drop_trans_ge"
+"drop_trans_ge_comm"
+"drop_trans_le"
+"drop_trans_lt"
+"eq_aarity_dec"
+"eq_bind2_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"
+"flat2"
+"Flat2"
+"fleq"
+"fleq_canc_dx"
+"fleq_canc_sn"
+"fleq_fpbg_trans"
+"fleq_fpbq"
+"fleq_fpbs"
+"fleq_fpb_trans"
+"fleq_intro"
+"fleq_inv_gen"
+"fleq_refl"
+"fleq_sym"
+"fleq_trans"
+"fpb"
+"fpb_cpx"
+"fpb_fpbg"
+"fpb_fpbg_trans"
+"fpb_fpbq"
+"fpb_fpbq_alt"
+"fpb_fpbs"
+"fpb_fpbsa_trans"
+"fpb_fqu"
+"fpbg"
+"fpbg_fleq_trans"
+"fpbg_fpbq_trans"
+"fpbg_fpbs_trans"
+"fpbg_fwd_fpbs"
+"fpbg_refl"
+"fpbg_trans"
+"fpb_inv_fleq"
+"fpb_lpx"
+"fpbq"
+"fpbqa"
+"fpbq_aaa_conf"
+"fpbqa_inv_fpbq"
+"fpbq_cpx"
+"fpbq_fpbg_trans"
+"fpbq_fpbqa"
+"fpbq_fpbs"
+"fpbq_fquq"
+"fpbq_ind_alt"
+"fpbq_inv_fpb_alt"
+"fpbq_lleq"
+"fpbq_lpx"
+"fpbq_refl"
+"fpbs"
+"fpbsa"
+"fpbs_aaa_conf"
+"fpbsa_inv_fpbs"
+"fpbs_cpxs_trans"
+"fpbs_cpx_trans_neq"
+"fpbs_fpbg"
+"fpbs_fpbg_trans"
+"fpbs_fpbsa"
+"fpbs_fpb_trans"
+"fpbs_fqup_trans"
+"fpbs_fqus_trans"
+"fpbs_ind"
+"fpbs_ind_dx"
+"fpbs_intro_alt"
+"fpbs_inv_alt"
+"fpbs_lleq_trans"
+"fpbs_lpxs_trans"
+"fpbs_refl"
+"fpbs_strap1"
+"fpbs_strap2"
+"fpbs_trans"
+"fqu"
+"fqu_bind_dx"
+"fqu_cpr_trans_dx"
+"fqu_cpr_trans_sn"
+"fqu_cpxs_trans"
+"fqu_cpxs_trans_neq"
+"fqu_cpx_trans"
+"fqu_cpx_trans_neq"
+"fqu_drop"
+"fqu_drop_lt"
+"fqu_flat_dx"
+"fqu_fqup"
+"fqu_fquq"
+"fqu_fwd_fw"
+"fqu_fwd_length_lref1"
+"fqu_fwd_length_lref1_aux"
+"fqu_inv_eq"
+"fqu_inv_eq_aux"
+"fqu_lpr_trans"
+"fqu_lpx_trans"
+"fqu_lref_O"
+"fqu_lref_S_lt"
+"fqup"
+"fqu_pair_sn"
+"fqup_ApplOmega_13"
+"fqup_bind_dx"
+"fqup_bind_dx_flat_dx"
+"fqup_cpxs_trans"
+"fqup_cpxs_trans_neq"
+"fqup_cpx_trans"
+"fqup_cpx_trans_neq"
+"fqup_drop"
+"fqup_flat_dx"
+"fqup_flat_dx_bind_dx"
+"fqup_flat_dx_pair_sn"
+"fqup_fpbg"
+"fqup_fpbs"
+"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"
+"fquq"
+"fquqa"
+"fquqa_drop"
+"fquqa_inv_fquq"
+"fquqa_refl"
+"fquq_bind_dx"
+"fquq_cpr_trans_dx"
+"fquq_cpr_trans_sn"
+"fquq_cpxs_trans"
+"fquq_cpxs_trans_neq"
+"fquq_cpx_trans"
+"fquq_cpx_trans_neq"
+"fquq_drop"
+"fquq_flat_dx"
+"fquq_fquqa"
+"fquq_fqus"
+"fquq_fwd_fw"
+"fquq_fwd_length_lref1"
+"fquq_fwd_length_lref1_aux"
+"fquq_inv_gen"
+"fquq_lpr_trans"
+"fquq_lpx_trans"
+"fquq_lref_O"
+"fquq_lstas_trans"
+"fquq_pair_sn"
+"fquq_refl"
+"fquq_sta_trans"
+"fqus"
+"fqus_cpxs_trans"
+"fqus_cpxs_trans_neq"
+"fqus_cpx_trans"
+"fqus_cpx_trans_neq"
+"fqus_drop"
+"fqus_fpbs"
+"fqus_fpbs_trans"
+"fqus_fqup_trans"
+"fqus_fwd_fw"
+"fqus_ind"
+"fqus_ind_dx"
+"fqus_inv_gen"
+"fqus_lpxs_fpbs"
+"fqus_lstas_trans"
+"fqus_refl"
+"fqus_strap1"
+"fqus_strap1_fqu"
+"fqus_strap2"
+"fqus_strap2_fqu"
+"fqu_sta_trans"
+"fqus_trans"
+"fqu_wf_ind"
+"frees"
+"frees_append"
+"frees_be"
+"frees_bind_dx"
+"frees_bind_dx_O"
+"frees_bind_sn"
+"frees_dec"
+"frees_eq"
+"frees_flat_dx"
+"frees_flat_sn"
+"frees_inv"
+"frees_inv_append"
+"frees_inv_append_aux"
+"frees_inv_bind"
+"frees_inv_bind_O"
+"frees_inv_flat"
+"frees_inv_gref"
+"frees_inv_lift_be"
+"frees_inv_lift_ge"
+"frees_inv_lref"
+"frees_inv_lref_free"
+"frees_inv_lref_ge"
+"frees_inv_lref_lt"
+"frees_inv_lref_skip"
+"frees_inv_sort"
+"frees_lift_ge"
+"frees_lref_be"
+"frees_lref_eq"
+"frees_lreq_conf"
+"frees_S"
+"frees_trans"
+"frees_weak"
+"fsb"
+"fsba"
+"fsba_fpbs_trans"
+"fsba_ind_alt"
+"fsba_intro"
+"fsba_inv_fsb"
+"fsb_fpbs_trans"
+"fsb_fsba"
+"fsb_ind_alt"
+"fsb_ind_fpbg"
+"fsb_intro"
+"fsb_inv_csx"
+"fw"
+"fw_lpair_sn"
+"fw_shift"
+"fw_tpair_dx"
+"fw_tpair_sn"
+"gcp"
+"gcp0_lifts"
+"gcp2_lifts"
+"gcp2_lifts_all"
+"gcr"
+"gcr_aaa"
+"gcr_lift"
+"gcr_lifts"
+"genv"
+"gget"
+"gget_dec"
+"gget_eq"
+"gget_gt"
+"gget_inv_eq"
+"gget_inv_gt"
+"gget_inv_lt"
+"gget_inv_lt_aux"
+"gget_lt"
+"gget_mono"
+"gget_total"
+"GRef"
+"ib2"
+"IH_da_cpr_lpr"
+"IH_lstas_cpr_lpr"
+"IH_snv_cpr_lpr"
+"IH_snv_lstas"
+"is_lift_dec"
+"item0"
+"item2"
+"LAtom"
+"lcosx"
+"lcosx_drop_trans_lt"
+"lcosx_inv_pair"
+"lcosx_inv_succ"
+"lcosx_inv_succ_aux"
+"lcosx_O"
+"lcosx_pair"
+"lcosx_skip"
+"lcosx_sort"
+"length"
+"length_inv_pos_dx"
+"length_inv_pos_dx_ltail"
+"length_inv_pos_sn"
+"length_inv_pos_sn_ltail"
+"length_inv_zero_dx"
+"length_inv_zero_sn"
+"lenv"
+"lenv_ind_alt"
+"lift"
+"lift_bind"
+"lift_conf_be"
+"lift_conf_O1"
+"lift_div_be"
+"lift_div_le"
+"lift_flat"
+"lift_fwd_pair1"
+"lift_fwd_pair2"
+"lift_fwd_tw"
+"lift_gref"
+"lift_inj"
+"lift_inv_bind1"
+"lift_inv_bind1_aux"
+"lift_inv_bind2"
+"lift_inv_bind2_aux"
+"lift_inv_flat1"
+"lift_inv_flat1_aux"
+"lift_inv_flat2"
+"lift_inv_flat2_aux"
+"lift_inv_gref1"
+"lift_inv_gref1_aux"
+"lift_inv_gref2"
+"lift_inv_gref2_aux"
+"lift_inv_lref1"
+"lift_inv_lref1_aux"
+"lift_inv_lref1_ge"
+"lift_inv_lref1_lt"
+"lift_inv_lref2"
+"lift_inv_lref2_aux"
+"lift_inv_lref2_be"
+"lift_inv_lref2_ge"
+"lift_inv_lref2_lt"
+"lift_inv_O2"
+"lift_inv_O2_aux"
+"lift_inv_pair_xy_x"
+"lift_inv_pair_xy_y"
+"lift_inv_sort1"
+"lift_inv_sort1_aux"
+"lift_inv_sort2"
+"lift_inv_sort2_aux"
+"lift_lref_ge"
+"lift_lref_ge_minus"
+"lift_lref_ge_minus_eq"
+"lift_lref_lt"
+"lift_mono"
+"lift_refl"
+"lifts"
+"lifts_applv"
+"lifts_bind"
+"lifts_cons"
+"lifts_flat"
+"lift_simple_dx"
+"lift_simple_sn"
+"lifts_inv_applv1"
+"lifts_inv_bind1"
+"lifts_inv_cons"
+"lifts_inv_cons_aux"
+"lifts_inv_flat1"
+"lifts_inv_gref1"
+"lifts_inv_lref1"
+"lifts_inv_nil"
+"lifts_inv_nil_aux"
+"lifts_inv_sort1"
+"lifts_lift_trans"
+"lifts_lift_trans_le"
+"lifts_nil"
+"lift_sort"
+"lift_split"
+"lifts_simple_dx"
+"lifts_simple_sn"
+"lifts_total"
+"lifts_trans"
+"liftsv"
+"liftsv_cons"
+"liftsv_liftv_trans_le"
+"liftsv_nil"
+"lift_total"
+"lift_trans_be"
+"lift_trans_ge"
+"lift_trans_le"
+"liftv"
+"liftv_cons"
+"liftv_inv_cons1"
+"liftv_inv_cons1_aux"
+"liftv_inv_nil1"
+"liftv_inv_nil1_aux"
+"liftv_mono"
+"liftv_nil"
+"liftv_total"
+"lleq"
+"lleq_aaa_trans"
+"lleq_bind"
+"lleq_bind_O"
+"lleq_bind_repl_O"
+"lleq_bind_repl_SO"
+"lleq_canc_dx"
+"lleq_canc_sn"
+"lleq_cpxs_trans"
+"lleq_cpx_trans"
+"lleq_dec"
+"lleq_flat"
+"lleq_fpbs"
+"lleq_fpbs_trans"
+"lleq_fpb_trans"
+"lleq_fqup_trans"
+"lleq_fquq_trans"
+"lleq_fqus_trans"
+"lleq_fqu_trans"
+"lleq_free"
+"lleq_fwd_bind_dx"
+"lleq_fwd_bind_O_dx"
+"lleq_fwd_bind_sn"
+"lleq_fwd_drop_dx"
+"lleq_fwd_drop_sn"
+"lleq_fwd_flat_dx"
+"lleq_fwd_flat_sn"
+"lleq_fwd_length"
+"lleq_fwd_lref"
+"lleq_fwd_lref_dx"
+"lleq_fwd_lref_sn"
+"lleq_ge"
+"lleq_ge_up"
+"lleq_gref"
+"lleq_ind"
+"lleq_ind_alt_r"
+"lleq_intro_alt"
+"lleq_intro_alt_r"
+"lleq_inv_alt"
+"lleq_inv_alt_r"
+"lleq_inv_bind"
+"lleq_inv_bind_O"
+"lleq_inv_flat"
+"lleq_inv_lift_be"
+"lleq_inv_lift_ge"
+"lleq_inv_lift_le"
+"lleq_inv_lref_ge"
+"lleq_inv_lref_ge_bi"
+"lleq_inv_lref_ge_dx"
+"lleq_inv_lref_ge_sn"
+"lleq_inv_S"
+"lleq_lift_ge"
+"lleq_lift_le"
+"lleq_llpx_sn_conf"
+"lleq_llpx_sn_trans"
+"lleq_lpxs_trans"
+"lleq_lpx_trans"
+"lleq_lref"
+"lleq_lreq_repl"
+"lleq_lreq_trans"
+"lleq_nlleq_trans"
+"lleq_refl"
+"lleq_skip"
+"lleq_sort"
+"lleq_sym"
+"lleq_trans"
+"lleq_transitive"
+"lleq_Y"
+"llor"
+"llor_atom"
+"llor_skip"
+"llor_tail_cofrees"
+"llor_tail_frees"
+"llor_total"
+"llpx_sn"
+"llpx_sn_alt"
+"llpx_sn_alt_inv_llpx_sn"
+"llpx_sn_alt_r"
+"llpx_sn_alt_r_bind"
+"llpx_sn_alt_r_flat"
+"llpx_sn_alt_r_free"
+"llpx_sn_alt_r_fwd_length"
+"llpx_sn_alt_r_fwd_lref"
+"llpx_sn_alt_r_gref"
+"llpx_sn_alt_r_ind_alt"
+"llpx_sn_alt_r_intro"
+"llpx_sn_alt_r_intro_alt"
+"llpx_sn_alt_r_inv_alt"
+"llpx_sn_alt_r_inv_bind"
+"llpx_sn_alt_r_inv_flat"
+"llpx_sn_alt_r_inv_lpx_sn"
+"llpx_sn_alt_r_lref"
+"llpx_sn_alt_r_skip"
+"llpx_sn_alt_r_sort"
+"llpx_sn_bind"
+"llpx_sn_bind_O"
+"llpx_sn_bind_repl_O"
+"llpx_sn_bind_repl_SO"
+"llpx_sn_co"
+"llpx_sn_dec"
+"llpx_sn_drop_conf_O"
+"llpx_sn_drop_trans_O"
+"llpx_sn_flat"
+"llpx_sn_free"
+"llpx_sn_frees_trans"
+"llpx_sn_frees_trans_aux"
+"llpx_sn_fwd_bind_dx"
+"llpx_sn_fwd_bind_O_dx"
+"llpx_sn_fwd_bind_sn"
+"llpx_sn_fwd_drop_dx"
+"llpx_sn_fwd_drop_sn"
+"llpx_sn_fwd_flat_dx"
+"llpx_sn_fwd_flat_sn"
+"llpx_sn_fwd_length"
+"llpx_sn_fwd_lref"
+"llpx_sn_fwd_lref_aux"
+"llpx_sn_fwd_lref_dx"
+"llpx_sn_fwd_lref_sn"
+"llpx_sn_fwd_pair_sn"
+"llpx_sn_ge"
+"llpx_sn_ge_up"
+"llpx_sn_gref"
+"llpx_sn_ind_alt_r"
+"llpx_sn_intro_alt_r"
+"llpx_sn_inv_alt_r"
+"llpx_sn_inv_bind"
+"llpx_sn_inv_bind_aux"
+"llpx_sn_inv_bind_O"
+"llpx_sn_inv_flat"
+"llpx_sn_inv_flat_aux"
+"llpx_sn_inv_lift_be"
+"llpx_sn_inv_lift_ge"
+"llpx_sn_inv_lift_le"
+"llpx_sn_inv_lift_O"
+"llpx_sn_inv_lref_ge_bi"
+"llpx_sn_inv_lref_ge_dx"
+"llpx_sn_inv_lref_ge_sn"
+"llpx_sn_inv_S"
+"llpx_sn_inv_S_aux"
+"llpx_sn_lift_ge"
+"llpx_sn_lift_le"
+"llpx_sn_llor_dx"
+"llpx_sn_llor_dx_sym"
+"llpx_sn_llor_fwd_sn"
+"llpx_sn_llpx_sn_alt"
+"llpx_sn_lpx_sn_alt_r"
+"llpx_sn_lref"
+"llpx_sn_lrefl"
+"llpx_sn_lreq_repl"
+"llpx_sn_lreq_trans"
+"llpx_sn_refl"
+"llpx_sn_skip"
+"llpx_sn_sort"
+"llpx_sn_TC_pair_dx"
+"llpx_sn_Y"
+"LPair"
+"lpair_ltail"
+"lpr"
+"lpr_aaa_conf"
+"lpr_conf"
+"lpr_cpcs_conf"
+"lpr_cpcs_trans"
+"lpr_cpr_conf"
+"lpr_cpr_conf_dx"
+"lpr_cpr_conf_sn"
+"lpr_cprs_conf"
+"lpr_cprs_trans"
+"lpr_cpr_trans"
+"lpr_drop_conf"
+"lpr_drop_trans_O1"
+"lpr_fpb"
+"lpr_fpbq"
+"lpr_fwd_length"
+"lpr_inv_atom1"
+"lpr_inv_atom2"
+"lpr_inv_pair1"
+"lpr_inv_pair2"
+"lpr_lprs"
+"lpr_lpx"
+"lpr_pair"
+"lpr_refl"
+"lprs"
+"lprs_aaa_conf"
+"lprs_conf"
+"lprs_cpcs_trans"
+"lprs_cpr_conf_dx"
+"lprs_cpr_conf_sn"
+"lprs_cprs_conf"
+"lprs_cprs_conf_dx"
+"lprs_cprs_conf_sn"
+"lprs_cprs_trans"
+"lprs_cpr_trans"
+"lprs_drop_conf"
+"lprs_drop_trans_O1"
+"lprs_fpbs"
+"lprs_fwd_length"
+"lprs_ind"
+"lprs_ind_alt"
+"lprs_ind_dx"
+"lprs_inv_atom1"
+"lprs_inv_atom2"
+"lprs_inv_pair1"
+"lprs_inv_pair2"
+"lprs_lpxs"
+"lprs_pair"
+"lprs_pair2"
+"lprs_pair_refl"
+"lprs_refl"
+"lprs_strap1"
+"lprs_strap2"
+"lprs_strip"
+"lprs_trans"
+"lpx"
+"lpx_aaa_conf"
+"lpx_cpx_frees_trans"
+"lpx_cpxs_trans"
+"lpx_cpx_trans"
+"lpx_drop_conf"
+"lpx_drop_trans_O1"
+"lpx_fqup_trans"
+"lpx_fquq_trans"
+"lpx_fqus_trans"
+"lpx_fqu_trans"
+"lpx_frees_trans"
+"lpx_fwd_length"
+"lpx_inv_atom1"
+"lpx_inv_atom2"
+"lpx_inv_pair"
+"lpx_inv_pair1"
+"lpx_inv_pair2"
+"lpx_lleq_fqup_trans"
+"lpx_lleq_fquq_trans"
+"lpx_lleq_fqus_trans"
+"lpx_lleq_fqu_trans"
+"lpx_lpxs"
+"lpx_pair"
+"lpx_refl"
+"lpxs"
+"lpxs_aaa_conf"
+"lpxs_cpxs_trans"
+"lpxs_cpx_trans"
+"lpxs_drop_conf"
+"lpxs_drop_trans_O1"
+"lpxs_fpbg"
+"lpxs_fpbs"
+"lpxs_fpbs_trans"
+"lpxs_fqup_trans"
+"lpxs_fquq_trans"
+"lpxs_fqus_trans"
+"lpxs_fwd_length"
+"lpxs_ind"
+"lpxs_ind_alt"
+"lpxs_ind_dx"
+"lpxs_inv_atom1"
+"lpxs_inv_atom2"
+"lpxs_inv_pair1"
+"lpxs_inv_pair2"
+"lpxs_lleq_fpbs"
+"lpxs_lleq_fqup_trans"
+"lpxs_lleq_fquq_trans"
+"lpxs_lleq_fqus_trans"
+"lpxs_lleq_fqu_trans"
+"lpx_sn"
+"lpx_sn_alt"
+"lpx_sn_alt_atom"
+"lpx_sn_alt_fwd_length"
+"lpx_sn_alt_inv_atom1"
+"lpx_sn_alt_inv_atom2"
+"lpx_sn_alt_inv_lpx_sn"
+"lpx_sn_alt_inv_pair1"
+"lpx_sn_alt_inv_pair2"
+"lpx_sn_alt_pair"
+"lpx_sn_atom"
+"lpx_sn_conf"
+"lpx_sn_confluent"
+"lpx_sn_deliftable_dropable"
+"lpx_sn_dropable"
+"lpx_sn_dropable_aux"
+"lpx_sn_drop_conf"
+"lpx_sn_drop_trans"
+"lpx_sn_fwd_length"
+"lpx_sn_intro_alt"
+"lpx_sn_inv_alt"
+"lpx_sn_inv_atom1"
+"lpx_sn_inv_atom1_aux"
+"lpx_sn_inv_atom2"
+"lpx_sn_inv_atom2_aux"
+"lpx_sn_inv_pair"
+"lpx_sn_inv_pair1"
+"lpx_sn_inv_pair1_aux"
+"lpx_sn_inv_pair2"
+"lpx_sn_inv_pair2_aux"
+"lpx_sn_liftable_dedropable"
+"lpxs_nlleq_inv_step_sn"
+"lpx_sn_llpx_sn"
+"lpx_sn_lpx_sn_alt"
+"lpx_sn_LTC_TC_lpx_sn"
+"lpx_sn_pair"
+"lpx_sn_refl"
+"lpx_sn_trans"
+"lpx_sn_transitive"
+"lpxs_pair"
+"lpxs_pair2"
+"lpxs_pair_refl"
+"lpxs_refl"
+"lpxs_strap1"
+"lpxs_strap2"
+"lpxs_trans"
+"LRef"
+"lreq"
+"lreq_atom"
+"lreq_canc_dx"
+"lreq_canc_sn"
+"lreq_cpxs_trans"
+"lreq_cpx_trans"
+"lreq_drop_conf_be"
+"lreq_drop_trans_be"
+"lreq_frees_trans"
+"lreq_fwd_length"
+"lreq_inv_atom1"
+"lreq_inv_atom1_aux"
+"lreq_inv_atom2"
+"lreq_inv_O_Y"
+"lreq_inv_O_Y_aux"
+"lreq_inv_pair"
+"lreq_inv_pair1"
+"lreq_inv_pair1_aux"
+"lreq_inv_pair2"
+"lreq_inv_succ"
+"lreq_inv_succ1"
+"lreq_inv_succ1_aux"
+"lreq_inv_succ2"
+"lreq_inv_zero1"
+"lreq_inv_zero1_aux"
+"lreq_inv_zero2"
+"lreq_join"
+"lreq_lleq_trans"
+"lreq_llpx_sn_trans"
+"lreq_lpxs_trans_lleq"
+"lreq_lpxs_trans_lleq_aux"
+"lreq_lpx_trans_lleq"
+"lreq_lpx_trans_lleq_aux"
+"lreq_O2"
+"lreq_pair"
+"lreq_pair_lt"
+"lreq_pair_O_Y"
+"lreq_refl"
+"lreq_succ"
+"lreq_succ_lt"
+"lreq_sym"
+"lreq_trans"
+"lreq_zero"
+"lstas"
+"lstas_aaa_conf"
+"lstas_appl"
+"lstas_bind"
+"lstas_cast"
+"lstas_conf"
+"lstas_conf_le"
+"lstas_correct"
+"lstas_cpcs_lpr"
+"lstas_cpr"
+"lstas_cpr_aux"
+"lstas_cpr_lpr"
+"lstas_cpr_lpr_aux"
+"lstas_cprs_lpr"
+"lstas_cprs_lpr_aux"
+"lstas_cpxs"
+"lstas_da_conf"
+"lstas_fpbg"
+"lstas_fpbs"
+"lstas_inv_appl1"
+"lstas_inv_appl1_aux"
+"lstas_inv_bind1"
+"lstas_inv_bind1_aux"
+"lstas_inv_cast1"
+"lstas_inv_cast1_aux"
+"lstas_inv_da"
+"lstas_inv_da_ge"
+"lstas_inv_gref1"
+"lstas_inv_gref1_aux"
+"lstas_inv_lift1"
+"lstas_inv_lref1"
+"lstas_inv_lref1_aux"
+"lstas_inv_lref1_O"
+"lstas_inv_lref1_S"
+"lstas_inv_refl_pos"
+"lstas_inv_sort1"
+"lstas_inv_sort1_aux"
+"lstas_ldef"
+"lstas_lift"
+"lstas_llpx_sn_conf"
+"lstas_lstas"
+"lstas_mono"
+"lstas_scpds"
+"lstas_scpds_aux"
+"lstas_scpds_trans"
+"lstas_scpes_trans"
+"lstas_sort"
+"lstas_split"
+"lstas_split_aux"
+"lstas_succ"
+"lstas_trans"
+"lstas_zero"
+"lsuba"
+"lsuba_aaa_conf"
+"lsuba_aaa_trans"
+"lsuba_atom"
+"lsuba_beta"
+"lsuba_drop_O1_conf"
+"lsuba_drop_O1_trans"
+"lsuba_fwd_lsubr"
+"lsuba_inv_atom1"
+"lsuba_inv_atom1_aux"
+"lsuba_inv_atom2"
+"lsuba_inv_atom2_aux"
+"lsuba_inv_pair1"
+"lsuba_inv_pair1_aux"
+"lsuba_inv_pair2"
+"lsuba_inv_pair2_aux"
+"lsuba_lsubc"
+"lsuba_pair"
+"lsuba_refl"
+"lsuba_trans"
+"lsubc"
+"lsubc_atom"
+"lsubc_beta"
+"lsubc_drop_O1_trans"
+"lsubc_fwd_lsubr"
+"lsubc_inv_atom1"
+"lsubc_inv_atom1_aux"
+"lsubc_inv_atom2"
+"lsubc_inv_atom2_aux"
+"lsubc_inv_pair1"
+"lsubc_inv_pair1_aux"
+"lsubc_inv_pair2"
+"lsubc_inv_pair2_aux"
+"lsubc_pair"
+"lsubc_refl"
+"lsubd"
+"lsubd_atom"
+"lsubd_beta"
+"lsubd_da_conf"
+"lsubd_da_trans"
+"lsubd_drop_O1_conf"
+"lsubd_drop_O1_trans"
+"lsubd_fwd_lsubr"
+"lsubd_inv_atom1"
+"lsubd_inv_atom1_aux"
+"lsubd_inv_atom2"
+"lsubd_inv_atom2_aux"
+"lsubd_inv_pair1"
+"lsubd_inv_pair1_aux"
+"lsubd_inv_pair2"
+"lsubd_inv_pair2_aux"
+"lsubd_pair"
+"lsubd_refl"
+"lsubd_trans"
+"lsubr"
+"lsubr_atom"
+"lsubr_beta"
+"lsubr_cpcs_trans"
+"lsubr_cprs_trans"
+"lsubr_cpr_trans"
+"lsubr_cpxs_trans"
+"lsubr_cpx_trans"
+"lsubr_fwd_drop2_abbr"
+"lsubr_fwd_drop2_pair"
+"lsubr_fwd_length"
+"lsubr_inv_abbr2"
+"lsubr_inv_abbr2_aux"
+"lsubr_inv_abst1"
+"lsubr_inv_abst1_aux"
+"lsubr_inv_atom1"
+"lsubr_inv_atom1_aux"
+"lsubr_inv_pair1"
+"lsubr_inv_pair1_aux"
+"lsubr_pair"
+"lsubr_refl"
+"lsubr_trans"
+"lsubsv"
+"lsubsv_atom"
+"lsubsv_beta"
+"lsubsv_cpcs_trans"
+"lsubsv_cprs_trans"
+"lsubsv_drop_O1_conf"
+"lsubsv_drop_O1_trans"
+"lsubsv_fwd_lsuba"
+"lsubsv_fwd_lsubd"
+"lsubsv_fwd_lsubr"
+"lsubsv_inv_atom1"
+"lsubsv_inv_atom1_aux"
+"lsubsv_inv_atom2"
+"lsubsv_inv_atom2_aux"
+"lsubsv_inv_pair1"
+"lsubsv_inv_pair1_aux"
+"lsubsv_inv_pair2"
+"lsubsv_inv_pair2_aux"
+"lsubsv_lstas_trans"
+"lsubsv_pair"
+"lsubsv_refl"
+"lsubsv_scpds_trans"
+"lsubsv_snv_trans"
+"lsubsv_sta_trans"
+"lsuby"
+"lsuby_atom"
+"lsuby_cpysa_trans"
+"lsuby_cpys_trans"
+"lsuby_cpy_trans"
+"lsuby_drop_trans_be"
+"lsuby_fwd_length"
+"lsuby_inv_atom1"
+"lsuby_inv_atom1_aux"
+"lsuby_inv_pair1"
+"lsuby_inv_pair1_aux"
+"lsuby_inv_pair2"
+"lsuby_inv_pair2_aux"
+"lsuby_inv_succ1"
+"lsuby_inv_succ1_aux"
+"lsuby_inv_succ2"
+"lsuby_inv_succ2_aux"
+"lsuby_inv_zero1"
+"lsuby_inv_zero1_aux"
+"lsuby_inv_zero2"
+"lsuby_inv_zero2_aux"
+"lsuby_O2"
+"lsuby_pair"
+"lsuby_pair_lt"
+"lsuby_pair_O_Y"
+"lsuby_refl"
+"lsuby_succ"
+"lsuby_succ_lt"
+"lsuby_sym"
+"lsuby_trans"
+"lsuby_zero"
+"lsx"
+"lsxa"
+"lsxa_ind"
+"lsxa_intro"
+"lsxa_intro_aux"
+"lsxa_intro_lpx"
+"lsxa_inv_lsx"
+"lsxa_lleq_trans"
+"lsxa_lpxs_trans"
+"lsx_atom"
+"lsx_bind"
+"lsx_bind_lpxs_aux"
+"lsx_cpx_trans_lcosx"
+"lsx_cpx_trans_O"
+"lsx_flat"
+"lsx_flat_lpxs"
+"lsx_fwd_bind_dx"
+"lsx_fwd_bind_sn"
+"lsx_fwd_flat_dx"
+"lsx_fwd_flat_sn"
+"lsx_fwd_lref_be"
+"lsx_fwd_pair_sn"
+"lsx_ge"
+"lsx_ge_up"
+"lsx_gref"
+"lsx_ind"
+"lsx_ind_alt"
+"lsx_intro"
+"lsx_intro_alt"
+"lsx_inv_bind"
+"lsx_inv_flat"
+"lsx_inv_lift_be"
+"lsx_inv_lift_ge"
+"lsx_inv_lift_le"
+"lsx_lift_ge"
+"lsx_lift_le"
+"lsx_lleq_trans"
+"lsx_lpxs_trans"
+"lsx_lpx_trans"
+"lsx_lref_be"
+"lsx_lref_be_lpxs"
+"lsx_lref_free"
+"lsx_lref_skip"
+"lsx_lreq_conf"
+"lsx_lsxa"
+"lsx_sort"
+"ltail_length"
+"lw"
+"lw_pair"
+"minuss"
+"minuss_ge"
+"minuss_inv_cons1"
+"minuss_inv_cons1_aux"
+"minuss_inv_cons1_ge"
+"minuss_inv_cons1_lt"
+"minuss_inv_nil1"
+"minuss_inv_nil1_aux"
+"minuss_lt"
+"minuss_nil"
+"mk_gcp"
+"mk_gcr"
+"mk_sd"
+"mk_sh"
+"nexts_dec"
+"nexts_inj"
+"nexts_le"
+"nexts_lt"
+"nf"
+"nlift_bind_dx"
+"nlift_bind_sn"
+"nlift_flat_dx"
+"nlift_flat_sn"
+"nlift_inv_bind"
+"nlift_inv_flat"
+"nlift_inv_lref_be_SO"
+"nlift_lref_be_SO"
+"nlleq_inv_bind"
+"nlleq_inv_bind_O"
+"nlleq_inv_flat"
+"nlleq_lleq_div"
+"nllpx_sn_inv_bind"
+"nllpx_sn_inv_bind_O"
+"nllpx_sn_inv_flat"
+"Omega1"
+"Omega2"
+"pluss"
+"pluss_inv_cons2"
+"pluss_inv_nil2"
+"rfw"
+"rfw_lpair_dx"
+"rfw_lpair_sn"
+"rfw_shift"
+"rfw_tpair_dx"
+"rfw_tpair_sn"
+"ri2"
+"S1"
+"S2"
+"S3"
+"S4"
+"S5"
+"S6"
+"S7"
+"scpds"
+"scpds_aaa_conf"
+"scpds_conf_eq"
+"scpds_cpr_lpr_aux"
+"scpds_cprs_trans"
+"scpds_div"
+"scpds_fwd_cprs"
+"scpds_fwd_cpxs"
+"scpds_inv_abbr_abst"
+"scpds_inv_abst1"
+"scpds_inv_lift1"
+"scpds_inv_lstas_eq"
+"scpds_lift"
+"scpds_strap1"
+"scpds_strap2"
+"scpes"
+"scpes_aaa_mono"
+"scpes_canc_dx"
+"scpes_canc_sn"
+"scpes_cpr_lpr_aux"
+"scpes_inv_abst2"
+"scpes_inv_lstas_eq"
+"scpes_le_aux"
+"scpes_refl"
+"scpes_sym"
+"scpes_trans"
+"sd"
+"sd_d"
+"sd_d_correct"
+"sd_d_SS"
+"sd_O"
+"sd_SO"
+"sh"
+"sh_N"
+"shnv"
+"shnv_cast"
+"shnv_inv_cast"
+"shnv_inv_cast_aux"
+"shnv_inv_snv"
+"simple"
+"simple_atom"
+"simple_flat"
+"simple_inv_bind"
+"simple_inv_bind_aux"
+"simple_inv_pair"
+"simple_tsts_repl_dx"
+"simple_tsts_repl_sn"
+"snv"
+"snv_appl"
+"snv_bind"
+"snv_cast"
+"snv_cast_scpes"
+"snv_cpr_lpr"
+"snv_cpr_lpr_aux"
+"snv_cprs_lpr"
+"snv_cprs_lpr_aux"
+"snv_extended"
+"snv_fqu_conf"
+"snv_fqup_conf"
+"snv_fquq_conf"
+"snv_fqus_conf"
+"snv_fwd_aaa"
+"snv_fwd_da"
+"snv_fwd_fsb"
+"snv_fwd_lstas"
+"snv_inv_appl"
+"snv_inv_appl_aux"
+"snv_inv_bind"
+"snv_inv_bind_aux"
+"snv_inv_cast"
+"snv_inv_cast_aux"
+"snv_inv_gref"
+"snv_inv_gref_aux"
+"snv_inv_lift"
+"snv_inv_lref"
+"snv_inv_lref_aux"
+"snv_lift"
+"snv_lref"
+"snv_lstas"
+"snv_lstas_aux"
+"snv_preserve"
+"snv_restricted"
+"snv_shnv_cast"
+"snv_sort"
+"Sort"
+"sta_cprs_scpds"
+"sta_cpx"
+"sta_cpx_aux"
+"sta_fpb"
+"sta_fpbg"
+"sta_fpbq"
+"sta_fpbs"
+"sta_ldec"
+"TAtom"
+"TC_lpx_sn_fwd_length"
+"TC_lpx_sn_ind"
+"TC_lpx_sn_inv_atom1"
+"TC_lpx_sn_inv_atom2"
+"TC_lpx_sn_inv_lpx_sn_LTC"
+"TC_lpx_sn_inv_pair1"
+"TC_lpx_sn_inv_pair1_aux"
+"TC_lpx_sn_inv_pair2"
+"TC_lpx_sn_pair"
+"TC_lpx_sn_pair_refl"
+"term"
+"tir_atom"
+"tix_lref"
+"TPair"
+"tpr_cpr"
+"tprs_cprs"
+"trr_inv_atom"
+"trx_inv_atom"
+"tsts"
+"tsts_atom"
+"tsts_canc_dx"
+"tsts_canc_sn"
+"tsts_dec"
+"tsts_inv_atom1"
+"tsts_inv_atom1_aux"
+"tsts_inv_atom2"
+"tsts_inv_atom2_aux"
+"tsts_inv_bind_applv_simple"
+"tsts_inv_pair1"
+"tsts_inv_pair1_aux"
+"tsts_inv_pair2"
+"tsts_inv_pair2_aux"
+"tsts_pair"
+"tsts_refl"
+"tsts_sym"
+"tsts_trans"
+"tw"
+"tw_pos"
+"unfold"
+"unfold_bind"
+"unfold_flat"
+"unfold_lref"
+"unfold_sort"