--- /dev/null
+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
projects / helm.git / blobdiff