Theoremsimp, imp, dual, dual, dual_iff, mem_gt, mem_lt, mono_left, mono_right, of_gt, of_lt, to_lt, to_nil, to_sep, trans_left, trans_right, weak, weak_left, weak_right, add_left, add_right, dist_le, dist_le', right, balance', dual, dual_iff, eq_node', induction, node', node3L, node3R, node4L, pos, rotateL, rotateL_size, rotateR, rotateR_size, size_eq, size_eq_zero, all_balance', all_balanceL, all_balanceR, all_dual, all_iff_forall, all_node', all_node3L, all_node3R, all_node4L, all_node4R, all_rotateL, all_rotateR, all_singleton, any_iff_exists, any_singleton, balanceL_eq_balance, balanceL_eq_balance', balanceR_eq_balance', balance_eq_balance', balance_sz_dual, balancedSz_down, balancedSz_up, balancedSz_zero, delta_lt_false, dual_balance', dual_balanceL, dual_balanceR, dual_dual, dual_eraseMax, dual_eraseMin, dual_insert, dual_node', dual_node3L, dual_node3R, dual_node4L, dual_node4R, dual_rotateL, dual_rotateR, emem_iff_all, emem_iff_mem_toList, equiv_iff, findMax'_all, findMax'_dual, findMax_dual, findMin'_all, findMin'_dual, findMin_dual, foldr_cons_eq_toList, length_toList, length_toList', merge_nil_left, merge_nil_right, merge_node, node3L_size, node3R_size, node4L_size, not_le_delta, pos_size_of_mem, raised_iff, rotateL_nil, rotateL_node, rotateR_nil, rotateR_node, size_balance', size_balanceL, size_balanceR, size_dual, size_eq_realSize, splitMax_eq, splitMin_eq, toList_nil, toList_node | 112 |