51 "acle_eq_monotonic_le"
53 "acle_le_monotonic_le"
75 "append_inj_length_dx"
76 "append_inj_length_sn"
111 "cext2_d_liftable2_sn"
118 "co_dedropable_sn_CTC"
119 "co_dedropable_sn_ltc"
130 "d1_liftable_liftable_all"
131 "d2_deliftable_sn_CTC"
132 "d2_deliftable_sn_ltc"
137 "d_deliftable1_isuni"
140 "d_deliftable2_sn_bi"
151 "deg_SO_inv_succ_aux"
160 "destruct_apair_apair_aux"
161 "destruct_lbind_lbind_aux"
162 "destruct_sort_sort_aux"
163 "destruct_tatom_tatom_aux"
164 "destruct_tpair_tpair_aux"
182 "drops_after_fwd_drop2"
184 "drops_atom2_sex_conf"
186 "drops_bind2_fwd_rfw"
189 "drops_conf_div_bind_isuni"
190 "drops_conf_div_fcla"
191 "drops_conf_div_isuni"
203 "drops_fwd_drop2_aux"
209 "drops_fwd_length_eq1"
210 "drops_fwd_length_eq2"
211 "drops_fwd_length_le4"
216 "drops_inv_atom1_aux"
218 "drops_inv_bind1_isuni"
219 "drops_inv_bind2_isuni"
220 "drops_inv_bind2_isuni_next"
222 "drops_inv_drop1_aux"
226 "drops_inv_length_eq"
228 "drops_inv_skip1_aux"
230 "drops_inv_skip2_aux"
235 "drops_inv_x_bind_xy"
237 "drops_isuni_fwd_drop2"
242 "drops_seq_trans_next"
243 "drops_sex_trans_next"
244 "drops_sex_trans_push"
248 "drops_split_trans_bind2"
257 "eq_false_inv_tpair_dx"
258 "eq_false_inv_tpair_sn"
269 "ext2_inv_pair_dx_aux"
271 "ext2_inv_pair_sn_aux"
275 "ext2_inv_unit_dx_aux"
277 "ext2_inv_unit_sn_aux"
316 "fqu_fwd_length_lref1"
317 "fqu_fwd_length_lref1_aux"
342 "fqup_bind_dx_flat_dx"
347 "fqup_flat_dx_bind_dx"
348 "fqup_flat_dx_pair_sn"
366 "fquq_fwd_length_lref1"
376 "fqus_inv_bind1_true"
381 "fqus_inv_gref1_bind"
383 "fqus_inv_lref1_bind"
384 "fqus_inv_refl_atom3"
386 "fqus_inv_sort1_bind"
387 "fqus_inv_zero1_pair"
410 "frees_inv_append_void"
411 "frees_inv_append_void_aux"
416 "frees_inv_bind_void"
417 "frees_inv_drops_next"
427 "frees_inv_lref_drops"
447 "frees_teqx_conf_reqx"
463 "fsle_frees_trans_eq"
510 "length_inv_succ_dx_ltail"
512 "length_inv_succ_sn_ltail"
533 "lex_drops_conf_pair"
534 "lex_drops_trans_pair"
547 "lex_liftable_dedropable_sn"
563 "liftsb_eq_repl_back"
595 "lifts_inv_bind1_aux"
597 "lifts_inv_bind2_aux"
599 "lifts_inv_flat1_aux"
601 "lifts_inv_flat2_aux"
603 "lifts_inv_gref1_aux"
605 "lifts_inv_gref2_aux"
607 "lifts_inv_lref1_aux"
608 "lifts_inv_lref1_uni"
610 "lifts_inv_lref2_aux"
611 "lifts_inv_lref2_uni"
612 "lifts_inv_lref2_uni_ge"
613 "lifts_inv_lref2_uni_lt"
614 "lifts_inv_pair_xy_x"
615 "lifts_inv_pair_xy_y"
616 "lifts_inv_push_succ_sn"
617 "lifts_inv_push_zero_sn"
619 "lifts_inv_sort1_aux"
621 "lifts_inv_sort2_aux"
624 "lifts_lref_ge_minus"
645 "liftsv_inv_cons1_aux"
647 "liftsv_inv_cons2_aux"
649 "liftsv_inv_nil1_aux"
651 "liftsv_inv_nil2_aux"
664 "lsuba_drops_conf_isuni"
665 "lsuba_drops_trans_isuni"
668 "lsuba_inv_atom1_aux"
670 "lsuba_inv_atom2_aux"
672 "lsuba_inv_bind1_aux"
674 "lsuba_inv_bind2_aux"
682 "lsubc_drops_trans_isuni"
685 "lsubc_inv_atom1_aux"
687 "lsubc_inv_atom2_aux"
689 "lsubc_inv_bind1_aux"
691 "lsubc_inv_bind2_aux"
699 "lsubf_eq_repl_back1"
700 "lsubf_eq_repl_back2"
707 "lsubf_fwd_lsubr_isdiv"
711 "lsubf_inv_atom1_aux"
713 "lsubf_inv_atom2_aux"
717 "lsubf_inv_pair1_aux"
719 "lsubf_inv_pair2_aux"
721 "lsubf_inv_push1_aux"
723 "lsubf_inv_push2_aux"
728 "lsubf_inv_unit1_aux"
730 "lsubf_inv_unit2_aux"
743 "lsubr_fwd_drops2_abbr"
744 "lsubr_fwd_drops2_bind"
750 "lsubr_inv_atom1_aux"
752 "lsubr_inv_atom2_aux"
754 "lsubr_inv_bind1_aux"
756 "lsubr_inv_bind2_aux"
769 "lveq_fwd_abst_bind_length_le"
770 "lveq_fwd_bind_abst_length_le"
774 "lveq_fwd_length_le_dx"
775 "lveq_fwd_length_le_sn"
776 "lveq_fwd_length_minus"
777 "lveq_fwd_length_plus"
782 "lveq_inj_void_dx_le"
783 "lveq_inj_void_sn_ge"
794 "lveq_inv_succ_sn_aux"
795 "lveq_inv_void_dx_length"
796 "lveq_inv_void_sn_length"
797 "lveq_inv_void_succ_dx"
798 "lveq_inv_void_succ_sn"
831 "req_inv_lref_bind_dx"
832 "req_inv_lref_bind_sn"
833 "req_inv_zero_pair_dx"
834 "req_inv_zero_pair_sn"
855 "reqx_fwd_bind_dx_void"
872 "reqx_inv_lref_bind_dx"
873 "reqx_inv_lref_bind_sn"
874 "reqx_inv_lref_pair_bi"
875 "reqx_inv_lref_pair_dx"
876 "reqx_inv_lref_pair_sn"
878 "reqx_inv_zero_pair_dx"
879 "reqx_inv_zero_pair_sn"
898 "rex_bind_dx_split_void"
909 "rex_fsge_compatible"
910 "rex_fsle_compatible"
912 "rex_fwd_bind_dx_void"
927 "rex_inv_gref_bind_dx"
928 "rex_inv_gref_bind_sn"
932 "rex_inv_lref_bind_dx"
933 "rex_inv_lref_bind_sn"
934 "rex_inv_lref_pair_bi"
935 "rex_inv_lref_pair_dx"
936 "rex_inv_lref_pair_sn"
937 "rex_inv_lref_unit_dx"
938 "rex_inv_lref_unit_sn"
940 "rex_inv_sort_bind_dx"
941 "rex_inv_sort_bind_sn"
943 "rex_inv_zero_length"
944 "rex_inv_zero_pair_dx"
945 "rex_inv_zero_pair_sn"
946 "rex_inv_zero_unit_dx"
947 "rex_inv_zero_unit_sn"
950 "rex_liftable_dedropable_sn"
961 "rexs_fwd_bind_dx_void"
974 "rexs_inv_gref_bind_dx"
975 "rexs_inv_gref_bind_sn"
978 "rexs_inv_sort_bind_dx"
979 "rexs_inv_sort_bind_sn"
1011 "rneqx_inv_bind_void"
1013 "rneqx_reqx_canc_dx"
1016 "rnex_inv_bind_void"
1018 "R_pw_confluent2_sex"
1038 "seq_co_dedropable_sn"
1039 "seq_co_dropable_dx"
1040 "seq_co_dropable_sn"
1041 "seq_drops_conf_next"
1042 "seq_drops_trans_next"
1065 "sex_co_dropable_dx"
1066 "sex_co_dropable_sn"
1070 "sex_dropable_dx_aux"
1071 "sex_drops_conf_next"
1072 "sex_drops_conf_push"
1073 "sex_drops_trans_next"
1074 "sex_drops_trans_push"
1099 "sex_liftable_co_dedropable_bi"
1100 "sex_liftable_co_dedropable_sn"
1123 "sex_trans_id_cfull"
1131 "sh_lt_nexts_inv_lt"
1137 "simple_inv_bind_aux"
1139 "simple_teqo_repl_dx"
1140 "simple_teqo_repl_sn"
1145 "s_rs_transitive_isid"
1146 "s_rs_transitive_lex_inv_isid"
1148 "tc_f_dedropable_sn"
1156 "teqo_inv_applv_bind_simple"
1158 "teqo_inv_gref1_aux"
1161 "teqo_inv_lref1_aux"
1164 "teqo_inv_pair1_aux"
1166 "teqo_inv_pair2_aux"
1168 "teqo_inv_sort1_aux"
1191 "teqx_inv_gref1_aux"
1196 "teqx_inv_lref1_aux"
1199 "teqx_inv_pair1_aux"
1201 "teqx_inv_pair_xy_x"
1202 "teqx_inv_pair_xy_y"
1204 "teqx_inv_sort1_aux"
1208 "teqx_lifts_inv_pair_sn"
1226 "tneqx_teqx_canc_dx"
1242 "tweq_inv_abbr_neg_sn"
1243 "tweq_inv_abbr_pos_bi"
1244 "tweq_inv_abbr_pos_sn"
1245 "tweq_inv_abbr_pos_x_lifts_y_y"
1247 "tweq_inv_abbr_sn_aux"
1249 "tweq_inv_abst_sn_aux"
1252 "tweq_inv_appl_sn_aux"
1255 "tweq_inv_cast_sn_aux"
1256 "tweq_inv_cast_xy_y"
1258 "tweq_inv_gref_sn_aux"
1261 "tweq_inv_lref_sn_aux"
1263 "tweq_inv_sort_sn_aux"