Description: Obsolete version of vtoclg as of 26-Jan-2025. (Contributed by NM, 17-Apr-1995) Avoid ax-12 . (Revised by SN, 20-Apr-2024) (New usage is discouraged.) (Proof modification is discouraged.)