Description: Alternate proof of cleljust . Compared with cleljustALT , it uses
nfv followed by equsexv instead of ax-5 followed by equsexhv ,
so it uses the idiom F/ x ph instead of ph -> A. x ph to express
nonfreeness. This style is generally preferred for later theorems.
(Contributed by NM, 28-Jan-2004)(Revised by Mario Carneiro, 21-Dec-2016)(Revised by BJ, 29-Dec-2020)(Proof modification is discouraged.)(New usage is discouraged.)