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