Description: Obsolete version of r19.37v as of 18-Jun-2023. (Contributed by NM, 2-Apr-2004) (Proof modification is discouraged.) (New usage is discouraged.)