TheoremscasesOn_of_add, casesOn_zero, comp_lift, freeAddMonoidCongr_of, freeAddMonoidCongr_symm_of, hom_eq, hom_eq_iff, hom_map_lift, inductionOn, inductionOn', length_add, length_eq_four, length_eq_one, length_eq_three, length_eq_two, length_eq_zero, length_of, length_reverse, length_zero, lift_apply, lift_comp_of, lift_eval_of, lift_ofList, lift_of_comp_eq_map, lift_restrict, lift_symm_apply, map_apply_map_symm_eq, map_comp, map_id, map_map, map_of, map_surjective, map_symm_apply_map_eq, mem_add, mem_map, mem_of, mem_of_self, notMem_zero, ofList_append, ofList_comp_toList, ofList_cons, ofList_flatten, ofList_map, ofList_nil, ofList_singleton, ofList_symm, ofList_toList, ofList_vadd, of_injective, of_ne_zero, of_vadd, recOn_of_add, recOn_zero, reverse_add, reverse_of, reverse_reverse, sumAux_eq, toList_add, toList_comp_ofList, toList_cons, toList_map, toList_nil, toList_of, toList_ofList, toList_of_add, toList_sum, toList_symm, toList_zero, vadd_def, zero_ne_of, casesOn_of_mul, casesOn_one, comp_lift, freeMonoidCongr_of, freeMonoidCongr_symm_of, hom_eq, hom_eq_iff, hom_map_lift, inductionOn, inductionOn', length_eq_four, length_eq_one, length_eq_three, length_eq_two, length_eq_zero, length_mul, length_of, length_one, length_reverse, lift_apply, lift_comp_of, lift_eval_of, lift_ofList, lift_of_comp_eq_map, lift_restrict, lift_symm_apply, map_apply_map_symm_eq, map_comp, map_id, map_map, map_of, map_surjective, map_symm_apply_map_eq, mem_map, mem_mul, mem_of, mem_of_self, notMem_one, ofList_append, ofList_comp_toList, ofList_cons, ofList_flatten, ofList_map, ofList_nil, ofList_singleton, ofList_smul, ofList_symm, ofList_toList, of_injective, of_ne_one, of_smul, one_ne_of, prodAux_eq, recOn_of_mul, recOn_one, reverse_mul, reverse_of, reverse_reverse, smul_def, toList_comp_ofList, toList_cons, toList_map, toList_mul, toList_nil, toList_of, toList_ofList, toList_of_mul, toList_one, toList_prod, toList_symm | 140 |