Description: Obsolete version of unex as of 21-Jul-2025. (Contributed by NM, 1-Jul-1994) (Proof modification is discouraged.) (New usage is discouraged.)