Description: Alternate proof of dveeq2 , shorter but requiring ax-11 . (Contributed by NM, 2-Jan-2002) (Revised by NM, 20-Jul-2015) (New usage is discouraged.) (Proof modification is discouraged.)