Description: Obsolete version of eubii as of 27-Sep-2023. (Contributed by NM, 9-Jul-1994) (Revised by Mario Carneiro, 6-Oct-2016) (Proof modification is discouraged.) (New usage is discouraged.)