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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/names.txt b/matita/matita/contribs/lambdadelta/basic_2/names.txt
index 852ff574b..b0dd49768 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/names.txt
+++ b/matita/matita/contribs/lambdadelta/basic_2/names.txt
@@ -1,1207 +1,1207 @@
-aaa_cpm_SO
-aaa_csx
-aaa_fsb
-aaa_ind_csx
-aaa_ind_csx_aux
-aaa_ind_csx_cpxs
-aaa_ind_csx_cpxs_aux
-aaa_ind_fpb
-aaa_ind_fpb_aux
-aaa_ind_fpbg
-aaa_ind_fpbg_aux
-cnr
-cnr_abbr_neg
-cnr_abst
-cnr_appl_simple
-cnr_dec_teqx
-cnr_gref
-cnr_inv_abbr_neg
-cnr_inv_abst
-cnr_inv_appl
-cnr_inv_cast
-cnr_inv_lifts
-cnr_inv_lref_abbr
-cnr_lifts
-cnr_lref_abst
-cnr_lref_atom
-cnr_lref_unit
-cnr_sort
-cnuw
-cnuw_abbr_neg
-cnuw_abst
-cnuw_appl_simple
-cnuw_atom_drops
-cnuw_cpms_trans
-cnuw_ctop
-cnuw_dec
-cnuw_dec_ex
-cnuw_fwd_appl
-cnuw_gref
-cnuw_inv_abbr_pos
-cnuw_inv_cast
-cnuw_inv_lifts
-cnuw_inv_zero_pair
-cnuw_lifts
-cnuw_lref
-cnuw_sort
-cnuw_unit_drops
-cnuw_zero_unit
-cnv
-cnv_acle_omega
-cnv_acle_one
-cnv_acle_trans
-cnv_appl
-cnv_appl_cpes
-cnv_appl_cpts
-cnv_appl_ge
-cnv_appl_ntas_ge
-cnv_bind
-cnv_cast
-cnv_cast_cpes
-cnv_cast_cpts
-cnv_cpcs_dec
-cnv_cpes_dec
-cnv_cpm_conf_lpr_appl_appl_aux
-cnv_cpm_conf_lpr_appl_beta_aux
-cnv_cpm_conf_lpr_appl_theta_aux
-cnv_cpm_conf_lpr_atom_atom_aux
-cnv_cpm_conf_lpr_atom_delta_aux
-cnv_cpm_conf_lpr_atom_ell_aux
-cnv_cpm_conf_lpr_atom_ess_aux
-cnv_cpm_conf_lpr_aux
-cnv_cpm_conf_lpr_beta_beta_aux
-cnv_cpm_conf_lpr_bind_bind_aux
-cnv_cpm_conf_lpr_bind_zeta_aux
-cnv_cpm_conf_lpr_cast_cast_aux
-cnv_cpm_conf_lpr_cast_ee_aux
-cnv_cpm_conf_lpr_cast_epsilon_aux
-cnv_cpm_conf_lpr_delta_delta_aux
-cnv_cpm_conf_lpr_delta_ell_aux
-cnv_cpm_conf_lpr_ee_ee_aux
-cnv_cpm_conf_lpr_epsilon_ee_aux
-cnv_cpm_conf_lpr_epsilon_epsilon_aux
-cnv_cpm_conf_lpr_sub
-cnv_cpm_conf_lpr_theta_theta_aux
-cnv_cpm_conf_lpr_zeta_zeta_aux
-cnv_cpmre_cpms_conf
-cnv_cpmre_mono
-cnv_cpmre_trans
-cnv_cpms_conf
-cnv_cpms_conf_eq
-cnv_cpms_conf_lpr
-cnv_cpms_conf_lpr_aux
-cnv_cpms_conf_lpr_refl_tneqx_sub
-cnv_cpms_conf_lpr_step_tneqx_sub
-cnv_cpms_conf_lpr_teqx_teqx_aux
-cnv_cpms_conf_lpr_teqx_tneqx_aux
-cnv_cpms_conf_lpr_tneqx_tneqx_aux
-cnv_cpms_fwd_appl_sn_decompose
-cnv_cpms_nta
-cnv_cpms_ntas
-cnv_cpms_strip_lpr_sub
-cnv_cpms_teqx_conf_lpr_aux
-cnv_cpms_teqx_strip_lpr_aux
-cnv_cpms_trans
-cnv_cpms_trans_lpr
-cnv_cpms_trans_lpr_sub
-cnv_cpm_teqx_conf_lpr
-cnv_cpm_teqx_conf_lpr_appl_appl_aux
-cnv_cpm_teqx_conf_lpr_atom_atom_aux
-cnv_cpm_teqx_conf_lpr_atom_ess_aux
-cnv_cpm_teqx_conf_lpr_aux
-cnv_cpm_teqx_conf_lpr_bind_bind_aux
-cnv_cpm_teqx_conf_lpr_cast_cast_aux
-cnv_cpm_teqx_cpm_trans_aux
-cnv_cpm_teqx_cpm_trans_sub
-cnv_cpm_trans
-cnv_cpm_trans_lpr
-cnv_cpm_trans_lpr_aux
-cnv_cpmuwe_mono
-cnv_cpmuwe_trans
-cnv_cpr_teqx_fwd_refl
-cnv_dec
-cnv_fpbg_refl_false
-cnv_fqu_conf
-cnv_fqup_conf
-cnv_fquq_conf
-cnv_fqus_conf
-cnv_fwd_aaa
-cnv_fwd_cpms_abst_dx_le
-cnv_fwd_cpm_SO
-cnv_fwd_cpms_total
-cnv_fwd_csx
-cnv_fwd_flat
-cnv_fwd_fsb
-cnv_fwd_pair_sn
-cnv_ind_cpes
-cnv_inv_appl
-cnv_inv_appl_aux
-cnv_inv_appl_cpes
-cnv_inv_appl_cpts
-cnv_inv_appl_ntas
-cnv_inv_bind
-cnv_inv_bind_aux
-cnv_inv_cast
-cnv_inv_cast_aux
-cnv_inv_cast_cpes
-cnv_inv_cast_cpts
-cnv_inv_gref
-cnv_inv_gref_aux
-cnv_inv_lifts
-cnv_inv_lref
-cnv_inv_lref_atom
-cnv_inv_lref_aux
-cnv_inv_lref_drops
-cnv_inv_lref_pair
-cnv_inv_lref_unit
-cnv_inv_zero
-cnv_inv_zero_aux
-cnv_lifts
-cnv_lprs_trans
-cnv_lpr_trans
-cnv_lref
-cnv_lref_drops
-cnv_nta_sn
-cnv_preserve
-cnv_R_cpmuwe_dec
-cnv_R_cpmuwe_total
-cnv_sort
-cnv_zero
-cnx
-cnx_abst
-cnx_appl_simple
-cnx_csx
-cnx_inv_abbr_neg
-cnx_inv_abbr_pos
-cnx_inv_abst
-cnx_inv_appl
-cnx_inv_cast
-cnx_inv_lifts
-cnx_inv_lref_pair
-cnx_lifts
-cnx_lref_atom
-cnx_lref_unit
-cnx_sort
-cnx_teqx_trans
-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_step_dx
-cpcs_cprs_step_sn
-cpcs_cpr_step_dx
-cpcs_cpr_step_sn
-cpcs_flat
-cpcs_flat_dx_cpr_rev
-cpcs_ind_dx
-cpcs_ind_sn
-cpcs_inv_abst_bi_dx
-cpcs_inv_abst_bi_sn
-cpcs_inv_abst_dx
-cpcs_inv_abst_sn
-cpcs_inv_cprs
-cpcs_inv_lifts_bi
-cpcs_inv_sort_abst
-cpcs_inv_sort_bi
-cpcs_lifts_bi
-cpcs_refl
-cpcs_step_dx
-cpcs_step_sn
-cpcs_strip
-cpcs_sym
-cpcs_trans
-cpc_sym
-cpes
-cpes_aaa_mono
-cpes_cpes_trans
-cpes_cpms_div
-cpes_cprs_trans
-cpes_fwd_abst_bi
-cpes_refl
-cpes_refl_aaa
-cpes_sym
-cpg
-cpg_appl
-cpg_atom
-cpg_beta
-cpg_bind
-cpg_cast
-cpg_cpx
-cpg_delta
-cpg_delta_drops
-cpg_ee
-cpg_ell
-cpg_ell_drops
-cpg_eps
-cpg_ess
-cpg_fwd_bind1_minus
-cpg_inv_abbr1
-cpg_inv_abst1
-cpg_inv_appl1
-cpg_inv_appl1_aux
-cpg_inv_appl1_simple
-cpg_inv_atom1
-cpg_inv_atom1_aux
-cpg_inv_atom1_drops
-cpg_inv_bind1
-cpg_inv_bind1_aux
-cpg_inv_cast1
-cpg_inv_cast1_aux
-cpg_inv_gref1
-cpg_inv_lifts_bi
-cpg_inv_lifts_sn
-cpg_inv_lref1
-cpg_inv_lref1_bind
-cpg_inv_lref1_drops
-cpg_inv_sort1
-cpg_inv_zero1
-cpg_inv_zero1_pair
-cpg_lifts_bi
-cpg_lifts_sn
-cpg_lref
-cpg_refl
-cpg_theta
-cpg_zeta
-cpm
-cpm_aaa_conf
-cpm_appl
-cpm_beta
-cpm_bind
-cpm_bind2
-cpm_bind_unit
-cpm_cast
-cpm_cpms
-cpm_delta
-cpm_delta_drops
-cpm_ee
-cpm_ell
-cpm_ell_drops
-cpm_eps
-cpm_ess
-cpm_fpb
-cpm_fpbq
-cpm_fsge_comp
-cpm_fwd_bind1_minus
-cpm_fwd_cpx
-cpm_fwd_plus
-cpm_fwd_plus_aux
-cpm_ind
-cpm_inv_abbr1
-cpm_inv_abst1
-cpm_inv_abst_bi
-cpm_inv_appl1
-cpm_inv_appl1_simple
-cpm_inv_atom1
-cpm_inv_atom1_drops
-cpm_inv_bind1
-cpm_inv_cast1
-cpm_inv_gref1
-cpm_inv_lifts_bi
-cpm_inv_lifts_sn
-cpm_inv_lref1
-cpm_inv_lref1_ctop
-cpm_inv_lref1_drops
-cpm_inv_sort1
-cpm_inv_zero1
-cpm_inv_zero1_unit
-cpm_lifts_bi
-cpm_lifts_sn
-cpm_lref
-cpmre
-cpmre_fwd_cpms
-cpmre_intro
-cpmre_total_aaa
-cpm_rex_conf
-cpms
-cpms_aaa_conf
-cpms_abst_dx_le_aaa
-cpms_appl
-cpms_appl_dx
-cpms_beta
-cpms_beta_dx
-cpms_beta_rc
-cpms_bind
-cpms_bind2_dx
-cpms_bind_alt
-cpms_bind_dx
-cpms_cast
-cpms_cast_sn
-cpms_cprre_trans
-cpms_cprs_trans
-cpms_delta
-cpms_delta_drops
-cpms_div
-cpms_ee
-cpms_ell
-cpms_ell_drops
-cpms_eps
-cpms_fpbg_trans
-cpms_fwd_cpxs
-cpms_fwd_fpbs
-cpms_ind_dx
-cpms_ind_sn
-cpms_inv_abbr_abst
-cpms_inv_abbr_sn_dx
-cpms_inv_abst_bi
-cpms_inv_abst_sn
-cpms_inv_abst_sn_cprs
-cpms_inv_appl_sn
-cpms_inv_cast1
-cpms_inv_delta_sn
-cpms_inv_ell_sn
-cpms_inv_gref1
-cpms_inv_lifts_bi
-cpms_inv_lifts_sn
-cpms_inv_lref1_ctop
-cpms_inv_lref1_drops
-cpms_inv_lref_sn
-cpms_inv_plus
-cpms_inv_sort1
-cpms_inv_succ_sn
-cpms_inv_zero1_unit
-cpms_lifts_bi
-cpms_lifts_sn
-cpms_lref
-cpm_sort
-cpms_reqx_conf_dx
-cpms_reqx_conf_sn
-cpms_sort
-cpms_step_dx
-cpms_step_sn
-cpms_teqx_ind_sn
-cpms_theta
-cpms_theta_dx
-cpms_theta_rc
-cpms_tneqx_fwd_fpbg
-cpms_tneqx_fwd_step_sn_aux
-cpms_total_aaa
-cpms_trans
-cpms_trans_swap
-cpms_zeta
-cpms_zeta_dx
-cpm_teqx_free
-cpm_teqx_ind
-cpm_teqx_inv_appl_sn
-cpm_teqx_inv_atom_sn
-cpm_teqx_inv_bind_dx
-cpm_teqx_inv_bind_sn
-cpm_teqx_inv_bind_sn_void
-cpm_teqx_inv_cast_sn
-cpm_teqx_inv_lref_sn
-cpm_theta
-cpm_tneqx_cpm_cpms_teqx_sym_fwd_fpbg
-cpm_tneqx_cpm_fpbg
-cpmuwe
-cpmuwe_abbr_neg
-cpmuwe_abst
-cpmuwe_ctop
-cpmuwe_fwd_cpms
-cpmuwe_gref
-cpmuwe_intro
-cpmuwe_sort
-cpmuwe_total_csx
-cpmuwe_zero_unit
-cpm_zeta
-cpr_abbr_pos_tneqx
-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_conf_cpcs
-cpr_cprs_div
-cpr_div
-cpr_ext
-cpr_flat
-cpr_ind
-cpr_inv_atom1
-cpr_inv_atom1_drops
-cpr_inv_cast1
-cpr_inv_flat1
-cpr_inv_gref1
-cpr_inv_lref1
-cpr_inv_lref1_drops
-cpr_inv_sort1
-cpr_inv_zero1
-cpr_pair_sn
-cprre_cprs_conf
-cpr_refl
-cprre_mono
-cprre_total_csx
-cprs_abbr_pos_twneq
-cprs_conf
-cprs_conf_cpcs
-cprs_cpr_conf_cpcs
-cprs_cpr_div
-cprs_CTC
-cprs_div
-cprs_ext
-cprs_flat
-cprs_flat_dx
-cprs_flat_sn
-cprs_ind_dx
-cprs_ind_sn
-cprs_inv_appl_sn
-cprs_inv_cast1
-cprs_inv_cnr_sn
-cprs_inv_CTC
-cprs_inv_lref1_drops
-cprs_inv_sort1
-cprs_lpr_conf_dx
-cprs_lpr_conf_sn
-cprs_nta_trans
-cprs_nta_trans_cnv
-cprs_refl
-cprs_step_dx
-cprs_step_sn
-cprs_strip
-cprs_trans
-cpr_subst
-cpt
-cpt_appl
-cpt_bind
-cpt_cast
-cpt_cpts
-cpt_delta
-cpt_delta_drops
-cpt_ee
-cpt_ell
-cpt_ell_drops
-cpt_ess
-cpt_fwd_cpm
-cpt_fwd_plus
-cpt_fwd_plus_aux
-cpt_ind
-cpt_inv_appl_sn
-cpt_inv_atom_sn
-cpt_inv_atom_sn_drops
-cpt_inv_bind_sn
-cpt_inv_cast_sn
-cpt_inv_gref_sn
-cpt_inv_lifts_bi
-cpt_inv_lifts_sn
-cpt_inv_lref_sn
-cpt_inv_lref_sn_ctop
-cpt_inv_lref_sn_drops
-cpt_inv_sort_sn
-cpt_inv_zero_sn
-cpt_inv_zero_sn_unit
-cpt_lifts_bi
-cpt_lifts_sn
-cpt_lref
-cpt_refl
-cpts
-cpts_appl_dx
-cpts_bind_dx
-cpts_cast_sn
-cpts_cpms_conf_eq
-cpts_cprs_trans
-cpts_delta
-cpts_delta_drops
-cpts_ee
-cpts_ell
-cpts_ell_drops
-cpts_fwd_cpms
-cpts_ind_dx
-cpts_ind_sn
-cpts_inv_cast_sn
-cpts_inv_delta_sn
-cpts_inv_ell_sn
-cpts_inv_gref_sn
-cpts_inv_lifts_bi
-cpts_inv_lifts_sn
-cpts_inv_lref_sn
-cpts_inv_lref_sn_ctop
-cpts_inv_lref_sn_drops
-cpts_inv_sort_sn
-cpts_inv_succ_sn
-cpts_inv_zero_sn_unit
-cpts_lifts_bi
-cpts_lifts_sn
-cpts_lref
-cpt_sort
-cpts_refl
-cpts_sort
-cpts_step_dx
-cpts_step_sn
-cpts_total_aaa
-cpx
-cpx_aaa_conf
-cpx_aaa_conf_lpx
-cpx_beta
-cpx_bind
-cpx_bind2
-cpx_bind_unit
-cpx_cpxs
-cpx_delta
-cpx_delta_drops
-cpx_ee
-cpx_eps
-cpx_ess
-cpx_ext
-cpx_flat
-cpx_fsge_comp
-cpx_fwd_bind1_minus
-cpx_ind
-cpx_inv_abbr1
-cpx_inv_abst1
-cpx_inv_appl1
-cpx_inv_appl1_simple
-cpx_inv_atom1
-cpx_inv_atom1_drops
-cpx_inv_bind1
-cpx_inv_cast1
-cpx_inv_flat1
-cpx_inv_gref1
-cpx_inv_lifts_bi
-cpx_inv_lifts_sn
-cpx_inv_lref1
-cpx_inv_lref1_bind
-cpx_inv_lref1_drops
-cpx_inv_sort1
-cpx_inv_zero1
-cpx_inv_zero1_pair
-cpx_lifts_bi
-cpx_lifts_sn
-cpx_lref
-cpx_pair_sn
-cpx_refl
-cpx_req_conf_sn
-cpx_reqx_conf
-cpx_reqx_conf_dx
-cpx_reqx_conf_sn
-cpx_rex_conf
-cpxs
-cpxs_aaa_conf
-cpxs_beta
-cpxs_beta_dx
-cpxs_beta_rc
-cpxs_bind
-cpxs_bind2_dx
-cpxs_bind_alt
-cpxs_bind_dx
-cpxs_cnx
-cpxs_delta
-cpxs_delta_drops
-cpxs_ee
-cpxs_eps
-cpxs_ext
-cpxs_flat
-cpxs_flat_dx
-cpxs_flat_sn
-cpxs_fpbg_trans
-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_drops
-cpxs_fwd_delta_drops_vector
-cpxs_fwd_sort
-cpxs_fwd_sort_vector
-cpxs_fwd_theta
-cpxs_fwd_theta_vector
-cpxs_ind
-cpxs_ind_dx
-cpxs_inv_abbr1_dx
-cpxs_inv_abst1
-cpxs_inv_appl1
-cpxs_inv_cast1
-cpxs_inv_cnx1
-cpxs_inv_lifts_bi
-cpxs_inv_lifts_sn
-cpxs_inv_lref1
-cpxs_inv_lref1_drops
-cpxs_inv_sort1
-cpxs_inv_zero1
-cpxs_lifts_bi
-cpxs_lifts_sn
-cpxs_lref
-cpxs_pair_sn
-cpxs_refl
-cpxs_reqx_conf
-cpxs_reqx_conf_dx
-cpxs_reqx_conf_sn
-cpxs_sort
-cpxs_strap1
-cpxs_strap2
-cpxs_teqx_fpbs
-cpxs_teqx_fpbs_trans
-cpxs_theta
-cpxs_theta_dx
-cpxs_theta_rc
-cpxs_tneqx_fpbg
-cpxs_tneqx_fwd_step_sn
-cpxs_trans
-cpx_subst
-cpxs_zeta
-cpxs_zeta_dx
-cpx_teqx_conf
-cpx_teqx_conf_rex
-cpx_theta
-cpx_zeta
-csx
-csx_abbr
-csx_abst
-csx_appl_beta
-csx_appl_beta_aux
-csx_appl_simple
-csx_appl_simple_teqo
-csx_appl_theta
-csx_appl_theta_aux
-csx_applv_beta
-csx_applv_cast
-csx_applv_cnx
-csx_applv_delta_drops
-csx_applv_sort
-csx_applv_theta
-csx_bind
-csx_cast
-csx_cpcs_dec
-csx_cpxs_trans
-csx_cpx_trans
-csx_feqx_conf
-csx_fpbq_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_bind_dx_unit
-csx_fwd_bind_dx_unit_aux
-csx_fwd_bind_unit
-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_cpxs
-csx_ind_cpxs_teqx
-csx_ind_fpb
-csx_ind_fpbg
-csx_intro
-csx_intro_cpxs
-csx_inv_lifts
-csx_inv_lref_drops
-csx_inv_lref_pair_drops
-csx_lifts
-csx_lpx_conf
-csx_lpxs_conf
-csx_lref_pair_drops
-csx_lsubr_conf
-csx_reqx_conf
-csx_reqx_trans
-csx_rsx
-csx_sort
-csx_teqx_trans
-csxv
-csxv_inv_cons
-drops_lprs_trans
-drops_lpr_trans
-drops_lpxs_trans
-drops_lpx_trans
-feqx_cpxs_trans
-feqx_cpx_trans
-feqx_fpbg_trans
-feqx_fpbs
-feqx_fpbs_trans
-feqx_fpb_trans
-feqx_lpxs_trans
-fleq_rpx
-fpb
-fpb_cpx
-fpb_fpbg
-fpb_fpbg_trans
-fpb_fpbq
-fpb_fpbq_fneqx
-fpb_fpbs
-fpb_fqu
-fpbg
-fpbg_cpms_trans
-fpbg_feqx_trans
-fpbg_fpbq_trans
-fpbg_fpbs_trans
-fpbg_fqu_trans
-fpbg_fwd_fpbs
-fpbg_teqx_div
-fpbg_trans
-fpb_inv_feqx
-fpb_lpx
-fpbq
-fpbq_aaa_conf
-fpbq_cpx
-fpbq_feqx
-fpbq_fneqx_inv_fpb
-fpbq_fpbg_trans
-fpbq_fpbs
-fpbq_fquq
-fpbq_inv_fpb
-fpbq_lpx
-fpbq_refl
-fpbs
-fpbs_aaa_conf
-fpbs_cpxs_teqx_fqup_lpx_trans
-fpbs_cpxs_trans
-fpbs_cpx_tneqx_trans
-fpbs_csx_conf
-fpbs_feqx_trans
-fpbs_fpbg_trans
-fpbs_fpb_trans
-fpbs_fqup_trans
-fpbs_fqus_trans
-fpbs_ind
-fpbs_ind_dx
-fpbs_intro_star
-fpbs_inv_fpbg
-fpbs_inv_star
-fpbs_lpxs_trans
-fpbs_lpx_trans
-fpbs_refl
-fpbs_strap1
-fpbs_strap2
-fpbs_teqx_trans
-fpbs_trans
-fqu_cpr_trans_dx
-fqu_cpr_trans_sn
-fqu_cpxs_trans
-fqu_cpxs_trans_tneqx
-fqu_cpx_trans
-fqu_cpx_trans_tneqx
-fqu_lpr_trans
-fqu_lpx_trans
-fqup_cpms_fwd_fpbg
-fqup_cpxs_trans
-fqup_cpxs_trans_tneqx
-fqup_cpx_trans
-fqup_cpx_trans_tneqx
-fqup_fpbg
-fqup_fpbg_trans
-fqup_fpbs
-fqup_fpbs_trans
-fquq_cpr_trans_dx
-fquq_cpr_trans_sn
-fquq_cpxs_trans
-fquq_cpxs_trans_tneqx
-fquq_cpx_trans
-fquq_cpx_trans_tneqx
-fquq_lpr_trans
-fquq_lpx_trans
-fqus_cpxs_trans
-fqus_cpxs_trans_tneqx
-fqus_cpx_trans
-fqus_cpx_trans_tneqx
-fqus_fpbs
-fqus_fpbs_trans
-fqus_lpxs_fpbs
-fsb
-fsb_feqx_trans
-fsb_fpbg_refl_false
-fsb_fpbs_trans
-fsb_ind_alt
-fsb_ind_fpbg
-fsb_ind_fpbg_fpbs
-fsb_intro
-fsb_intro_fpbg
-fsb_inv_csx
-IH_cnv_cpm_conf_lpr
-IH_cnv_cpms_conf_lpr
-IH_cnv_cpms_strip_lpr
-IH_cnv_cpms_trans_lpr
-IH_cnv_cpm_teqx_conf_lpr
-IH_cnv_cpm_teqx_cpm_trans
-IH_cnv_cpm_trans_lpr
-IH_cpr_conf_lpr
-jsx
-jsx_atom
-jsx_bind
-jsx_csx_conf
-jsx_fwd_bind_sn
-jsx_fwd_drops_atom_sn
-jsx_fwd_drops_pair_sn
-jsx_fwd_drops_unit_sn
-jsx_fwd_lsubr
-jsx_inv_atom_sn
-jsx_inv_atom_sn_aux
-jsx_inv_bind_sn
-jsx_inv_bind_sn_aux
-jsx_inv_pair_sn
-jsx_inv_void_sn
-jsx_pair
-jsx_refl
-jsx_trans
-lfsx_atom
-lpr
-lpr_aaa_conf
-lpr_bind
-lpr_bind_refl_dx
-lpr_conf
-lpr_cpcs_conf
-lpr_cpcs_trans
-lpr_cpms_trans
-lpr_cpm_trans
-lpr_cpr_conf
-lpr_cpr_conf_dx
-lpr_cpr_conf_sn
-lpr_cprs_conf
-lpr_cprs_trans
-lpr_cpr_trans
-lpr_drops_conf
-lpr_drops_trans
-lpr_fpb
-lpr_fpbq
-lpr_fquq_trans
-lpr_fqu_trans
-lpr_fwd_length
-lpr_fwd_lpx
-lpr_inv_atom_dx
-lpr_inv_atom_sn
-lpr_inv_bind_dx
-lpr_inv_bind_sn
-lpr_inv_pair
-lpr_inv_pair_dx
-lpr_inv_pair_sn
-lpr_inv_unit_dx
-lpr_inv_unit_sn
-lpr_lprs
-lpr_pair
-lpr_refl
-lprs
-lprs_aaa_conf
-lprs_bind_refl_dx
-lprs_conf
-lprs_cpcs_trans
-lprs_cpms_trans
-lprs_cpm_trans
-lprs_cpr_conf_dx
-lprs_cpr_conf_sn
-lprs_cprs_conf
-lprs_cprs_conf_dx
-lprs_cprs_conf_sn
-lprs_CTC
-lprs_drops_conf
-lprs_drops_trans
-lprs_fwd_length
-lprs_fwd_lpxs
-lprs_ind
-lprs_ind_dx
-lprs_ind_sn
-lprs_inv_atom_dx
-lprs_inv_atom_sn
-lprs_inv_CTC
-lprs_inv_pair_dx
-lprs_inv_pair_sn
-lprs_inv_TC
-lprs_pair
-lprs_pair_dx
-lprs_refl
-lprs_step_dx
-lprs_step_sn
-lprs_strip
-lprs_TC
-lprs_trans
-lpx
-lpx_aaa_conf
-lpx_bind
-lpx_bind_refl_dx
-lpx_cpx_conf_fsge
-lpx_cpxs_trans
-lpx_cpx_trans
-lpx_drops_conf
-lpx_drops_trans
-lpx_fqup_trans
-lpx_fquq_trans
-lpx_fqus_trans
-lpx_fqu_trans
-lpx_fsge_comp
-lpx_fwd_length
-lpx_inv_atom_dx
-lpx_inv_atom_sn
-lpx_inv_bind_dx
-lpx_inv_bind_sn
-lpx_inv_pair
-lpx_inv_pair_dx
-lpx_inv_pair_sn
-lpx_inv_unit_dx
-lpx_inv_unit_sn
-lpx_lpxs
-lpx_pair
-lpx_refl
-lpx_rpx
-lpxs
-lpxs_aaa_conf
-lpxs_bind_refl_dx
-lpxs_cpxs_trans
-lpxs_cpx_trans
-lpxs_drops_conf
-lpxs_drops_trans
-lpxs_feqx_fpbs
-lpxs_fpbs
-lpxs_fpbs_trans
-lpxs_fwd_length
-lpxs_ind
-lpxs_ind_dx
-lpxs_ind_sn
-lpxs_inv_atom_dx
-lpxs_inv_atom_sn
-lpxs_inv_bind_sn
-lpxs_inv_pair_dx
-lpxs_inv_pair_sn
-lpxs_pair
-lpxs_pair_dx
-lpxs_refl
-lpxs_rneqx_fpbg
-lpxs_rneqx_inv_step_sn
-lpxs_step_dx
-lpxs_step_sn
-lpxs_trans
-lsubr_cpcs_trans
-lsubr_cpg_trans
-lsubr_cpms_trans
-lsubr_cpm_trans
-lsubr_cpxs_trans
-lsubr_cpx_trans
-lsubsv_fwd_lsuba
-lsubv
-lsubv_atom
-lsubv_beta
-lsubv_bind
-lsubv_cnv_trans
-lsubv_cpcs_trans
-lsubv_cpms_trans
-lsubv_drops_conf_isuni
-lsubv_drops_trans_isuni
-lsubv_fwd_lsubr
-lsubv_inv_abst_sn
-lsubv_inv_atom_dx
-lsubv_inv_atom_dx_aux
-lsubv_inv_atom_sn
-lsubv_inv_atom_sn_aux
-lsubv_inv_bind_dx
-lsubv_inv_bind_dx_aux
-lsubv_inv_bind_sn
-lsubv_inv_bind_sn_aux
-lsubv_refl
-lsubv_trans
-nta
-nta_abst_predicative
-nta_abst_repellent
-nta_appl
-nta_appl_abst
-nta_appl_ntas_pos
-nta_appl_ntas_zero
-nta_bind_cnv
-nta_cast
-nta_cast_old
-nta_conv
-nta_conv_cnv
-nta_cpcs_bi
-nta_cpcs_conf
-nta_cpcs_conf_cnv
-nta_cpr_conf
-nta_cpr_conf_lpr
-nta_cprs_conf
-nta_cprs_trans
-nta_fwd_aaa
-nta_fwd_cnv_dx
-nta_fwd_cnv_sn
-nta_fwd_correct
-nta_fwd_fsb
-nta_ind_cnv
-nta_ind_ext_cnv
-nta_ind_ext_cnv_mixed
-nta_ind_rest_cnv
-nta_inference_dec
-nta_inv_abst_bi_cnv
-nta_inv_appl_sn
-nta_inv_appl_sn_ntas
-nta_inv_bind_sn_cnv
-nta_inv_cast_sn
-nta_inv_cast_sn_old
-nta_inv_gref_sn
-nta_inv_ldec_sn_cnv
-nta_inv_ldef_sn
-nta_inv_lifts_sn
-nta_inv_lref_sn
-nta_inv_lref_sn_drops_cnv
-nta_inv_pure_sn_cnv
-nta_inv_sort_sn
-nta_ldec_cnv
-nta_ldec_drops_cnv
-nta_ldef
-nta_ldef_drops
-nta_lifts_bi
-nta_lifts_sn
-nta_lpr_conf
-nta_lprs_conf
-nta_lref
-nta_mono
-nta_ntas
-nta_pure_cnv
-ntas
-ntas_bind_cnv
-ntas_fwd_cnv_dx
-ntas_fwd_cnv_sn
-ntas_ind_bi_nta
-ntas_intro
-ntas_inv_appl_sn
-ntas_inv_nta
-ntas_inv_plus
-ntas_inv_zero
-nta_sort
-ntas_refl
-ntas_sort
-ntas_step_dx
-ntas_step_sn
-ntas_trans
-ntas_zero
-nta_typecheck
-nta_typecheck_dec
-R_cpmuwe
-R_cpmuwe_total_csx
-req_cpx_trans
-reqx_cpxs_trans
-reqx_cpx_trans
-reqx_fpb_trans
-reqx_lpxs_trans
-reqx_lpx_trans
-reqx_rpx_trans
-rpr_fsge_comp
-rpx
-rpx_atom
-rpx_bind
-rpx_bind_dx_split
-rpx_bind_dx_split_void
-rpx_bind_repl_dx
-rpx_bind_void
-rpx_cpx_conf
-rpx_cpx_conf_fsge
-rpx_cpx_conf_fsge_dx
-rpx_flat
-rpx_flat_dx_split
-rpx_fsge_comp
-rpx_fwd_bind_dx
-rpx_fwd_bind_dx_void
-rpx_fwd_flat_dx
-rpx_fwd_length
-rpx_fwd_pair_sn
-rpx_gref
-rpx_inv_atom_dx
-rpx_inv_atom_sn
-rpx_inv_bind
-rpx_inv_bind_void
-rpx_inv_flat
-rpx_inv_gref
-rpx_inv_gref_bind_dx
-rpx_inv_gref_bind_sn
-rpx_inv_lifts_bi
-rpx_inv_lifts_dx
-rpx_inv_lifts_sn
-rpx_inv_lpx_req
-rpx_inv_lref
-rpx_inv_lref_bind_dx
-rpx_inv_lref_bind_sn
-rpx_inv_sort
-rpx_inv_sort_bind_dx
-rpx_inv_sort_bind_sn
-rpx_inv_zero_length
-rpx_inv_zero_pair_dx
-rpx_inv_zero_pair_sn
-rpx_lifts_sn
-rpx_lref
-rpx_pair
-rpx_pair_refl
-rpx_pair_sn_split
-rpx_refl
-rpx_reqx_conf
-rpx_sort
-rpx_teqx_conf
-rpx_teqx_div
-rsx
-rsx_bind
-rsx_bind_lpxs_aux
-rsx_bind_lpxs_void_aux
-rsx_bind_void
-rsx_cpxs_trans
-rsx_cpx_trans
-rsx_cpx_trans_jsx
-rsx_flat
-rsx_flat_lpxs
-rsx_fwd_bind_dx_void
-rsx_fwd_flat_dx
-rsx_fwd_lref_pair_csx
-rsx_fwd_lref_pair_csx_aux
-rsx_fwd_lref_pair_csx_drops
-rsx_fwd_lref_pair_drops
-rsx_fwd_pair
-rsx_fwd_pair_aux
-rsx_fwd_pair_sn
-rsx_gref
-rsx_ind
-rsx_ind_lpxs
-rsx_ind_lpxs_reqx
-rsx_intro
-rsx_intro_lpxs
-rsx_inv_bind_void
-rsx_inv_flat
-rsx_inv_lifts
-rsx_inv_lref_drops
-rsx_inv_lref_pair
-rsx_inv_lref_pair_drops
-rsx_jsx_trans
-rsx_lifts
-rsx_lpxs_trans
-rsx_lpx_trans
-rsx_lref_atom_drops
-rsx_lref_pair
-rsx_lref_pair_drops
-rsx_lref_pair_lpxs
-rsx_lref_unit_drops
-rsx_reqx_trans
-rsx_sort
-rsx_unit
-teqx_cpxs_trans
-teqx_cpx_trans
-teqx_fpbs_trans
-teqx_fpb_trans
-teqx_reqx_lpx_fpbs
+"aaa_cpm_SO"
+"aaa_csx"
+"aaa_fsb"
+"aaa_ind_csx"
+"aaa_ind_csx_aux"
+"aaa_ind_csx_cpxs"
+"aaa_ind_csx_cpxs_aux"
+"aaa_ind_fpb"
+"aaa_ind_fpb_aux"
+"aaa_ind_fpbg"
+"aaa_ind_fpbg_aux"
+"cnr"
+"cnr_abbr_neg"
+"cnr_abst"
+"cnr_appl_simple"
+"cnr_dec_teqx"
+"cnr_gref"
+"cnr_inv_abbr_neg"
+"cnr_inv_abst"
+"cnr_inv_appl"
+"cnr_inv_cast"
+"cnr_inv_lifts"
+"cnr_inv_lref_abbr"
+"cnr_lifts"
+"cnr_lref_abst"
+"cnr_lref_atom"
+"cnr_lref_unit"
+"cnr_sort"
+"cnuw"
+"cnuw_abbr_neg"
+"cnuw_abst"
+"cnuw_appl_simple"
+"cnuw_atom_drops"
+"cnuw_cpms_trans"
+"cnuw_ctop"
+"cnuw_dec"
+"cnuw_dec_ex"
+"cnuw_fwd_appl"
+"cnuw_gref"
+"cnuw_inv_abbr_pos"
+"cnuw_inv_cast"
+"cnuw_inv_lifts"
+"cnuw_inv_zero_pair"
+"cnuw_lifts"
+"cnuw_lref"
+"cnuw_sort"
+"cnuw_unit_drops"
+"cnuw_zero_unit"
+"cnv"
+"cnv_acle_omega"
+"cnv_acle_one"
+"cnv_acle_trans"
+"cnv_appl"
+"cnv_appl_cpes"
+"cnv_appl_cpts"
+"cnv_appl_ge"
+"cnv_appl_ntas_ge"
+"cnv_bind"
+"cnv_cast"
+"cnv_cast_cpes"
+"cnv_cast_cpts"
+"cnv_cpcs_dec"
+"cnv_cpes_dec"
+"cnv_cpm_conf_lpr_appl_appl_aux"
+"cnv_cpm_conf_lpr_appl_beta_aux"
+"cnv_cpm_conf_lpr_appl_theta_aux"
+"cnv_cpm_conf_lpr_atom_atom_aux"
+"cnv_cpm_conf_lpr_atom_delta_aux"
+"cnv_cpm_conf_lpr_atom_ell_aux"
+"cnv_cpm_conf_lpr_atom_ess_aux"
+"cnv_cpm_conf_lpr_aux"
+"cnv_cpm_conf_lpr_beta_beta_aux"
+"cnv_cpm_conf_lpr_bind_bind_aux"
+"cnv_cpm_conf_lpr_bind_zeta_aux"
+"cnv_cpm_conf_lpr_cast_cast_aux"
+"cnv_cpm_conf_lpr_cast_ee_aux"
+"cnv_cpm_conf_lpr_cast_epsilon_aux"
+"cnv_cpm_conf_lpr_delta_delta_aux"
+"cnv_cpm_conf_lpr_delta_ell_aux"
+"cnv_cpm_conf_lpr_ee_ee_aux"
+"cnv_cpm_conf_lpr_epsilon_ee_aux"
+"cnv_cpm_conf_lpr_epsilon_epsilon_aux"
+"cnv_cpm_conf_lpr_sub"
+"cnv_cpm_conf_lpr_theta_theta_aux"
+"cnv_cpm_conf_lpr_zeta_zeta_aux"
+"cnv_cpmre_cpms_conf"
+"cnv_cpmre_mono"
+"cnv_cpmre_trans"
+"cnv_cpms_conf"
+"cnv_cpms_conf_eq"
+"cnv_cpms_conf_lpr"
+"cnv_cpms_conf_lpr_aux"
+"cnv_cpms_conf_lpr_refl_tneqx_sub"
+"cnv_cpms_conf_lpr_step_tneqx_sub"
+"cnv_cpms_conf_lpr_teqx_teqx_aux"
+"cnv_cpms_conf_lpr_teqx_tneqx_aux"
+"cnv_cpms_conf_lpr_tneqx_tneqx_aux"
+"cnv_cpms_fwd_appl_sn_decompose"
+"cnv_cpms_nta"
+"cnv_cpms_ntas"
+"cnv_cpms_strip_lpr_sub"
+"cnv_cpms_teqx_conf_lpr_aux"
+"cnv_cpms_teqx_strip_lpr_aux"
+"cnv_cpms_trans"
+"cnv_cpms_trans_lpr"
+"cnv_cpms_trans_lpr_sub"
+"cnv_cpm_teqx_conf_lpr"
+"cnv_cpm_teqx_conf_lpr_appl_appl_aux"
+"cnv_cpm_teqx_conf_lpr_atom_atom_aux"
+"cnv_cpm_teqx_conf_lpr_atom_ess_aux"
+"cnv_cpm_teqx_conf_lpr_aux"
+"cnv_cpm_teqx_conf_lpr_bind_bind_aux"
+"cnv_cpm_teqx_conf_lpr_cast_cast_aux"
+"cnv_cpm_teqx_cpm_trans_aux"
+"cnv_cpm_teqx_cpm_trans_sub"
+"cnv_cpm_trans"
+"cnv_cpm_trans_lpr"
+"cnv_cpm_trans_lpr_aux"
+"cnv_cpmuwe_mono"
+"cnv_cpmuwe_trans"
+"cnv_cpr_teqx_fwd_refl"
+"cnv_dec"
+"cnv_fpbg_refl_false"
+"cnv_fqu_conf"
+"cnv_fqup_conf"
+"cnv_fquq_conf"
+"cnv_fqus_conf"
+"cnv_fwd_aaa"
+"cnv_fwd_cpms_abst_dx_le"
+"cnv_fwd_cpm_SO"
+"cnv_fwd_cpms_total"
+"cnv_fwd_csx"
+"cnv_fwd_flat"
+"cnv_fwd_fsb"
+"cnv_fwd_pair_sn"
+"cnv_ind_cpes"
+"cnv_inv_appl"
+"cnv_inv_appl_aux"
+"cnv_inv_appl_cpes"
+"cnv_inv_appl_cpts"
+"cnv_inv_appl_ntas"
+"cnv_inv_bind"
+"cnv_inv_bind_aux"
+"cnv_inv_cast"
+"cnv_inv_cast_aux"
+"cnv_inv_cast_cpes"
+"cnv_inv_cast_cpts"
+"cnv_inv_gref"
+"cnv_inv_gref_aux"
+"cnv_inv_lifts"
+"cnv_inv_lref"
+"cnv_inv_lref_atom"
+"cnv_inv_lref_aux"
+"cnv_inv_lref_drops"
+"cnv_inv_lref_pair"
+"cnv_inv_lref_unit"
+"cnv_inv_zero"
+"cnv_inv_zero_aux"
+"cnv_lifts"
+"cnv_lprs_trans"
+"cnv_lpr_trans"
+"cnv_lref"
+"cnv_lref_drops"
+"cnv_nta_sn"
+"cnv_preserve"
+"cnv_R_cpmuwe_dec"
+"cnv_R_cpmuwe_total"
+"cnv_sort"
+"cnv_zero"
+"cnx"
+"cnx_abst"
+"cnx_appl_simple"
+"cnx_csx"
+"cnx_inv_abbr_neg"
+"cnx_inv_abbr_pos"
+"cnx_inv_abst"
+"cnx_inv_appl"
+"cnx_inv_cast"
+"cnx_inv_lifts"
+"cnx_inv_lref_pair"
+"cnx_lifts"
+"cnx_lref_atom"
+"cnx_lref_unit"
+"cnx_sort"
+"cnx_teqx_trans"
+"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_step_dx"
+"cpcs_cprs_step_sn"
+"cpcs_cpr_step_dx"
+"cpcs_cpr_step_sn"
+"cpcs_flat"
+"cpcs_flat_dx_cpr_rev"
+"cpcs_ind_dx"
+"cpcs_ind_sn"
+"cpcs_inv_abst_bi_dx"
+"cpcs_inv_abst_bi_sn"
+"cpcs_inv_abst_dx"
+"cpcs_inv_abst_sn"
+"cpcs_inv_cprs"
+"cpcs_inv_lifts_bi"
+"cpcs_inv_sort_abst"
+"cpcs_inv_sort_bi"
+"cpcs_lifts_bi"
+"cpcs_refl"
+"cpcs_step_dx"
+"cpcs_step_sn"
+"cpcs_strip"
+"cpcs_sym"
+"cpcs_trans"
+"cpc_sym"
+"cpes"
+"cpes_aaa_mono"
+"cpes_cpes_trans"
+"cpes_cpms_div"
+"cpes_cprs_trans"
+"cpes_fwd_abst_bi"
+"cpes_refl"
+"cpes_refl_aaa"
+"cpes_sym"
+"cpg"
+"cpg_appl"
+"cpg_atom"
+"cpg_beta"
+"cpg_bind"
+"cpg_cast"
+"cpg_cpx"
+"cpg_delta"
+"cpg_delta_drops"
+"cpg_ee"
+"cpg_ell"
+"cpg_ell_drops"
+"cpg_eps"
+"cpg_ess"
+"cpg_fwd_bind1_minus"
+"cpg_inv_abbr1"
+"cpg_inv_abst1"
+"cpg_inv_appl1"
+"cpg_inv_appl1_aux"
+"cpg_inv_appl1_simple"
+"cpg_inv_atom1"
+"cpg_inv_atom1_aux"
+"cpg_inv_atom1_drops"
+"cpg_inv_bind1"
+"cpg_inv_bind1_aux"
+"cpg_inv_cast1"
+"cpg_inv_cast1_aux"
+"cpg_inv_gref1"
+"cpg_inv_lifts_bi"
+"cpg_inv_lifts_sn"
+"cpg_inv_lref1"
+"cpg_inv_lref1_bind"
+"cpg_inv_lref1_drops"
+"cpg_inv_sort1"
+"cpg_inv_zero1"
+"cpg_inv_zero1_pair"
+"cpg_lifts_bi"
+"cpg_lifts_sn"
+"cpg_lref"
+"cpg_refl"
+"cpg_theta"
+"cpg_zeta"
+"cpm"
+"cpm_aaa_conf"
+"cpm_appl"
+"cpm_beta"
+"cpm_bind"
+"cpm_bind2"
+"cpm_bind_unit"
+"cpm_cast"
+"cpm_cpms"
+"cpm_delta"
+"cpm_delta_drops"
+"cpm_ee"
+"cpm_ell"
+"cpm_ell_drops"
+"cpm_eps"
+"cpm_ess"
+"cpm_fpb"
+"cpm_fpbq"
+"cpm_fsge_comp"
+"cpm_fwd_bind1_minus"
+"cpm_fwd_cpx"
+"cpm_fwd_plus"
+"cpm_fwd_plus_aux"
+"cpm_ind"
+"cpm_inv_abbr1"
+"cpm_inv_abst1"
+"cpm_inv_abst_bi"
+"cpm_inv_appl1"
+"cpm_inv_appl1_simple"
+"cpm_inv_atom1"
+"cpm_inv_atom1_drops"
+"cpm_inv_bind1"
+"cpm_inv_cast1"
+"cpm_inv_gref1"
+"cpm_inv_lifts_bi"
+"cpm_inv_lifts_sn"
+"cpm_inv_lref1"
+"cpm_inv_lref1_ctop"
+"cpm_inv_lref1_drops"
+"cpm_inv_sort1"
+"cpm_inv_zero1"
+"cpm_inv_zero1_unit"
+"cpm_lifts_bi"
+"cpm_lifts_sn"
+"cpm_lref"
+"cpmre"
+"cpmre_fwd_cpms"
+"cpmre_intro"
+"cpmre_total_aaa"
+"cpm_rex_conf"
+"cpms"
+"cpms_aaa_conf"
+"cpms_abst_dx_le_aaa"
+"cpms_appl"
+"cpms_appl_dx"
+"cpms_beta"
+"cpms_beta_dx"
+"cpms_beta_rc"
+"cpms_bind"
+"cpms_bind2_dx"
+"cpms_bind_alt"
+"cpms_bind_dx"
+"cpms_cast"
+"cpms_cast_sn"
+"cpms_cprre_trans"
+"cpms_cprs_trans"
+"cpms_delta"
+"cpms_delta_drops"
+"cpms_div"
+"cpms_ee"
+"cpms_ell"
+"cpms_ell_drops"
+"cpms_eps"
+"cpms_fpbg_trans"
+"cpms_fwd_cpxs"
+"cpms_fwd_fpbs"
+"cpms_ind_dx"
+"cpms_ind_sn"
+"cpms_inv_abbr_abst"
+"cpms_inv_abbr_sn_dx"
+"cpms_inv_abst_bi"
+"cpms_inv_abst_sn"
+"cpms_inv_abst_sn_cprs"
+"cpms_inv_appl_sn"
+"cpms_inv_cast1"
+"cpms_inv_delta_sn"
+"cpms_inv_ell_sn"
+"cpms_inv_gref1"
+"cpms_inv_lifts_bi"
+"cpms_inv_lifts_sn"
+"cpms_inv_lref1_ctop"
+"cpms_inv_lref1_drops"
+"cpms_inv_lref_sn"
+"cpms_inv_plus"
+"cpms_inv_sort1"
+"cpms_inv_succ_sn"
+"cpms_inv_zero1_unit"
+"cpms_lifts_bi"
+"cpms_lifts_sn"
+"cpms_lref"
+"cpm_sort"
+"cpms_reqx_conf_dx"
+"cpms_reqx_conf_sn"
+"cpms_sort"
+"cpms_step_dx"
+"cpms_step_sn"
+"cpms_teqx_ind_sn"
+"cpms_theta"
+"cpms_theta_dx"
+"cpms_theta_rc"
+"cpms_tneqx_fwd_fpbg"
+"cpms_tneqx_fwd_step_sn_aux"
+"cpms_total_aaa"
+"cpms_trans"
+"cpms_trans_swap"
+"cpms_zeta"
+"cpms_zeta_dx"
+"cpm_teqx_free"
+"cpm_teqx_ind"
+"cpm_teqx_inv_appl_sn"
+"cpm_teqx_inv_atom_sn"
+"cpm_teqx_inv_bind_dx"
+"cpm_teqx_inv_bind_sn"
+"cpm_teqx_inv_bind_sn_void"
+"cpm_teqx_inv_cast_sn"
+"cpm_teqx_inv_lref_sn"
+"cpm_theta"
+"cpm_tneqx_cpm_cpms_teqx_sym_fwd_fpbg"
+"cpm_tneqx_cpm_fpbg"
+"cpmuwe"
+"cpmuwe_abbr_neg"
+"cpmuwe_abst"
+"cpmuwe_ctop"
+"cpmuwe_fwd_cpms"
+"cpmuwe_gref"
+"cpmuwe_intro"
+"cpmuwe_sort"
+"cpmuwe_total_csx"
+"cpmuwe_zero_unit"
+"cpm_zeta"
+"cpr_abbr_pos_tneqx"
+"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_conf_cpcs"
+"cpr_cprs_div"
+"cpr_div"
+"cpr_ext"
+"cpr_flat"
+"cpr_ind"
+"cpr_inv_atom1"
+"cpr_inv_atom1_drops"
+"cpr_inv_cast1"
+"cpr_inv_flat1"
+"cpr_inv_gref1"
+"cpr_inv_lref1"
+"cpr_inv_lref1_drops"
+"cpr_inv_sort1"
+"cpr_inv_zero1"
+"cpr_pair_sn"
+"cprre_cprs_conf"
+"cpr_refl"
+"cprre_mono"
+"cprre_total_csx"
+"cprs_abbr_pos_twneq"
+"cprs_conf"
+"cprs_conf_cpcs"
+"cprs_cpr_conf_cpcs"
+"cprs_cpr_div"
+"cprs_CTC"
+"cprs_div"
+"cprs_ext"
+"cprs_flat"
+"cprs_flat_dx"
+"cprs_flat_sn"
+"cprs_ind_dx"
+"cprs_ind_sn"
+"cprs_inv_appl_sn"
+"cprs_inv_cast1"
+"cprs_inv_cnr_sn"
+"cprs_inv_CTC"
+"cprs_inv_lref1_drops"
+"cprs_inv_sort1"
+"cprs_lpr_conf_dx"
+"cprs_lpr_conf_sn"
+"cprs_nta_trans"
+"cprs_nta_trans_cnv"
+"cprs_refl"
+"cprs_step_dx"
+"cprs_step_sn"
+"cprs_strip"
+"cprs_trans"
+"cpr_subst"
+"cpt"
+"cpt_appl"
+"cpt_bind"
+"cpt_cast"
+"cpt_cpts"
+"cpt_delta"
+"cpt_delta_drops"
+"cpt_ee"
+"cpt_ell"
+"cpt_ell_drops"
+"cpt_ess"
+"cpt_fwd_cpm"
+"cpt_fwd_plus"
+"cpt_fwd_plus_aux"
+"cpt_ind"
+"cpt_inv_appl_sn"
+"cpt_inv_atom_sn"
+"cpt_inv_atom_sn_drops"
+"cpt_inv_bind_sn"
+"cpt_inv_cast_sn"
+"cpt_inv_gref_sn"
+"cpt_inv_lifts_bi"
+"cpt_inv_lifts_sn"
+"cpt_inv_lref_sn"
+"cpt_inv_lref_sn_ctop"
+"cpt_inv_lref_sn_drops"
+"cpt_inv_sort_sn"
+"cpt_inv_zero_sn"
+"cpt_inv_zero_sn_unit"
+"cpt_lifts_bi"
+"cpt_lifts_sn"
+"cpt_lref"
+"cpt_refl"
+"cpts"
+"cpts_appl_dx"
+"cpts_bind_dx"
+"cpts_cast_sn"
+"cpts_cpms_conf_eq"
+"cpts_cprs_trans"
+"cpts_delta"
+"cpts_delta_drops"
+"cpts_ee"
+"cpts_ell"
+"cpts_ell_drops"
+"cpts_fwd_cpms"
+"cpts_ind_dx"
+"cpts_ind_sn"
+"cpts_inv_cast_sn"
+"cpts_inv_delta_sn"
+"cpts_inv_ell_sn"
+"cpts_inv_gref_sn"
+"cpts_inv_lifts_bi"
+"cpts_inv_lifts_sn"
+"cpts_inv_lref_sn"
+"cpts_inv_lref_sn_ctop"
+"cpts_inv_lref_sn_drops"
+"cpts_inv_sort_sn"
+"cpts_inv_succ_sn"
+"cpts_inv_zero_sn_unit"
+"cpts_lifts_bi"
+"cpts_lifts_sn"
+"cpts_lref"
+"cpt_sort"
+"cpts_refl"
+"cpts_sort"
+"cpts_step_dx"
+"cpts_step_sn"
+"cpts_total_aaa"
+"cpx"
+"cpx_aaa_conf"
+"cpx_aaa_conf_lpx"
+"cpx_beta"
+"cpx_bind"
+"cpx_bind2"
+"cpx_bind_unit"
+"cpx_cpxs"
+"cpx_delta"
+"cpx_delta_drops"
+"cpx_ee"
+"cpx_eps"
+"cpx_ess"
+"cpx_ext"
+"cpx_flat"
+"cpx_fsge_comp"
+"cpx_fwd_bind1_minus"
+"cpx_ind"
+"cpx_inv_abbr1"
+"cpx_inv_abst1"
+"cpx_inv_appl1"
+"cpx_inv_appl1_simple"
+"cpx_inv_atom1"
+"cpx_inv_atom1_drops"
+"cpx_inv_bind1"
+"cpx_inv_cast1"
+"cpx_inv_flat1"
+"cpx_inv_gref1"
+"cpx_inv_lifts_bi"
+"cpx_inv_lifts_sn"
+"cpx_inv_lref1"
+"cpx_inv_lref1_bind"
+"cpx_inv_lref1_drops"
+"cpx_inv_sort1"
+"cpx_inv_zero1"
+"cpx_inv_zero1_pair"
+"cpx_lifts_bi"
+"cpx_lifts_sn"
+"cpx_lref"
+"cpx_pair_sn"
+"cpx_refl"
+"cpx_req_conf_sn"
+"cpx_reqx_conf"
+"cpx_reqx_conf_dx"
+"cpx_reqx_conf_sn"
+"cpx_rex_conf"
+"cpxs"
+"cpxs_aaa_conf"
+"cpxs_beta"
+"cpxs_beta_dx"
+"cpxs_beta_rc"
+"cpxs_bind"
+"cpxs_bind2_dx"
+"cpxs_bind_alt"
+"cpxs_bind_dx"
+"cpxs_cnx"
+"cpxs_delta"
+"cpxs_delta_drops"
+"cpxs_ee"
+"cpxs_eps"
+"cpxs_ext"
+"cpxs_flat"
+"cpxs_flat_dx"
+"cpxs_flat_sn"
+"cpxs_fpbg_trans"
+"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_drops"
+"cpxs_fwd_delta_drops_vector"
+"cpxs_fwd_sort"
+"cpxs_fwd_sort_vector"
+"cpxs_fwd_theta"
+"cpxs_fwd_theta_vector"
+"cpxs_ind"
+"cpxs_ind_dx"
+"cpxs_inv_abbr1_dx"
+"cpxs_inv_abst1"
+"cpxs_inv_appl1"
+"cpxs_inv_cast1"
+"cpxs_inv_cnx1"
+"cpxs_inv_lifts_bi"
+"cpxs_inv_lifts_sn"
+"cpxs_inv_lref1"
+"cpxs_inv_lref1_drops"
+"cpxs_inv_sort1"
+"cpxs_inv_zero1"
+"cpxs_lifts_bi"
+"cpxs_lifts_sn"
+"cpxs_lref"
+"cpxs_pair_sn"
+"cpxs_refl"
+"cpxs_reqx_conf"
+"cpxs_reqx_conf_dx"
+"cpxs_reqx_conf_sn"
+"cpxs_sort"
+"cpxs_strap1"
+"cpxs_strap2"
+"cpxs_teqx_fpbs"
+"cpxs_teqx_fpbs_trans"
+"cpxs_theta"
+"cpxs_theta_dx"
+"cpxs_theta_rc"
+"cpxs_tneqx_fpbg"
+"cpxs_tneqx_fwd_step_sn"
+"cpxs_trans"
+"cpx_subst"
+"cpxs_zeta"
+"cpxs_zeta_dx"
+"cpx_teqx_conf"
+"cpx_teqx_conf_rex"
+"cpx_theta"
+"cpx_zeta"
+"csx"
+"csx_abbr"
+"csx_abst"
+"csx_appl_beta"
+"csx_appl_beta_aux"
+"csx_appl_simple"
+"csx_appl_simple_teqo"
+"csx_appl_theta"
+"csx_appl_theta_aux"
+"csx_applv_beta"
+"csx_applv_cast"
+"csx_applv_cnx"
+"csx_applv_delta_drops"
+"csx_applv_sort"
+"csx_applv_theta"
+"csx_bind"
+"csx_cast"
+"csx_cpcs_dec"
+"csx_cpxs_trans"
+"csx_cpx_trans"
+"csx_feqx_conf"
+"csx_fpbq_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_bind_dx_unit"
+"csx_fwd_bind_dx_unit_aux"
+"csx_fwd_bind_unit"
+"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_cpxs"
+"csx_ind_cpxs_teqx"
+"csx_ind_fpb"
+"csx_ind_fpbg"
+"csx_intro"
+"csx_intro_cpxs"
+"csx_inv_lifts"
+"csx_inv_lref_drops"
+"csx_inv_lref_pair_drops"
+"csx_lifts"
+"csx_lpx_conf"
+"csx_lpxs_conf"
+"csx_lref_pair_drops"
+"csx_lsubr_conf"
+"csx_reqx_conf"
+"csx_reqx_trans"
+"csx_rsx"
+"csx_sort"
+"csx_teqx_trans"
+"csxv"
+"csxv_inv_cons"
+"drops_lprs_trans"
+"drops_lpr_trans"
+"drops_lpxs_trans"
+"drops_lpx_trans"
+"feqx_cpxs_trans"
+"feqx_cpx_trans"
+"feqx_fpbg_trans"
+"feqx_fpbs"
+"feqx_fpbs_trans"
+"feqx_fpb_trans"
+"feqx_lpxs_trans"
+"fleq_rpx"
+"fpb"
+"fpb_cpx"
+"fpb_fpbg"
+"fpb_fpbg_trans"
+"fpb_fpbq"
+"fpb_fpbq_fneqx"
+"fpb_fpbs"
+"fpb_fqu"
+"fpbg"
+"fpbg_cpms_trans"
+"fpbg_feqx_trans"
+"fpbg_fpbq_trans"
+"fpbg_fpbs_trans"
+"fpbg_fqu_trans"
+"fpbg_fwd_fpbs"
+"fpbg_teqx_div"
+"fpbg_trans"
+"fpb_inv_feqx"
+"fpb_lpx"
+"fpbq"
+"fpbq_aaa_conf"
+"fpbq_cpx"
+"fpbq_feqx"
+"fpbq_fneqx_inv_fpb"
+"fpbq_fpbg_trans"
+"fpbq_fpbs"
+"fpbq_fquq"
+"fpbq_inv_fpb"
+"fpbq_lpx"
+"fpbq_refl"
+"fpbs"
+"fpbs_aaa_conf"
+"fpbs_cpxs_teqx_fqup_lpx_trans"
+"fpbs_cpxs_trans"
+"fpbs_cpx_tneqx_trans"
+"fpbs_csx_conf"
+"fpbs_feqx_trans"
+"fpbs_fpbg_trans"
+"fpbs_fpb_trans"
+"fpbs_fqup_trans"
+"fpbs_fqus_trans"
+"fpbs_ind"
+"fpbs_ind_dx"
+"fpbs_intro_star"
+"fpbs_inv_fpbg"
+"fpbs_inv_star"
+"fpbs_lpxs_trans"
+"fpbs_lpx_trans"
+"fpbs_refl"
+"fpbs_strap1"
+"fpbs_strap2"
+"fpbs_teqx_trans"
+"fpbs_trans"
+"fqu_cpr_trans_dx"
+"fqu_cpr_trans_sn"
+"fqu_cpxs_trans"
+"fqu_cpxs_trans_tneqx"
+"fqu_cpx_trans"
+"fqu_cpx_trans_tneqx"
+"fqu_lpr_trans"
+"fqu_lpx_trans"
+"fqup_cpms_fwd_fpbg"
+"fqup_cpxs_trans"
+"fqup_cpxs_trans_tneqx"
+"fqup_cpx_trans"
+"fqup_cpx_trans_tneqx"
+"fqup_fpbg"
+"fqup_fpbg_trans"
+"fqup_fpbs"
+"fqup_fpbs_trans"
+"fquq_cpr_trans_dx"
+"fquq_cpr_trans_sn"
+"fquq_cpxs_trans"
+"fquq_cpxs_trans_tneqx"
+"fquq_cpx_trans"
+"fquq_cpx_trans_tneqx"
+"fquq_lpr_trans"
+"fquq_lpx_trans"
+"fqus_cpxs_trans"
+"fqus_cpxs_trans_tneqx"
+"fqus_cpx_trans"
+"fqus_cpx_trans_tneqx"
+"fqus_fpbs"
+"fqus_fpbs_trans"
+"fqus_lpxs_fpbs"
+"fsb"
+"fsb_feqx_trans"
+"fsb_fpbg_refl_false"
+"fsb_fpbs_trans"
+"fsb_ind_alt"
+"fsb_ind_fpbg"
+"fsb_ind_fpbg_fpbs"
+"fsb_intro"
+"fsb_intro_fpbg"
+"fsb_inv_csx"
+"IH_cnv_cpm_conf_lpr"
+"IH_cnv_cpms_conf_lpr"
+"IH_cnv_cpms_strip_lpr"
+"IH_cnv_cpms_trans_lpr"
+"IH_cnv_cpm_teqx_conf_lpr"
+"IH_cnv_cpm_teqx_cpm_trans"
+"IH_cnv_cpm_trans_lpr"
+"IH_cpr_conf_lpr"
+"jsx"
+"jsx_atom"
+"jsx_bind"
+"jsx_csx_conf"
+"jsx_fwd_bind_sn"
+"jsx_fwd_drops_atom_sn"
+"jsx_fwd_drops_pair_sn"
+"jsx_fwd_drops_unit_sn"
+"jsx_fwd_lsubr"
+"jsx_inv_atom_sn"
+"jsx_inv_atom_sn_aux"
+"jsx_inv_bind_sn"
+"jsx_inv_bind_sn_aux"
+"jsx_inv_pair_sn"
+"jsx_inv_void_sn"
+"jsx_pair"
+"jsx_refl"
+"jsx_trans"
+"lfsx_atom"
+"lpr"
+"lpr_aaa_conf"
+"lpr_bind"
+"lpr_bind_refl_dx"
+"lpr_conf"
+"lpr_cpcs_conf"
+"lpr_cpcs_trans"
+"lpr_cpms_trans"
+"lpr_cpm_trans"
+"lpr_cpr_conf"
+"lpr_cpr_conf_dx"
+"lpr_cpr_conf_sn"
+"lpr_cprs_conf"
+"lpr_cprs_trans"
+"lpr_cpr_trans"
+"lpr_drops_conf"
+"lpr_drops_trans"
+"lpr_fpb"
+"lpr_fpbq"
+"lpr_fquq_trans"
+"lpr_fqu_trans"
+"lpr_fwd_length"
+"lpr_fwd_lpx"
+"lpr_inv_atom_dx"
+"lpr_inv_atom_sn"
+"lpr_inv_bind_dx"
+"lpr_inv_bind_sn"
+"lpr_inv_pair"
+"lpr_inv_pair_dx"
+"lpr_inv_pair_sn"
+"lpr_inv_unit_dx"
+"lpr_inv_unit_sn"
+"lpr_lprs"
+"lpr_pair"
+"lpr_refl"
+"lprs"
+"lprs_aaa_conf"
+"lprs_bind_refl_dx"
+"lprs_conf"
+"lprs_cpcs_trans"
+"lprs_cpms_trans"
+"lprs_cpm_trans"
+"lprs_cpr_conf_dx"
+"lprs_cpr_conf_sn"
+"lprs_cprs_conf"
+"lprs_cprs_conf_dx"
+"lprs_cprs_conf_sn"
+"lprs_CTC"
+"lprs_drops_conf"
+"lprs_drops_trans"
+"lprs_fwd_length"
+"lprs_fwd_lpxs"
+"lprs_ind"
+"lprs_ind_dx"
+"lprs_ind_sn"
+"lprs_inv_atom_dx"
+"lprs_inv_atom_sn"
+"lprs_inv_CTC"
+"lprs_inv_pair_dx"
+"lprs_inv_pair_sn"
+"lprs_inv_TC"
+"lprs_pair"
+"lprs_pair_dx"
+"lprs_refl"
+"lprs_step_dx"
+"lprs_step_sn"
+"lprs_strip"
+"lprs_TC"
+"lprs_trans"
+"lpx"
+"lpx_aaa_conf"
+"lpx_bind"
+"lpx_bind_refl_dx"
+"lpx_cpx_conf_fsge"
+"lpx_cpxs_trans"
+"lpx_cpx_trans"
+"lpx_drops_conf"
+"lpx_drops_trans"
+"lpx_fqup_trans"
+"lpx_fquq_trans"
+"lpx_fqus_trans"
+"lpx_fqu_trans"
+"lpx_fsge_comp"
+"lpx_fwd_length"
+"lpx_inv_atom_dx"
+"lpx_inv_atom_sn"
+"lpx_inv_bind_dx"
+"lpx_inv_bind_sn"
+"lpx_inv_pair"
+"lpx_inv_pair_dx"
+"lpx_inv_pair_sn"
+"lpx_inv_unit_dx"
+"lpx_inv_unit_sn"
+"lpx_lpxs"
+"lpx_pair"
+"lpx_refl"
+"lpx_rpx"
+"lpxs"
+"lpxs_aaa_conf"
+"lpxs_bind_refl_dx"
+"lpxs_cpxs_trans"
+"lpxs_cpx_trans"
+"lpxs_drops_conf"
+"lpxs_drops_trans"
+"lpxs_feqx_fpbs"
+"lpxs_fpbs"
+"lpxs_fpbs_trans"
+"lpxs_fwd_length"
+"lpxs_ind"
+"lpxs_ind_dx"
+"lpxs_ind_sn"
+"lpxs_inv_atom_dx"
+"lpxs_inv_atom_sn"
+"lpxs_inv_bind_sn"
+"lpxs_inv_pair_dx"
+"lpxs_inv_pair_sn"
+"lpxs_pair"
+"lpxs_pair_dx"
+"lpxs_refl"
+"lpxs_rneqx_fpbg"
+"lpxs_rneqx_inv_step_sn"
+"lpxs_step_dx"
+"lpxs_step_sn"
+"lpxs_trans"
+"lsubr_cpcs_trans"
+"lsubr_cpg_trans"
+"lsubr_cpms_trans"
+"lsubr_cpm_trans"
+"lsubr_cpxs_trans"
+"lsubr_cpx_trans"
+"lsubsv_fwd_lsuba"
+"lsubv"
+"lsubv_atom"
+"lsubv_beta"
+"lsubv_bind"
+"lsubv_cnv_trans"
+"lsubv_cpcs_trans"
+"lsubv_cpms_trans"
+"lsubv_drops_conf_isuni"
+"lsubv_drops_trans_isuni"
+"lsubv_fwd_lsubr"
+"lsubv_inv_abst_sn"
+"lsubv_inv_atom_dx"
+"lsubv_inv_atom_dx_aux"
+"lsubv_inv_atom_sn"
+"lsubv_inv_atom_sn_aux"
+"lsubv_inv_bind_dx"
+"lsubv_inv_bind_dx_aux"
+"lsubv_inv_bind_sn"
+"lsubv_inv_bind_sn_aux"
+"lsubv_refl"
+"lsubv_trans"
+"nta"
+"nta_abst_predicative"
+"nta_abst_repellent"
+"nta_appl"
+"nta_appl_abst"
+"nta_appl_ntas_pos"
+"nta_appl_ntas_zero"
+"nta_bind_cnv"
+"nta_cast"
+"nta_cast_old"
+"nta_conv"
+"nta_conv_cnv"
+"nta_cpcs_bi"
+"nta_cpcs_conf"
+"nta_cpcs_conf_cnv"
+"nta_cpr_conf"
+"nta_cpr_conf_lpr"
+"nta_cprs_conf"
+"nta_cprs_trans"
+"nta_fwd_aaa"
+"nta_fwd_cnv_dx"
+"nta_fwd_cnv_sn"
+"nta_fwd_correct"
+"nta_fwd_fsb"
+"nta_ind_cnv"
+"nta_ind_ext_cnv"
+"nta_ind_ext_cnv_mixed"
+"nta_ind_rest_cnv"
+"nta_inference_dec"
+"nta_inv_abst_bi_cnv"
+"nta_inv_appl_sn"
+"nta_inv_appl_sn_ntas"
+"nta_inv_bind_sn_cnv"
+"nta_inv_cast_sn"
+"nta_inv_cast_sn_old"
+"nta_inv_gref_sn"
+"nta_inv_ldec_sn_cnv"
+"nta_inv_ldef_sn"
+"nta_inv_lifts_sn"
+"nta_inv_lref_sn"
+"nta_inv_lref_sn_drops_cnv"
+"nta_inv_pure_sn_cnv"
+"nta_inv_sort_sn"
+"nta_ldec_cnv"
+"nta_ldec_drops_cnv"
+"nta_ldef"
+"nta_ldef_drops"
+"nta_lifts_bi"
+"nta_lifts_sn"
+"nta_lpr_conf"
+"nta_lprs_conf"
+"nta_lref"
+"nta_mono"
+"nta_ntas"
+"nta_pure_cnv"
+"ntas"
+"ntas_bind_cnv"
+"ntas_fwd_cnv_dx"
+"ntas_fwd_cnv_sn"
+"ntas_ind_bi_nta"
+"ntas_intro"
+"ntas_inv_appl_sn"
+"ntas_inv_nta"
+"ntas_inv_plus"
+"ntas_inv_zero"
+"nta_sort"
+"ntas_refl"
+"ntas_sort"
+"ntas_step_dx"
+"ntas_step_sn"
+"ntas_trans"
+"ntas_zero"
+"nta_typecheck"
+"nta_typecheck_dec"
+"R_cpmuwe"
+"R_cpmuwe_total_csx"
+"req_cpx_trans"
+"reqx_cpxs_trans"
+"reqx_cpx_trans"
+"reqx_fpb_trans"
+"reqx_lpxs_trans"
+"reqx_lpx_trans"
+"reqx_rpx_trans"
+"rpr_fsge_comp"
+"rpx"
+"rpx_atom"
+"rpx_bind"
+"rpx_bind_dx_split"
+"rpx_bind_dx_split_void"
+"rpx_bind_repl_dx"
+"rpx_bind_void"
+"rpx_cpx_conf"
+"rpx_cpx_conf_fsge"
+"rpx_cpx_conf_fsge_dx"
+"rpx_flat"
+"rpx_flat_dx_split"
+"rpx_fsge_comp"
+"rpx_fwd_bind_dx"
+"rpx_fwd_bind_dx_void"
+"rpx_fwd_flat_dx"
+"rpx_fwd_length"
+"rpx_fwd_pair_sn"
+"rpx_gref"
+"rpx_inv_atom_dx"
+"rpx_inv_atom_sn"
+"rpx_inv_bind"
+"rpx_inv_bind_void"
+"rpx_inv_flat"
+"rpx_inv_gref"
+"rpx_inv_gref_bind_dx"
+"rpx_inv_gref_bind_sn"
+"rpx_inv_lifts_bi"
+"rpx_inv_lifts_dx"
+"rpx_inv_lifts_sn"
+"rpx_inv_lpx_req"
+"rpx_inv_lref"
+"rpx_inv_lref_bind_dx"
+"rpx_inv_lref_bind_sn"
+"rpx_inv_sort"
+"rpx_inv_sort_bind_dx"
+"rpx_inv_sort_bind_sn"
+"rpx_inv_zero_length"
+"rpx_inv_zero_pair_dx"
+"rpx_inv_zero_pair_sn"
+"rpx_lifts_sn"
+"rpx_lref"
+"rpx_pair"
+"rpx_pair_refl"
+"rpx_pair_sn_split"
+"rpx_refl"
+"rpx_reqx_conf"
+"rpx_sort"
+"rpx_teqx_conf"
+"rpx_teqx_div"
+"rsx"
+"rsx_bind"
+"rsx_bind_lpxs_aux"
+"rsx_bind_lpxs_void_aux"
+"rsx_bind_void"
+"rsx_cpxs_trans"
+"rsx_cpx_trans"
+"rsx_cpx_trans_jsx"
+"rsx_flat"
+"rsx_flat_lpxs"
+"rsx_fwd_bind_dx_void"
+"rsx_fwd_flat_dx"
+"rsx_fwd_lref_pair_csx"
+"rsx_fwd_lref_pair_csx_aux"
+"rsx_fwd_lref_pair_csx_drops"
+"rsx_fwd_lref_pair_drops"
+"rsx_fwd_pair"
+"rsx_fwd_pair_aux"
+"rsx_fwd_pair_sn"
+"rsx_gref"
+"rsx_ind"
+"rsx_ind_lpxs"
+"rsx_ind_lpxs_reqx"
+"rsx_intro"
+"rsx_intro_lpxs"
+"rsx_inv_bind_void"
+"rsx_inv_flat"
+"rsx_inv_lifts"
+"rsx_inv_lref_drops"
+"rsx_inv_lref_pair"
+"rsx_inv_lref_pair_drops"
+"rsx_jsx_trans"
+"rsx_lifts"
+"rsx_lpxs_trans"
+"rsx_lpx_trans"
+"rsx_lref_atom_drops"
+"rsx_lref_pair"
+"rsx_lref_pair_drops"
+"rsx_lref_pair_lpxs"
+"rsx_lref_unit_drops"
+"rsx_reqx_trans"
+"rsx_sort"
+"rsx_unit"
+"teqx_cpxs_trans"
+"teqx_cpx_trans"
+"teqx_fpbs_trans"
+"teqx_fpb_trans"
+"teqx_reqx_lpx_fpbs"