Theoremsappend_overlap, infix, nil, not_step, of_forall_not_step, red_iff_eq, singleton, append_left, append_left_iff, append_right, cons, cons_cons_iff, cons_left_iff, cons_not, cons_not_rev, diamond, diamond_aux, length, negRev, not_rev, sublist, to_red, antisymm, append_append, append_append_left_iff, church_rosser, cons_cons, cons_cons_iff, cons_nil_iff_singleton, exact, length, length_le, negRev, neg_of_red_of_ne, nil_iff, not_step_nil, not_step_singleton, red_iff_addIrreducible, refl, singleton_iff, sizeof_of_step, step_negRev_iff, sublist, to_append_iff, trans, add_bind, add_mk, closure_eq_range, closure_range_of, equivalence_join_red, eqvGen_step_iff_join_red, ext_hom, ext_hom_iff, freeAddGroupCongr_apply, freeAddGroupCongr_refl, freeAddGroupCongr_symm, freeAddGroupCongr_trans, induction_on, instLawfulMonad, isReduced_cons_cons, isReduced_iff_not_step, join_red_of_step, lift_apply_of, lift_eq_sum_map, lift_mk, lift_of_apply, lift_of_eq_id, lift_symm_apply, lift_unique, comp, id, id', mk, of, unique, map_add, map_eq_lift, map_neg, map_pure, map_zero, negRev_append, negRev_bijective, negRev_cons, negRev_empty, negRev_injective, negRev_involutive, negRev_length, negRev_negRev, negRev_surjective, neg_bind, neg_mk, nsmul_mk, of_injective, pure_bind, quot_liftOn_mk, quot_lift_mk, quot_map_mk, quot_mk_eq_mk, range_lift_eq_closure, range_lift_le, red_negRev_iff, of, unique, sum_mk, zero_bind, zero_eq_mk, append_overlap, infix, nil, not_step, of_forall_not_step, red_iff_eq, singleton, append_left, append_left_iff, append_right, cons, cons_cons_iff, cons_left_iff, cons_not, cons_not_rev, diamond, diamond_aux, invRev, length, not_rev, sublist, to_red, antisymm, append_append, append_append_left_iff, church_rosser, cons_cons, cons_cons_iff, cons_nil_iff_singleton, exact, invRev, inv_of_red_of_ne, length, length_le, nil_iff, not_step_nil, not_step_singleton, red_iff_irreducible, refl, singleton_iff, sizeof_of_step, step_invRev_iff, sublist, to_append_iff, trans, closure_eq_range, closure_range_of, equivalence_join_red, eqvGen_step_iff_join_red, ext_hom, ext_hom_iff, freeGroupCongr_apply, freeGroupCongr_refl, freeGroupCongr_symm, freeGroupCongr_trans, induction_on, instLawfulMonad, invRev_append, invRev_bijective, invRev_cons, invRev_empty, invRev_injective, invRev_invRev, invRev_involutive, invRev_length, invRev_surjective, inv_bind, inv_mk, isReduced_cons_cons, isReduced_iff_not_step, join_red_of_step, lift_apply_of, lift_eq_prod_map, lift_mk, lift_of_apply, lift_of_eq_id, lift_symm_apply, lift_unique, comp, id, id', mk, of, unique, map_eq_lift, map_inv, map_mul, map_one, map_pure, mul_bind, mul_mk, of_injective, one_bind, one_eq_mk, pow_mk, of, unique, prod_mk, pure_bind, quot_liftOn_mk, quot_lift_mk, quot_map_mk, quot_mk_eq_mk, range_lift_eq_closure, range_lift_le, red_invRev_iff, map_inv, map_mul, map_one, of, sum_mk | 217 |